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) 

然後打印模型。