使用 Z3Py 将 Z3 CNF 公式转换为列表表示形式

Question

给定CNF中的Z3公式，是否可以使用Z3Py将其转换为列表表示？我想这样做是为了更容易地访问和操作文字。如果Python是一种函数式语言，我可能会做类似的事情

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 公式的列表表示形式？

Answer 1

没有模式匹配，但 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 变量本身。那是因为克里斯托夫·温特斯泰格的警告。如果您打算对这些列表进行任何处理，则符号__eq__很可能不是您想要的。

---

我不知道您要解决什么问题，但是如果您自己生成CNF，请考虑从一开始就以列表列表形式生成它们。将列表列表转换为 Z3 表达式比将列表转换为 Z3 表达式更容易。

Answer 2

我无论如何都

不是 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)

但是，元素比较似乎给出了一些意想不到的结果，例如：

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

在这一点上，我不确定我是否以意想不到的方式使用 Python 列表，或者这是否是 Z3 Python API 问题。