使用CUDD/DDDMP包将BDD存储在文件中？

Question

我已经成功地使用CUDD包创建了BDD。我也能够使用一些已经构建的工具来可视化它。我感兴趣的是使用DDDMP软件包CUDD将BDD存储在文件中。我读到Dddmp_cuddBddStore()是为我们这样做的。我找不到任何使用这一功能的例子。它的论点有点复杂。任何使用该函数的小例子都会有很大的帮助。

Answer 1

dd包的的CUDD提供了DDDMP包的接口。下面是一个示例，它创建布尔函数的BDD，将其保存到DDDMP文件，然后从该文件加载它。

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_)

Cython模块dd/cudd.pyx的源代码包括如何使用函数Dddmp_cuddBddStore和Dddmp_cuddBddLoad的示例。

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

用模块dd安装dd.cudd描述了这里，可以概括为

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

这将下载和构建CUDD，并构建和安装dd到CUDD的Cython绑定。