Split case_split handler into two parts

Refactoring of the function `case_split`. OptimAE introduces
a new kind of case_split: `optimized_split`. The previous code
manages all the case splits in a single function even if AE
processes optimized ones in a complete different way. This commit
divides the function `case_split` into two functions:
- `case_split` mostly as it was before OptimAE
- `optimizing_split` which try to optimize one case split by call.

src/lib/reasoners/adt_rel.ml

@@ -682,11 +682,10 @@ let assume env uf la =
 
 let two = Numbers.Q.from_int 2
 
-let case_split env _ ~for_model ~to_optimize =
-  if to_optimize != None || Options.get_disable_adts () ||
-     not (Options.get_enable_adts_cs())
+let case_split env _uf ~for_model =
+  if Options.get_disable_adts () || not (Options.get_enable_adts_cs())
   then
-    Sig_rel.Split []
+    []
   else
     begin
       assert (not for_model);
@@ -703,12 +702,14 @@ let case_split env _ ~for_model ~to_optimize =
             "found hs = %a" Hs.print hs;
         (* cs on negative version would be better in general *)
         let cs =  LR.mkv_builtin false (Sy.IsConstr hs) [r] in
-        Sig_rel.Split [ cs, true, Th_util.CS(None, Th_util.Th_adt, two) ]
+        [ cs, true, Th_util.CS(None, Th_util.Th_adt, two) ]
       with Not_found ->
         Debug.no_case_split ();
-        Sig_rel.Split []
+        []
     end
 
+let optimizing_split _env _uf _opt_split = None
+
 let query env uf (ra, _, ex, _) =
   if Options.get_disable_adts () then None
   else

src/lib/reasoners/arrays_rel.ml

@@ -384,21 +384,19 @@ let new_equalities env eqs la class_of =
 (* choisir une egalite sur laquelle on fait un case-split *)
 let two = Numbers.Q.from_int 2
 
-let case_split env _ ~for_model:_ ~to_optimize =
+let case_split env _uf ~for_model:_ =
   (*if Numbers.Q.compare
     (Numbers.Q.mult two env.size_splits) (max_split ()) <= 0  ||
     Numbers.Q.sign  (max_split ()) < 0 then*)
-  if to_optimize != None then
-    (* no classical splits if we have something to optimize *)
-    Sig_rel.Split []
-  else
-    try
-      let a = LR.neg (LRset.choose env.split) in
-      Debug.case_split a;
-      Sig_rel.Split [LR.view a, true, Th_util.CS (None, Th_util.Th_arrays, two)]
-    with Not_found ->
-      Debug.case_split_none ();
-      Sig_rel.Split []
+  try
+    let a = LR.neg (LRset.choose env.split) in
+    Debug.case_split a;
+    [LR.view a, true, Th_util.CS (None, Th_util.Th_arrays, two)]
+  with Not_found ->
+    Debug.case_split_none ();
+    []
+
+let optimizing_split _env _uf _opt_split = None
 
 let count_splits env la =
   let nb =

src/lib/reasoners/bitv_rel.ml

@@ -34,7 +34,8 @@ let empty _ = ()
 let assume _ _ _ =
   (), { Sig_rel.assume = []; remove = []}
 let query _ _ _ = None
-let case_split _ _ ~for_model:_ ~to_optimize:_ = Sig_rel.Split []
+let case_split _env _uf ~for_model:_ = []
+let optimizing_split _env _uf _opt_split = None
 let add env _ _ _ = env, []
 let new_terms _ = Expr.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []

src/lib/reasoners/ccx.ml

@@ -66,10 +66,10 @@ module type S = sig
     r Sig_rel.facts ->
     t * (r Sig_rel.literal * Explanation.t * Th_util.lit_origin) list
 
-  val case_split :
-    t -> for_model:bool ->
-    to_optimize: Th_util.optimized_split option ->
-    Sig_rel.case_split * t
+  val case_split : t -> for_model:bool -> Th_util.case_split list * t
+  val optimizing_split :
+    t -> Th_util.optimized_split -> Th_util.optimized_split option
+
   val query :  t -> E.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
   val class_of : t -> Expr.t -> Expr.Set.t
@@ -690,16 +690,18 @@ module Main : S = struct
 
   (* End: new implementation of add, add_term, assume_literals and all that *)
 
-  let case_split env ~for_model ~to_optimize =
-    let cs = Rel.case_split env.relation env.uf ~for_model ~to_optimize in
+  let case_split env ~for_model =
+    let cs = Rel.case_split env.relation env.uf ~for_model in
     match cs with
-    | Sig_rel.Split [] when for_model ->
+    | [] when for_model ->
       let l, uf = Uf.assign_next env.uf in
-      (* try to not to modify uf in the future. It's currently done only
-         to add fresh terms in UF to avoid loops *)
-      Sig_rel.Split l, {env with uf}
-    | Sig_rel.Split _ -> cs, env
-    | Sig_rel.Optimized_split _ -> cs, env
+      (* TODO: Try to not to modify uf in the future. It's currently done only
+         to add fresh terms in UF to avoid loops. *)
+      l, {env with uf}
+    | _ -> cs, env
+
+  let optimizing_split env opt_split =
+    Rel.optimizing_split env.relation env.uf opt_split
 
   let query env a =
     let ra, ex_ra = term_canonical_view env a Ex.empty in

src/lib/reasoners/ccx.mli

@@ -58,10 +58,10 @@ module type S = sig
     r Sig_rel.facts ->
     t * (r Sig_rel.literal * Explanation.t * Th_util.lit_origin) list
 
-  val case_split :
-    t -> for_model:bool ->
-    to_optimize: Th_util.optimized_split option ->
-    Sig_rel.case_split * t
+  val case_split : t -> for_model:bool -> Th_util.case_split list * t
+  val optimizing_split :
+    t -> Th_util.optimized_split -> Th_util.optimized_split option
+
   val query :  t -> Expr.t -> Th_util.answer
   val new_terms : t -> Expr.Set.t
   val class_of : t -> Expr.t -> Expr.Set.t

src/lib/reasoners/enum_rel.ml

@@ -244,40 +244,37 @@ let assume env uf la =
 
 let add env _ r _ = add_aux env r, []
 
-let case_split env uf ~for_model ~to_optimize =
-  if to_optimize != None then
-    (* no classical splits if we have something to optimize *)
-    Sig_rel.Split []
-  else
-    let acc = MX.fold
-        (fun r (hss, _) acc ->
-           let x, _ = Uf.find_r uf r in
-           match Sh.embed x with
-           | Cons _ -> acc (* already bound to an Enum const *)
-           | _ -> (* cs even if sz below is equal to 1 *)
-             let sz = HSS.cardinal hss in
-             match acc with
-             | Some (n,_,_) when n <= sz -> acc
-             | _ -> Some (sz, r, HSS.choose hss)
-        ) env.mx None
-    in
-    match acc with
-    | Some (n,r,hs) ->
-      let n = Numbers.Q.from_int n in
-      if for_model ||
-         Numbers.Q.compare
-           (Numbers.Q.mult n env.size_splits) (Options.get_max_split ()) <= 0
-         || Numbers.Q.sign  (Options.get_max_split ()) < 0
-      then
-        let r' = Sh.is_mine (Cons(hs,X.type_info r)) in
-        Debug.case_split r r';
-        Sig_rel.Split
-          [LR.mkv_eq r r', true, Th_util.CS (None, Th_util.Th_sum, n)]
-      else
-        Sig_rel.Split []
-    | None ->
-      Debug.no_case_split ();
-      Sig_rel.Split []
+let case_split env uf ~for_model =
+  let acc = MX.fold
+      (fun r (hss, _) acc ->
+         let x, _ = Uf.find_r uf r in
+         match Sh.embed x with
+         | Cons _ -> acc (* already bound to an Enum const *)
+         | _ -> (* cs even if sz below is equal to 1 *)
+           let sz = HSS.cardinal hss in
+           match acc with
+           | Some (n,_,_) when n <= sz -> acc
+           | _ -> Some (sz, r, HSS.choose hss)
+      ) env.mx None
+  in
+  match acc with
+  | Some (n,r,hs) ->
+    let n = Numbers.Q.from_int n in
+    if for_model ||
+       Numbers.Q.compare
+         (Numbers.Q.mult n env.size_splits) (Options.get_max_split ()) <= 0
+       || Numbers.Q.sign  (Options.get_max_split ()) < 0
+    then
+      let r' = Sh.is_mine (Cons(hs,X.type_info r)) in
+      Debug.case_split r r';
+      [LR.mkv_eq r r', true, Th_util.CS (None, Th_util.Th_sum, n)]
+    else
+      []
+  | None ->
+    Debug.no_case_split ();
+    []
+
+let optimizing_split _env _uf _opt_split = None
 
 let query env uf a_ex =
   try ignore(assume env uf [a_ex]); None

src/lib/reasoners/intervalCalculus.ml

@@ -2092,87 +2092,84 @@ let mk_const_term c ty =
   | Ty.Treal -> E.real c
   | _ -> assert false
 
-let optimizing_split env uf opt =
-  (* soundness: if there are expressions to optmize, this should be
-     done without waiting for ~for_model flag to be true *)
-  let {Th_util.order; r = r; is_max = to_max; e; value } = opt in
-  assert (match value with
-      | Unknown -> true
-      | _ -> false
-    );
-  let repr, _ = Uf.find uf e in
-  let ty = E.type_info e in
-  let r1 = r in (* instead of repr, which may be a constant *)
-  let p = poly_of repr in
-  match P.is_const p with
-  | Some optim ->
-    Printer.print_dbg "%a has a %s: %a@."
-      E.print e
-      (if to_max then "maximum" else "minimum")
-      Q.print optim;
-    let r2 = alien_of (P.create [] optim  ty) in
-    let t2 = mk_const_term optim ty in
-    Debug.case_split r1 r2;
-    let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
-    let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
-    Sig_rel.Optimized_split { opt with value = Value s; }
-
-  | None ->
-    let sim = if ty == Ty.Tint then env.int_sim else env.rat_sim in
-    let p = if to_max then p else P.mult_const Q.m_one p in
-    let l, c = P.to_list p in
-    let l = List.rev_map (fun (x, y) -> y, x) (List.rev l) in
-    let sim, mx_res = Sim.Solve.maximize sim (Sim.Core.P.from_list l) in
-    match Sim.Result.get mx_res sim with
-    | Sim.Core.Unknown -> assert false
-    | Sim.Core.Sat _   -> assert false (* because we maximized *)
-    | Sim.Core.Unsat _ -> assert false (* we know sim is SAT *)
-    | Sim.Core.Unbounded _ ->
-      Printer.print_dbg
-        "%a is unbounded. Let other methods assign a value for it@."
-        E.print e;
-      let value = if to_max then Th_util.Pinfinity else Th_util.Minfinity in
-      Sig_rel.Optimized_split { opt with value }
-
-    | Sim.Core.Max(mx,_sol) ->
-      let {Sim.Core.max_v; _} = Lazy.force mx in
-      let max_p = Q.add max_v.bvalue.v c in
-      let optim = if to_max then max_p else Q.mult Q.m_one max_p in
-      Printer.print_dbg "%a has a %s: %a@."
-        E.print e
-        (if to_max then "maximum" else "minimum")
-        Q.print optim;
-
-      let r2 = alien_of (P.create [] optim  ty) in
-      Debug.case_split r1 r2;
-      let t2 = mk_const_term optim ty in
-      let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
-      let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
-      Sig_rel.Optimized_split { opt with value = Value s; }
-
-
-let case_split env uf ~for_model ~to_optimize =
-  match to_optimize with
-  | Some x ->
-    if is_num_term x.Th_util.e then
-      optimizing_split env uf x
+let case_split env uf ~for_model =
+  let res = default_case_split env uf ~for_model in
+  match res with
+  | [] ->
+    if not for_model then []
     else
-      (* Some other theory should find an optimium for e *)
-      Sig_rel.Split []
+      begin
+        match case_split_union_of_intervals env uf with
+        | [] -> model_from_unbounded_domains env uf
+        | l -> l
+      end
+  | _ -> res
+
+let optimizing_split env uf opt_split =
+  if not @@ is_num_term opt_split.Th_util.e then
+    (* Some other theory should find an optimium value for e. *)
+    None
+  else
+    begin
+      (* soundness: if there are expressions to optmize, this should be
+         done without waiting for ~for_model flag to be true *)
+      let {Th_util.order; r = r; is_max = to_max; e; value } = opt_split in
+      assert (match value with
+          | Unknown -> true
+          | _ -> false
+        );
+      let repr, _ = Uf.find uf e in
+      let ty = E.type_info e in
+      let r1 = r in (* instead of repr, which may be a constant *)
+      let p = poly_of repr in
+      match P.is_const p with
+      | Some optim ->
+        Printer.print_dbg "%a has a %s: %a@."
+          E.print e
+          (if to_max then "maximum" else "minimum")
+          Q.print optim;
+        let r2 = alien_of (P.create [] optim  ty) in
+        let t2 = mk_const_term optim ty in
+        Debug.case_split r1 r2;
+        let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
+        let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
+        Some { opt_split with value = Value s }
 
-  | None ->
-    let res = default_case_split env uf ~for_model in
-    match res with
-    | [] ->
-      if not for_model then Sig_rel.Split []
-      else
+      | None ->
         begin
-          match case_split_union_of_intervals env uf with
-          | [] -> Sig_rel.Split (model_from_unbounded_domains env uf)
-          | l -> Sig_rel.Split l
+          let sim = if ty == Ty.Tint then env.int_sim else env.rat_sim in
+          let p = if to_max then p else P.mult_const Q.m_one p in
+          let l, c = P.to_list p in
+          let l = List.rev_map (fun (x, y) -> y, x) (List.rev l) in
+          let sim, mx_res = Sim.Solve.maximize sim (Sim.Core.P.from_list l) in
+          match Sim.Result.get mx_res sim with
+          | Sim.Core.Unknown -> assert false
+          | Sim.Core.Sat _   -> assert false (* because we maximized *)
+          | Sim.Core.Unsat _ -> assert false (* we know sim is SAT *)
+          | Sim.Core.Unbounded _ ->
+            Printer.print_dbg
+              "%a is unbounded. Let other methods assign a value for it@."
+              E.print e;
+            let value = if to_max then Th_util.Pinfinity else Th_util.Minfinity in
+            Some { opt_split with value }
+
+          | Sim.Core.Max(mx,_sol) ->
+            let {Sim.Core.max_v; _} = Lazy.force mx in
+            let max_p = Q.add max_v.bvalue.v c in
+            let optim = if to_max then max_p else Q.mult Q.m_one max_p in
+            Printer.print_dbg "%a has a %s: %a@."
+              E.print e
+              (if to_max then "maximum" else "minimum")
+              Q.print optim;
+
+            let r2 = alien_of (P.create [] optim  ty) in
+            Debug.case_split r1 r2;
+            let t2 = mk_const_term optim ty in
+            let o = Some {Th_util.opt_ord = order; opt_val = Th_util.Value t2} in
+            let s = LR.mkv_eq r1 r2, true, Th_util.CS (o, Th_util.Th_arith, Q.one) in
+            Some { opt_split with value = Value s; }
         end
-    | _ -> Sig_rel.Split res
-
+    end
 (*** part dedicated to FPA reasoning ************************************)
 
 let best_interval_of optimized env p =

src/lib/reasoners/ite_rel.ml

@@ -221,7 +221,9 @@ let assume env uf la =
       raise e
   else assume env uf la
 
-let case_split _ _ ~for_model:_ ~to_optimize:_ = Sig_rel.Split []
+let case_split _env _uf ~for_model:_ = []
+
+let optimizing_split _env _uf _opt_split = None
 
 let query _ _ _ = None
 

src/lib/reasoners/records_rel.ml

@@ -34,7 +34,8 @@ let empty _ = ()
 let assume _ _ _ =
   (), { Sig_rel.assume = []; remove = []}
 let query _ _ _ = None
-let case_split _ _ ~for_model:_ ~to_optimize:_ = Sig_rel.Split []
+let case_split _env _uf ~for_model:_ = []
+let optimizing_split _env _uf _opt_split = None
 let add env _ _ _ = env, []
 let new_terms _ = Expr.Set.empty
 let instantiate ~do_syntactic_matching:_ _ env _ _ = env, []