New algorithm for variable ordering based on FORCE.

1 files changed, 85 insertions, 8 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 1eac551..fd31670 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -788,6 +788,12 @@ end = struct
         in
         v_ecl
 
+    let rec extract_const_vars_root (ecl, _, _) =
+        List.fold_left
+          (fun l (_, x, v) -> match v with 
+                | EItem _ -> x::l
+                | _ -> l)
+          [] ecl
 
     (*
       scope_constrict : id list -> (id * id) list -> id list
@@ -818,8 +824,7 @@ end = struct
             0 cp_i
         in
 
-        let best = Array.make n 0 in
-        for i = 0 to n-1 do best.(i) <- i done;
+        let best = Array.init n (fun i -> i) in
 
         let usefull = ref true in
         Format.printf "SCA";
@@ -855,6 +860,58 @@ end = struct
         Array.to_list (Array.map (Array.get var_i) best)
 
     (*
+      force_ordering : id list -> (float * id list) list -> id list
+
+      Determine a good ordering for enumerate variables based on the FORCE algorithm
+    *)
+    let force_ordering vars groups =
+        let var_i = Array.of_list vars in
+        let n = Array.length var_i in
+
+        let i_var = Hashtbl.create n in
+        Array.iteri (fun i v -> Hashtbl.add i_var v i) var_i;
+        Hashtbl.add i_var "#BEGIN" (-1);
+
+        let ngroups = List.map
+          (fun (w, l) -> w, List.map (Hashtbl.find i_var) l)
+          groups in
+
+        let ord = Array.init n (fun i -> i) in
+
+        for iter = 0 to 500 do
+            let rev = Array.make n (-1) in
+            for i = 0 to n-1 do rev.(ord.(i)) <- i done;
+
+            let bw = Array.make n 0. in
+            let w = Array.make n 0. in
+
+            let gfun (gw, l) =
+              let sp = List.fold_left (+.) 0.
+                (List.map
+                  (fun i -> if i = -1 then -.gw else float_of_int (rev.(i))) l)
+              in
+              let b = sp /. float_of_int (List.length l) in
+              List.iter (fun i -> if i >= 0 then begin
+                          bw.(i) <- bw.(i) +. (gw *. b);
+                          w.(i) <- w.(i) +. gw end)
+                  l 
+            in
+            List.iter gfun ngroups;
+
+            let b = Array.init n
+              (fun i ->
+                if w.(i) = 0. then
+                    float_of_int i
+                else bw.(i) /. w.(i)) in
+                    
+            let ol = List.sort
+              (fun i j -> Pervasives.compare b.(i) b.(j))
+              (Array.to_list ord) in
+            Array.blit (Array.of_list ol) 0 ord 0 n
+        done;
+        List.map (Array.get var_i) (Array.to_list ord)
+
+    (*
       init_env : cmdline_opt -> rooted_prog -> env
     *)
     let init_env opt rp =
@@ -893,13 +950,31 @@ end = struct
 
         let lv = extract_linked_evars_root init_cl
             @ extract_linked_evars_root cl_g in
-
         let lv = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv)) in
-        let evars_ord = time "SCA" (fun () -> scope_constrict evars lv) in
-        let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in
-        let vb, vc = List.partition (fun n -> is_suffix n "state") vb in
-        let evars_ord = (List.rev va) @ vb @ vc in
+
+        let lv_f = List.map (fun (a, b) -> (1.0, [a; b])) lv in
+        let lv_f = lv_f @ (List.map (fun v -> (10.0, ["#BEGIN"; v]))
+          (extract_const_vars_root cl)) in
+        let lv_f = lv_f @ (List.map (fun v -> (5.0, ["#BEGIN"; v]))
+          (List.filter (fun n -> is_suffix n "init") evars)) in
+        let lv_f = lv_f @ (List.map (fun v -> (3.0, ["#BEGIN"; v]))
+          (List.filter (fun n -> is_suffix n "state") evars)) in
+        let evars_ord =
+          if true then
+            time "FORCE" (fun () -> force_ordering evars lv_f)
+          else
+            time "SCA" (fun () -> scope_constrict evars lv)
+        in
+
+        let evars_ord =
+          if false then
+            let va, vb = List.partition (fun n -> is_suffix n "init") evars_ord in
+            let vb, vc = List.partition (fun n -> is_suffix n "state") vb in
+            (List.rev va) @ vb @ vc
+          else
+            evars_ord
+        in
 
         let ev_order = Hashtbl.create (List.length evars) in
         List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -1015,10 +1090,12 @@ end = struct
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
         edd_dump_graphviz acc "/tmp/graph-final0.dot";
+
         Format.printf "Finishing up...@.";
         let final = edd_apply_cl acc e.cl in
         edd_dump_graphviz final "/tmp/graph-final.dot";
-        (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*)
+        if e.opt.verbose_ci then
+          Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;
 
         (* Check guarantees *)
         let check_guarantee (id, f) =