z3py：存在量词的使用
z3py: Usage of existential quantifier
这个脚本
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) declaring function and Quantifier in Z3)，但有些东西没有解决。
在这种情况下，您如何使用存在量词来获得充分的答案？
existential 绑定了一个不同的 x，其范围仅限于公式的主体。因此，您的约束实际上是 (0 ≤ x < 10) ∧ (∃ x' . f(x') == 4)。 x = 0 的模型满足这两个合取；特别是，第二个合取在此模型中得到满足，因为 x' 可能是 2.
看来您想进一步限制 x，而不仅仅是通过不等式。尝试以下（未测试）
solver.add(x >= 0, x < 10, f(x) == 4)
然后打印模型。
这个脚本
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) declaring function and Quantifier in Z3)，但有些东西没有解决。
在这种情况下，您如何使用存在量词来获得充分的答案？
existential 绑定了一个不同的 x，其范围仅限于公式的主体。因此，您的约束实际上是 (0 ≤ x < 10) ∧ (∃ x' . f(x') == 4)。 x = 0 的模型满足这两个合取；特别是，第二个合取在此模型中得到满足，因为 x' 可能是 2.
看来您想进一步限制 x，而不仅仅是通过不等式。尝试以下（未测试）
solver.add(x >= 0, x < 10, f(x) == 4)
然后打印模型。