1

[1] で説明されている決定/インスタンス化手順 (その実装を含む) の「実際的な」影響をテストすることに興味があります。

私は欲しい：

1) SMT ベンチマークを取得し、(おそらく完全な) インスタンス化されたバージョンを返し、戦略を適用する「ツール」。これが不可能な場合は、

2) この戦略を実装する Z3 バージョンと、オンとオフを切り替えるオプション。

それについて私を助けてもらえますか？

[1] Modulo Theories による充足可能性における定量化された数式の完全なインスタンス化

4

1 に答える 1

1

私の知る限り、SMT ベンチマークのインスタンス化されたバージョンを返すツールはありません。Z3 は、[1] のセクション 6 で説明されている Model-Based Quantifier Instantiation (MBQI) を使用して、オンデマンドで量指定子をインスタンス化します。最新の Z3 の実際のループは、このセクションで説明したものよりも複雑です。

MBQI モジュールを有効/無効にする方法に関する注意事項を次に示します。

  • まず、コマンドを使用して自動構成を無効にする必要があります

(set-option :auto-config false)

  • Z3 4.x は、量指定子の処理に MBQI と E-Matching を使用します。両方を無効にするコマンドを使用する必要があります。
(set-option :ematching false)
(set-option :mbqi false)
  • それらを有効にするには、次を使用する必要があります。
(set-option :ematching true)
(set-option :mbqi true)

これらのオプションを使用すると、さまざまな問題で MBQI と E-Matching の効果を確認できます。E マッチングのみを使用する場合、Z3unknownは量指定子を含む充足可能な問題に対して返されることに注意してください。

MBQI モジュールは、ファイルsrc/smt/smt_model_finder.cppとsrc/smt/smt_model_checker.cpp. ファイルsrc/smt/smt_model_finder.cppは本質的に、普遍的に量化された式を満たす可能性のあるモデルで、量指定子のない式用に作成されたモデルを変換しています。このクラスauf_solverは、設定された制約を実際に「解決」し、[1] で説明されている射影関数を「構築」するクラスであることに注意してください。

MBQI モジュールによって生成された実際のインスタンスをトレースしたい場合は、 でメソッドvoid model_checker::assert_new_instances()を変更できsrc/smt/smt_model_checker.cppます。これらのメソッドには、tout(トレース出力) にデータを送信するいくつかのトレース コマンドが既にあることに注意してください。に置き換えtoutてstd::cout、標準出力に関する情報を取得できます。たとえば、次のコードを追加すると、ユニバーサル量指定子qが (MBQI モジュールによって) 何らかのバインディングでインスタンス化されるたびに、Z3 は標準出力に情報を表示します。

std::cout << "[New-instance]\n" << mk_pp(q, m_manager) << "\n";
std::cout << "[Bindings]\n";
for (unsigned i = 0; i < num_decls; i++) {
    expr * b = inst->m_bindings[i];
    std::cout << mk_pp(b, m_manager) << "\n";
}
std::cout << "[End-New-Instance]\n";
于 2012-11-19T19:15:15.137 に答える