Passing model by argument in optimize_models

src/lib/reasoners/satml_frontend.ml

@@ -1273,11 +1273,11 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       else mk_gt ty_op
     end
 
-  let rec optimize_models env =
-    (* Models must be saved before asserting a new formula in [env] as
-       they may be altered if a contradiction arises below. More precisely,
-       - There is no need to force [env.last_saved_model], as the closure that
-         computes the model has captured the correct theory environment in
+  let capture_models env =
+    (* Models must be saved before asserting a new formula in [optimize_models]
+       as they may be altered if a contradiction arises. More precisely,
+       - There is no need to force [env.last_saved_model], as this closure
+         has captured the correct theory environment in
          [SAT.compute_concrete_model].
        - [env.last_saved_objectives] is pure and only needs to be saved
          without additional precautions.
@@ -1290,7 +1290,9 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       | Some objs -> objs
       | None -> assert false
     in
-    let bmdl = capture_bmodel env in
+    fmdl, omdl, capture_bmodel env
+
+  let rec optimize_models (fmdl, omdl, bmdl) env =
     let acc =
       try
         Objective.Model.fold (fun { e; is_max; _ } value acc ->
@@ -1339,7 +1341,8 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
           unsat_rec env;
           assert false
         with
-        | I_dont_know -> optimize_models env
+        | I_dont_know ->
+          optimize_models (capture_models env) env
         | IUnsat _ex ->
           (* The unsatisfability of [env] means that the objectives cannot
              be further optimized.
@@ -1355,24 +1358,20 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
       unsat_rec env
     with
     | I_dont_know ->
-      (* It is more reliable to verify the presence of objectives at
-         the current assertion level by referring to the objective model
-         stored in the current theory environment, rather than checking
-         the emptiness of [env.last_saved_objectives]. *)
-      let curr_objs = Th.get_objectives @@ SAT.current_tbox env.satml in
-      if Objective.Model.is_empty curr_objs then
-        raise I_dont_know
-      else (
+      match env.last_saved_objectives with
+      | None -> raise I_dont_know
+      | Some omdl when Objective.Model.is_empty omdl -> raise I_dont_know
+      | Some _ ->
         (* An additional assertion level is inserted around [optimize_models]
            to revert to a consistent SAT environment after reaching an
            unsatisfiable state in [optimize_models]. *)
         push env 1;
-        let fmdl, omdl, bmdl = optimize_models env in
+        let fmdl, omdl, bmdl = optimize_models (capture_models env) env in
         pop env 1;
         env.last_saved_model <- fmdl;
         env.last_saved_objectives <- Some omdl;
         env.last_saved_bmodel <- Some bmdl;
-        raise I_dont_know)
+        raise I_dont_know
 
   let unsat env gf =
     assert (SAT.decision_level env.satml <= SAT.assertion_level env.satml);