z3 - Z3INIオプションの詳細なドキュメント

Question

Z3のINIオプションの詳細なドキュメントはありますか。QF_BVの問題に最適なオプションを見つけるために、試行錯誤のアプローチをとらなければなりませんでした。z3の実行を高速化するオプションが他にもあるかどうかはまだわかりません。誰かがINIオプションの既存の詳細な説明を指摘できれば素晴らしいと思います。

ありがとう。

Answer 1

現在、Z3を再構築しており、「千」のパラメーターを持つソルバーというアプローチから離れています。Z3は、ソルバーを組み合わせて戦略を指定するための、よりモジュール化された柔軟なアプローチに移行しています。この新しいアプローチの詳細については、次のドラフトを参照してください。

INIオプションに関しては、それらのいくつかは非推奨であり、新しいアプローチへの移行をまだ完了していないためにのみ存在します。これらのオプションのいくつかは特定のプロジェクトのために追加され、現在は廃止されています。これらは、下位互換性のためにのみ存在します。

QF_BVに関して、Z3 3.2には2つのQF_BVソルバーが含まれています。古い（2.xのもの）と新しいものです。新しい（公式の）ものは、Z3の公式入力形式であるSMT2.0でのみ使用できます。SMT 1.0、Simplify、およびZ3の低レベル入力フォーマットは廃止されました。Z3 3.xのパフォーマンスの向上のほとんどは、SMT2.0入力フォーマットを使用する場合にのみ利用できます。

数か月以内に、戦略仕様言語がZ3で正式にサポートされる予定です。使用方法を説明するチュートリアルとドキュメントがあります。それまでの間、QF_BVなどのロジックにはデフォルト構成とSMT2.0入力フォーマットを使用することを強くお勧めします。