使用Z3为特定CHC系统的猜测解决方案找到反例？ [英] Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?

问题描述

假设我有以下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但至少不满足上述三个方程中的一个的值？(例如：X=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]

显示x=1违反约束。(您可以编写代码，以便它准确地告诉您违反了哪个约束，但我离题了。)

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

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

打印：

Invariant is valid

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

这篇关于使用Z3为特定CHC系统的猜测解决方案找到反例？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！