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. --- abstract/abs_interp_dynpart.ml | 2 +- abstract/abs_interp_edd.ml | 58 ++++++++++++++++++++++++------------------ abstract/varenv.ml | 11 ++++++-- 3 files changed, 43 insertions(+), 28 deletions(-) (limited to 'abstract') 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: @[[%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 } -- cgit v1.2.3