我无法将处理器的两个内核与并行 Z3 3.2(来自 bin_mt 或 x64_mt 目录)与 PAR_NUM_THREADS=2 一起使用在 Windows7 上。与单线程版本相同 50% 且没有时间差异。
这些逻辑支持并行版本还是仅适用于 QF_IDL？
最佳答案
错误地，Z3 3.2 中没有包含并行执行。这就是为什么在设置 PAR_NUM_THREADS=2 时 Z3 仍然按顺序运行的原因. Z3 团队已更正错误，因此并行功能将在下一个版本中可用。
编辑:
正如@Leo 在评论中提到的，Z3 4.1 现在计划使用并行功能。
关于parallel-processing - Z3 的并行版本是否适用于 BV 逻辑？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/9700679/