BDDs play an important role in circuit verification and model checking, and for several applications, it is valuable to draw BDDs as directed acyclic graphs in SWISH. This strengthens the use of SWI-Prolog and SWISH as a teaching tool when BDDs are involved. Importantly, using library(clpb) is much more convenient than resorting to a lower-level library to produce BDDs.
When using CPLP(B) in SWISH, BDDs can be drawn using the bdd renderer. However, this still falls a bit short in cases where the projection to sat/1 residual goals takes too long. The main shortcoming is that setting Prolog flags in SWISH does not affect the projection to residual goals. A way to work around this is shown in SWISH issue 25.
The main task left in this roadmap item is to carefully think through the interface between renderers and constraint libraries, so that such cases can be handled more uniformly. See SWISH issue 27 for a discussion of the issues involved.
BDDs play an important role in circuit verification and model checking, and for several applications, it is valuable to draw BDDs as directed acyclic graphs in SWISH. This strengthens the use of SWI-Prolog and SWISH as a teaching tool when BDDs are involved. Importantly, using
library(clpb)is much more convenient than resorting to a lower-level library to produce BDDs.When using CPLP(B) in SWISH, BDDs can be drawn using the bdd renderer. However, this still falls a bit short in cases where the projection to
sat/1residual goals takes too long. The main shortcoming is that setting Prolog flags in SWISH does not affect the projection to residual goals. A way to work around this is shown in SWISH issue 25.The main task left in this roadmap item is to carefully think through the interface between renderers and constraint libraries, so that such cases can be handled more uniformly. See SWISH issue 27 for a discussion of the issues involved.