使用 Z3 查找特定 CHC 系统的 'guess solution' 的反例？

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]

表明 x=1 违反了约束条件。（您可以编写代码，以便它也准确地告诉您违反了哪个约束，但我离题了。）

如果您提供有效的解决方案会怎样？让我们看看：

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

这会打印：

Invariant is valid

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

使用 Z3 查找特定 CHC 系统的 'guess solution' 的反例？

Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?

z3

z3py