GSOC'25 Add support for parallel invocation of solvers to solve a PC

[RehanChalana]

This pr adds support for parallel invocation of solver and adds a new config symbolic.do_parallel_mode.

I could not figure out a nice solution to how can we use parallel invocation when we have to compute solutions from solvers in SymbolicConstraintsGeneral.solve(pc) method because Z3 contexts are not thread safe, The contexts are created in the executor threads but call for getting the solution happens in main thread and it can lead to crashes or concurrency issues.

I am looking for some guidance on it. For now I am using sequential execution in the solve() method but mostly the isSatisfiable() method is used to check if the PC is SAT/UNSAT for path exploration and there parallel invocation is working good!

[sohah]

I could not figure out a nice solution to how can we use parallel invocation when we have to compute solutions from solvers in SymbolicConstraintsGeneral.solve(pc) method because Z3 contexts are not thread safe, The contexts are created in the executor threads but call for getting the solution happens in main thread and it can lead to crashes or concurrency issues.

Hi Rehan,
It sounds like you need to change how we get the model to the main thread. The main thread should not be making any call to collect the model, at least directly from the solving thread. The thread after it is done, should return the model, or even place it in a temp that is later read by the main thread. I think you should be get an object representing the model from the thread after it is done.

[sohah]

Hi @RehanChalana , any update on that PR?

[RehanChalana]

Hi! @sohah , I haven’t been able to make further progress on the PR due to college and other commitments. With placement season going on, I may not be able to work on it in the near future either. Apologies for the delay, and thank you for understanding.