Fix 1023

[Halbaroth]

This PR addresses the issue #1023 about inconsistent SAT environments after optimization.

The basic idea is simple. Before optimizing the model in Satml_frontend, we push an additional assertion level.
The first-order model, the boolean model and the objectives are saved before asserting any new formula during the
optimization. The latest consistent models are restored after popping the assertion level.

This PR also includes a refactoring of the optimization implementation in Satml_frontend which improves the readability.

[Halbaroth]

It seems that it does not solve #1023 ...
The script:

open AltErgoLib

module Container = (val Sat_solver.get_current ())
module SAT = Container.Make (Theory.Main_Default)

let mk_gf ff =
  Expr.{
    ff;
    origin_name = "";
    gdist = 1;
    hdist = 1;
    trigger_depth = max_int;
    nb_reductions = 0;
    age = 0;
    lem = None;
    mf = false;
    gf = false;
    from_terms = [];
    theory_elim = true
  }

let () =
  let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in
  let gf = mk_gf Expr.Ints.(x <= ~$10) in
  let env = SAT.empty () in
  SAT.declare env (Hstring.make "x", [], Ty.Tint);
  SAT.assume env gf Explanation.empty;
  let _ : unit =
    try
      let _ : Explanation.t = SAT.unsat env (mk_gf Expr.faux) in
      ()
    with _ -> ()
  in
  SAT.assume env gf Explanation.empty

still raises Unsat at the last command :/

[Halbaroth]

I made some progress. The previous script failed because I used Expr.faux instead of Expr.vrai ... now the following script works as expected:

open AltErgoLib

module SAT = Satml_frontend.Make (Theory.Main_Default)

let mk_gf ff =
  Expr.{
    ff;
    origin_name = "";
    gdist = 1;
    hdist = 1;
    trigger_depth = max_int;
    nb_reductions = 0;
    age = 0;
    lem = None;
    mf = false;
    gf = false;
    from_terms = [];
    theory_elim = true
  }

let check_sat =
  let vrai =
    Expr.{ff = vrai;
       origin_name = "vrai";
       hdist = -1;
       gdist = 0;
       trigger_depth = max_int;
       nb_reductions = 0;
       age = 0;
       lem= None;
       mf= false;
       gf=true;
       from_terms = [];
       theory_elim = true;
    }
  in fun env ->
  match SAT.unsat env vrai with
  | _ex -> Fmt.pr "unsat@."
  | exception SAT.I_dont_know ->
      let mdl = Option.get (SAT.get_model env) in
      Fmt.pr "unknown:@ %a@." Models.pp mdl
  | exception SAT.Sat -> Fmt.pr "sat@."

let () =
  Options.set_interpretation ILast;
  Options.set_debug_optimize true;
  let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in
  let gf = mk_gf Expr.Ints.(x <= ~$10) in
  let env = SAT.empty () in
  SAT.declare env (Hstring.make "x", [], Ty.Tint);
  SAT.assume env gf Explanation.empty;
  SAT.optimize env (Objective.Function.mk ~is_max:true x);
  check_sat env;
  assert (not @@ SAT.is_unsat env);
  SAT.assume env gf Explanation.empty;
  check_sat env

I temporary added a function is_unsat in the SAT solver API in order to check that the underlying SatML solver of Satml_frontend is not unsat after optimization.

Strangely, this script also works on next... but SAT.is_unsat env is true! So it seems that there is another bug on next, and this PR could mask it...

[Halbaroth]

#1294 should fix the bug on next. I didn't rebase this PR on #1294 to keep the smaller diff.