Microsoft Z3 Dot Net API, Cloning Solver

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. 

Я могу Offcourse создать клон себя мой, создавая массив решателя и утверждать в каждом из них во время процесса утверждения, но я не хочу, чтобы сделать это , поскольку это может быть неэффективным.

Я использую dot net API. Поэтому, если кто-нибудь может ответить мне в контексте dot net api, это было бы более полезно.

Answer 1

Существует способ перевода решателей между контекстами. Использовать это.

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

Помните, что контексты не являются поточно, поэтому используют различные контексты в разных потоках.