diff options
Diffstat (limited to 'main.ml')
| -rw-r--r-- | main.ml | 25 |
1 files changed, 23 insertions, 2 deletions
@@ -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 |