Binary Decision Diagrams

A Binary Decision Diagram (BDD) represents a boolean function \( \{ 0, 1 \}^n \rightarrow \{ 0, 1 \} \) over a finite domain of \( n \) boolean input variables. More...

Collaboration diagram for Binary Decision Diagrams:

Modules
	Basic Constructors
	Construction of constants, variables, and cubes.
	Basic Operations
	Basic Boolean operations.
	Variable Substitution
	Variable substitution and reordering.
	Transition System Operations
	Relational operations on BDDs.
	Predicates
	Predicative information on BDDs.
	Counting Operations
	Numerical information on BDDs.
	Input Variables
	Information on variables in BDDs.
	Conversion to BDDs
	Conversion from Zero-suppressed Decision Diagrams .
	Visualization
	Printing of .dot files.

Classes
class	adiar::__bdd
	A (possibly) unreduced Binary Decision Diagram. More...
class	adiar::bdd
	A reduced Binary Decision Diagram. More...

Detailed Description

A Binary Decision Diagram (BDD) represents a boolean function \( \{ 0, 1 \}^n \rightarrow \{ 0, 1 \} \) over a finite domain of \( n \) boolean input variables.

The bdd class takes care of reference counting and optimal garbage collection of the underlying files. To ensure the most disk-space is available, try to release your bdd objects as quickly as possible and/or minimise the number of lvalues of said type.

An exec_policy can be provided as an optional first argument for (most) of the BDD functions. This provides you with the ability to change settings on the algorithm execution, e.g. the type of priority queue and algorithm used.