【发布时间】：2016-10-05 02:28:17
【问题描述】：
我想建立一个完全专用于 Z3 的系统。假设它有 4 个核心，我想使用机器的所有功能。
我将求解具有大约 1000 个增量断言的大型公式。
我想以并行方式求解公式。我读过this question，发现应该为解决公式的每个实例创建一个唯一的Context。
然后我的问题是，使用完整系统资源（4 核）和使用增量断言解决公式的最佳方式是什么？我是否应该为每个核心创建一个上下文并以某种方式同步推送和弹出它们以逐步解决公式？
谢谢
【问题讨论】：
-
我认为没有“最佳”方式，这实际上取决于您要解决的问题。如果您使用 API，则必须为每个线程/进程使用单独的上下文。我不认为每个线程/进程有多个上下文的充分理由。
-
所以你会为每个核心创建一个上下文？每个上下文会使用不同的核心吗？由于将有 1000 个断言将通过 4 个上下文逐步解决，这意味着重复信息 4 次（每个核心 1 个）。我说的对吗？有没有比在每个上下文中都有每个断言更好的方法呢？谢谢@ChristophWintersteiger
标签： c++ multithreading z3 multicore