Library of decision diagrams and algorithms on them.
Project description
About
A pure-Python package for manipulating:
Binary decision diagrams (BDDs).
Multi-valued decision diagrams (MDDs).
as well as Cython bindings to the C libraries:
These bindings expose almost identical interfaces as the Python implementation. The intended workflow is:
develop your algorithm in pure Python (easy to debug and introspect),
use the bindings to benchmark and deploy
Your code remains the same.
An ordered BDD is represented using dictionaries for the successors, unique table, and reference counts. Nodes are positive integers, and edges signed integers. A complemented edge is represented as a negative integer. Garbage collection uses reference counting.
Contains:
All the standard functions defined, e.g., by Bryant.
Rudell’s sifting algorithm for variable reordering.
Reordering to obtain a given order.
Quantified Boolean expression parser that creates BDD nodes.
Pre/Image computation (relational product).
Renaming variables to their neighbors.
Conversion from BDDs to MDDs.
Conversion functions to `networkx <https://networkx.github.io/>`__ and `pydot <http://pypi.python.org/pydot>`__ graphs.
BDDs have methods to dump and load them as nested dicts using pickle.
BDDs dumped by CUDD can be loaded using a PLY-based parser for the header, and a fast simple by-line parser for the main body of nodes.
Cython bindings to CUDD
Cython bindings to BuDDy
Examples
Two interfaces are available:
convenience: the module `dd.autoref <https://github.com/johnyf/dd/blob/master/dd/autoref.py>`__ wraps dd.bdd and takes care of reference counting, using `__del__ <https://docs.python.org/2/reference/datamodel.html#object.__del__>`__.
“low level”: the module `dd.bdd <https://github.com/johnyf/dd/blob/master/dd/bdd.py>`__ requires that the user in/decrement the reference counters associated with nodes that are used outside of a BDD.
Automated reference counting
The module dd.autoref wraps the pure-Python BDD implementation in dd.bdd. A Function object wraps a node and decrements its reference count when disposed by Python’s garbage collector:
from dd.autoref import BDD, Function
bdd = BDD()
for var in ['x', 'y']:
bdd.add_var(var)
x = bdd.var('x')
not_x = ~ x
y = bdd.var('y')
u = not_x | y
v = Function.from_expr('x -> y', bdd)
assert u == v
CUDD
The interface to CUDD in dd.cudd looks similar to dd.autoref, including automated reference counting:
from dd import cudd
bdd = cudd.BDD()
for var in ['x', 'y']:
bdd.add_var(var)
xy = bdd.add_expr('x & y')
u = bdd.quantify(xy, {'x', 'y'}, forall=False)
assert u == bdd.True, u
Reference counting by the user
The pure-Python module dd.bdd can be used directly, which allows access more extensive than dd.autoref. The n variables in a dd.bdd.BDD are ordered from 0 (top level) to n-1 (bottom level). The terminal node 1 is at level n.
from dd.bdd import BDD
ordering = dict(x=0, y=1)
bdd = BDD(ordering)
bdd.add_var('z')
Boolean expressions can be added with the method BDD.add_expr:
u = bdd.add_expr('x | y')
v = bdd.add_expr('!x | z')
w = bdd.apply('and', u, v)
w = bdd.apply('&', u, v)
r = bdd.apply('->', u, w)
Garbage collection is triggered either explicitly by the user, or when invoking the reordering algorithm. If we invoked garbage collection next, then the nodes u, v, w would be deleted. To prevent this from happening, their reference counts should be incremented. For example, if we want to prevent w from being collected as gargabe, then
bdd.incref(w)
To decrement the reference count:
bdd.decref(w)
The more useful functions in dd.bdd are rename, image, preimage, reorder, to_nx, to_pydot.
Use the method BDD.dump to write a BDD to a pickle file, and BDD.load to load it back. A CUDD dddmp file can be loaded using the function dd.dddmp.load.
Examples of how dd can be used to implement symbolic algorithms can be found in the `omega package <https://github.com/johnyf/omega/blob/master/doc/doc.md>`__.
Installation
pure-Python
Recommended to use pip, because the latest version will install dependencies before dd:
pip install dd
Otherwise:
python setup.py install
If you use the latter, remember to install ply before dd. If ply is absent, then the parser tables will not be cached. You can
Optional: For graph layout, `pydot <http://pypi.python.org/pydot>`__ and graphviz are required. Using pip, these can be installed as extra called dot:
pip install dd[dot]
Cython bindings
dd fetching CUDD
By default, the package will try to compile the Cython bindings to CUDD. If it fails, then it installs the Python modules only. You can select either or both extensions by the setup.py options --cudd and --buddy.
Pass --fetch to setup.py to tell it to download, unpack, and make CUDD. For example:
python setup.py install --fetch
These options can be passed to pip too, using the `--install-option <https://pip.pypa.io/en/latest/reference/pip_install.html#per-requirement-overrides>`__ in a requirements file, for example:
dd >= 0.1.1 --install-option="--fetch" --install-option="--cudd"
The command line behavior of pip is currently different, so
pip install --install-option="--fetch" dd
will propagate option --fetch to dependencies, and so raise an error.
User fetching build dependencies
If you build and install CUDD or BuDDy yourself, then ensure that:
the header files and libraries of either CUDD or BuDDy are present, and
suitable compiler, include, linking, and library flags are passed, either by setting environment variables prior to calling pip, or by editing the file `download.py <https://github.com/johnyf/dd/blob/master/download.py>`__.
Tests
Require nose and the extras. Run with:
cd tests/
nosetests
If the extension module dd.cudd has not been compiled and installed, then the CUDD tests will fail.
License
BSD-3, see file LICENSE.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.