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

1 files changed, 21 insertions, 0 deletions

diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 1aa17b4..5d51837 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -49,6 +49,26 @@ let rec extract_const_vars_root (ecl, _, _) =
       [] ecl
 
 
+let extract_choice_groups f =
+  let rec aux w = function
+      | BNot n -> aux w n
+      | BRel _ | BConst _ -> [], []
+      | BEnumCons(_, x, EItem _) -> [], [x]
+      | BEnumCons(_, x, EIdent y) -> [], [y]
+      | BAnd(a, b) | BOr(a, b) ->
+        let ga, va = aux w a in
+        let gb, vb = aux w b in
+        ga@gb, va@vb
+      | BTernary(c, a, b) ->
+        let gc, vc = aux (w /. 3.) c in
+        let ga, va = aux (w /. 2.) a in
+        let gb, vb = aux (w /. 2.) b in
+        let v = uniq_sorted (List.sort compare (vc@va@vb)) in
+        (w, v)::(gc@ga@gb), v
+  in
+  fst (aux 0.6 f)
+
+
 
 (*
   scope_constrict : id list -> (id * id) list -> id list
@@ -215,6 +235,7 @@ let mk_varenv (rp : rooted_prog) f cl =
     let lv_f = lv_f @
       (List.map (fun v -> (0.7, [v; "L"^v]))
         (List.filter (fun n -> List.mem ("L"^n) evars) evars)) in
+    let lv_f = lv_f @ (extract_choice_groups f) in
     let evars_ord =
       if true then
         time "FORCE" (fun () -> force_ordering evars lv_f)