Python中的多处理Z3答案

【问题标题】：Multiprocessing Z3 in PythonPython中的多处理Z3
【发布时间】：2021-06-23 22:46:04
【问题描述】：

我有一大堆我希望 Z3 在我的 Python 项目中合成的各种类型的对象。由于与要合成的每个对象相关联的约束是独立的，因此该过程可以完全并行化。也就是说，不是一次合成一个值，如果我有一台 4 核的机器，我可以同时合成 4 个值。为此，我们必须使用 Python 的 multiprocessing 包而不是 threading（由于 GIL 以及工作负载应该受 CPU 限制的事实）。

为简单起见，假设我有一个简单的str 合成器，它合成一个新的str，它在字典上小于给定的输入value，如下所示：

def lt_constraint(value):
    solver = Solver()
    # do a number of processing on 'value', which is an input string
    # ... define char and _chars in code here
    template = Concat(Re(StringVal(value[:offset])), char, Star(_chars))
    solver.add(InRe(String("var"), template))
    if solver.check() == sat:
        value = solver.model()[self.var]
        return convert_to_str(value)

现在如果我有多个values，我想并行运行上面的函数：

from pathos.multiprocessing import ProcessingPool as Pool
with Pool(processes=4) as pool:
    value_list = ['This', 'is', 'an', 'example']
    synthesized_strs = pool.map(lt_constraint, value_list)

我使用pathos 希望它能处理酸洗问题，但我仍然收到此错误：

TypeError: cannot pickle 're.Match' object

我认为这是因为 Z3 使用了re 中的方法，并且在酸洗lt_constraint() 时需要酸洗它们，但dill 不能酸洗这些。

对于我的情况，是否有任何其他方法可以并行化 Z3（除了为re 自己实施酸洗或其他方法）？

谢谢！

【问题讨论】：

如果你的框架依赖于酸洗/序列化，你必须自己实现。 Solver.to_string 为您提供求解器中约束的文本表示，但将它们加载到另一个求解器中可能不一定是轻松的。并行设置的一个常见使用模式是在每个线程/核心上简单地使用 Z3 上下文，并且为每个上下文创建所有约束（还有在上下文之间转换的转换函数）。

标签： python parallel-processing pickle z3 z3py

【解决方案1】：

当您包含整个代码时，Stack-overflow 的效果最好，因此人们可以尝试使用它。话虽如此，我在以下方面很幸运：

from z3 import *
import concurrent.futures

def getVal(value):
    solver = Solver()
    var = Int('var')
    solver.add(var > value)
    if solver.check() == sat:
        return solver.model()[var].as_long()
    else:
        return 'CANT SOLVE'

with concurrent.futures.ThreadPoolExecutor() as executor:
    futures = [executor.submit(getVal, i) for i in [1, 2, 3]]
    results = [f.result() for f in futures]
    print(results)

打印出来：

$ python3.9 a.py
[2, 3, 4]

如果没有您实际构建lt_constraint 的详细信息，很难判断这是否适用于您的情况。但似乎使用 concurrent.futures 库与 z3 配合得很好；只要使用简单的约束。试试这个，看看它是否也能处理你的情况。如果不;请将完整代码发布为最小可重现示例。见https://stackoverflow.com/help/minimal-reproducible-example

【讨论】：