diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index 56b366e..a439995 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -779,6 +779,37 @@ 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 *) + let facts = get_root_true f in + let f, rp, _ = List.fold_left + (fun (f, (rp : rooted_prog), repls) eq -> + match eq with + | BEnumCons(E_EQ, a, EIdent b) + when a.[0] <> 'L' && b.[0] <> 'L' -> + + let a = try List.assoc a repls with Not_found -> a in + let b = try List.assoc b repls with Not_found -> b in + + if a = b then + f, rp, repls + else begin + let keep, repl = + if String.length a <= String.length b + then a, b + else b, a + in + Format.printf "Replacing %s with %s@." repl keep; + let f = formula_replace_evars [repl, keep; "L"^repl, "L"^keep] f in + 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 + f, rp, repls + end + | _ -> f, rp, repls) + (f, rp, []) facts in + Format.printf "Complete formula after simpl:@.%a@.@." + Formula_printer.print_expr f; let init_f = simplify_k [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)] f in let f = simplify_k [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] f in |