Z3 中的并行求解

Question

Z3 4.8.1 中的新功能之一是并行求解：

并行模式可用于选定的理论，包括 QF_BV。通过设置 parallel.enable=true Z3 将产生与可用 CPU 内核数量成正比的工作线程数量，以在目标上应用立方体和征服解决方案。

它提到只parallel.enable=true需要设置，但我找不到parallel在代码中结构。

有人可以提供一些示例代码来了解如何实现这个新功能吗？

谢谢

Answer 1

简短回答：正如@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)

这与@LeventErkrok 在另一个问题上使用 z3 工具观察到的差异相匹配。

它提到只需要设置 parallel.enable=true ，但我在代码中找不到该并行结构。

（我很好奇 Z3 的全部内容，所以我还查看了 C++ 源代码中的 parallel.enable。所以这就是我的答案开始的地方，在知道更多答案的人之前。我的发现留给任何感兴趣的人...... )

长答案：如果您正在查看 z3 本身的源代码，您将找不到名为parallelwhere you'd write的 C++ 对象parallel.enable = true;。它是存储在由字符串名称管理的配置对象中的属性。该配置对象称为parallel_params，它不在 GitHub 中，因为它是作为构建过程的一部分生成的src/solver/parallel_params.hpp

这些属性及其默认值的规范是.pyg文件中的每个模块。这只是 Python，它由构建准备过程加载并且eval() 已经定义了一些东西。并行求解器选项在 中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为“True”而不是“False”作为其默认值。结果是生成的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); }

Answer 2

从命令行

如果您使用的是 z3 可执行文件，那么您只需在命令行中传递设置即可。也就是说，如果您的脚本在 file 中a.smt2，请使用：

 z3 parallel.enable=true a.smt2

z3 将在处理基准时使用并行求解器。例如：

$ cat a.smt2
(set-logic QF_AUFBV )
(set-option :produce-models true)
(declare-fun a () (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(assert (bvult a b))
(check-sat)
(get-model)

定期调用：

$ z3 a.smt2
sat
(model
  (define-fun a () (_ BitVec 32)
    #x00000000)
  (define-fun b () (_ BitVec 32)
    #x00000001)
)

并行模式：

$ z3 parallel.enable=true a.smt2
(tactic.parallel :progress 0% :closed 0 :open 1)
(tactic.parallel :progress 100% :status sat :closed 0 :open 0)
sat
(model
  (define-fun a () (_ BitVec 32)
    #x00000000)
  (define-fun b () (_ BitVec 32)
    #x00000001)
)

请注意有关在第二次运行中执行并行模式的额外注释。

以编程方式

如果您要问如何从编程 API 中使用它？对于 Python，它看起来像：

from z3 import *
set_param('parallel.enable', True)

我确信其他 API 也有类似的调用。（警告：我自己并没有实际使用/测试过这个功能；而且由于它是相当新的，可能不是所有的编程 API 都支持它。如果是这种情况，希望你得到一个很好的警告/错误！）