假设我有一个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 …先前问题中指出的安装问题仍然存在.我曾尝试在Windows XP SP3 32位和Windows 7 64位下安装Z3 4.3.0和4.1.这些组合都不起作用!我能够做" from z3 import *",但是init()Z3 dll的失败.我的Python版本是2.7.3.Z3独立和Python独立工作,但没有很多抱怨它们不能一起工作.
这将有助于获得最新的安装配方,回答以下问题:
应该使用哪个Z3下载(源版本,预编译版本)？
应该使用哪个Python版本？
在init()调用中应该引用哪个或哪些Z3 DLL？一个例子会有所帮助(包括带空格的路径的原始字符串用法).
应该使用哪些Z3 Python源文件(Z3的某些下载有*.py文件,其他有*.pyc文件)？编译的Python文件是否与多个Python版本兼容？
如何设置PATH和PYTHONPATH？
如何以自动提供Z3初始化的方式调用Python的IDLE shell？
对不起,如果这听起来像是一个新手问题,但......