使用 z3/python Web 界面,如果我问:
x = Real ('x')
solve(x * x == 2, show=True)
我很好地理解:
Problem:
[x·x = 2]
Solution:
[x = -1.4142135623?]
我认为以下 smt-lib2 脚本会有相同的解决方案:
(set-option :produce-models true)
(declare-fun s0 () Real)
(assert (= 2.0 (* s0 s0)))
(check-sat)
唉,我对 z3 (v3.2) 感到未知
。
我怀疑问题出在非线性项(* s0 s0)
上,而Python接口(interface)在某种程度上并没有受到这个问题的影响。有没有办法在 smt-lib2 中编写相同的代码来获取模型?
最佳答案
尝试your example通过 Z3 Web 界面,我得到了 sat
的结果。
Z3 Web 界面和 Z3Py 基于 Z3 v4.0,因此我认为该问题在即将发布的版本中已得到解决。
关于python - z3/python 实数,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/9969616/