diff options
Diffstat (limited to 'abstract/abs_interp_edd.ml')
| -rw-r--r-- | abstract/abs_interp_edd.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml index b139f9e..56b366e 100644 --- a/abstract/abs_interp_edd.ml +++ b/abstract/abs_interp_edd.ml @@ -588,7 +588,6 @@ end = struct (* program expressions *) init_cl : conslist; cl : conslist; - cl_g : conslist; guarantees : (id * bool_expr) list; } @@ -773,18 +772,24 @@ end = struct init_env : cmdline_opt -> rooted_prog -> env *) let init_env opt rp = - let init_f, f = Transform.f_of_prog rp false in - let _, f_g = Transform.f_of_prog rp true in + let f = Transform.f_of_prog_incl_init rp false in + + let f = simplify_k (get_root_true f) f in + Format.printf "Complete formula:@.%a@.@." Formula_printer.print_expr f; + + (* 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 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 let init_f = simplify_k (get_root_true init_f) init_f in let f = simplify_k (get_root_true f) f in - let f_g = simplify_k (get_root_true f_g) f_g in Format.printf "Init formula:@.%a@.@." Formula_printer.print_expr init_f; Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; let cl = Formula.conslist_of_f f in - let cl_g = Formula.conslist_of_f f_g in let init_cl = Formula.conslist_of_f init_f in Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl; @@ -795,10 +800,10 @@ end = struct guarantees; Format.printf "@."; - let ve = mk_varenv rp f_g cl_g in + let ve = mk_varenv rp f cl in - { rp; opt; ve; init_cl; cl; cl_g; guarantees; } + { rp; opt; ve; init_cl; cl; guarantees; } |