使用Z3为特定CHC系统的猜测解决方案找到反例? [英] Use Z3 to find counterexamples for a 'guess solution' to a particular CHC system?
本文介绍了使用Z3为特定CHC系统的猜测解决方案找到反例?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
假设我有以下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屋!
查看全文