Not much : find acceptably good ordering for variables.

1 files changed, 28 insertions, 55 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 5b3b0ec..f08be44 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -91,6 +91,7 @@ end = struct
         | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true
         | _ -> false
 
+
     let new_node_fun () =
         let nc = ref 0 in
         let node_memo = Hashtbl.create 12 in
@@ -128,7 +129,6 @@ end = struct
       edd_print : Format.formatter -> edd_v -> unit
     *)
     let edd_print fmt v =
-        let max_n = ref 0 in
         let max_v = ref 0 in
 
         let print_nodes = Queue.create () in
@@ -248,10 +248,10 @@ end = struct
                   then vid, vid2
                   else vid2, vid
             in
-            let n = ref 0 in
+            let nc = ref 0 in
             let nb x =
-              incr n;
-              DChoice(!n, b,
+              incr nc;
+              DChoice(!nc, b,
                     List.map (fun v -> if op v x then v, DTop else v, DBot)
                       (List.assoc b ve.evars))
             in
@@ -270,9 +270,6 @@ end = struct
 
         let f f_rec na nb =
           match na, nb with
-          | DTop, _ | _, DTop -> DTop
-          | DBot, DBot -> DBot
-
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             let kl = List.map2
                 (fun (ta, ba) (tb, bb) -> assert (ta = tb);
@@ -289,13 +286,8 @@ end = struct
             in
             dq v kl
 
-          | DBot, DVal (i, _) ->
-              get_leaf (Hashtbl.find b.leaves i)
-          | DVal (i, _), DBot ->
-              get_leaf (Hashtbl.find a.leaves i)
-          | DVal (u, _), DVal (v, _) ->
-            let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-            get_leaf x
+          | DTop, _ | _, DTop -> DTop
+          | DBot, DBot -> DBot
 
           | DChoice(_,va, la), _ ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
@@ -303,6 +295,14 @@ end = struct
           | _, DChoice(_, vb, lb) ->
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
+
+          | DVal (u, _), DVal (v, _) ->
+            let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
+          | DVal(u, _), DBot ->
+            get_leaf (Hashtbl.find a.leaves u)
+          | DBot, DVal(v, _) ->
+            get_leaf (Hashtbl.find b.leaves v)
         in
           { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
 
@@ -313,9 +313,6 @@ end = struct
 
         let f f_rec na nb =
           match na, nb with
-          | DBot, _ | _, DBot -> DBot
-          | DTop, DTop -> DTop
-
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             let kl = List.map2
                 (fun (ta, ba) (tb, bb) -> assert (ta = tb);
@@ -332,13 +329,8 @@ end = struct
             in
             dq v kl
 
-          | DTop, DVal (i, _) ->
-            get_leaf (Hashtbl.find b.leaves i)
-          | DVal (i, _), DTop ->
-            get_leaf (Hashtbl.find a.leaves i)
-          | DVal (u, _) , DVal (v, _) ->
-            let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-            get_leaf x
+          | DBot, _ | _, DBot -> DBot
+          | DTop, DTop -> DTop
 
           | DChoice(_, va, la), _ ->
             let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
@@ -346,6 +338,14 @@ end = struct
           | _, DChoice(_, vb, lb) ->
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
+
+          | DVal (u, _) , DVal (v, _) ->
+            let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
+          | DVal(u, _), DTop ->
+            get_leaf (Hashtbl.find a.leaves u)
+          | DTop, DVal(v, _) ->
+            get_leaf (Hashtbl.find b.leaves v)
         in
           { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
 
@@ -757,30 +757,6 @@ end = struct
         in
         v_ecl
 
-    let rec extract_linked_evars(ecl, _, r) =
-        let v_ecl = List.fold_left
-            (fun c (_, x, v) -> match v with
-                | EIdent y -> (x, y)::c
-                | _ -> c)
-            [] ecl
-        in
-        let v_ecl2 =
-          let q = List.fold_left
-            (fun c (_, x, v) -> match v with
-              | EItem _ -> x::c | _ -> c)
-            [] ecl
-          in
-          match q with
-          | [x; y] -> [x, y]
-          | [x; y; z] -> [x, y; y, z; z, x]
-          | _ -> []
-        in
-        let rec aux = function
-          | CLTrue | CLFalse -> []
-          | CLAnd(a, b) -> aux a @ aux b
-          | CLOr(a, b) -> extract_linked_evars a @ extract_linked_evars b
-        in
-        v_ecl @ v_ecl2 @ aux r
 
     (*
       scope_constrict : id list -> (id * id) list -> id list
@@ -885,15 +861,12 @@ end = struct
         (* calculate order for enumerated variables *)
         let evars = List.map fst enum_vars in
 
-        let lv1 = extract_linked_evars_root init_cl
+        let lv = extract_linked_evars_root init_cl
             @ extract_linked_evars_root cl_g in
-        let lv2 = extract_linked_evars init_cl @ extract_linked_evars cl_g in
 
-        let lv1 = uniq_sorted
-             (List.sort Pervasives.compare (List.map ord_couple lv1)) in
-        let lv2 = uniq_sorted
-             (List.sort Pervasives.compare (List.map ord_couple lv2)) in
-        let evars_ord = time "SCA" (fun () -> scope_constrict evars ( lv1 )) 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