如果我要求使用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,因此我认为此问题已在即将发布的版本中解决.