pyeda.boolalg.bdd — Binary Decision Diagrams

The pyeda.boolalg.bdd module implements Boolean functions represented as binary decision diagrams.

Interface Functions:

Interface Classes:

Interface Functions

pyeda.boolalg.bdd.bddvar(name, index=None)[source]

Return a unique BDD variable.

A Boolean variable is an abstract numerical quantity that may assume any value in the set \(B = \{0, 1\}\). The bddvar function returns a unique Boolean variable instance represented by a binary decision diagram. Variable instances may be used to symbolically construct larger BDDs.

A variable is defined by one or more names, and zero or more indices. Multiple names establish hierarchical namespaces, and multiple indices group several related variables. If the name parameter is a single str, it will be converted to (name, ). The index parameter is optional; when empty, it will be converted to an empty tuple (). If the index parameter is a single int, it will be converted to (index, ).

Given identical names and indices, the bddvar function will always return the same variable:

>>> bddvar('a', 0) is bddvar('a', 0)

To create several single-letter variables:

>>> a, b, c, d = map(bddvar, "abcd")

To create variables with multiple names (inner-most first):

>>> fifo_push = bddvar(('push', 'fifo'))
>>> fifo_pop = bddvar(('pop', 'fifo'))

See also

For creating arrays of variables with incremental indices, we recommend using the pyeda.boolalg.bfarray.bddvars() function.


Convert an expression into a binary decision diagram.

pyeda.boolalg.bdd.bdd2expr(bdd, conj=False)[source]

Convert a binary decision diagram into an expression.


Convert an untyped point into a BDD point.

Interface Classes

class pyeda.boolalg.bdd.BDDNode(root, lo, hi)[source]

Binary decision diagram node


Never construct a BDDNode instance directly. They will automically be created and destroyed during symbolic manipulation.

class pyeda.boolalg.bdd.BinaryDecisionDiagram(node)[source]

Boolean function represented by a binary decision diagram


Never construct a BinaryDecisionDiagram instance directly. They will automatically be created and destroyed during symbolic manipulation.


Iterate through nodes in DFS pre-order.


Iterate through nodes in DFS post-order.


Iterate through nodes in BFS order.


Return whether this BDD is equivalent to another.


Convert to DOT language representation.

class pyeda.boolalg.bdd.BDDConstant(node)[source]

Binary decision diagram constant


Never construct a BDDConstant instance directly. Use the int values 0 and 1 instead.

class pyeda.boolalg.bdd.BDDVariable(bvar)[source]

Binary decision diagram variable


Never construct a BDDVariable instance directly. Use the bddvar() function instead.