使用 Z3 查找特定 CHC 系统的"猜测解决方案"的反例？

Question

假设我有以下CHC系统(I(x(是未知谓词(：

(x = 0) -> I(x) 
(x < 5) / I(x) / (x' = x + 1) -> I(x') 
I(x) / (x >= 5) -> x = 5

现在假设我猜测I(x(的解为x<2(实际上是一个错误的猜测(。我可以为Z3Py编写代码吗？以(I(检查它是否是有效的解决方案，以及(ii(如果它不正确，则查找反例，即满足x<2，但不满足上述3个方程中的至少一个？(例如：x=1，这是一个反例，因为它不满足第二个方程？(

Answer 1

当然。进行这种推理的方法是断言所有约束的连词的否定，并询问z3是否能满足它。如果否定结果是可满足的，那么你就有了一个反例。如果它是unsat，那么你就知道你的不变量是好的。

这里有一种方法来编码这个想法，以一种通用的方式，通过约束生成器和猜测的不变量参数化：

from z3 import *
def Check(mkConstraints, I):
s = Solver()
# Add the negation of the conjunction of constraints
s.add(Not(mkConstraints(I)))
r = s.check()
if r == sat:
print("Not a valid invariant. Counter-example:")
print(s.model())
elif r == unsat:
print("Invariant is valid")
else:
print("Solver said: %s" % r)

考虑到这一点，我们可以在一个函数中对您的特定情况进行编码：

def System(I):
x, xp = Ints('x xp')
# (x = 0) -> I(x)
c1 = Implies(x == 0, I(x))
# (x < 5) / I(x) / (x' = x + 1) -> I(x')
c2 = Implies(And(x < 5, I(x), xp == x+1), I(xp))
# I(x) / (x >= 5) -> x = 5
c3 = Implies(And(I(x), x >= 5), x == 5)
return And(c1, c2, c3)

现在我们可以查询：

Check(System, lambda x: x < 2)

以上打印：

Not a valid invariant. Counter-example:
[xp = 2, x = 1]

表明CCD_ 2违反了约束。(您可以进行编码，这样它也会告诉您违反了哪个约束，但我跑题了。(

如果您提供了有效的解决方案，会发生什么？让我们看看：

Check(System, lambda x: x <= 5)

这个打印：

Invariant is valid

注意，我们不需要任何量词，因为顶级变量在z3中充当存在变量，我们所需要做的就是找出是否有违反约束的赋值。