1

レオナルド：迅速な返信ありがとうございます！とても有難い。

次のスクリプトをZ3にフィードすると、次のようになります。

(set-option :MBQI true)
(set-option :produce-models true)
(declare-fun s1 ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((s0 (_ BitVec 16))) (bvuge s0 (s1 s0))))
(check-sat)
(get-model)
(eval (s1 #x0000))

s1Z3は、恒等関数が与えられているモデルを正常に構築します。ただし、evalを呼び出すと、Z3がタイムアウトします。設定する必要のある特定のオプションはありますか？

また、次の行を削除すると、次のことに気付きました。

(set-option :MBQI true)

次に、Z3が応答しunknownます。QBVFは決定可能であるため、オプションを設定する必要があるのは少し驚きでした。すべてのQBVF問題でMBQIを設定する必要があるのtrueは事実ですか、それともこのインスタンスに特別な何かがありますか？

ありがとう..

4

1 に答える 1

1

Z3には、数量詞を処理するためのいくつかのエンジンがあります。Eマッチング、MBQI、重ね合わせなどです。QBVFは決定可能なフラグメントですが、MBQIエンジンのみが決定できます。E-matchingモジュールは、数式が不十分であることを示す場合にのみ効果的です。満足のいくインスタンスの場合、常に失敗します（不明を返します）。重ね合わせモジュールは、純粋な（理論のない）一階述語論理式で効果的です。

Z3の一部のバージョンでは、MBQIモジュールは非常に高価であるため、デフォルトで有効になっていません。VCCやSpec＃などの一部のアプリケーションは、MBQIでサポートできる決定可能なフラグメントに含まれていない非常に複雑な定量化された式を使用します。したがって、MBQIモジュールは、これらのアプリケーションのオーバーヘッドにすぎません。Z3 3.1（Z3 Webサイトからダウンロード可能）では、MBQIはデフォルトで有効になっています。

今後のZ33.2では、ロジックUFBVが正式にサポートされる予定です。UFBVは、QBVFのSMT-LIB名です。したがって、使用できるようになり(set-logic UFBV)、Z3はこのロジック用に自動的に構成されます。

コマンドに関してはeval、これはバグです。修正します。修正はZ33.2で利用可能になります。

于 2011-09-09T18:32:34.723 に答える