Implement selection of disjunction variables for EDDs.

Next (?) : leaves can store information on evars.

3 files changed, 43 insertions, 28 deletions

diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 2ff950a..bbd8d19 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -221,7 +221,7 @@ end = struct
           guarantees;
         Format.printf "@.";
         
-        let ve = mk_varenv rp f (conslist_of_f f) in
+        let ve = mk_varenv rp opt.disjunct f (conslist_of_f f) in
 
         let env = {
           rp; opt; ve; f; guarantees;
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 722dc1a..cdf3c7e 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -259,30 +259,37 @@ end = struct
     *)
     let edd_of_cons ve (op, vid, r) =
         let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
-
-        let leaves = Hashtbl.create 1 in
-
-        let root = match r with
-        | EItem x ->
-          DChoice(0, vid,
-              List.map (fun v -> if op v x then v, DTop else v, DBot)
-                (List.assoc vid ve.evars))      
-        | EIdent vid2 ->
-            let a, b =
-                if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2
-                  then vid, vid2
-                  else vid2, vid
-            in
-            let nc = ref 0 in
-            let nb x =
-              incr nc;
-              DChoice(!nc, b,
-                    List.map (fun v -> if op v x then v, DTop else v, DBot)
-                      (List.assoc b ve.evars))
+        if not (List.mem vid ve.d_vars) 
+          then edd_top ve
+          else
+            let leaves = Hashtbl.create 1 in
+            let root = match r with
+            | EItem x ->
+              DChoice(0, vid,
+                  List.map (fun v -> if op v x then v, DTop else v, DBot)
+                    (List.assoc vid ve.evars))      
+            | EIdent vid2 ->
+                if not (List.mem vid2 ve.d_vars)
+                  then DTop
+                  else
+                    let a, b =
+                        if Hashtbl.find ve.ev_order vid
+                            < Hashtbl.find ve.ev_order vid2
+                          then vid, vid2
+                          else vid2, vid
+                    in
+                    let nc = ref 0 in
+                    let nb x =
+                      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
+                    DChoice(0, a, List.map
+                      (fun x -> x, nb x)
+                      (List.assoc a ve.evars))
             in
-            DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
-        in
-        { ve; root; leaves }
+            { ve; root; leaves }
 
     (*
       edd_join : edd_v -> edd_v -> edd_v
@@ -570,7 +577,8 @@ end = struct
             all_vars = [];
             cycle = [];
             forget = [];
-            forget_inv = []; } in
+            forget_inv = [];
+            d_vars = ["x"; "y"; "z"] } in
         Hashtbl.add ve.ev_order "x" 0;
         Hashtbl.add ve.ev_order "y" 1;
         Hashtbl.add ve.ev_order "z" 2;
@@ -856,7 +864,7 @@ end = struct
           guarantees;
         Format.printf "@.";
         
-        let ve = mk_varenv rp f cl in
+        let ve = mk_varenv rp opt.disjunct f cl in
 
         { rp; opt; ve; init_cl; cl; guarantees; }
 
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index cf29edf..bcfa77a 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -17,6 +17,7 @@ type varenv = {
 
     last_vars     : (bool * id * typ) list;
     all_vars      : (bool * id * typ) list;
+    d_vars        : id list;
 
     cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
     forget        : (id * typ) list;          (* s'(x) not specified *)
@@ -228,7 +229,7 @@ let force_ordering vars groups =
   - cycle, forget
 *)
 
-let mk_varenv (rp : rooted_prog) f cl =
+let mk_varenv (rp : rooted_prog) disj_fun f cl =
     (* add variables from LASTs *)
     let last_vars = uniq_sorted 
       (List.sort compare (extract_last_vars f)) in
@@ -311,6 +312,12 @@ let mk_varenv (rp : rooted_prog) f cl =
           not (List.exists (fun (_, b, _) -> b = id) cycle))
         all_vars) in
 
-    { evars = enum_vars; nvars = num_vars; ev_order;
+    (* use specified disjunction variables *)
+    let d_vars = List.filter disj_fun
+        (List.map (fun (id, _) -> id) enum_vars) in
+    Format.printf "Disjunction variables: @[<hov>[%a]@]@."
+      (print_list Formula_printer.print_id ", ") d_vars;
+
+    { evars = enum_vars; nvars = num_vars; ev_order; d_vars;
       last_vars; all_vars; cycle; forget; forget_inv }