From 8bba764aaade1839b62be7c4f24292f8dc85ada8 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Wed, 30 Jul 2014 10:37:28 +0200 Subject: Implement selection of disjunction variables for EDDs. Next (?) : leaves can store information on evars. --- main.ml | 25 +++++++++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) (limited to 'main.ml') 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 -- cgit v1.2.3