Returns the number of variables max_var. Default value is 0, which means that bdds cannot be created until the module is initialized using set_max_var.

Displays a bdd as a tree.

The root variable of a bdd. Convention: Zero and One have variable max_var+1

The low and high parts of a bdd, respectively. low and high raise Invalid_argument on Zero and One.

Builds a bdd node. Raises Invalid_argument is the variable is out of 1..max_var.

Builds the bdd reduced to a single variable.

Builds bdds for negation, conjunction, disjunction, implication, and logical equivalence.

mk_exists f b (resp. mk_forall f b) quantifies bdd b over all variables v for which f v holds. For example: mk_exists x. x /\ y produces y, mk_exists x. x \/ y produces one, mk_forall x. x /\ y produces zero and mk_forall x. x \/ y produces y. See test/quant_elim.ml.

extract_known_values b returns a map indexed by variables, associated to Boolean values. In that map, a variable v is associated to true (resp. false) if bdd b entails v to have this value, that is b -> v=true (resp b -> v=false) is a tautology.

Applies the given Boolean function to two bdds. Caveat: Do not use this function to compute the usual Boolean operations (conjunction, disjunction, etc.). Use instead the operations above (mk_and, etc.), which are more efficient.

constrain f g is the generalized cofactor, sometimes written f ↓ g. It is defined for any function g <> false so that f = (g /\ (f ↓ g)) \/ (~g /\ (f ↓ ~g)). Setting g to a variable x gives the classical Shannon cofactors: f = (x /\ (f ↓ x)) \/ (~x /\ (f ↓ ~x)). For f' = constrain f g, f' xs = f xs if g xs, the graph of f' is often simper than that of f, but not always. Note also that (∃xs, (α ↓ β)(xs)) = (∃xs, (α /\ β)(xs)), but constrain is, in general, less costly to calculate than mk_and. See, e.g., Raymond 2008, "Synchronous program verification with Lustre/Lesar", §7.9.

For f' = restriction f g, f' xs = f xs if g xs, and the graph of f' is a subset of that of f. I.e., f' is a smaller version of f for input vectors in the "care set" g. See, e.g., Raymond 2008, "Synchronous program verification with Lustre/Lesar", §7.9.

restrict t v b is the bdd for t[b/v], that is, t where variable v is assigned the truth value b.

Builds a bdd from a propositional formula f. Raises Invalid_argument if f contains a variable out of 1..max_var.

Builds a propositional formula from the given BDD. The returned formula is only build using if-then-else (Fite) and variables (Fvar).

Builds a ``compact'' formula from the given BDD. The returned formula is only built using conjunctions, disjunctions, variables, negations of variables, and if-then-else where the if condition is a variable.

Checks if a bdd is satisfiable i.e. different from zero

Checks if a bdd is a tautology i.e. equal to one

Checks if a bdd is equivalent to another bdd

entails b1 b2 checks that b1 entails b2, in other words b1 implies b2

Counts the number of different ways to satisfy a bdd.

Returns one truth assignment which satisfies a bdd, if any. The result is chosen deterministically. Raises Not_found if the bdd is zero

Returns one truth assignment which satisfies a bdd, if any. The result is chosen randomly. Raises Not_found if the bdd is zero

Returns all truth assignments which satisfy a bdd b.

Prints as compound if-then-else expressions

Prints as Boolean expressions, with fallback to if-then-else expressions when nothing is more compact

Returns the number of clauses when the bdd is printed in conjunctive normal form. This is the number of lines when the bdd is printed with function print_dimacs below, each line having up to max_var literals.

Prints a bdd in conjunctive normal form using the DIMACS format.

Warning: The output may be exponential in the size of the bdd. The number of clauses (that is, the number of lines printed) is given by cnf_size.

Prints a DOT output of a given bdd.

• deprecated

  Use print_dot instead.

• deprecated

  Use print_dot instead.

Renders a given bdd using DOT and runs the shell command "dot -Tps <file> | gv -"

Returns the number of internal nodes of the bdd (i.e. nodes Zero and One are not counted). This is proportional to the space used internally by the bdd (7 words per node).

Returns statistics on the internal nodes tables (one for each variable). The numbers are, in order: table length, number of entries, sum of bucket lengths, smallest bucket length, median bucket length, biggest bucket length.