1
、私が尋ねる場合：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）でunknownを取得します。
私は問題が非線形の用語(* s0 s0)であると思っていますが、これはどうやらPythonインターフェイスには影響しません。モデルを取得するためにsmt-lib2で同じコードを書く方法はありますか？
かなり正しい！これはs0の値に対して返される値です。 （root）（obsolete）（root-obj（+（^ 2））1））） "root-obj"関数が解釈されます。 Z3をクエリする他のツールがどのようにして実数を得ることができるかを示します。 –
それは私があまりにも不思議です。うまくいけば@Leoはそれを明確にすることができます。 – pad
Z3 4.0は、代数的な非合理的な数値をrepredentするためにroot-objを使用します。単変量多項式と索引で構成されています。上のroot-objはx^2 - 2の最初の根を表す-1.41 ... '（set-option：pp-decimal true）を使って10進表記で結果を表示するようにSMT 2.0に頼むことができます。 '制約解消や代数的数論に慣れていない群衆に到達することが目的なので、z3pyではデフォルトで小数点以下を使用しました。 –