CODEWITHSUNDEEP
z3
Amarjit Datta
Amarjit Datta

Reputation: 271

Microsoft Z3 Dot Net API, Cloning Solver

I want to run my z3 code on multiple threads parallelly. In my program structure, I initialize my Z3 solver first with all assertions and then ask for satisfiable solution.

Is there any way to clone Z3 solver, so that I can create multiple clones and pass the clone to multiple threads?

My idea is...

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.

I can offcourse create the clone myself my creating an array of solver and assert in each of them during the assertion process, but I don't want to do that, as that may not be efficient.

I am using dot net API. So if anyone can answer me in dot net api context, it would be more helpful.

Upvotes: 1

Views: 169

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

There is a method to translate solvers between contexts. Use this.

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

Remember that contexts are not thread safe, so use different contexts in different threads.

Upvotes: 4

Related Questions