This is a pre-production deployment of Warehouse. Changes made here affect the production instance of PyPI (pypi.python.org).
Help us improve Python packaging - Donate today!

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:
`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
Release History

Release History

This version
History Node

0.5.1

History Node

0.5.0

History Node

0.4.3

History Node

0.4.2

History Node

0.4.1

History Node

0.4.0

History Node

0.3.1

History Node

0.3.0

History Node

0.2.2

History Node

0.2.1

History Node

0.2.0

History Node

0.1.3

History Node

0.1.2

History Node

0.1.1

History Node

0.0.4

History Node

0.0.3

History Node

0.0.2

History Node

0.0.1

Download Files

Download Files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

File Name & Checksum SHA256 Checksum Help Version File Type Upload Date
dd-0.5.1.tar.gz (354.1 kB) Copy SHA256 Checksum SHA256 Source Mar 23, 2017

Supported By

WebFaction WebFaction Technical Writing Elastic Elastic Search Pingdom Pingdom Monitoring Dyn Dyn DNS Sentry Sentry Error Logging CloudAMQP CloudAMQP RabbitMQ Heroku Heroku PaaS Kabu Creative Kabu Creative UX & Design Fastly Fastly CDN DigiCert DigiCert EV Certificate Rackspace Rackspace Cloud Servers DreamHost DreamHost Log Hosting