Add assertion levels in SatML

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 ->