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的作者。