pyeda.boolalg.bdd — Binary Decision Diagrams¶
The pyeda.boolalg.bdd module implements Boolean functions represented as binary decision diagrams.
Interface Functions:
- bddvar() — Return a unique BDD variable
- expr2bdd() — Convert an expression into a binary decision diagram
- bdd2expr() — Convert a binary decision diagram into an expression
- upoint2bddpoint() — Convert an untyped point into a BDD point
- ite() — BDD if-then-else operator
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) 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, use the pyeda.boolalg.bfarray.bddvars() function.
- pyeda.boolalg.bdd.bdd2expr(bdd, conj=False)[source]¶
Convert a binary decision diagram into an expression.
This function will always return an expression in two-level form. If conj is False, return a sum of products (SOP). Otherwise, return a product of sums (POS).
For example:
>>> a, b = map(bddvar, 'ab') >>> bdd2expr(~a & b | a & ~b) Or(And(~a, b), And(a, ~b))
- pyeda.boolalg.bdd.upoint2bddpoint(upoint)[source]¶
Convert an untyped point into a BDD point.
See also
For definitions of points an untyped points, see the pyeda.boolalg.boolfunc module.
- pyeda.boolalg.bdd.ite(f, g, h)[source]¶
BDD if-then-else (ITE) operator
The f, g, and h arguments are BDDs.
The ITE(f, g, h) operator means “if f is true, return g, else return h”.
It is equivalent to:
- DNF form: f & g | ~f & h
- CNF form: (~f | g) & (f | h)
Interface Classes¶
- class pyeda.boolalg.bdd.BDDNode(root, lo, hi)[source]¶
Binary decision diagram node
A BDD node represents one cofactor in the decomposition of a Boolean function. Nodes are uniquely identified by a root integer, lo child node, and hi child node:
- root is the cofactor variable’s uniqid attribute
- lo is the zero cofactor node
- hi is the one cofactor node
The root of the zero node is -2, and the root of the one node is -1. Both zero/one nodes have lo=None and hi=None.
Do NOT create BDD nodes using the BDDNode constructor. BDD node instances are managed internally.
- class pyeda.boolalg.bdd.BinaryDecisionDiagram(node)[source]¶
Boolean function represented by a binary decision diagram
See also
This is a subclass of pyeda.boolalg.boolfunc.Function
BDDs have a single attribute, node, that points to a node in the managed unique table.
There are two ways to construct a BDD:
- Convert an expression using the expr2bdd function.
- Use operators on existing BDDs.
Use the bddvar function to create BDD variables, and use the Python ~|&^ operators for NOT, OR, AND, XOR.
For example:
>>> a, b, c, d = map(bddvar, 'abcd') >>> f = ~a | b & c ^ d
The BinaryDecisionDiagram class is useful for type checking, e.g. isinstance(f, BinaryDecisionDiagram).
Do NOT create a BDD using the BinaryDecisionDiagram constructor. BDD instances are managed internally, and you will not be able to use the Python is operator to establish formal equivalence with manually constructed BDDs.
- equivalent(other)[source]¶
Return whether this BDD is equivalent to other.
You can also use Python’s is operator for BDD equivalency testing.
For example:
>>> a, b, c = map(bddvar, 'abc') >>> f1 = a ^ b ^ c >>> f2 = a & ~b & ~c | ~a & b & ~c | ~a & ~b & c | a & b & c >>> f1 is f2 True
- to_dot(name='BDD')[source]¶
Convert to DOT language representation.
See the DOT language reference for details.
- class pyeda.boolalg.bdd.BDDConstant(node)[source]¶
Binary decision diagram constant zero/one
The BDDConstant class is useful for type checking, e.g. isinstance(f, BDDConstant).
Do NOT create a BDD using the BDDConstant constructor. BDD instances are managed internally, and the BDD zero/one instances are singletons.