1 files changed, 18 insertions, 0 deletions
diff --git a/abstract/formula.ml b/abstract/formula.ml
index f2a3bd1..5cbe0c9 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -263,3 +263,21 @@ let rec formula_replace_evars repls e =
   | x -> x
 
 
+
+(*
+  Extract all cases that make a formula true, to a limited degree
+
+  [A || B; not (A || B)] -> A; (B && (not A)); not A && not B]
+*)
+
+let rec split_cases c =
+  let c = List.map eliminate_not c in
+  let u, l = List.fold_left
+    (fun (u, l) c ->
+      match c with
+      | BOr(a, b) ->
+        true, a::(BAnd(BNot a, b))::l
+      | x -> u, x::l)
+    (false, []) c
+  in
+    if u then split_cases l else l