Parallel solving in Z3

Question

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

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.

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?

Thank you

Answer 1

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

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)

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

---

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

(I was curious what Z3 was all about, so I also went looking in the C++ sources for parallel.enable. So that's where my answer started out from, before people who knew more answered. My findings left here for anyone interested...)

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

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.

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.

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

Answer 2

From the command line

If you are using the z3 executable, then you simply pass the setting in the command line. That is, if your script is in file a.smt2, use:

 z3 parallel.enable=true a.smt2

and z3 will use the parallel solver as it processes the benchmark. For instance:

$ 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)

Regular call:

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

Parallel mode:

$ 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)
)

Note the extra comments regarding the execution of the parallel mode in the second run.

Programmatically

If you're asking about how to use it from the programmatic API? For Python, it would look like:

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

I'm sure other API's have similar calls. (Caveat: I haven't actually used/tested this feature myself; and since it's rather new, it might be the case that not all programmatic APIs support it. Hopefully, you get a nice warning/error if that's the case!)