Library of decision diagrams and algorithms on them, in pure Python, as well as Cython bindings to CUDD, Sylvan, and BuDDy.
Project description
[![Build Status][build_img]][travis]
[![Coverage Status][coverage]][coveralls]
About
=====
A pure-Python (3 and 2) package for manipulating:
- [Binary decision diagrams](https://en.wikipedia.org/wiki/Binary_decision_diagram) (BDDs).
- [Multi-valued decision diagrams](http://dx.doi.org/10.1109/ICCAD.1990.129849) (MDDs).
as well as [Cython](http://cython.org/) bindings to the C libraries:
- [CUDD](http://vlsi.colorado.edu/~fabio/CUDD/)
- [Sylvan](https://github.com/utwente-fmt/sylvan) (multi-core parallelization)
- [BuDDy](http://buddy.sourceforge.net)
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](https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf).
- Dynamic variable reordering using [Rudell's sifting algorithm](http://www.eecg.toronto.edu/~ece1767/project/rud.pdf).
- Reordering to obtain a given order.
- Parser of quantified Boolean expressions in either
[TLA+](https://en.wikipedia.org/wiki/TLA%2B) or
[Promela](https://en.wikipedia.org/wiki/Promela) syntax.
- Pre/Image computation (relational product).
- Renaming variables.
- Conversion from BDDs to MDDs.
- Conversion functions to [`networkx`](https://networkx.github.io/) and
[`pydot`](https://pypi.python.org/pypi/pydot) graphs.
- BDDs have methods to `dump` and `load` them using `pickle`.
- 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`](https://github.com/johnyf/omega/blob/master/omega/symbolic/fol.py)
from the [`omega` package](https://github.com/johnyf/omega/blob/master/doc/doc.md).
Documentation
=============
In the [Markdown](https://en.wikipedia.org/wiki/Markdown) file
[`doc.md`](https://github.com/johnyf/dd/blob/master/doc.md).
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:
```python
from dd.autoref import BDD, Function
bdd = BDD()
[bdd.add_var(var) for var in ['x', 'y']]
u = bdd.add_expr('x => y') # TLA+ syntax
u = bdd.add_expr('x -> y') # Promela syntax
# alternative
x = bdd.var('x')
not_x = ~ x
y = bdd.var('y')
v = not_x | y
assert u == v
```
## CUDD
The interface to CUDD in `dd.cudd` looks similar to `dd.autoref`,
including automated reference counting:
```python
from dd import cudd
bdd = cudd.BDD()
[bdd.add_var(var) for var in ['x', y'']]
u = bdd.add_expr('\E x, y: x /\ y')
assert u == bdd.true, u
# longer alternative
xy = bdd.add_expr('x /\ y')
u = bdd.exist(['x', 'y'], xy)
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`.
```python
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`:
```python
# using TLA+ syntax
u = bdd.add_expr('x \/ y')
v = bdd.add_expr('~ x \/ z')
w = bdd.apply('/\\', u, v)
r = bdd.apply('=>', u, w)
# using Promela syntax
u = bdd.add_expr('x | y')
v = bdd.add_expr('!x | z')
w = bdd.apply('&', u, v)
r = bdd.apply('->', u, w)
# w = bdd.apply('and', u, v) # also available
```
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 garbage, then
```python
bdd.incref(w)
```
To decrement the reference count:
```python
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`.
Installation
============
## pure-Python
Recommended to use `pip`, because the latest version will install
dependencies before `dd`:
```shell
pip install dd
```
Otherwise:
```shell
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, affecting performance.
For graph layout with `pydot`,
[graphviz](http://graphviz.org/) needs to be installed.
## Cython bindings
### `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`
- `--sylvan`
- `--buddy`
Pass `--fetch` to `setup.py` to tell it to download, unpack, and `make` CUDD v3.0.0. For example:
```shell
pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*
python setup.py install --fetch --cudd
```
The path to an existing CUDD build directory can be passed as an argument:
```shell
python setup.py install --cudd="/home/user/cudd"
```
If you prefer defining installation directories, then follow [Cython's instructions](http://cython.readthedocs.io/en/latest/src/tutorial/clibraries.html#compiling-and-linking) 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:
```shell
git clone git@github.com:johnyf/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`](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](https://github.com/pypa/pip/issues/1883), so
```shell
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](https://en.wikipedia.org/wiki/Environment_variable)
prior to calling `pip`, or by editing the file [`download.py`](https://github.com/johnyf/dd/blob/master/download.py).
Currently, `download.py` expects to find Sylvan under `dd/sylvan` and built with [Autotools](https://en.wikipedia.org/wiki/GNU_Build_System) (for an example, see `.travis.yml`).
If the path differs in your environment, remember to update it.
Tests
=====
Require [`nose`](https://pypi.python.org/pypi/nose) and the extras. Run with:
```shell
cd tests/
nosetests
```
If the extension module `dd.cudd` has not been compiled and installed,
then the CUDD tests will fail.
License
=======
[BSD-3](http://opensource.org/licenses/BSD-3-Clause), see file `LICENSE`.
[build_img]: https://travis-ci.org/johnyf/dd.svg?branch=master
[travis]: https://travis-ci.org/johnyf/dd
[coverage]: https://coveralls.io/repos/johnyf/dd/badge.svg?branch=master
[coveralls]: https://coveralls.io/r/johnyf/dd?branch=master
[![Coverage Status][coverage]][coveralls]
About
=====
A pure-Python (3 and 2) package for manipulating:
- [Binary decision diagrams](https://en.wikipedia.org/wiki/Binary_decision_diagram) (BDDs).
- [Multi-valued decision diagrams](http://dx.doi.org/10.1109/ICCAD.1990.129849) (MDDs).
as well as [Cython](http://cython.org/) bindings to the C libraries:
- [CUDD](http://vlsi.colorado.edu/~fabio/CUDD/)
- [Sylvan](https://github.com/utwente-fmt/sylvan) (multi-core parallelization)
- [BuDDy](http://buddy.sourceforge.net)
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](https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf).
- Dynamic variable reordering using [Rudell's sifting algorithm](http://www.eecg.toronto.edu/~ece1767/project/rud.pdf).
- Reordering to obtain a given order.
- Parser of quantified Boolean expressions in either
[TLA+](https://en.wikipedia.org/wiki/TLA%2B) or
[Promela](https://en.wikipedia.org/wiki/Promela) syntax.
- Pre/Image computation (relational product).
- Renaming variables.
- Conversion from BDDs to MDDs.
- Conversion functions to [`networkx`](https://networkx.github.io/) and
[`pydot`](https://pypi.python.org/pypi/pydot) graphs.
- BDDs have methods to `dump` and `load` them using `pickle`.
- 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`](https://github.com/johnyf/omega/blob/master/omega/symbolic/fol.py)
from the [`omega` package](https://github.com/johnyf/omega/blob/master/doc/doc.md).
Documentation
=============
In the [Markdown](https://en.wikipedia.org/wiki/Markdown) file
[`doc.md`](https://github.com/johnyf/dd/blob/master/doc.md).
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:
```python
from dd.autoref import BDD, Function
bdd = BDD()
[bdd.add_var(var) for var in ['x', 'y']]
u = bdd.add_expr('x => y') # TLA+ syntax
u = bdd.add_expr('x -> y') # Promela syntax
# alternative
x = bdd.var('x')
not_x = ~ x
y = bdd.var('y')
v = not_x | y
assert u == v
```
## CUDD
The interface to CUDD in `dd.cudd` looks similar to `dd.autoref`,
including automated reference counting:
```python
from dd import cudd
bdd = cudd.BDD()
[bdd.add_var(var) for var in ['x', y'']]
u = bdd.add_expr('\E x, y: x /\ y')
assert u == bdd.true, u
# longer alternative
xy = bdd.add_expr('x /\ y')
u = bdd.exist(['x', 'y'], xy)
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`.
```python
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`:
```python
# using TLA+ syntax
u = bdd.add_expr('x \/ y')
v = bdd.add_expr('~ x \/ z')
w = bdd.apply('/\\', u, v)
r = bdd.apply('=>', u, w)
# using Promela syntax
u = bdd.add_expr('x | y')
v = bdd.add_expr('!x | z')
w = bdd.apply('&', u, v)
r = bdd.apply('->', u, w)
# w = bdd.apply('and', u, v) # also available
```
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 garbage, then
```python
bdd.incref(w)
```
To decrement the reference count:
```python
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`.
Installation
============
## pure-Python
Recommended to use `pip`, because the latest version will install
dependencies before `dd`:
```shell
pip install dd
```
Otherwise:
```shell
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, affecting performance.
For graph layout with `pydot`,
[graphviz](http://graphviz.org/) needs to be installed.
## Cython bindings
### `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`
- `--sylvan`
- `--buddy`
Pass `--fetch` to `setup.py` to tell it to download, unpack, and `make` CUDD v3.0.0. For example:
```shell
pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*
python setup.py install --fetch --cudd
```
The path to an existing CUDD build directory can be passed as an argument:
```shell
python setup.py install --cudd="/home/user/cudd"
```
If you prefer defining installation directories, then follow [Cython's instructions](http://cython.readthedocs.io/en/latest/src/tutorial/clibraries.html#compiling-and-linking) 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:
```shell
git clone git@github.com:johnyf/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`](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](https://github.com/pypa/pip/issues/1883), so
```shell
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](https://en.wikipedia.org/wiki/Environment_variable)
prior to calling `pip`, or by editing the file [`download.py`](https://github.com/johnyf/dd/blob/master/download.py).
Currently, `download.py` expects to find Sylvan under `dd/sylvan` and built with [Autotools](https://en.wikipedia.org/wiki/GNU_Build_System) (for an example, see `.travis.yml`).
If the path differs in your environment, remember to update it.
Tests
=====
Require [`nose`](https://pypi.python.org/pypi/nose) and the extras. Run with:
```shell
cd tests/
nosetests
```
If the extension module `dd.cudd` has not been compiled and installed,
then the CUDD tests will fail.
License
=======
[BSD-3](http://opensource.org/licenses/BSD-3-Clause), see file `LICENSE`.
[build_img]: https://travis-ci.org/johnyf/dd.svg?branch=master
[travis]: https://travis-ci.org/johnyf/dd
[coverage]: https://coveralls.io/repos/johnyf/dd/badge.svg?branch=master
[coveralls]: https://coveralls.io/r/johnyf/dd?branch=master
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.
Source Distribution
dd-0.5.0.tar.gz
(341.1 kB
view hashes)