我是 z3 的新手。我正在嘗試使用 z3 運行以下 python 示例。
from z3 import *
x = Real('x')
y = Real('y')
s = Solver()
s.add(And(x y>1,x==0.00001,y==0.1))
print(s.check())
回傳的結果是sat，我認為這是不正確的，因為 x y=0.10001<1。我也列印出求解器
[And(x y > 1, x == 1/0, y == 1/10)]
我注意到其中分母為 0 的項 x==1/0。我正在使用在 macOS 10.14.6 Mojave 上運行的 Python 3.9.8、z3-solver 4.8.12.0。
我還在裝有 Ubuntu 20.04、python3.8 和 z3-solver 4.8.10.0 的機器上嘗試了完全相同的示例。回傳的結果是unsat，列印出求解器時，分母中沒有 0。
有誰知道我在這里做錯了什么？非常感謝您提前。
uj5u.com熱心網友回復：
我不能用 z3 4.8.14 復制這個；它列印的地方unsat，就像你在 4.8.10 中發現的那樣。您應該簡單地升級您的 z3 版本。
之前有關于此的問題，并且在某些化身中出現小數字，例如0.00001未正確翻譯。我懷疑你也有同樣的痛苦。請參閱此處：為什么 Z3 將小實數“四舍五入”為 1.0/0.0？
升級是最好的；如果您無法嘗試那里的建議：與其使用0.00001，不如嘗試Q(1, 100000)。
轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/375678.html
上一篇：如何在Swift5中以編程方式在特定螢屏（即主顯示幕而不是外部顯示幕）上顯示視窗？[蘋果系統;Xcode15]
下一篇：理解gitpush語法的含義