diff options
| -rw-r--r-- | abstract/abs_interp_dynpart.ml | 2 | ||||
| -rw-r--r-- | abstract/abs_interp_edd.ml | 58 | ||||
| -rw-r--r-- | abstract/varenv.ml | 11 | ||||
| -rw-r--r-- | main.ml | 25 |
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 } @@ -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 |