使用 z3 解决无量词 VC

Question

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

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

根据我的理解，本文建议将图 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 在此生成 sat；但我不太确定这是否是论文的正确翻译。 （特别是，符号a1[i1 ← 0][k1] 或暗示序列A -> B -> C 都需要正确翻译。你似乎完全错过了暗示序列中的C 部分。我没有研究过这篇论文，所以我不确定这些应该是什么意思。）

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