`eval`をタイムアウトに呼び出す

Question

Leonardo：迅速な返信をありがとう！とても有難い。

私は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)) 

Z3が正常にアイデンティティ機能を付与されs1モデルを構築します。しかし、evalを呼び出すと、Z3はタイムアウトします。私が設定する必要がある特定のオプションはありますか？

(set-option :MBQI true) 

その後Z3はunknownを応答します。

はまた、私は行を削除する場合ことに気づきました。 QBVFは決定可能なので、それは私がオプションを設定する必要があったのは少し驚きでした。すべてのQBVFの問題でMBQIをtrueに設定する必要があるのでしょうか、またはこのインスタンスに関して何か特別なことがありますか？ QBVFが決定可能フラグメントであるが、唯一のMBQIエンジンがそれを決めることができる等のE-マッチング、MBQI、重ね合わせ、 ：

おかげで..

Answer 1

Z3は、いくつかの数量を処理するためのエンジンを持っています。 Eマッチングモジュールは、式が満たされないことを示す場合にのみ有効です。 充足可能なインスタンスが常に失敗（不明を返します）します。 重畳モジュールは、純粋な（理論無し）一次論理式で有効です。

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

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

evalコマンドについては、これはバグですので、修正します。修正はZ3 3.2で利用可能になります。