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) declaring function和Quantifier in Z3）去的事，但不奏效。

在这种情况下，你如何使用存在的量词来获得充分的答案？

Answer 1

存在与不同的x绑定，其范围仅限于公式的主体。因此，您的约束实际上是（0≤x < 10）∧（∃x'。f（x'）== 4）。这两个连词都满足一个模型，其中x = 0;特别是在该模型中满足第二个合并因为x'可能是。

看来，你想进一步约束x，不仅仅是不平等。试试以下（未经测试）

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

然后打印模型。