About
A pure-Python (3 and 2) package for manipulating:
- Binary decision diagrams (BDDs).
- Multi-valued decision diagrams (MDDs).
as well as Cython bindings to the C libraries:
- CUDD (also read the introduction, and note that the original link for CUDD is http://vlsi.colorado.edu/~fabio/CUDD/)
- Sylvan (multi-core parallelization)
- BuDDy
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.
Contains:
- All the standard functions defined, e.g., by Bryant.
- Dynamic variable reordering using Rudell's sifting algorithm.
- Reordering to obtain a given order.
- Parser of quantified Boolean expressions in either TLA+ or Promela syntax.
- Pre/Image computation (relational product).
- Renaming variables.
- Zero-suppressed binary decision diagrams (ZDDs) in CUDD
- Conversion from BDDs to MDDs.
- Conversion functions to
networkx
andpydot
graphs. - BDDs have methods to
dump
andload
them usingpickle
. - BDDs dumped by CUDD's DDDMP can be loaded using fast iterative parser.
- Garbage collection using reference counting
If you prefer to work with integer variables instead of Booleans, and have
BDD computations occur underneath, then use the module
omega.symbolic.fol
from the omega
package.
If you are interested in computing minimal covers (two-level logic minimization)
then use the module omega.symbolic.cover
of the omega
package.
The method omega.symbolic.fol.Context.to_expr
converts BDDs to minimal
formulas in disjunctive normal form (DNF).
Documentation
Examples
The module dd.autoref
wraps the pure-Python BDD implementation dd.bdd
.
The API of dd.cudd
is almost identical to dd.autoref
.
You can skip details about dd.bdd
, unless you want to implement recursive
BDD operations at a low level.
from dd.autoref import BDD
bdd = BDD()
bdd.declare('x', 'y', 'z', 'w')
# conjunction (in TLA+ syntax)
u = bdd.add_expr('x /\ y') # operators `&, |` are supported too
print(u.support)
# substitute variables for variables (rename)
rename = dict(x='z', y='w')
v = bdd.let(rename, u)
# substitute constants for variables (cofactor)
values = dict(x=True, y=False)
v = bdd.let(values, u)
# substitute BDDs for variables (compose)
d = dict(x=bdd.add_expr('z \/ w'))
v = bdd.let(d, u)
# infix operators
v = bdd.var('z') & bdd.var('w')
v = ~ v
# quantify
u = bdd.add_expr('\E x, y: x \/ y')
# less readable but faster alternative
u = bdd.var('x') | bdd.var('y')
u = bdd.exist(['x', 'y'], u)
assert u == bdd.true, u
# inline BDD references
u = bdd.add_expr('x /\ {v}'.format(v=v))
# satisfying assignments (models)
d = bdd.pick(u, care_vars=['x', 'y'])
for d in bdd.pick_iter(u):
print(d)
n = bdd.count(u)
To run the same code with CUDD installed, change the first line to:
from dd.cudd import BDD
Most useful functionality is available via method of the class BDD
.
A few of the functions can prove handy too, mainly 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
.
A Function
object wraps each BDD node and decrements its reference count
when disposed by Python's garbage collector. Lower-level details are
discussed in the documentation.
For using ZDDs, change the first line to
from dd.cudd_zdd import ZDD as BDD
Installation
pure-Python
From the Python Package Index (PyPI) using the
package installer pip
:
pip install dd
Locally:
pip install .
For graph layout with pydot
, install also graphviz.
Cython bindings
Wheel files with compiled CUDD
As of dd
version 0.5.3, manylinux2014_x86_64
wheel files are
available from PyPI for some Python
versions. These wheel files contain the module dd.cudd
with the CUDD
library compiled and linked.
If you have a Linux system and Python version compatible with one of the
available wheels, then pip install dd
will install dd.cudd
, so you need
not compile CUDD. Otherwise, see below.
dd
fetching CUDD
By default, the package installs only the Python modules.
You can select to install any Cython extensions using
the setup.py
options:
--cudd
: build module of CUDD BDDs--cudd_zdd
: build module of CUDD ZDDs--sylvan
: build module of Sylvan BDDs--buddy
: build module of BuDDy BDDs
Pass --fetch
to setup.py
to tell it to download, unpack, and
make
CUDD v3.0.0. For example:
pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*/
python setup.py install --fetch --cudd --cudd_zdd
The path to an existing CUDD build directory can be passed as an argument:
python setup.py install --cudd="/home/user/cudd"
If you prefer defining installation directories, then follow Cython's instructions
to define CFLAGS
and LDFLAGS
before running setup.py
.
You need to have copied CuddInt.h
to the installation's include location
(CUDD omits it).
If building from the repository, then first install cython
. For example:
git clone git@github.com:tulip-control/dd
cd dd
pip install cython # not needed if building from PyPI distro
python setup.py install --fetch --cudd
The above options can be passed to pip
too, using the --install-option
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 installing build dependencies
If you build and install CUDD, Sylvan, or BuDDy yourself, then ensure that:
- the header files and libraries 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 filedownload.py
.
Currently, download.py
expects to find Sylvan under dd/sylvan
and built with Autotools
(for an example, see .travis.yml
).
If the path differs in your environment, remember to update it.
BuDDy can be downloaded and compiled as follows:
curl -L https://sourceforge.net/projects/buddy/files/buddy/BuDDy%202.4/buddy-2.4.tar.gz/download -o buddy-2.4.tar.gz
tar -xzf buddy-2.4.tar.gz
cd buddy-2.4/
./configure # as described in the README file of BuDDy
make
make install # installs to `/usr/local/include/` and `/usr/local/lib/`
# The installation location can be changed with `./configure --prefix=/where/to/install`
pip uninstall -y dd
python setup.py install --buddy # passes `-lbdd` to the compiler
and the installation confirmed by invoking in another directory:
python -c "import dd.buddy"
dd.cudd
and dd.cudd_zdd
in the wheel
Licensing of the compiled modules These notes apply to the compiled modules dd.cudd
and dd.cudd_zdd
that are
contained in the wheel file on
PyPI (namely the files dd/cudd.cpython-39-x86_64-linux-gnu.so
and
dd/cudd_zdd.cpython-39-x86_64-linux-gnu.so
in the *.whl
file, which can
be obtained using unzip
).
These notes do not apply to the source code of the modules
dd.cudd
and dd.cudd_zdd
.
The source distribution of dd
on PyPI is distributed under a 3-clause BSD
license.
The following libraries and their headers were used when building the modules
dd.cudd
and dd.cudd_zdd
that are included in the wheel:
The licenses of Python and CUDD are included in the wheel archive.
Cython does not add its license to C code that it generates.
GCC was used to compile the modules dd.cudd
and dd.cudd_zdd
in the wheel,
and the GCC runtime library exception
applies.
The modules dd.cudd
and dd.cudd_zdd
in the wheel dynamically link to the:
- Linux kernel (in particular
linux-vdso.so.1
), which allows system calls (see the kernel's fileCOPYING
and the explicit syscall exception in the fileLICENSES/exceptions/Linux-syscall-note
) - GNU C Library (glibc) (in particular
libpthread.so.0
,libc.so.6
,/lib64/ld-linux-x86-64.so.2
), which uses the LGPLv2.1 that allows dynamic linking, and other licenses. These licenses are included in the wheel file and apply to the GNU C Library that is dynamically linked.
Tests
Require nose
. Run with:
cd tests/
nosetests
Tests of Cython modules that were not installed will fail.
License
BSD-3, see file LICENSE
.