使用 z3 解决无量词 VC

Question

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

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

据我了解，该论文建议将图 6 中生成的 VC 传递给任何 SMT 求解器，因为 VC 现在没有量词，可以由任何 SMT 求解器求解。（如果我在这方面有误，请纠正我。）

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

编辑：我的目标是找到图 6 中 VC 的解决方案。我应该添加什么作为要由 z3 推断的 return 类型的不变 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)
来解决这个问题
虽然您可以在 z3Py 中编写符号 A <= B <= C，但它并不代表您认为的意思。您需要将其拆分为两部分并使用连词。
最好将约束拆分为多行，更易于调试
布尔取反是Not，不是not

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

所以，我上面给出的编码，虽然经过z3，但绝对不是论文中的实际情况。但希望这会让您入门。

使用 z3 解决无量词 VC

solving quantifier-free VC using z3

quantifiers

first-order-logic

z3

hoare-logic

z3py