CUDD的布尔表达式解析器

Question

我在C上使用CUDD库来制作二进制决策图。我想知道是否有某种方法将布尔表达式作为字符串转换为二元决策图。

谢谢！

Answer 1

有几个项目已经包含了解析字符串到BDD的功能。

例如，在https://github.com/LTLMoP/slugs/blob/master/src/synthesisContextBasics.cpp的第22-64行，您可以找到一个简单的解析器，用于在C++中使用波兰范式布尔公式。在假定变量已经被分配，并且表示变量的节点的BDD引用被存储在数组“变量[..]”中，并且它们各自的名称被存储在“变量名[...]”中。将总体思想调整为C相对简单。该代码中的类“BF”是“DdNode *”引用的包装。

如果你想要中缀表示法，你总是可以使用yacc/lex来构建一个简单的解析器，它可以为你做到这一点。

Answer 2

另一种可能性是在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的作者。