使用Z3Py將Z3 CNF公式轉換爲列表列表形式

給定CNF中的Z3公式，是否可以使用Z3Py將其轉換爲列表列表形式？我想這樣做是爲了更方便地訪問和操作文字。如果Python是一種功能語言，我可能會做類似使用Z3Py將Z3 CNF公式轉換爲列表列表形式

def cnf2list(fm) : 
    match fm with 
    | And(P,Q) -> cnf2list(P) + cnf2list(Q) 
    | P -> clause2list(P) 

def clause2list(fm) : 
    match fm with 
    | Or(P,Q) -> clause2list(P) + clause2list(Q) 
    | P -> [P]

但我不知道我可以在Python中做到這一點。是否有可能像上面那樣執行模式匹配（或者使用一些完全不同的方法）來獲得Z3 CNF公式的列表表示？

來源

2016-06-07 user287393

沒有模式匹配，但z3py允許檢查Z3表達式：

def clause2list(expr): 
    if z3.is_const(expr): 
     return [str(expr)] 
    elif z3.is_or(expr): 
     return [atom for disjunct in expr.children() 
        for atom in clause2list(disjunct)] 
    else: 
     assert False, ('not supported', expr) 

x, y, z = z3.Bools('x y z') 
print(clause2list(z3.Or(x, y, z))) 
# ['x', 'y', 'z']

支持否定，連詞和真假文字留給作爲一個練習:) 見z3.py，CTRL-F 「def is_」。

請注意，我的實現返回變量名稱列表而不是Z3變量本身。這是因爲Christoph Wintersteiger's警告。如果您打算對這些列表進行任何處理，那麼符號__eq__很可能不是您想要的。

我不知道你想解決什麼問題，但如果要生成的CNF自己，考慮在列表中，列出了生產它們從一開始形成。將列表列表轉換爲Z3表達式比其他方式更容易。

來源

2016-06-07 22:23:43

我不以任何方式Python的專家，但簡單地把括號[...]周圍的表達式，然後使用上述連結+操作者構造一些列表，例如，像這樣：

from z3 import * 

x = Int('x') 
y = Int('y') 
z = Int('z') 

print(x) 
print(y) 
print(z) 
lst = [x] + [y] 
print(lst) 
s = sum(lst) 
print(s) 
lst.reverse() 
print(lst) 
print(x in lst)

然而，元素comparsions似乎給了一些意想不到的結果，比如這些：

print(z in lst) 
print(lst.count(x))

在這一點上我不知道我是否使用以意想不到的方式Python列表，或者是否這是一個Python的Z3 API問題。

來源

2016-06-07 12:29:52

這是定製'__eq__'的必然結果。 –

根據[這些規則]，列表成員資格測試'x in xs'大致等於'any（bool（x == el）for el in xs）'，而bool（）' （https://docs.python.org/3/reference/datamodel.html#object.__bool__）。這種行爲當然不足以犧牲符號'=='的便利性，但我認爲可能有小的改進。考慮添加引發異常的方法'__bool__'，以防止這種用法。我非常肯定，在具體布爾上下文中使用符號布爾表達式的大多數情況都是錯誤。 –

太好了，謝謝你解釋@VladShcherbina！我將繼續添加__bool__方法。 –

使用Z3Py將Z3 CNF公式轉換爲列表列表形式

回答

相關問題