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

5 files changed, 97 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index a6cc2d8..ffa531c 100644
--- a/Makefile
+++ b/Makefile
@@ -24,6 +24,7 @@ SRC= 	main.ml \
 		abstract/formula_printer.ml \
 		abstract/transform.ml \
 		\
+		abstract/varenv.ml \
 		abstract/abs_interp.ml \
 		abstract/abs_interp_edd.ml \
 		interpret/interpret.ml \
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index cb5ae9c..2597a63 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -171,7 +171,6 @@ end = struct
 
         (* program expressions *)
         cl          : conslist;
-        cl_g        : conslist;
         guarantees  : (id * bool_expr) list;
 
         (* abstract interpretation *)
@@ -275,13 +274,11 @@ end = struct
     *)
     let init_state opt rp =
       let init_f, f = Transform.f_of_prog rp false in
-      let _, f_g = Transform.f_of_prog rp true in
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
       Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
 
       let init_cl = conslist_of_f init_f in
       let cl = Formula.conslist_of_f f in
-      let cl_g = Formula.conslist_of_f f_g in
       Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
       
       let guarantees = Transform.guarantees_of_prog rp in
@@ -294,7 +291,7 @@ end = struct
 
       (* add variables from LASTs *)
       let last_vars = uniq_sorted
-        (List.sort compare (Transform.extract_last_vars f_g)) in
+        (List.sort compare (Transform.extract_last_vars f)) in
       let last_vars = List.map
         (fun id ->
           let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
@@ -336,7 +333,7 @@ end = struct
 
       let st = 
       { rp; opt; enum_vars; num_vars; all_vars;
-         cl; cl_g; guarantees;
+         cl; guarantees;
         cycle; forget; acc_d_vars; d_vars; top;
         env = Hashtbl.create 12; delta; widen } in
 
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 56b366e..a439995 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -779,6 +779,37 @@ end = struct
 
         (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *)
         (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *)
+        let facts = get_root_true f in
+        let f, rp, _ = List.fold_left
+          (fun (f, (rp : rooted_prog), repls) eq ->
+            match eq with
+            | BEnumCons(E_EQ, a, EIdent b)
+                when a.[0] <> 'L' && b.[0] <> 'L' ->
+
+              let a = try List.assoc a repls with Not_found -> a in
+              let b = try List.assoc b repls with Not_found -> b in
+
+              if a = b then
+                f, rp, repls
+              else begin
+                let keep, repl =
+                  if String.length a <= String.length b
+                    then a, b
+                    else b, a
+                in
+                Format.printf "Replacing %s with %s@." repl keep;
+                let f = formula_replace_evars [repl, keep; "L"^repl, "L"^keep] f in
+                let rp =
+                  { rp with all_vars =
+                      List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in
+                let repls = (repl, keep)::
+                  (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in
+                f, rp, repls
+              end
+            | _ -> f, rp, repls)
+          (f, rp, []) facts in
+        Format.printf "Complete formula after simpl:@.%a@.@."
+            Formula_printer.print_expr f;
 
         let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in
         let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in
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
+
+
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)