Implement selection of disjunction variables for EDDs.

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

4 files changed, 66 insertions, 30 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 }
 
diff --git a/main.ml b/main.ml
index c283328..f130b6c 100644
--- a/main.ml
+++ b/main.ml
@@ -54,7 +54,7 @@ let ai_root = ref "test"
 let ai_widen_delay = ref 5
 let ai_no_time_scopes = ref "all"
 let ai_init_scopes = ref "all"
-let ai_disj_v = ref ""
+let ai_disj_v = ref "all"
 let ai_max_dp_depth = ref 10
 let ai_max_dp_width = ref 100
 let ai_vci = ref false
@@ -187,6 +187,27 @@ let () =
           || !ai_edd_itv_dp || !ai_edd_rel_dp then
       begin
           let comma_split = Str.split (Str.regexp ",") in
+          let match_s s pat =
+            let n, m = String.length s, String.length pat in
+            let memo = Array.make_matrix (n+1) (m+1) None in
+            let rec aux i j =
+              match memo.(i).(j) with
+              | Some x -> x
+              | None ->
+                let x =
+                  if i = n && j = m
+                    then true
+                  else if j = m && i < n
+                    then false
+                  else if i = n && j < m
+                    then pat.[j] = '*' && aux i (j+1)
+                  else
+                    if pat.[j] = '*'
+                      then aux (i+1) j || aux i (j+1)
+                      else s.[i] = pat.[j] && aux (i+1) (j+1)
+                in memo.(i).(j) <- Some x; x
+            in aux 0 0
+          in
           let select_f x =
               if x = "all" then
                 (fun _ -> true)
@@ -195,7 +216,7 @@ let () =
               else if String.length x > 5 && String.sub x 0 5 = "last+" then
                 let psl = comma_split
                   (String.sub x 5 (String.length x - 5)) in
-                (fun i -> i.[0] = 'L' || List.mem i psl)
+                (fun i -> i.[0] = 'L' || List.exists (match_s i) psl)
               else
                  (fun i -> List.mem i (comma_split x))
           in