z3 / python实数
作者:互联网
如果我要求使用z3 / python网络界面,请执行以下操作:
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接口不以某种方式受其困扰.有没有一种方法可以在smt-lib2中对相同的代码进行编码以获得模型?
解决方法:
尝试使用Z3 Web界面your example,我得到了sat的结果.
Z3 Web界面和Z3Py基于Z3 v4.0,因此我认为此问题已在即将发布的版本中解决.
标签:z3,python 来源: https://codeday.me/bug/20191012/1902196.html