ScottWest
ScottWest

Reputation: 1936

Copying Z3 Solver

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

Answers (1)

Leonardo de Moura
Leonardo de Moura

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

Related Questions