Solving formulas in parallel with z3

Question

Let's say I have a z3 solver with a certain number of asserted constraints that are satisfiable. Let S be a set of constraints, I would like to verify for every constraint in S whether the formula is still satisfiable when adding the constraint to the solver. This can be easily done sequentially in such a fashion:

results = []

for constraint in S:
  solver.push()
  solver.add(constraint)
  results.append(solver.check() == z3.sat)
  solver.pop()

print all(results)

Now, I would like to parallelize this to speed things up, but I'm not sure how to do it properly with z3.

Here is an attempt. Consider the following simple example. All variables are non negative integers and have to sum to 1. Now I would like to verify whether every variable x can independently be made > 0. Obviously it is the case; let x = 1 and assign 0 to the other variables. Here is a possible parallel implementation:

from multiprocessing import Pool
from functools import partial
import z3

def parallel_function(f):
    def easy_parallize(f, sequence):
        pool   = Pool(processes=4)
        result = pool.map(f, sequence)

        pool.close()
        pool.join()

        return result

    return partial(easy_parallize, f)

def check(v):
    global solver
    global variables

    solver.push()
    solver.add(variables[v] > 0)
    result = solver.check() == z3.sat
    solver.pop()

    return result

RANGE = range(1000)
solver = z3.Solver()
variables = [z3.Int('x_{}'.format(i)) for i in RANGE]

solver.add([var >= 0 for var in variables])
solver.add(z3.Sum(variables) == 1)

check.parallel = parallel_function(check)
results = check.parallel(RANGE)
print all(results)

Surprisingly this works perfectly on my machine: the results are sound and it is much faster. However, I doubt that it is safe since I'm working on a single global solver and I can easily imagine the push/pops to happen concurrently. Is there any clean/safe way to achieve this with z3py?

Answer 1

Indeed, this might work for a first test, but not in general. Parallel solving on a single Context is not supported and there will definitely be data races and segfaults later.

In Python, the Context object is hidden, so most users won't have to deal with it, but to run things in parallel, we need to set up one Context per thread and then pass the right one to all other functions (which implicitly used the hidden Context before). Note that all expressions, solvers, tactics, etc, all depend on one particular Context, so if objects need to cross that boundary we need to translate them (see translate(...) in AstRef and similar).

See also Multi-threaded Z3? and When will the Z3 parallel version be reactivated?