Z3py無法解決電源操作員

Question

我是Z3py的新手，並且使用了最新的z3py z3-4.4.2.4e7a867cd995-x64-win。但是，我只是想知道爲什麼z3py無法解決以下代碼。

from z3 import * 
x = Int('x') 
s = Solver() 
s.add(x**2 == 4) 
print s.check() 

我不明而不是坐在。

Answer 1

當x = Int('x')更改爲x = Real('x')時，您可以獲得sat。

我認爲解決發展方程的規定有一個規則，變量的類型應該是Real。