AllSat computes the list of all models of a BDD by enumerating all paths from the root to the true-leaf as truth assignments to indices.

Apply a binary boolean operator to two given BDDs.

convert a BoolExpr to a Bdd (it is assumed that the atoms of e are at least a subset of the atom set used with Initialize) and that there are no nested BoolNext operators in the formula

BoolExpr2Index maps a boolean atom to an AtomIndex. It is the reverse function of Index2BoolExpr.

This function derives a formula in conjunctive normal form from a BDD. The CNF is given as a set of sets of literals with an obvious meaning.

This function derives a formula in disjunctive normal form from a BDD. The DNF is given as a set of sets of literals with an obvious meaning.

This function derives a formula in Shannon normal form from a BDD. Of course, the formula can have an exponential size also for a small BDD.

Check whether bddAdr1 implies bddAdr0. This is done without constructing the Bdd for the implication and therefore usually faster and produces no garbage nodes.

Compose replaces nodes labeled with vi by bddAdrA in bddAdrB.

Constrain careAdr bddAdr computes a BDD that is equivalent to bddAdr at least in those cases where BDD careAdr holds. If careAdr is false, the result may differ arbitrarily from bddAdr. Usually, the resulting BDD is smaller and thus, the values outside the care set are chosen for minimization of bddAdr.

Computing a Craig interpolant of two BDDs

Compute the number of satisfying cubes.

Enumerate all permutations by a sequence of swaps according to the Steinhaus-Johnson-Trotter algorithm. The resulting list is a list of integers where integer i denotes a swap(i,i-1) of a list of elements [0..n]. Note that the result list has size (n!-1) and can be used for determining the optimal variable ordering in that these swaps are used to enumerate all orderings. A better use is by heuristics like the WindowPermutation or Sifting.

This function enumerates all BDDs for all the Boolean functions over the atoms listed in eL (which were used to Initialize the BDD package).

Existential quantification: The set of variables that are existentially quantified is provided as a conjunction of these variables as a BDD varBddAdr (thus the negative cofactors of varBddAdr are all false).

Relation product: propositional formulas r(x,e) and q(e,y) over sets of variables x,e,y, we compute the propositional formula p(x,y) = exists e. r(x,e) & q(e,y). If r and q are interpreted as binary relations, this implements therefore the relation product. This is an important function for model checking to compute existential predecessor and successor states (up to renaming of old and new variables).

Universal quantification: The set of variables that are universally quantified is provided as a conjunction of these variables as a BDD varBddAdr (thus the negative cofactors of varBddAdr are all false).

GarbageCollect removes all nodes except for those used by the given list of BDDs (their roots are given) from the internal data structures. The removed nodes are then reused by the MkBddNode.

Compute the if-then-else operation of given BDDs bddCond, bdd1 and bdd0.

Index2BoolExpr maps an index to the corresponding boolean expression. It is the reverse to function BoolExpr2Index.

IndexHead maps an index to the first BDDNode labeled by this index; the other nodes with this index are found by following the nxt pointers

This function is used to initialize the BDD module with a list of boolean atoms eL. Note that this defines the initial ordering as given in eL and that the list must not contain multiple occurrences of the same expression.

check whether the BDD is the False leaf

check whether the BDD is the True leaf

the BDD memory that maps BddAdrs to BddNodes

Function MkBddNode checks whether a node with the specified components already exists and if so returns its address; otherwise such a node is created and its address is returned. If there are nodes that are declared to be reusable by GarbageCollect, then these nodes are reused.

This function implements a generic conjunction which produces less garbage than repeated calls to Apply CONJ.

This function implements a generic disjunction which produces less garbage than repeated calls to Apply CONJ.

Compute the negation of a BDD.

NextSat is used to compute the model of a BDD bddAdr that is the next one found in a neg-pos traversal over the BDD starting from the path determined by the given model. The function returns a pair (success,model) where success holds if another model has been found, and if so, model is that model. Otherwise, model is the empty map.

Count the number of internal nodes of a list of BDDs (shared nodes are only counted once).

OneSat computes a satisfying truth assignment of a BDD. The result is a map that assigns some of the BDD indices a boolean truth values. If an index vi is not mapped to a boolean value, then vi is a don't care value in this assignment. Note that the result is only a model if bddAdr>0 holds.

OptimalVarOrder computes for a list of BDDs the optimal variable ordering by checking all permutations of the variable orders. It is of course a very expensive algorithm whose runtime depends on n! since we enumerate all orderings (in contrast to [FrSu87]). The function computes a triple (varOrd,numNodes,voL) where varOrd is one of the optimal variable orderings, numNodes is the number of nodes needed for it, and voL is the list of pairs (varOrd,numNodes) for all variable orderings.

Print a truth assignment to the atoms. The map maps AtomIndices to a boolean value, however, the map may be partial, so that AtomIndices are don't cares.

Relabel works similar to Compose: It replaces all atoms in a given BDD with address bddAdr according to the substitution rho. Its use is in particular for replacing now- and next-variables in model-checking. It is assumed that rho maps all variables occurring in bddAdr to other atoms.

Restrict careAdr bddAdr computes a BDD that is equivalent to bddAdr on the care set "careAdr", but possibly different if careAdr is false. In contrast to Constrain, the BDD computed by Restrict will never depend on new variables.

Compute the number of satisfying assignments.

SetAllocNodes determines the number of BDD nodes that are initially created, and that are added if that number should not be sufficient. The default value without calling this function is 1000000 nodes, and will be changed by this function.

Compute the set of internal nodes that belong to one of the given BDDs.

Sifting is the well-known sifting algorithm to optimize the variable ordering with polynomially many swap operations. If printFlag is true then the swap operations and the numbers of nodes are printed. At the end, the BDDs have the best variable ordering found by sifting.

Solves a propositional logic formula phi by means of the BDD package. If there is no model, the result is None, otherwise, a model is returned as a mapping of BoolExpr to boolean truth values. Caution: This function initializes the BDD package with the atoms of the given expression.

SwapSequence computes for two arrays that contain the same elements, a list of swap operations to transform the first array into the second one. The swap sequence is computed by bubblesort like moves. To apply it on variable orderings, do not forget to add the leaf nodes like Array.append [|BoolConst false; BoolConst true|] varOrder

SwapVar is used as basic operation for optimizing variable orderings. The function swaps the assignment of the indices vi and vi-1 to boolean expressions so that the variable ordering is changed. Note that vi must be greater than 2 since BDD variables cannot be changed with leafs. Note that the indices are still kept in the order 0,1,2,... so that only Index2BoolExpr is changed together will all existing BDDs.

Write a list of BDDs in DOT format to an output stream. If writeLF holds, also the false leafs are drawn, otherwise only true leafs are shown and missing edges point to the not shown false-leaf. If writeNxt holds, also the next-pointers between nodes labeled with the same AtomIndex are drawn.

Write all BDDs of the current manager in DOT format to an output stream. If writeLF holds, also the false leafs are drawn, otherwise only true leafs are shown and missing edges point to the not shown false-leaf. If writeNxt holds, also the next-pointers between nodes labeled with the same AtomIndex are drawn.