From 354e8ed50b1fc1b6dadc1a2a8d54837b5b47e6be Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Thu, 10 Jul 2014 13:29:01 +0200
Subject: DP locations defined by abstract values and not by formula.

---
 abstract/formula.ml | 20 --------------------
 1 file changed, 20 deletions(-)

(limited to 'abstract/formula.ml')

diff --git a/abstract/formula.ml b/abstract/formula.ml
index a124a84..f2a3bd1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -263,23 +263,3 @@ 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
-      | BTernary(c, a, b) ->
-        true, (BAnd(c, a))::(BAnd(BNot c, b))::l
-      | x -> u, x::l)
-    (false, []) c
-  in
-    if u then split_cases l else l
-- 
cgit v1.2.3