查看z3py中的单个断言

Question

在求解器上声明断言后，如何从所有断言中获取和利用单个断言?所以，如果s.assertions可以被转换成一个列表，我们就可以访问一个单独的语句。这是不可能的。我通过以下关于"BitVecs"的断言以及我想要得到的内容来解释。

from z3 import *
s = Solver()
x,y,z,w   = BitVecs("x y z w",7)    #rows
a,b,c,d,e = BitVecs("a b c d e",7)  #cols
constr = [x&a==a,x&b==b,x&c!=c,x&d!=d,x&e!=e,
y&a==a,y&b!=b,y&c!=c,y&d!=d,y&e==e,
z&a!=a,z&b==b,z&c==c,z&d==d,z&e!=e,
w&a!=a,w&b==b,w&c!=c,w&d==d,w&e==e ]
s.add(constr)
R = [x,y,z,w]
C = [a,b,c,d,e]
s.assertions()

我需要一个矩阵(列表的列表)，表明R,C-对是否具有==或!=类型的"constr"。因此，声明的constr的矩阵是

[[1,1,0,0,0],
[1,0,0,0,1],
[0,1,1,1,0],
[0,1,0,1,1]]

.

Answer 1

这是一件很奇怪的事情。您正在自己构造这些断言，因此最好只是跟踪您如何构造它们以找出它们包含的内容。

如果这些来自其他来源(我认为是可能的)，那么您将不得不"解析"。将它们还原为AST形式，并遍历它们的结构以回答诸如"什么是变量"、"什么是连接词"等形式的问题。等。这样做需要理解z3py如何在内部表示这些对象。虽然这是可能的，但我非常怀疑这是您想要做的事情，除非您正在开发一个应该处理所有事情的库。(也就是说，既然你知道你在构造什么，那就在别处跟踪它。)

但是，如果你想分析这些表达式，最好的方法是研究AST结构。您必须熟悉这个文件:https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py的内容，特别是decl和children等函数。