7

定理証明ツールz3は、数式を解くのにかなりの時間がかかります。これは、簡単に処理できるはずです。これをよりよく理解し、おそらくz3への入力を最適化するために、z3が解決プロセスの一部として生成する内部制約を確認したいと思いました。コマンドラインからz3を使用する場合、バックエンドソルバー用にz3が生成する数式を出力するにはどうすればよいですか？

4

1 に答える 1

12

Z3 コマンド ライン ツールには、そのようなオプションはありません。さらに、Z3 にはいくつかのソルバーと前処理ステップが含まれています。どの手順が役立つかは不明です。Z3 のソース コードは、https://github.com/Z3Prover/z3で入手できます。Z3 をデバッグ モードでコンパイルすると、追加のコマンド ライン オプションが提供されます-tr:<tag>。このオプションは、情報を選択的にダンプするために使用できます。たとえば、ソース ファイルnlsat_solver.cppには次の命令が含まれています。

TRACE("nlsat", tout << "starting search...\n"; display(tout); 
               tout << "\nvar order:\n"; 
               display_vars(tout););

コマンド ライン オプション-tr:nlsatは、Z3 に上記の命令を実行するように指示します。toutトレース出力ストリームです。ファイルに保存されます.z3-trace。Z3 ソースはこれらのTRACEコマンドでいっぱいです。コードが利用可能であるため、独自のトレース コマンドをコードに追加することもできます。

例を投稿すると、前処理と解決にどの Z3 コンポーネントが使用されているかがわかります。次に、トレースを有効にする「タグ」を選択できます。

EDIT（制約が投稿された後）：あなたの例は、整数と実数の非線形演算が混在しています。Z3の新しい非線形算術ソルバー (nlsat) は、 をサポートしていませんto_int。したがって、Z3 汎用ソルバーを使用して問題を解決します。このソルバーはほとんどすべてを受け入れますが、非線形実数演算については完全ではありません。このソルバーの非線形サポートは、区間解析とグロブナー基底計算に基づいています。このソルバーは、フォルダsrc/smt(不安定ブランチ内) に実装されています。算術モジュールはファイルに実装されていますtheory_arith*。適切なトレース コマンド ライン オプションは -tr:after_reduce. 前処理後の一連の制約が表示されます。ボトルネックは演算モジュール (theory_arith*）。

補足事項:

  • 問題は決定不能な断片にあります: 整数と実数の非線形演算が混在しています。つまり、このフラグメントに対して健全で完全なソルバーを作成することは不可能です。もちろん、実際に見つけたインスタンスを解決するソルバーを作成できます。nlsatを扱えるように拡張できると思いますto_int。

  • を避ければto_int使えるようになりますnlsat。問題は、非線形実数演算フラグメントにあります。to_intエンコーディングでは が重要なように思われるため、これが難しい場合があることは理解しています。

  • z3.codeplex.com の「unstable」ブランチのコードは、「master」ブランチの公式バージョンよりもはるかによく構成されています。すぐに「マスター」ブランチとマージします。ソースコードで遊んでみたい場合は、「不安定な」ブランチを取得できます。

  • 「unstable」ブランチは新しいビルド システムを使用します。トレース サポートを使用してリリース バージョンをビルドできます。-tMakefile を生成するときにオプションを使用するだけです。

python スクリプト/mk_make.py -t

  • Z3 がデバッグ モードでコンパイルされている場合AUTO_CONFIG=false、デフォルトでこのオプションが使用されます。したがって、「リリース」モードの動作を再現するには、コマンド ライン オプションを指定する必要がありますAUTO_CONFIG=true。
于 2012-10-27T18:37:55.053 に答える