Reputation: 1936
I have seen in the post: Is it possible to clone Z3_context? that the ability to copy/clone the solver was planned for addition to Z3, to facilitate some backtracking behaviour. I have looked in the C API documentation and I could not currently find a way to do this.
Is it now possible to copy the solver through the C API?
Upvotes: 1
Views: 821
Reputation: 21475
The API does not have a method for copying a Solver object, but it can be simulated using Z3_solver_get_assertions
and Z3_solver_assert
. The idea is to create a new Solver object, and copy the assertions from the old to the new.
Upvotes: 2