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

The optimization module is supposed to help us build an optimized model,
so it doesn't make much sense to start optimizing before we start
actually looking for a model.

Previously, we were kind of forced into it because it would be incorrect
to perform case splits before optimizing. Now that optimization is
integrated directly into the SAT solver, it is fully independent from
case splits, and this restriction does not apply any longer.

This fixes issues where we would try to optimize eagerly in a small
solution space and would end up enumerating the solution space before
performing examining some decisions that would prune it for us, which is
exactly what happened in #1222.

Separate optimization (`do_optimize`) from case splitting
(`do_case_split`) at the `Theory` level, and perform optimization in
`compute_concrete_model`, i.e. at the time we switch to model
generation (note: this limits the impact of optimization on unsat
problems).

Also change the order of decisions to consider optimized splits last for
consistency, although that should not have much impact in practice.

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