使用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公式转换为列表列表形式

回答

相关问题