# 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).