微软Z3点网应用编程接口，克隆解算器

Question

我想在多线程上并行运行我的z3代码。在我的程序结构中，我首先使用所有断言初始化Z3求解器，然后请求可满足的解决方案。

有没有办法克隆Z3求解器，这样我就可以创建多个克隆，并将克隆传递给多个线程？

我的想法是..。

Solver slvr1;
//initialize and add all assertions on solver 1.
//then create N number of clone solvers.
//Finally run each solver clone on each thread.

当然，我可以自己创建克隆，在断言过程中创建一个求解器数组并在每个求解器中进行断言，但我不想这样做，因为这可能效率不高。

我正在使用.Net API。因此，如果有人可以在.Net api上下文中回答我，那将会更有帮助。

Answer 1

有一种方法可以在上下文之间转换求解器。使用这个。

https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/Solver.cs

记住，上下文不是线程安全的，所以在不同的线程中使用不同的上下文。