Incremental solving in Z3 using push command

Question

I am using Z3's python api to do some kind of incremental solving. I push constraints to the solver iteratively while checking for unsatisfiability at each step using solver.push() command. I want to understand whether Z3 would use the learned lemmas from previous constraints or the satisfying solution previously obtained when solving with a newly added constraint. I never use the solver.pop() command. Where can I get more details about how the work done in previous iterations is used?

Answer 1

Z3 has multiple solvers, but only one of them really supports incremental solving and reuse work from previous calls. By default, Z3 will automatically switch to the incremental solver whenever you execute a solver.push(). This solver alsos reuse previously learned clauses. The learned clauses are deleted when a solver.pop() is executed. Z3 also support another mechanism for incremental solving that is not based on push and pop. Here are some related posts:

• Soft/Hard constraints in Z3

• How to use z3 incrementally and model without propositional value ？

• Incremental calls to Z3 on UFBV with and without push calls