s Z3 无效模型的反例

Question

这是问题的扩展： 使用 Z3 查找特定 CHC 系统的"猜测解决方案"的反例？

在下面的代码中，我尝试使用 Z3 来获取 s 反例到我满足一些 CHC 子句的猜测候选者：

from z3 import *

x, xp = Ints('x xp') 
P = lambda x: x == 0
B = lambda x: x < 5
T = lambda x, xp: xp == x + 1
Q = lambda x: x == 5 
s = 10
def Check(mkConstraints, I, P , B, T , Q):
s = Solver()
# Add the negation of the conjunction of constraints
s.add(Not(mkConstraints(I, P , B, T , Q)))
r = s.check()
if r == sat:
return s.model()
elif r == unsat:
return {}
else:
print("Solver can't verify or disprove, it says: %s for invariant %s" %(r, I))
def System(I, P , B, T , Q):

# P(x) -> I(x)
c1 = Implies(P(x), I(x))
# P(x) / B(x) / T(x,xp) -> I(xp) 
c2 = Implies(And(B(x), I(x), T(x, xp)) , I(xp))
# I(x) / ~B(x) -> Q(x)
c3 = Implies(And(I(x), Not(B(x))), Q(x))
return And(c1, c2, c3)

cex_List = []
I_guess = lambda x: x < 3

for i in range(s):
cex = Check(System, I_guess, P , B , T , Q)
I_guess = lambda t: Or(I_guess(t) , t == cex['x'])
cex_List.append( cex[x] )
print(cex_List )

这个想法是使用 Z3 学习一个反例 x0 来猜测不变量 I，然后运行 Z3 来学习一个 I || 的反例(x == x0) 等等，直到我们得到 s 反例。但是，以下代码给出"递归错误：超出最大递归深度 '.我很困惑，因为我什至没有在任何地方以深度> 1 递归。谁能描述出了什么问题？

Answer 1

你的问题真的与z3无关;而是Python的特点。考虑一下：

f = lambda x: x
f = lambda x: f(x)
print(f(5))

如果你运行这个程序，你也会看到它落入了同一个无限递归循环，因为当你"到达"到内f时，外f再次绑定到自身。在您的情况下，这显示在以下行中：

I_guess = lambda t: Or(I_guess(t) , t == cex['x'])

通过使I_guess递归而落入相同的陷阱，这是您不希望的。

避免这种情况的方法是使用中间变量。这很丑陋，违反直觉，但这就是蟒蛇的方式！对于上面的示例，您可以将其编写为：

f = lambda x: x
g = f
f = lambda x: g(x)
print(f(5))

因此，您需要对I_guess变量执行相同的技巧。 请注意，由于您是迭代更新函数，因此您需要确保在每个步骤中记住该函数，而不是一遍又一遍地使用相同的名称。也就是说，每次创建新函数时捕获旧版本。当应用于上述情况时，它将如下所示：

f = lambda x: x
f = lambda x, old_f=f: old_f(x)
print(f(5))

这将确保迭代不会破坏捕获的函数。将此想法应用于您的问题，您可以按如下方式编写代码：

for i in range(s):
cex = Check(System, I_guess, P, B, T, Q)
I_guess = lambda t, old_I_guess=I_guess: Or(old_I_guess(t), t == cex[x])
cex_List.append(cex[x])

运行时，这将打印：

[2, 2, 2, 2, 2, 2, 2, 2, 2, 2]

没有任何无限递归问题。(这是否是正确的输出或您真正想要做的事情，我不确定。在我看来，你需要告诉 z3 给你一个"不同"的解决方案，也许你忘记了这样做。但这是一个不同的问题。我们在这里讨论的是一个Python问题，而不是z3建模。