CUDD 的布尔表达式解析器答案

【问题标题】：Boolean Expression Parser for CUDDCUDD 的布尔表达式解析器
【发布时间】：2015-07-10 16:23:32
【问题描述】：

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

谢谢！

【问题讨论】：

我没有直接的答案，但您可能想看看 Sean Weaver 的 BDD Visualizer。

【解决方案1】：

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

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

如果你想要中缀符号，你总是可以使用 yacc/lex 来构建一个简单的解析器来为你做这件事。

【讨论】：

【解决方案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 files 是 available from PyPI，其中包括 CUDD 的编译版本。因此，在任何 Python 版本与轮子匹配的 Linux 环境中，pip install dd 也将安装 dd.cudd，链接到 CUDD。

注意：我是包dd的作者。

【讨论】：