unit_tenv

src/lib/reasoners/satml.ml

@@ -261,6 +261,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       mutable unit_tenv : Th.t;
 
       mutable tenv_queue : Th.t Vec.t;
+      mutable unit_tenv_queue : Th.t Vec.t;
 
       mutable tatoms_queue : Atom.atom Queue.t;
       (** Queue of atoms that have been added to the [trail] through either
@@ -470,6 +471,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       unit_tenv = Th.empty();
 
       tenv_queue = Vec.make 100 ~dummy:(Th.empty());
+      unit_tenv_queue = Vec.make 100 ~dummy:(Th.empty());
 
       tatoms_queue = Queue.create ();
 
@@ -965,9 +967,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         (fun acc (ta : Atom.atom) ->
            assert (ta.is_true);
            assert (ta.var.level >= 0);
-           if ta.var.level = 0 then begin
+           if ta.var.level <= Vec.size env.increm_guards then begin
              incr nb_f;
-             (ta.lit, Ex.empty, 0, env.cpt_current_propagations) :: acc
+             (ta.lit, Ex.empty, ta.var.level, env.cpt_current_propagations) :: acc
            end
            else acc
         )[] lazy_q
@@ -1969,6 +1971,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     guard.neg.is_guard <- false;
     cancel_until env env.next_dec_guard;
     Vec.push env.increm_guards guard;
+    Vec.push env.unit_tenv_queue env.unit_tenv;
     env.is_unsat_cpt <- if env.is_unsat then env.is_unsat_cpt + 1 else 0
 
   let remove_guarded g env (vec : Atom.clause Vec.t) =
@@ -1990,6 +1993,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     let g = Vec.pop env.increm_guards in
     env.is_unsat <- env.is_unsat_cpt <> 0;
     env.is_unsat_cpt <- max 0 (env.is_unsat_cpt - 1);
+    env.unit_tenv <- Vec.pop env.unit_tenv_queue;
     g.is_guard <- false;
     g.neg.is_guard <- false;
     assert (not g.var.na.is_true); (* atom not false *)

src/lib/reasoners/satml_frontend.ml

@@ -605,7 +605,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         (fun f _ sa ->
            Debug.atoms_from_sat_branch f;
            match atoms_from_sat_branch f with
-           | None   -> assert false
+           | None   -> sa (* TODO: can occur with incremental solving but maybe we want to make sure it doesn't *)
            | Some l -> List.fold_left (fun sa a -> SE.add a sa) sa l
         ) env.conj SE.empty