Adapt non-EDD disjunction interpret to use two set of disjunction vars.

1 files changed, 15 insertions, 20 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 787c6d6..cb5ae9c 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -177,7 +177,8 @@ end = struct
         (* abstract interpretation *)
         cycle       : (id * id * typ) list;     (* s'(x) = s(y) *)
         forget      : (id * typ) list;          (* s'(x) not specified *)
-        d_vars      : id list;                  (* disjunction variables *)
+        d_vars      : id list;                  (* disjunction variables when calculating *)
+        acc_d_vars  : id list;                  (* disjunction variables in accumulator *)
         top         : case_v;
         env         : (case, case_v) Hashtbl.t;
         mutable delta : case list;
@@ -187,7 +188,7 @@ end = struct
     (*
       print_st : Formatter.t -> st -> unit
     *)
-    let print_st fmt st = print_aux fmt st.d_vars st.env
+    let print_st fmt st = print_aux fmt st.acc_d_vars st.env
 
     (*
       add_case : st -> case_v -> unit
@@ -219,7 +220,7 @@ end = struct
               | [en] -> aux en (v::vals) q
               | _ -> assert false)
             (ED.project enum p)
-      in aux enum [] st.d_vars
+      in aux enum [] st.acc_d_vars
 
   
     (*
@@ -265,7 +266,7 @@ end = struct
             (enum, num) st.forget
 
     let dd_pass_cycle st (v : dd_v) =
-      let vv = dd_bot v.d_vars in
+      let vv = dd_bot st.acc_d_vars in
       Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
       vv
 
@@ -326,29 +327,23 @@ end = struct
       (* actually, don't calculate them, rely on user input *)
       let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k)
           (List.map (fun (id, _) -> id) enum_vars) in
+      let acc_d_vars = List.filter (fun i -> i.[0] = 'L') d_vars in 
 
       (* setup abstract data *)
       let top = ED.top enum_vars, ND.top num_vars in
       let delta = [] in
       let widen = Hashtbl.create 12 in
 
-      (* calculate initial state and environment *)
-      let init_s = dd_bot d_vars in
-
-      List.iter (fun ed -> dd_add_case init_s ed)
-        (apply_cl_get_all_cases top init_cl);
-
-      let env_dd = apply_cl init_s init_cl in (* useless refinement ? *)
-
       let st = 
       { rp; opt; enum_vars; num_vars; all_vars;
          cl; cl_g; guarantees;
-        cycle; forget; d_vars; top;
-        env = Hashtbl.create 1; delta; widen } in
+        cycle; forget; acc_d_vars; d_vars; top;
+        env = Hashtbl.create 12; delta; widen } in
 
-      let env_dd_pass = dd_pass_cycle st env_dd in
+      (* calculate initial state and environment *)
+      List.iter (fun ed -> add_case st (pass_cycle st ed))
+        (apply_cl_get_all_cases top init_cl);
 
-      let st = { st with env = env_dd_pass.data } in
       Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
 
       st
@@ -370,10 +365,10 @@ end = struct
     let set_target_case st env case =
       List.fold_left2
         (fun env id v ->
-          if List.exists (fun (id2, _) -> id2 = "N"^id) st.enum_vars then
-            dd_apply_econs env (E_EQ, "N"^id, EItem v)
+          if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+            dd_apply_econs env (E_EQ, id, EItem v)
           else env)
-        env st.d_vars case
+        env st.acc_d_vars case
 
     (*
       do_prog : rooted_prog -> unit
@@ -395,7 +390,7 @@ end = struct
             (print_list Formula_printer.print_id ", ") case;
         
         let start = try Hashtbl.find st.env case with Not_found -> assert false in
-        let start_dd = dd_singleton st.d_vars start in
+        let start_dd = dd_singleton st.acc_d_vars start in
         let f i =
           let i = dd_singleton st.d_vars i in
           let i' = set_target_case st i case in