From e06a4102e5b2a81c7b1c24323cafc863eefbc0cb Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 9 Jul 2014 18:06:43 +0200
Subject: Now it's starting to work...

---
 abstract/formula.ml | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'abstract/formula.ml')

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
-- 
cgit v1.2.3