solving quantifier-free VC using z3

Question

我正在阅读这篇研究论文：http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.365.9467&rep=rep1&type=pdf

因此，总之，他们正在通过实例化(通过E匹配(将量化的霍恩子句转换为无量词的霍恩子句，由此产生的验证条件(VC(如图所示。本文第6段。

根据我的理解，本文建议将图6中得到的VC传递给任何SMT求解器，因为VC现在不含量词，并且可以由任何SMT解算器求解。(如果我错了，请纠正我。(

因此，为了理解这一点，我尝试用z3py对图6中的VC进行编码。

编辑：我的目标是找到图6中VC的解决方案。作为将由z3推断的不变量P的返回类型，我应该添加什么？使用z3有更好的方法吗？感谢您抽出时间！

这是代码：

from z3 import *
Z = IntSort()
B = BoolSort()
k0, k1, k2, N1, N2 = Ints('k0, k1, k2, N1, N2')
i0, i1, i2 = Ints('i0, i1, i2')
P = Function('P', B, Z)
a0 = Array('a0', Z, B)
a1 = Array('a1', Z, B)
a2 = Array('a2', Z, B)

prove(And(Implies(i0 == 0, P( Select(a0,k0), i0) ), 
Implies(And(P(Select(a1, k1),i1), i1<N1), P(Select(Store(a1, i1, 0)), i1+1) ),
Implies(And(P(Select(a2,k2), i2), not(i2<N2)), Implies(0<=k2<=N2, a2[k2]) ))) 

Answer 1

z3Py代码中存在许多编码问题。这里有一个它的重新编码，它至少通过z3没有任何错误：

from z3 import *
Z = IntSort()
B = BoolSort()
k0, k1, k2, N1, N2 = Ints("k0 k1 k2 N1 N2")
i0, i1, i2 = Ints("i0 i1 i2")
P = Function('P', B, Z, B)
a0 = Array('a0', Z, B)
a1 = Array('a1', Z, B)
a2 = Array('a2', Z, B)
s = Solver()
s.add(Implies(i0 == 0, P(Select(a0, k0), i0)))
s.add(Implies(And(P(Select(a1,k1),i1), i1<N1), P(Select(Store(a1, i1, False), k1), i1+1)))
s.add(Implies(And(P(Select(a2,k2),i2), Not(i2<N2)), Implies(And(0<=k2, k2<=N2), a2[k2])))
print(s.sexpr())
print(s.check())

我在你的代码中添加了一些修复程序：

函数P是一个谓词，因此它的最终类型是bool。通过说P = Function('P', B, Z, B)来解决这个问题

符号A <= B <= C，虽然你可以用z3Py写它，但它并不意味着你认为它意味着什么。你需要把它分成两部分并使用连词。

将约束拆分为多行是一个更好的想法，更容易调试

布尔否定是Not，它不是not

等。而z3在此基础上产生CCD_ 6；但我不太确定这是否是论文的正确翻译。(特别是，符号a1[i1 ← 0][k1]或含义序列A -> B -> C都需要正确翻译。你似乎完全错过了含义序列中的C部分。我没有研究过这篇论文，所以我不确定这些应该是什么意思。(

所以，我上面给出的编码，虽然经过z3，但绝对不是论文中的实际条件。但希望这能让你开始。