我正在研究一个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 .另一个资源(再次:在Windows上安装Z3 + Python)从莱昂纳多自己说,"Z3使用线程本地存储",我猜,这将沉没整个事业,但是a)答案是从2012年开始,所以也许是事情已经改变了,并且b)也许它使用线程本地存储来处理一些不相关的东西？
无论如何,多线程Z3是否可能(来自Python)？我不想将设置阶段推进子进程......