CUDD的布尔表达式解析器
答
有几个项目已经包含了解析字符串到BDD的功能。
例如,在https://github.com/LTLMoP/slugs/blob/master/src/synthesisContextBasics.cpp的第22-64行,您可以找到一个简单的解析器,用于在C++中使用波兰范式布尔公式。在假定变量已经被分配,并且表示变量的节点的BDD引用被存储在数组“变量[..]”中,并且它们各自的名称被存储在“变量名[...]”中。将总体思想调整为C相对简单。该代码中的类“BF”是“DdNode *”引用的包装。
如果你想要中缀表示法,你总是可以使用yacc/lex来构建一个简单的解析器,它可以为你做到这一点。
答
另一种可能性是在Python配合使用,用Cython绑定CUDD:
from dd import cudd
bdd = cudd.BDD()
bdd.declare('a', 'b')
u = bdd.add_expr('a /\ ~ b')
s = bdd.to_expr(u)
print(s)
截至dd == 0.5.3
,wheel files可以从PyPI将包括CUDD的编译版本。因此,pip install dd
也将在任何Linux版本环境中安装CUDD,并且Python版本与车轮匹配(3.5或3.6)。
声明:我是包dd
的作者。
我没有直接的答案,但是你可能想看看Sean Weaver的[BDD Visualizer](http://www.cs.uc.edu/~weaversa/BDD_Visualizer.html)。 –