时间戳

首页 > 解决方案 > Z3 中的并行求解

c++ - Z3 中的并行求解

问题描述

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

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

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

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

谢谢

标签： c++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)

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

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

（我很好奇 Z3 是关于什么的，所以我也去寻找并行的 C++ 源代码。这就是我的答案开始的地方，在知道更多答案的人之前。我的发现留给任何感兴趣的人...... )

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

这些属性及其默认值的规范是.pyg文件中的每个模块。这只是由构建准备过程加载的 Python，并且eval()'d 定义了一些东西。并行求解器选项位于 中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); }

推荐阅读