Invalid SAT environment while optimizing

[Halbaroth]

The current implementation of unsat_rec_prem is wrong in presence of optimization if we try to use the SAT API directly. Consider the input problem:

(set-option :produce-models true)
(set-logic ALL)
(declare-const x Int)
(assert (<= x 10))
(maximize x)
(check-sat)

This problem is SAT and we expect to be able to reuse the environment after the (check-sat) statement. If we use the Dolmen frontend, it's okay because we throw away the previous environment and produce a fresh environment with all the assertions before each (check-sat).

If we use the imperative SAT API, we want to write:

let env = SAT.empty () in 
SAT.declare env `x`;
SAT.assume env `x <= 10`;
SAT.optimize env ~is_max:true `x`;
SAT.unsat env;
SAT.assume env `x <= 10`;

But the current implementation will raise the exception Unsat during the last statement. The reason is simple: in analyze_unknown_for_objectives we call again the solver until getting an unsatisfiable context. In other words, in presence of optimization, the environment env after calling SAT.unsat is always unsatisfiable. In the previous example, it will contain both the assertions x <= 10 and x > 10.

A naive solution consists in protecting the penultimate environment by using the push/pop mechanism and retrieve the model and objectives values produced before popping. Notice that we shouldn't produce an environment with extra push levels, otherwise the behaviour of the pop statement will be wrong after calling SAT.unsat.

To implement this solution, we can save the new assertions discovered in analyze_unknown_for_objectives in a stack, perform a (push 1) and a (pop 1) around the assume and unsat in unsat_rec_prem and after getting an unsat exception, get the tail of the stack and assert it without push/pop around it.

If you have a better solution, I'll be glad to implement it ;)