satML: add missing case-split strategies

OCamlPro · Sep 21, 2023 · 1674081 · 1674081
1 parent 09e53da
commit 1674081
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 6 deletions.
diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
@@ -95,6 +95,8 @@ module type SAT_ML = sig
 
   val assume_simple : t -> Atom.atom list list -> unit
 
+  val do_case_split : t -> Util.case_split_policy -> conflict_origin
+
   val decide : t -> Atom.atom -> unit
   val conflict_analyze_and_fix : t -> conflict_origin -> unit
 
@@ -703,11 +705,9 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
 
   let do_case_split env origin =
-    if Options.get_case_split_policy () != Util.AfterTheoryAssume then
-      failwith
-        "Only AfterTheoryAssume case-split policy is supported by satML";
     try
-      let tenv, _ = Th.do_case_split env.tenv origin in
+      let tenv, _terms = Th.do_case_split env.tenv origin in
+      (* TODO: terms not added to matching !!! *)
       env.tenv <- tenv;
       C_none
     with Ex.Inconsistent (expl, _) ->

diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli
@@ -89,6 +89,7 @@ module type SAT_ML = sig
 
   val reason_of_deduction: Atom.atom -> Atom.Set.t
   val assume_simple : t -> Atom.atom list list -> unit
+  val do_case_split : t -> Util.case_split_policy -> conflict_origin
 
   val decide : t -> Atom.atom -> unit
   val conflict_analyze_and_fix : t -> conflict_origin -> unit
@@ -99,4 +100,3 @@ module type SAT_ML = sig
 end
 
 module Make (Th : Theory.S) : SAT_ML with type th = Th.t
-
diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml
@@ -978,13 +978,19 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
            [ greedy_mconf (), "greedy-inst", true , false;
              greedier_mconf (), "greedier-inst", true, false])
 
+  let do_case_split env policy =
+    match SAT.do_case_split env.satml policy with
+    | C_none -> env
+    | C_bool _ -> assert false
+    | C_theory expl -> raise (Ex.Inconsistent (expl, []))
+
   let rec unsat_rec env ~first_call:_ : unit =
     try SAT.solve env.satml; assert false
     with
     | Satml.Unsat lc -> raise (IUnsat (env, make_explanation lc))
     | Satml.Sat ->
       try
-        (*if first_call then SAT.cancel_until 0;*)
+        let env = do_case_split env Util.BeforeMatching in
         let env = {env with nb_mrounds = env.nb_mrounds + 1}
                   [@ocaml.ppwarning
                     "TODO: first intantiation a la DfsSAT before searching ..."]
@@ -999,6 +1005,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         (*let strat = Auto in*)
         let dec_lvl = SAT.decision_level env.satml in
         let env, updated = instantiation env strat dec_lvl in
+        let env = do_case_split env Util.AfterMatching in
         let env, updated =
           if not updated && strat != Auto then instantiation env Auto dec_lvl
           else env, updated