# The BDD renderer #### Synopsis :- use_rendering(bdd). #### Options supported None #### Reconised terms The `bdd` renderer recognises CLP(B) residual goals of `library(clpb)` and draws them as Binary Decision Diagrams (BDDs). Both kinds of residual goals that `library(clpb)` can emit are supported by this renderer: By default, `library(clpb)` emits `sat/1` residual goals. These are first translated to BDDs by this renderer. In cases where the projection to `sat/1` goals is too costly, you can set the Prolog flag `clpb_residuals` to `bdd` yourself, and use `copy_term/3` to obtain a BDD representation of the residual goals. Currently, setting this flag does not affect the SWISH toplevel, so you also need to use `del_attrs/1` to avoid the costly projection. See below for an example. In both cases, the graphviz renderer is used for the final output.
## Examples The first example simply enables the `bdd` renderer and posts a CLP(B) query to show the residual goal as a BDD.
:- use_rendering(bdd). :- use_module(library(clpb)).
sat(X+Y).
The second example sets `clpb_residuals` to `bdd` in order to prevent the costly projection to `sat/1` goals. Note that this also requires the use of `del_attrs/1` and—since renderers are not invoked on subterms—introducing a new variable for the single residual goal that represents the BDD.
:- use_rendering(bdd). :- use_module(library(clpb)). :- set_prolog_flag(clpb_residuals, bdd).
length(Vs, 20), sat(card([2],Vs)), copy_term(Vs, Vs, [BDD]), maplist(del_attrs, Vs).
Building on this idea, the third example shows that you can impose an arbitrary *order* on the variables in the BDD by first stating a tautology like `+[1,V1,V2,...]`. This orders the variables in the same way they appear in this list.
sat(+[1,Z,Y,X]), sat(X+Y+Z), Vs = [X,Y,Z], copy_term(Vs, Vs, [BDD]), maplist(del_attrs, Vs).