3

私は Z3 を使用して、CUTE、DART、または (おそらく) SAGE と非常によく似た、深さ優先の順序で状態空間を探索するシンボリック エグゼキューターによって生成されたパス条件を解決しています。Z3 のさまざまな使用方法を実験しています。極端な場合、すべてのクエリを Z3 に送信し、その直後に (リセット) します。もう 1 つは、すべての追加の分岐制約を (プッシュ) し、パス条件を正しく弱めるために必要な最小限のバックトラックを (ポップ) (ポップ) します。問題は、すべての状況で他の戦略よりもうまく機能する戦略がないように見えることです。プッシュは最高の利点を提供するようですが、すべてのクエリの後に Z3 をリセットすると、プッシュ/ポップを実行するよりも 1 桁以上高速になるいくつかのケースに遭遇しました。通信のオーバーヘッドはごくわずかであることに注意してください。ほとんどすべての時間が check-sat 内で費やされます。

共有する経験がある人、または Z3 によって内部的に保持されている状態 (レンマなど) に関する何らかの兆候があり、その動作を明確にするのに役立ちますか? また、他の SMT ソルバーの動作はどうですか?

4

1 に答える 1

4

次のリリース (v4.3.2) では、役に立つ機能が公開されます。Z3 のデフォルト ソルバーは、非インクリメンタル ソルバーとインクリメンタル ソルバーを組み合わせたものです。push/を使用するpop(またはcheckを呼び出さずに複数の を使用するreset) 場合、Z3 はインクリメンタル ソルバーを使用します。次のリリースでは、インクリメンタル ソルバーにタイムアウトを提供できます。インクリメンタル ソルバーが指定されたタイムアウト内に問題を解決できない場合、Z3 は自動的に非インクリメンタル ソルバーに切り替えます。おそらく、この機能を使用すると、「両方の世界」を最大限に活用できるようになるでしょう。次のリリース候補のソース コードを取得するには、次を使用する必要があります。

git clone https://git01.codeplex.com/z3 -b rc

それをコンパイルするには、次を使用します

cd z3
python scripts/mk_make.py
cd build
make

インクリメンタル ソルバーのタイムアウトを設定するには、次のコマンド ライン オプションを指定する必要があります。

 combined_solver.solver2_timeout=<time in milliseconds>

プログラム API を使用している場合は、新しい API で次のことができます。

Z3_global_param_set(Z3_string param_id, Z3_string param_value)

次のリリースでは、パラメータを設定するための新しいフレームワークが導入されることに注意してください。これにより、ユーザーは内部 Z3 モジュールのパラメーターを設定できます。

于 2013-01-13T18:24:59.203 に答える