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

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 OCamlPro#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.

Author: bclement-ocp

src/lib/reasoners/satml.ml

@@ -1796,37 +1796,36 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       make_decision env atom
 
   and pick_branch_lit env =
-    match env.next_optimized_split with
-    | Some (fn, value, atom) ->
-      env.next_optimized_split <- None;
-      let v = atom.var in
-      if v.level >= 0 then (
-        assert (v.pa.is_true || v.na.is_true);
-        if atom.is_true then
-          env.tenv <- Th.add_objective env.tenv fn value;
-        pick_branch_lit env
-      ) else (
-        make_decision env atom;
-        if atom.is_true then
-          env.tenv <- Th.add_objective env.tenv fn value
-      )
-    | None ->
-      match env.next_decisions with
-      | atom :: tl ->
-        env.next_decisions <- tl;
+    match env.next_decisions with
+    | atom :: tl ->
+      env.next_decisions <- tl;
+      pick_branch_aux env atom
+    | [] ->
+      match env.next_split with
+      | Some atom ->
+        env.next_split <- None;
         pick_branch_aux env atom
-      | [] ->
-        match env.next_split with
-        | Some atom ->
-          env.next_split <- None;
-          pick_branch_aux env atom
-        | None ->
-          match Vheap.pop_min env.order with
-          | v -> pick_branch_aux env v.na
-          | exception Not_found ->
-            if Options.get_cdcl_tableaux_inst () then
-              assert (Matoms.is_empty env.lazy_cnf);
-            raise_notrace Sat
+      | None ->
+        match Vheap.pop_min env.order with
+        | v -> pick_branch_aux env v.na
+        | exception Not_found ->
+          if Options.get_cdcl_tableaux_inst () then
+            assert (Matoms.is_empty env.lazy_cnf);
+          match env.next_optimized_split with
+          | Some (fn, value, atom) ->
+            env.next_optimized_split <- None;
+            let v = atom.var in
+            if v.level >= 0 then (
+              assert (v.pa.is_true || v.na.is_true);
+              if atom.is_true then
+                env.tenv <- Th.add_objective env.tenv fn value;
+              pick_branch_lit env
+            ) else (
+              make_decision env atom;
+              if atom.is_true then
+                env.tenv <- Th.add_objective env.tenv fn value
+            )
+          | None -> raise Sat
 
   let pick_branch_lit env =
     if env.next_dec_guard < Vec.size env.increm_guards then
@@ -1941,6 +1940,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
+      env.tenv <- 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 -> t
   val do_case_split :
     ?acts:Shostak.Literal.t Th_util.acts ->
     t -> Util.case_split_policy -> t * Expr.Set.t
@@ -670,33 +672,29 @@ 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;
+      t
+    | None -> t
+
+  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 +963,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:_ env = env
   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 -> t
   val do_case_split :
     ?acts:Shostak.Literal.t Th_util.acts ->
     t -> Util.case_split_policy -> t * Expr.Set.t