Z3 INIオプションの詳細な文書

Question

ZIのINIオプションの詳細な文書はありますか？ QF_BVの問題に対する最良の選択肢を理解するためには、試行錯誤のアプローチが必要でした。 z3をもっと速く走らせるオプションがあるかどうかはまだ分かりません。誰かがINIオプションの既存の詳細な説明を指し示すことができれば幸いです。

ありがとうございました。

Answer 1

現在、Z3を再構築し、アプローチから離れています：「1000」パラメータを持つソルバー。 Z3は、ソルバーを組み合わせて戦略を指定するために、モジュラーで柔軟なアプローチに移行しています。 この新しいアプローチの詳細については、draftをご覧ください。

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

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

数ヶ月で、戦略仕様言語がZ3で正式にサポートされる予定です。 チュートリアルと使用方法を説明するドキュメントを用意します。 その間、QF_BVなどのロジックにはデフォルト設定とSMT 2.0入力形式を使用することを強くお勧めします。