3

I have successfully created BDD using CUDD package. I am also able to visualize it using some already built tool. I am interested in storing BDD in a file using DDDMP package of CUDD. I read that Dddmp_cuddBddStore() is doing that for us. I am not able to find any examples of using that function. Its arguments are a little complex. Any small example using that function will be a great help.

Lunivore
  • 17,277
  • 4
  • 47
  • 92
hemant yadav
  • 31
  • 1
  • 2
  • 1
    Inside the dddmp package is usually a file called testdddmp.c (https://github.com/prismmodelchecker/cudd/blob/master/dddmp/testdddmp.c). There are a few examples of storing bdds also with Dddmp_cuddBddStore. – David Speck Jan 28 '20 at 11:35

1 Answers1

2

An interface to the DDDMP package is available with the Cython bindings to CUDD of the Python package dd. An example that creates the BDD of a Boolean function, saves it to a DDDMP file, and then loads it from that file, is the following.

from dd import cudd as _bdd

bdd = _bdd.BDD()
bdd.declare('x', 'y')

# The BDD node for the conjunction of variables x and y
u = bdd.add_expr('x /\ y')

# save to a DDDMP file (the file extension matters,
# for example a PDF extension would result in plotting
# a diagram using GraphViz)
bdd.dump('storage.dddmp', [u])

# load the BDD from the DDDMP file
u_ = bdd.load('storage.dddmp')
assert u == u_, (u, u_)

The source code of the Cython module dd/cudd.pyx includes an example of how to use the functions Dddmp_cuddBddStore and Dddmp_cuddBddLoad

https://github.com/tulip-control/dd/blob/b625dd46120e2e1f5a12190332e6191d07681ee8/dd/cudd.pyx#L1157-L1222

Installation of dd with the module dd.cudd is described here and could be summarized as

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

This will download and build CUDD, and build and install the Cython bindings of dd to CUDD.

0 _
  • 10,524
  • 11
  • 77
  • 109