diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index a439995..23d4734 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -557,7 +557,8 @@ end = struct last_vars = []; all_vars = []; cycle = []; - forget = []; } in + forget = []; + forget_inv = []; } in Hashtbl.add ve.ev_order "x" 0; Hashtbl.add ve.ev_order "y" 1; Hashtbl.add ve.ev_order "z" 2; @@ -755,13 +756,10 @@ end = struct let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in let ef, nf = List.fold_left - (fun (ef, nf) (_, var, t) -> - if var.[0] <> 'N' then - match t with - | TEnum _ -> var::ef, nf - | TReal | TInt -> ef, var::nf - else ef, nf) - ([], []) env.rp.all_vars in + (fun (ef, nf) (var, t) -> match t with + | TEnum _ -> var::ef, nf + | TReal | TInt -> ef, var::nf) + ([], []) env.ve.forget_inv in let v = edd_forget_vars v ef in edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf) @@ -779,8 +777,9 @@ end = struct (* HERE POSSIBILITY OF SIMPLIFYING EQUATIONS SUCH AS x = y OR x = v *) (* IF SUCH AN EQUATION APPEARS IN get_root_true f THEN IT IS ALWAYS TRUE *) + (* WHY THE **** AM I SHOUTING LIKE THAT ? *) let facts = get_root_true f in - let f, rp, _ = List.fold_left + let f, rp, repls = List.fold_left (fun (f, (rp : rooted_prog), repls) eq -> match eq with | BEnumCons(E_EQ, a, EIdent b) @@ -802,8 +801,12 @@ end = struct let rp = { rp with all_vars = List.filter (fun (_, id, _) -> id <> repl) rp.all_vars } in - let repls = (repl, keep):: - (List.map (fun (r, k) -> r, if k = repl then keep else k) repls) in + let repls = (repl, keep; "L"^repl, "L"^keep):: + (List.map + (fun (r, k) -> r, + if k = repl then keep else + if k = "L"^repl then "L"^keep else k) + repls) in f, rp, repls end | _ -> f, rp, repls) @@ -825,6 +828,9 @@ end = struct Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; let guarantees = Transform.guarantees_of_prog rp in + let guarantees = List.map + (fun (id, f) -> id, formula_replace_evars repls f) + guarantees in Format.printf "Guarantees:@."; List.iter (fun (id, f) -> Format.printf " %s: %a@." id Formula_printer.print_expr f) |