z3 - 非線形算術および未解釈関数

Question

(declare-const x Real)
(declare-fun f (Real) Real)
(assert (= (f 1.0) 0.0))
(assert (= (* x x) (* 1.0 1.0)))
(check-sat)
(get-model)

私は2つの独立したアサーションを持っています。1つは非線形算術と他の未解釈の関数です。Z3は、上記の問題に「モデルが利用できません」を与えます。ロジックを両方を同時に処理できるものに設定する方法はありますか？ありがとうございました。

Answer 1

新しい非線形ソルバーは、まだ他の理論 (配列、未解釈関数、ビットベクトル) と統合されていません。Z3 4.0 では、非線形算術アサーションのみを含む問題を解決するためにのみ使用できます。これは、将来のバージョンで変更される予定です。