根据http://research.microsoft.com/en-us/um/people/leonardo/z3_doc/parallel.html如果我使用 .smt 文件，我可以从 z3 命令行设置 CC_NUM_THREADS=4。
如果我使用 z3py api，我该如何执行此操作？
最佳答案
支持引理共享的投资组合求解器不是最新版本 Z3 的一部分。因此，不支持这些参数，并且也不支持允许每个参数有多个值的参数格式(在命令行上或通过 python)。
也就是说，仍然有一种方法可以利用多核，这就是 par-or 策略；例如，参见 Z3 Strategy Tutorial (搜索 par-or)。该示例展示了如何通过 SMT2 输入语言并行运行多个策略(在本例中使用不同的随机种子)；在 z3py 中我们将使用 ParOr function创建这样一个并行策略。
关于z3 - z3py中如何设置核心数，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/22071915/