Z3（NET API）の充足可能性のモデリング/チェックに必要なメモリと時間を確認するには

Question

私はZ3とYicesといくつかの研究上の問題を解決するために1年未満で作業しています。これらのソルバを使用して、私は常に性能、特にモデリング/チェック（満足度）に必要な時間と空間（メモリ）の2つを評価する必要があります。 Z3の場合、私はそれらを直接見つける手がかりは見つけられませんでした。私は "統計"（Z3 NET APIで提供されている "DisplayStatistics"機能を使用）を試して、次のような出力を見つけました：

num。競合：122

num。決定：2245

num。伝播：27884（バイナリ：21129）

num。再起動：1

num。最終チェック：1

num。分。リット：52

num。追加された数：3766

num。 mk bool var：2782

num。デルブールvar：658

num。 mk enode：1723

num。 del enode：78

num。 mk句：3622

num。 del句：1517

num。 mk bin句：3067

num。 mk lits：18935

num。競合：28

num。行を追加：5091

num。ピボット：328

num。アサート下限：2597

num。上位アサート：3416

num。 diseertをアサート：1353

num。バインドされた小道具：787

num。固定式：697

num。オフセットeqs：866

num。擬似番号：34

num。 eq。アダプタ：820

私は、使用されたメモリ/時間を理解するためにこれらの値をどのように解釈するのか分かりません。実行時間を見つける方法はいくつかあります（Stopwatchのようなタイマークラスを使用します）。しかし、スペースが必要な場合には、私は何も見つかりませんでした。モデリングに必要なブール変数（低レベル、SATソルバ）の数を得ることができれば、私にとってはうまくいくでしょう。

誰でも私に解決策を見せることができれば嬉しいです。

Answer 1

あなたはどのバージョンのZ3を使用していますか？最新バージョン（Z3 3.2）には、メモリ消費統計が含まれています。 max. heap sizeと表示されます。つまり、Z3の性能を評価する最良の方法は、z3.exeを使用することです。 Z3実行可能ファイルは、時間とメモリ消費を報告します。さらに、いくつかのパフォーマンス改善はまだAPIを通じて利用できません。

いくつかのアプリケーションでは、テキストインターフェイスが理想的なオプションです。つまり、アプリケーションはパイプを介してSMT 2.0コマンドを使用してZ3プロセスと通信します。主な利点は次のとおりです。異なるSMTソルバーを使用して比較するのは非常に簡単です。 Z3を殺して再起動するのは簡単です。いくつかの異なるプロセスを作成できます。 Z3が死んでもアプリケーションは死ぬことはありません。もちろん、このソリューションは、何千もの簡単なクエリを実行するアプリケーションや、Z3との緊密な統合を必要とするアプリケーション（たとえばScala^Z3）には適していません。