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[...]”中。比较简单。该代码中的类“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，可从 PyPI 获得包含 CUDD 编译版本的轮文件。因此，在任何具有与轮子匹配的 Python 版本的 Linux 环境中，也将安装链接到 CUDD。pip install dddd.cudd

注意：我是 package 的作者dd。