Add simplification pass && better heuristic for BDDs based on ternaries.

1 files changed, 42 insertions, 9 deletions

diff --git a/abstract/formula.ml b/abstract/formula.ml
index 4c2c397..f2a3bd1 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -212,15 +212,10 @@ let rec simplify true_eqs e =
         (simplify true_eqs a)
         (simplify true_eqs b)
     | BTernary(c, a, b) ->
-      let c, a, b =
-        simplify true_eqs c,
-        simplify true_eqs a,
-        simplify true_eqs b in
-      begin match c with
-      | BConst true -> a
-      | BConst false -> b
-      | _ -> BTernary(c, a, b)
-      end
+      f_ternary
+        (simplify true_eqs c)
+        (simplify true_eqs a)
+        (simplify true_eqs b)
     | BNot(n) ->
       begin match simplify true_eqs n with
       | BConst e -> BConst (not e)
@@ -230,3 +225,41 @@ let rec simplify true_eqs e =
     
 let rec simplify_k true_eqs e =
   List.fold_left f_and (simplify true_eqs e) true_eqs
+  
+
+
+(*
+  Simplify a formula replacing a variable with another
+*)
+
+let rec formula_replace_evars repls e =
+  let new_name x =
+    try List.assoc x repls
+    with Not_found -> x
+  in
+  match e with
+  | BOr(a, b) ->
+    f_or (formula_replace_evars repls a) (formula_replace_evars repls b)
+  | BAnd(a, b) ->
+    f_and (formula_replace_evars repls a) (formula_replace_evars repls b)
+  | BTernary(c, a, b) ->
+    f_ternary
+      (formula_replace_evars repls c)
+      (formula_replace_evars repls a)
+      (formula_replace_evars repls b)
+  | BNot(n) ->
+    begin match formula_replace_evars repls n with
+    | BConst e -> BConst (not e)
+    | x -> BNot x
+    end
+  | BEnumCons (op, a, EIdent b) ->
+    let a', b' = new_name a, new_name b in
+    if a' = b' then
+      match op with | E_EQ -> BConst true | E_NE -> BConst false
+    else
+      BEnumCons(op, a', EIdent b')
+  | BEnumCons (op, a, EItem x) ->
+    BEnumCons (op, new_name a, EItem x)
+  | x -> x
+
+