Microsoft Z3 Dot Net-API, Klonen Löser

Question

Ich möchte meinen Z3-Code auf mehrere Threads parallel ausführen. In meiner Programmstruktur initialisiere ich zunächst meinen Z3-Solver mit allen Aussagen und frage dann nach einer erfüllbaren Lösung.

Gibt es eine Möglichkeit, Z3-Solver zu klonen, so dass ich mehrere Klone erstellen und den Klon an mehrere Threads übergeben kann?

Meine Idee ist ...

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. 

ich offcourse den Klon erstellen kann mir eine Reihe von Solver meine Schaffung und in jeder von ihnen während der Behauptung Prozess geltend machen, aber ich möchte nicht, dass zu tun, weil das vielleicht nicht effizient ist.

Ich verwende dot net API. Wenn mir jemand im dot net api-Kontext antworten kann, wäre es hilfreicher.

Answer 1

Es gibt eine Methode, um Solver zwischen Kontexten zu übersetzen. Benutze das. Denken Sie daran,

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

dass Kontexte nicht sicher Fadens, so verwenden unterschiedliche Kontexte in verschiedenen Threads.