Parallel Solving

[lolpro11]

https://stackoverflow.com/questions/53246030/parallel-solving-in-z3
Hello,
Is it possible to add in Parallel Solving for Z3 in rust?
Should be a simple binding, or am I missing something here?
Thanks

[pleich]

Technically all functionality should already be in place. You need to add the option to the solver parameters, something like:

 let mut params = Params::new(&ctx);
 params.set_bool("parallel.enable", true);

let solver = Solver::new(&ctx);
solver.set_params(&Params::new(&ctx));

[toolCHAINZ]

Agreed that this should work, with a caveat: don't expect to flip a switch and suddenly see Z3 using 100% of all cores.

z3's tactics and theories have differing levels of "parallel-friendliness". Parallelism is something that it can take advantage of sometimes, not that it will. if you look around for references to "cube" or "cube-and-conquer" in the Z3 docs you'll find some (short) discussion on this.

I've never seen it actually use these parallel strategies in my own work (perhaps my problems are not the right type), so I can't confirm this works. In fact I ended up getting paralleism by structuring my problem such that it could be dispatched to separate contexts in separate threads manually.

The example by @pleich lines up with all existing documentation for z3, so there's no reason why it shouldn't work if you do have a parallelizable problem.