Z3中的并行求解 [英] Parallel solving in Z3

问题描述

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

One of the new features in Z3 4.8.1 is parallel solving:

并行模式可用于包括QF_BV在内的选择理论.经过设置parallel.enable = true Z3将产生许多工作线程与可应用多维数据集和征服解决目标.

A parallel mode is available for select theories, including QF_BV. By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the number of available CPU cores to apply cube and conquer solving on the goal.

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

It mentions that just parallel.enable=true needs to be set but I can't find that parallel structure in the code.

有人可以提供一些示例代码来查看如何实现此新功能吗?

Can someone provide some example code to see how to implement this new feature?

谢谢

推荐答案

简短回答:正如@LeventErkok指出的那样， parallel.enable = true 的语法适用于在命令行中使用z3可执行文件本身.正如他所说的那样，如果 @Claies的链接已表明，您正在使用绑定，则需要使用相关的 set_param()方法.对于 set_param("parallel.enable"，true);

Short answer: As @LeventErkok points out, the syntax of parallel.enable=true is for use in the command line to the z3 executable itself. And as he says and @Claies's link had indicated, if you are using a binding, you will want to use the relevant set_param() method. For C++ that is set_param("parallel.enable", true);

当我将其添加到 C ++绑定示例，它基本上给出了相同的输出...尽管它向stderr吐出了一些额外的信息，但是像这样的一行代码:

When I added this to the C++ binding example, it gave basically the same output...though it spat out some extra information to stderr, a bunch of lines like:

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

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

Which matches @LeventErkrok's observed difference using the z3 tool on another problem.

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

It mentions that just parallel.enable=true needs to be set but I can't find that parallel structure in the code.

((我很好奇Z3的全部功能，所以我也一直在C ++源代码中寻找parallel.enable.因此，这是我的答案从哪里开始的，在知道更多答案的人之前.我的发现留在这里)对于任何有兴趣的人...)

长答案::如果您正在查看z3本身的源代码，则找不到在其中编写的名为 parallel 的C ++对象.parallel.enable = true; .它是存储在由字符串名称管理的配置对象中的属性.该配置对象称为 parallel_params ，它不在GitHub中，因为它是在构建过程中生成的，生成到 src/solver/parallel_params.hpp

Long answer: If you're looking through the sources for z3 itself, you won't find a C++ object called parallel where you'd write parallel.enable = true;. It's a property stored in a configuration object managed by string names. That configuration object is called parallel_params, it's not in GitHub because it is generated as part of the build process, into src/solver/parallel_params.hpp

这些属性及其默认值的规范是 .pyg 文件中的每个模块的.这只是Python，由构建准备过程加载，并且 eval()并定义了一些内容.并行求解器选项位于 src/solver/parallel_params.pyg ，例如:

The specification for these properties and their defaults is per-module in a .pyg file. This is just Python which is loaded by the build preparation process and eval()'d with a few things defined. The parallel solver options are in src/solver/parallel_params.pyg, e.g.:

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 .

If you want to change these defaults while building z3, it looks like you have to edit the .pyg file, as there seems no parameterization for something like python scripts/mk_make.py parallel.enable=true.

作为更改此文件如何影响定义并行属性的已生成标头的示例，我直接修改了 parallel_params.pyg ，使其默认设置为"True"而不是"False".结果是对生成的 src/solver/parallel_params.hpp 文件进行以下两行比较:

As an example of how changing this file affects the generated header defining the parallel properties, I directly modified parallel_params.pyg to say "True" instead of "False" for its default. The consequence was the following 2-line diff to the generated src/solver/parallel_params.hpp file:

-- 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); }

这篇关于Z3中的并行求解的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！