私は C API/JNA/Scala 経由で SMT2 で Z3 を使用していますが、かなりうまく機能しているようです。
増分解法を試してみたい。最初に、Z3_parse_smtlib2_stringを使用してこれを翻訳します。
(declare-fun x () Int)
(assert (>= x 0))
(check-sat)
(get-model)
次に、 Z3_ast を取得し、それをZ3_solver_assertを介してソルバーに入れ、Z3_solver_checkでチェックし、 Z3_solver_get_model を介してモデルを取得します(この例では、チェックが満足できるものを返した場合)。これまでのところ問題はありません。
しかし、さらに次のようなことを主張したい場合:
(assert (= x 1))
Z3_parse_smtlib2_stringが呼び出された時点で動けなくなります。これは、x が不明な定数であると不平を言うためです。2番目のスニペットにdeclare-funも追加すると、無効な引数エラーが発生します。この変数は既に環境に存在するべきではありませんか? Z3_parse_smtlib2_stringの追加パラメーターを設定する必要がありますか? 以前に解析された式からそれらを取得するにはどうすればよいですか?
また、(set-option :global-decls true)を使用しても機能しませんでした。これは、Z3 がこのオプション値を初期化後に変更できないことを通知したためです。
この問題を解決する方法を知っている人はいますか?