多线程Z3？

Question

我正在从事一个Python项目，目前我正试图以一些可怕的方式加快速度:我设置了我的Z3解决程序，然后分叉进程，让Z3在子进程中执行解决方案，并将模型的可泡沫化表示传递给父进程。

这很好，代表了我所要做的第一步:父进程现在不再受CPU约束。下一步是多线程父进程，这样我们就可以并行地求解多个Z3求解器。

我确信在设置阶段我已经互斥了对Z3的任何并发访问，而且在任何时候只有一个线程应该接触到Z3。然而，尽管如此，我还是在libz3.so中得到了随机段错误。需要注意的是，在这一点上，接触Z3的并不总是同一个线程--相同的对象(不是求解者本身，而是表达式)可能在不同的时间由不同的线程处理。

我的问题是，多线程Z3是可能的吗？这里有一个简短的注释(http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html)，它说“从多个线程访问Z3对象是不安全的”，我想这会回答我的问题，但我希望这意味着不应该同时从多个线程访问Z3。另一种资源(Again: Installing Z3 + Python on Windows)来自莱昂纳多自己，它说"Z3使用线程本地存储“，我想这会毁掉整个任务，但是( a)答案是从2012年开始的，所以也许事情已经改变了，而b)也许它使用线程本地存储来处理一些无关的东西？

无论如何，多线程Z3 (来自Python)是可能的吗？我不想把安装阶段推到子进程中.

Answer 1

Z3确实使用线程本地存储，但据我所见，在代码中只剩下一个点(用于跟踪每个线程正在使用多少内存；在memory_manager.cpp中)，但这不应该对您看到的症状负责。

如果每个线程都严格地只使用它自己的上下文对象(Z3_context，或者在Python类上下文中)，那么Z3应该在多线程设置中表现得很好。这意味着通过一个上下文创建的任何对象都不能以任何方式与另一个上下文的对象交互；如果需要的话，所有对象都必须首先从一个上下文转换到另一个上下文，例如在Python中通过如下函数(.)在ASTRef课堂上。

尽管如此，肯定还有一些bug需要修复。当看到随机段错误时，我的第一个目标是垃圾收集器，因为它可能与Z3的引用计数(在其他API中是这样的)没有很好的交互。当同时创建多个上下文对象时，也会触发一个已知的bug (尽管在我的待办事项列表中.)