2

カスタム理論プラグインを作成しましたが、現時点では何もしません。コールバックはすべて実装および登録されていますが、単純に返されます。次に、Z3_parse_smtlib2_string を使用して一連の declare-consts、declare-fun、および assert を読み込み、結果の ast を Z3_assert_cnstr に渡します。Z3_check_and_get_model への後続の呼び出しは、次のエラーで失敗します。

mk_fresh_ext_data コールバックはユーザー理論用に設定されていません。Z3_theory_set_mk_fresh_ext_data_callback を使用する必要があります

私の知る限り、Z3_theory_set_mk_fresh_ext_data_callback は存在しません。

同じ文字列を使用しますが、理論プラグインを登録せずに、Z3_check_and_get_model は sat を返し、期待どおりのモデルを提供します。

バージョン 4 と Linux 64 ビット ライブラリを使用しています。

完全な例はこちら: http://pastebin.com/hLJ8hFf1

4

1 に答える 1

1

問題は、モデルベースの量指定子インスタンス化モジュール (MBQI) です。このモジュールは、メインの論理エンジンのコピーを作成しようとします。コピーを作成するには、Z3 はすべての理論プラグインをコピーする必要があります。それはすべての組み込み理論に対して実行できますが、外部理論に対しては実行できません。

元のセオリー プラグイン API は、MBQI モジュールより前に実装されていたため、自身のコピーをサポートしていませんでした。APIZ3_theory_set_mk_fresh_ext_data_callbackはそのためのものです。ただし、いくつかの理由でまだ公開されていません。主な問題は、Z3 4.0 にソルバー用の新しい API があることです。現在の理論プラグイン API は、新しいソルバー API と互換性がありません。それらを統合する方法を検討しています。Z3 4.0 では、セオリー プラグインは古い (非推奨の) ソルバー API でのみ機能します。

説明した問題を回避するには、MBQI モジュールを無効にするだけです。MBQI=false作成時に設定することで可能ですZ3_context。C では、次のコード フラグメントを使用してこれを行うことができます。

Z3_config cfg; 
Z3_context ctx;
cfg = Z3_mk_config();
Z3_set_param_value(cfg, "MBQI", "false");
ctx = Z3_mk_context(cfg);

これは、プラグインが量指定子のない式で機能する理由も説明しています。MBQI モジュールは、この種の式には使用されません。

于 2012-07-25T16:46:25.627 に答える