Z3での並列解法

簡単な答え： @LeventErkokが指摘しているように、の構文はparallel.enable=true、z3実行可能ファイル自体のコマンドラインで使用するためのものです。そして彼が言い、@ Claiesのリンクが示しているように、バインディングを使用している場合は、関連するset_param()方法を使用することをお勧めします。C ++の場合set_param("parallel.enable", true);

これをC ++バインディングの例に追加すると、基本的に同じ出力が得られました... stderrにいくつかの追加情報を吐き出しましたが、次のような一連の行があります。

(tactic.parallel :progress 0% :closed 0 :open 1)
(tactic.parallel :progress 100% :status sat :closed 0 :open 0)

これは、別の問題でz3ツールを使用して@LeventErkrokが観察した違いと一致します。

parallel.enable = trueを設定する必要があると記載されていますが、コード内にその並列構造が見つかりません。

（Z3が何であるか興味があったので、parallel.enableのC ++ソースも調べました。それで、もっと知っている人が答える前に、そこから答えが始まりました。私の発見は、興味のある人のためにここに残されました... ）

長い答え： z3自体のソースを調べている場合、parallelどこに書き込むかというC ++オブジェクトは見つかりませんparallel.enable = true;。これは、文字列名によって管理される構成オブジェクトに格納されているプロパティです。その構成オブジェクトは呼び出されますがparallel_params、ビルドプロセスの一部として生成されるため、GitHubにはありません。src/solver/parallel_params.hpp

これらのプロパティとそのデフォルトの仕様は、.pygファイル内のモジュールごとです。これは、ビルド準備プロセスによってロードされ、いくつかの定義が含まれたeval（）されたPythonです。並列ソルバーのオプションはsrc/solver/parallel_params.pyg次のとおりです。

def_module_params('parallel',
    description='parameters for parallel solver',
    class_name='parallel_params',
    export=True,
    params=(
        ('enable', BOOL, False, 'enable parallel solver ...'),
        ('threads.max', UINT, 10000, 'caps maximal number of threads ...'),
        # ...etc.

z3のビルド中にこれらのデフォルトを変更したい場合は.pyg、のようなパラメータ化がないように見えるため、ファイルを編集する必要があるようpython scripts/mk_make.py parallel.enable=trueです。

このファイルを変更すると、並列プロパティを定義する生成されたヘッダーにどのように影響するかの例として、parallel_params.pygデフォルトで「False」ではなく「True」と言うように直接変更しました。その結果、生成されたsrc/solver/parallel_params.hppファイルに対して次の2行の差分が作成されました。

-- a/src/solver/parallel_params.hpp
+++ b/src/solver/parallel_params.hpp
@@ -9,7 +9,7 @@ struct parallel_params {
   parallel_params(params_ref const & _p = params_ref::get_empty()):
      p(_p), g(gparams::get_module("parallel")) {}
   static void collect_param_descrs(param_descrs & d) {
-    d.insert("enable", CPK_BOOL, "enable parallel solver by default on selected tactics (for QF_BV)", "false","parallel");
+    d.insert("enable", CPK_BOOL, "enable parallel solver by default on selected tactics (for QF_BV)", "true","parallel");
     d.insert("threads.max", CPK_UINT, "caps maximal number of threads below the number of processors", "10000","parallel");
     d.insert("conquer.batch_size", CPK_UINT, "number of cubes to batch together for fast conquer", "100","parallel");
     d.insert("conquer.restart.max", CPK_UINT, "maximal number of restarts during conquer phase", "5","parallel");
@@ -23,7 +23,7 @@ struct parallel_params {
      REG_MODULE_PARAMS('parallel', 'parallel_params::collect_param_descrs')
      REG_MODULE_DESCRIPTION('parallel', 'parameters for parallel solver')
   */
-  bool enable() const { return p.get_bool("enable", g, false); }
+  bool enable() const { return p.get_bool("enable", g, true); }
   unsigned threads_max() const { return p.get_uint("threads.max", g, 10000u); }
   unsigned conquer_batch_size() const { return p.get_uint("conquer.batch_size", g, 100u); }
   unsigned conquer_restart_max() const { return p.get_uint("conquer.restart.max", g, 5u); }