假设我有一个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>很明显是这样的;设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 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)

令人惊讶的是,这在我的机器上完美运行：结果是合理的,而且速度更快.但是,我怀疑它是安全的,因为我正在研究一个单一的全局求解器,我可以很容易地想象推/弹同时发生.是否有任何干净/安全的方法来实现z3py？

解决方法:

实际上,这可能适用于第一次测试,但不是一般的.不支持在单个Context上并行求解,以后肯定会出现数据争用和段错误.

在Python中,Context对象是隐藏的,因此大多数用户不必处理它,但是为了并行运行,我们需要为每个线程设置一个Context,然后将正确的一个传递给所有其他函数(隐含地)之前使用了隐藏的Context.请注意,所有表达式,求解器,策略等都依赖于一个特定的Context,因此如果对象需要越过该边界,我们需要翻译它们(请参阅AstRef中的translate(…)等).

另见Multi-threaded Z3?和When will the Z3 parallel version be reactivated?