2

SMTLIB2式の完全なモデルが必要です。

http://pastebin.com/KiwFJTrK

Z3（バージョン3.2および4.0）は、すべての変数の値を返しますが、var4の値は返しません。私は次のようないくつかの構成設定を試しました

MODEL_COMPLETION = true

しかし、それはうまくいかなかったようです。誰か提案がありますか？比較すると、CVC3はモデル（var4を含む）を返すため、SMTLIBまたは私の例の問題ではありません。

これが必要な理由は、ここで詳しく説明されています。つまり、増分解決にCAPIを使用したいと思います。このため、関数Z3_parse_smtlib2_stringを複数回使用する必要があります。この関数には、以前に宣言された関数と定数がパラメーターとして必要です。これらの種類の関数は、Z3_parse_smtlib2_stringではなく、z3_parse_smtlib_stringが呼び出されたときにのみ機能するため、Z3_get_smtlib_declを介してこの情報を取得できません。

4

1 に答える 1

3

スクリプトの先頭に次のオプションを追加すると、この問題を回避できます。

(set-option :auto-config false)

次のリリースのために修正します。何が起こっているのかを簡単に説明します。Z3 には、0 ～ 1 の整数問題のソルバーがあります。前処理の後、スクリプトは Z3 によって 0-1 整数問題としてタグ付けされます。の値はvar4、問題が 0-1 の問題として表示される場合は「ドント ケア」ですが、整数の問題として表示される場合は「ドント ケア」ではありません ( var40 または 1 でなければなりません)。 . デフォルトでは、Z3 は「don't care」変数の値を表示しません。

モデルに含まれていない定数のMODEL_COMPLETION=true値を要求すると、モデルが完成します。たとえば、 を実行する(eval var4)と、Z3 は の解釈を生成しvar4ます。

于 2012-06-20T15:04:55.533 に答える