dd 0.5.1

[![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:
`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 [e-mail]: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