pyeda.boolalg.bdd — Binary Decision Diagrams

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

Interface Functions:

• bddvar()
• expr2bdd()
• bdd2expr()
• upoint2bddpoint()

Interface Classes:

• BDDNode
• BinaryDecisionDiagram
• BDDConstant
• BDDVariable

Interface Functions

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

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)
True

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.

pyeda.boolalg.bdd.expr2bdd(expr)

Convert an expression into a binary decision diagram.

pyeda.boolalg.bdd.bdd2expr(bdd, conj=False)

Convert a binary decision diagram into an expression.

pyeda.boolalg.bdd.upoint2bddpoint(upoint)

Convert an untyped point into a BDD point.

Interface Classes

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

Binary decision diagram node

Note

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

class pyeda.boolalg.bdd.BinaryDecisionDiagram(node)

Boolean function represented by a binary decision diagram

Note

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

dfs_preorder()

Iterate through nodes in DFS pre-order.

dfs_postorder()

Iterate through nodes in DFS post-order.

bfs()

Iterate through nodes in BFS order.

equivalent(other)

Return whether this BDD is equivalent to another.

to_dot(name='BDD')

Convert to DOT language representation.

class pyeda.boolalg.bdd.BDDConstant(node)

Binary decision diagram constant

Note

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

class pyeda.boolalg.bdd.BDDVariable(bvar)

Binary decision diagram variable

Note

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