c++ - 在多核服务器中使用 Z3

Question

我想建立一个完全专用于 Z3 的系统。假设它有 4 个内核，我想使用机器的所有功能。

我将解决具有大约 1000 个增量断言的大型公式。

我想以并行方式求解公式。我读过 this question我看到应该为每个求解公式的实例创建一个唯一的 Context。

那么我的问题是，使用完整系统资源(4 核)和使用增量断言求解公式的最佳方法是什么？我是否应该为每个核心创建一个上下文并以某种方式同步推送和弹出以逐步解决公式？

谢谢

Answer 1

通过一个上下文创建的表达式不能在另一个上下文中使用。所以，是的，如果那些核心/上下文需要相同的表达式，则必须复制和/或翻译它们(另请参见 Z3_translate )。