From 108f38029404e8eb4b37c8892345917edfb3cac7 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 4 Jul 2014 17:20:51 +0200 Subject: Adapt domain with non-EDD disjunctions ; it doesn't work very well ! --- abstract/abs_interp_edd.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'abstract/abs_interp_edd.ml') diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 35bdbfb..8ea0012 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -936,6 +936,14 @@ end = struct let init_cl = Formula.conslist_of_f init_f in Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; + let guarantees = Transform.guarantees_of_prog rp in + Format.printf "Guarantees:@."; + List.iter (fun (id, f) -> + Format.printf " %s: %a@." id Formula_printer.print_expr f) + guarantees; + Format.printf "@."; + + (* add variables from LASTs *) let last_vars = uniq_sorted (List.sort compare (Transform.extract_last_vars f_g)) in let last_vars = List.map (fun id -> @@ -955,12 +963,6 @@ end = struct | TReal -> (id, true)::nv, ev) ([], []) all_vars in - let guarantees = Transform.guarantees_of_prog rp in - Format.printf "Guarantees:@."; - List.iter (fun (id, f) -> - Format.printf " %s: %a@." id Formula_printer.print_expr f) - guarantees; - Format.printf "@."; (* calculate order for enumerated variables *) let evars = List.map fst enum_vars in -- cgit v1.2.3