0

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

因此，总而言之，他们正在通过实例化（通过 E 匹配）将量化的 horn 子句转换为无量词的 horn 子句，结果验证条件（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]) )))
4

1 回答 1

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，但绝对不是论文中的实际条件。但希望这会让你开始。

于 2020-10-20T17:15:13.140 回答