BFSOrder generates a breadth-first-search variable ordering for the given formula.

CNF transforms a given formula into a CNF by using a BDD.

CNFWithHandler transforms a given formula into a CNF by using a BDD.

Compile creates a BDD for a given formula.

CompileLiterals creates a BDD for a conjunction of literals with a given kernel.

CompileWithHandler creates a BDD for a given formula with the given bddHandler.

CompileWithKernel creates a BDD for a given formula with a given kernel.

CompileWithKernelAndHandler creates a BDD for a given formula with a given kernel and bddHandler.

CompileWithVarOrder creates a BDD for a given formula and a variable ordering.

CompileWithVarOrderAndHandler creates a BDD for a given formula, variable ordering, and bddHandler.

DefaultGenerator returns a BDD generator with sensible defaults.

DFSOrder generates a depth-first-search variable ordering for the given formula.

DNF transforms a given formula into a DNF by using a BDD.

DNFWithHandler transforms a given formula into a DNF by using a BDD.

ForceOrder generates a variable ordering for the given formula according to the FORCE ordering due to Aloul, Markov, and Sakallah.

GenerateGraphical generates a graphical representation of the given bdd with the configuration of the generator.

HandlerWithNodes returns a new BDD NodesHandler for the given bound of BDD nodes.

HandlerWithTimeout returns a new BDD TimoutHandler for the given timout.

MaxToMinOrder generates a variable ordering sorting the variables from maximal to minimal occurrence in the input formula.

MinToMaxOrder generates a variable ordering sorting the variables from minimal to maximal occurrence in the input formula.

NewKernel constructs a newBdd BDD kernel with numVars the number of variables on the kernel, nodeSize the initial number of nodes in the internal node table, and cacheSize the fixed size of the internal node cache.

NewKernelWithOrdering constructs a newBdd BDD kernel with ordering the list of ordered variables, nodeSize the initial number of nodes in the internal node table, and cacheSize the fixed size of the internal node cache.

no reordering.

random reordering (should only be used for testing).

sifting.

iterative sifting.

sliding window of size 2.

sliding window of size 2 iterative.

sliding window of size 3.

sliding window of size 3 iterative.

A BDD is a canonical representation of a Boolean formula.

ConstantNode represents a terminal node in a BDD.

A GraphicalGenerator is used to configure the graphical representation of a BDD as mermaid or Graphviz graphic.

InnerNode represents an inner node in a BDD.

A Kernel holds all internal data structures used during the compilation, especially the node cache.

A NodesHandler aborts the BDD compilation dependent on the number of nodes which are generated during the compilation.

Statistics holds fields with internal kernel statistics.

A TimeoutHandler aborts the BDD compilation dependent on the time it takes to generate the BDD.

A Handler for a BDD can abort the compilation of a BDD.

Node represents a node in a BDD.