Implement selection of disjunction variables for EDDs.

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

1 files changed, 23 insertions, 2 deletions

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