Add assertion levels in SatML

`Satml_frontend` assumes that `assume` and `check_sat` are always called
on a SatML environment with no prior decisions. It works in the current
codebase because, in the presence of pop/push, we always restart from a
fresh environment.

The assertion:
```ocaml
assert (SAT.decision_level env.satml == 0)
```
is replaced with:
```ocaml
assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml)
```

Notice that we cannot enforce the assertion:
```ocaml
assert (SAT.decision_level env.satml = SAT.assertion_level env.satml)
```
Consider for instance:
```ocaml
let env = SAT.env () in
SAT.push env 1;
SAT.assume env f; (* <--- HERE *)
...
```
Internally, `SAT.assume env f` adds the formula `g => f` into the
environment of SatML where `g` is a guard formula introduced in
`SAT.push`. But `SatML.assume` does not decide the guard formula [g], so
the decision level is 0 but the assertion level is 1.
Guards are decided (with the highest priority) in `SatML.solve`, which
is called by `SAT.unsat`.

I didn't add the new assertion into `SAT.assume_th_elt` because this
function is only used for handling the theory concept in native language and
we always invoke it at the assertion level 0.

src/lib/reasoners/satml.ml

@@ -121,6 +121,7 @@ module type SAT_ML = sig
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
   val decision_level : t -> int
+  val assertion_level : t -> int
   val cancel_until : t -> int -> unit
 
   val exists_in_lazy_cnf : t -> FF.t -> bool
@@ -583,6 +584,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     end
 
   let decision_level env = Vec.size env.trail_lim
+  let[@inline always] assertion_level env = Vec.size env.increm_guards
 
   let nb_choices env = env.nchoices
   let nb_assigns env = Vec.size env.trail - nb_choices env

src/lib/reasoners/satml.mli

@@ -77,6 +77,11 @@ module type SAT_ML = sig
 
   val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
   val decision_level : t -> int
+
+  val assertion_level : t -> int
+  (** Returns the number of active assertion levels, that is the number of
+      levels introduced with [push] that have not yet been popped. *)
+
   val cancel_until : t -> int -> unit
 
   val exists_in_lazy_cnf : t -> Flat_Formula.t -> bool
@@ -90,7 +95,11 @@ module type SAT_ML = sig
   val conflict_analyze_and_fix : t -> conflict_origin -> unit
 
   val push : t -> Satml_types.Atom.atom -> unit
+  (** [push env g] adds a new assertion level. The formula [g] is used in
+      [Satml_frontend] to guard all formulas asserted at this level. *)
+
   val pop : t -> unit
+  (** [pop env] pops the latest assertion level. *)
 
   val optimize : t -> Objective.Function.t -> unit
   (** [optimize env fn] adds the objection [fn] to the environment

src/lib/reasoners/satml_frontend.ml

@@ -1328,6 +1328,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
     {gf with E.ff = E.mk_imp current_guard gf.E.ff}
 
   let unsat env gf =
+    assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml);
     checks_implemented_features ();
     let gf = add_guard env gf in
     Debug.unsat gf;
@@ -1337,7 +1338,6 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       Inst.add_terms env.inst
         (E.max_ground_terms_rec_of_form gf.E.ff) gf;
     try
-      assert (SAT.decision_level env.satml == 0);
       let _updated = assume_aux ~dec_lvl:0 env [gf] in
       let max_t = max_term_depth_in_sat env in
       env.inst <- Inst.register_max_term_depth env.inst max_t;
@@ -1357,7 +1357,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
 
   let assume env gf _dep =
     (* dep currently not used. No unsat-cores in satML yet *)
-    assert (SAT.decision_level env.satml == 0);
+    assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml);
     try ignore (assume_aux ~dec_lvl:0 env [add_guard env gf])
     with | IUnsat (_env, dep) -> raise (Unsat dep)
          | Util.Timeout ->