我正在进行一个Python项目,在其中试图以一些可怕的方式加快速度:我设置了我的Z3求解器,然后分叉进程,并让Z3在子进程中执行求解并将模型的可选表示传递回父进程。
这很有效,也代表我正在尝试的第一阶段:父进程现在不再被CPU限制。下一步是多线程化父进程,以便我们可以并行解决多个Z3求解器。
我相当确定我已经在设置阶段互斥地访问了任何Z3,并且在任何时候只有一个线程应该触及Z3。但是,尽管如此,我仍然会在libz3.so中遇到随机的segfaults。需要注意的是,在这一点上,不总是同一个线程触及Z3 -- 相同的对象(不是求解器本身,而是表达式)可能在不同的时间由不同的线程处理。