使用z3解决无量词VC

如何解决使用z3解决无量词VC

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

因此，总而言之，他们通过实例化（通过E匹配）将量化的horn子句转换为无量词的horn子句，并在本文的图6中给出了验证条件（VCs）。

根据我的理解，本文建议将图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,N2')
    i0,i1,i2 = Ints('i0,i2')

    P = Function('P',B,Z)

    a0 = Array('a0',Z,B)
    a1 = Array('a1',B)
    a2 = Array('a2',B)


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

解决方法

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',B)
a1 = Array('a1',B)
a2 = Array('a2',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,False),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)

  即可解决此问题

• A <= B <= C表示法虽然可以在z3Py中编写，但并不表示您认为的含义。您需要将其分为两部分并使用结合。

• 将约束分为多行，更易于调试是一个更好的主意

• 布尔否定是Not，不是not

等尽管z3对此产生sat；但我不确定这是否是本文的正确翻译。 （特别是符号a1[i1 ← 0][k1]或含义序列A -> B -> C都必须正确翻译。您似乎完全错过了含义序列的C部分。我还没有t研究了这篇论文，所以我不确定这些是什么意思。）

因此，我上面给出的编码经过z3时，绝对不是本文中实际的条件。但是希望这可以帮助您入门。