小编Mic*_*din的帖子

假设我有一个z3求解器，其中包含一定数量的可满足的已声明约束。假设S为一组约束，我想为S中的每个约束验证将约束添加到求解器时公式是否仍可满足要求。可以通过以下方式轻松地按顺序完成此操作：

results = []

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

print all(results)

现在，我想并行化它来加快处理速度，但是我不确定如何使用z3正确地执行此操作。

这是一个尝试。考虑下面的简单示例。所有变量都是非负整数，并且必须求和为1。现在，我想验证每个变量x是否可以独立地设为> 0。令x = 1并将0赋给其他变量。这是一个可能的并行实现：

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 …