fix(opt): Only perform optimization when building a model

src/lib/reasoners/satml.ml

@@ -1941,6 +1941,23 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       conflict_analyze_and_fix env (C_theory ex);
       compute_concrete_model ~declared_ids env
 
+  let compute_concrete_model ~declared_ids env =
+    assert (is_sat env);
+
+    (* Make sure all objectives are optimized before starting model
+       generation. This can cause us to backtrack some of the splits
+       done at the theory level, which is fine, because we don't care
+       about these at the SAT level. *)
+    let rec loop env =
+      let acts = theory_slice env in
+      Th.do_optimize ~acts env.tenv;
+      if not (is_sat env) then
+        try solve env; assert false
+        with Sat -> loop env
+      else
+        compute_concrete_model ~declared_ids env
+    in loop env
+
   exception Trivial
 
   let partition atoms init =

src/lib/reasoners/theory.ml

@@ -57,6 +57,8 @@ module type S = sig
   val extract_ground_terms : t -> Expr.Set.t
   val get_real_env : t -> Ccx.Main.t
   val get_case_split_env : t -> Ccx.Main.t
+  val do_optimize :
+    acts:Shostak.Literal.t Th_util.acts -> t -> unit
   val do_case_split :
     ?acts:Shostak.Literal.t Th_util.acts ->
     t -> Util.case_split_policy -> t * Expr.Set.t
@@ -670,33 +672,28 @@ module Main_Default : S = struct
     else
       [], t
 
-  let do_optimize acts objectives t =
+  let do_optimize ~acts t =
+    let objectives = t.objectives in
     match Objective.Model.next_unknown objectives with
     | Some obj ->
       let add_objective = acts.Th_util.acts_add_objective in
-      optimize_obj ~for_model:false add_objective obj t;
+      optimize_obj ~for_model:false add_objective obj t
+    | None -> ()
+
+  let do_sat_splits acts t =
+    let splits, t = sat_splits t in
+    match splits with
+    | [] -> do_case_split_aux t ~for_model:false
+    | (lview, _, _) :: _ ->
+      let lit = Shostak.(Literal.make @@ LSem (L.make lview)) in
+      acts.Th_util.acts_add_split lit;
       t, SE.empty
-    | None ->
-      let splits, t = sat_splits t in
-      match splits with
-      | [] ->
-        do_case_split_aux t ~for_model:false
-      | (lview, _, _) :: _ ->
-        let lit = Shostak.(Literal.make @@ LSem (L.make lview)) in
-        acts.Th_util.acts_add_split lit;
-        t, SE.empty
-
-  let do_case_split_or_optimize ?acts t =
-    match acts with
-    | Some acts ->
-      do_optimize acts t.objectives t
-    | None ->
-      do_case_split_aux t ~for_model:false
-
 
   let do_case_split ?acts t origin =
     if Options.get_case_split_policy () == origin then
-      do_case_split_or_optimize ?acts t
+      match acts with
+      | Some acts -> do_sat_splits acts t
+      | None -> do_case_split_aux t ~for_model:false
     else
       t, SE.empty
 
@@ -965,6 +962,7 @@ module Main_Empty : S = struct
 
   let get_real_env _ = CC_X.empty
   let get_case_split_env _ = CC_X.empty
+  let do_optimize ~acts:_ _ = ()
   let do_case_split ?acts:_ env _ = env, E.Set.empty
   let add_term env _ ~add_in_cs:_ = env
   let compute_concrete_model ~acts:_ _env = ()

src/lib/reasoners/theory.mli

@@ -48,6 +48,8 @@ module type S = sig
   val extract_ground_terms : t -> Expr.Set.t
   val get_real_env : t -> Ccx.Main.t
   val get_case_split_env : t -> Ccx.Main.t
+  val do_optimize :
+    acts:Shostak.Literal.t Th_util.acts -> t -> unit
   val do_case_split :
     ?acts:Shostak.Literal.t Th_util.acts ->
     t -> Util.case_split_policy -> t * Expr.Set.t