This is a pre-production deployment of Warehouse, however changes made here WILL affect the production instance of PyPI.
Latest Version Dependencies status unknown Test status unknown Test coverage unknown
Project Description
[![Build Status][build_img]][travis]
[![Coverage Status][coverage]][coveralls]


About
=====

A pure-Python (2 and 3) 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.

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](https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf)
- [Rudell's sifting algorithm](http://www.eecg.toronto.edu/~ece1767/project/rud.pdf)
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`](https://pypi.python.org/pypi/pydot) graphs.
- BDDs have methods to `dump` and `load` them as nested `dict`s using `pickle`.
- BDDs dumped by CUDD can be loaded using a
[PLY](https://github.com/dabeaz/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


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`.

Expressions in both [TLA+](https://en.wikipedia.org/wiki/TLA%2B) and [Promela](https://en.wikipedia.org/wiki/Promela) syntax are supported.


## 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`.

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

```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. For example:

```shell
pip download dd --no-deps
tar xzf dd-*.tar.gz
cd dd-*
python setup.py install --fetch --cudd
```

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

0.4.1

This version

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.4.0

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.3.1

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.3.0

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.2.2

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.2.1

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.2.0

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.1.3

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.1.2

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.1.1

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.0.4

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.0.3

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.0.2

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

0.0.1

History Node

TODO: Figure out how to actually get changelog content.

Changelog content for this version goes here.

Donec et mollis dolor. Praesent et diam eget libero egestas mattis sit amet vitae augue. Nam tincidunt congue enim, ut porta lorem lacinia consectetur. Donec ut libero sed arcu vehicula ultricies a non tortor. Lorem ipsum dolor sit amet, consectetur adipiscing elit.

Show More

Download Files

Download Files

TODO: Brief introduction on what you do with files - including link to relevant help section.

File Name & Checksum SHA256 Checksum Help Version File Type Upload Date
dd-0.4.1.tar.gz (316.9 kB) Copy SHA256 Checksum SHA256 Source Sep 9, 2016

Supported By

WebFaction WebFaction Technical Writing Elastic Elastic Search Pingdom Pingdom Monitoring Dyn Dyn DNS HPE HPE Development 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