z3 - 你如何在z3py中设置核心数

Question

根据http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html如果我使用 .smt 文件，我可以从 z3 命令行设置 CC_NUM_THREADS=4。

如果我使用的是 z3py api，我该怎么做？

Answer 1

支持引理共享的投资组合求解器不是 Z3 最新版本的一部分。因此不支持这些参数，也不支持允许每个参数有多个值的参数格式（在命令行上或通过 python）。

也就是说，仍然有一种利用多核的方法，这是 par-or 策略；例如，参见Z3 策略教程（搜索 par-or）。该示例展示了如何通过 SMT2 输入语言并行运行多个策略（在此示例中使用不同的随机种子）；在 z3py 中，我们将使用ParOr 函数来创建这样的并行策略。