z3/python 实数 [英] z3/python reals
问题描述
使用 z3/python 网络界面,如果我问:
With the z3/python web interface, if I ask:
x = Real ('x')
solve(x * x == 2, show=True)
我很清楚:
Problem:
[x·x = 2]
Solution:
[x = -1.4142135623?]
我认为以下 smt-lib2 脚本会有相同的解决方案:
I thought the following smt-lib2 script would have the same solution:
(set-option :produce-models true)
(declare-fun s0 () Real)
(assert (= 2.0 (* s0 s0)))
(check-sat)
唉,我在 z3 (v3.2) 中得到 unknown
.
Alas, I get unknown
with z3 (v3.2).
我怀疑问题出在非线性项 (* s0 s0)
上,python 接口不知何故不受此影响.有没有办法在 smt-lib2 中编写相同的代码来获得模型?
I suspect the problem is with the non-linear term (* s0 s0)
, which the python interface somehow doesn't suffer from. Is there a way to code the same in smt-lib2 to get a model?
推荐答案
将 您的示例与 Z3 web 一起尝试界面,我得到sat
的结果.
Try your example with Z3 web interface, I get a result of sat
.
Z3 网页界面和 Z3Py 基于 Z3 v4.0,所以我认为这个问题在即将发布的版本中得到解决.
Z3 web interface and Z3Py are based on Z3 v4.0, so I think the problem is fixed in the upcoming release.
这篇关于z3/python 实数的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!