c - CUDD的布尔表达式解析器

Question

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

谢谢!

Answer 1

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

例如，在https://github.com/LTLMoP/slugs/blob/master/src/synthesisContextBasics.cpp，第22-64行，您可以找到一个简单的解析器，用于在c++中优化标准形式布尔公式。At假设变量已经被分配，表示变量的节点的BDD引用存储在数组"variables[..]"中。，它们各自的名称存储在"variabeNames[…]"将一般思想应用于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(r'a / ~ b')
expr = bdd.to_expr(u)
print(expr)

从dd == 0.5.6开始，wheel文件可以从包含CUDD编译版本的PyPI中获得。因此，在任何Linux环境中，只要Python版本与车轮匹配，pip install dd也将安装dd.cudd，链接到CUDD。

注意:我是dd包的作者。