在多核服务器中使用Z3

Question

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

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

我想以平行的方式解决公式。我读过this question，我发现应该为解决公式的每个实例创建一个独特的Context。

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

由于

Answer 1

表达式不能在另一个上下文中使用。所以，是的，如果这些内核/上下文需要相同的表达式，则它们将不得不被复制和/或翻译（另请参阅Z3_translate）。