z3py:存在量词的用法

Question

此脚本

from z3 import *
solver = z3.Solver()
x = Int('x')
def f(y):
return y+y
solver.add(x >= 0, x < 10, Exists(x, f(x) == 4) )
print solver.check()
print solver.model()

给我

sat
[x = 0]

作为答案。这不是我想要或期望的。作为我想看到的答案

sat
[x = 2]

我发现另外两个帖子朝着类似的方向发展((Z3Py(声明函数和Z3中的量词(，但有些事情没有解决。

在这种情况下，您如何使用存在量词来获得足够的答案？

Answer 1

存在主义绑定了不同的x，其范围仅限于公式的主体。因此，您的约束实际上是(0 ≤ x <10( ∧ (∃ x' . f(x'( == 4(。两个合相都由x = 0的模型满足;特别是，第二个合相在此模型中得到满足，因为x'可能是2。

似乎你想进一步约束x，而不仅仅是不等式。尝试以下操作(未测试(

solver.add(x >= 0, x < 10, f(x) == 4)

，然后打印模型。