diff options
| -rw-r--r-- | abstract/abs_interp.ml | 41 |
1 files changed, 26 insertions, 15 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index d706f35..00f7fad 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -179,33 +179,44 @@ end = struct let st = init_state widen_delay p root in let pnew = st.env in + let pnew_c = E.apply_cl pnew st.cl in let stay, stay_c = loop st pnew (E.vbottom pnew) in - let final = E.join (E.apply_cl pnew st.cl) stay_c in + Format.printf "@.@[<hov>New %a@]@.@." + E.print_all pnew_c; + Format.printf "@[<hov>Stay %a@]@.@." + E.print_all stay_c; + + let final = E.join pnew_c stay_c in Format.printf "@[<hov>Final %a@]@.@." E.print_all final; let check_guarantee (id, f) = - Format.printf "@[<hv>%s:@ %a@ " - id Formula_printer.print_expr f; - let z = E.apply_f final (BAnd(f, st.f)) in + let cl = Formula.conslist_of_f f in + Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥ @ " + id Formula_printer.print_conslist cl; + let z = E.apply_cl final cl in if E.is_bot z then Format.printf "OK@]@ " else Format.printf "FAIL@]@ " in - Format.printf "Guarantees: @[<v 0>"; - List.iter check_guarantee st.guarantees; - Format.printf "@]@."; - - Format.printf "Probes:@[<v>"; - List.iter (fun (p, id, _) -> - if p then Format.printf " %a ∊ %a@ " - Formula_printer.print_id id - E.print_itv (E.var_itv final id)) - st.all_vars; - Format.printf "@]@." + if st.guarantees <> [] then begin + Format.printf "Guarantee @[<v 0>"; + List.iter check_guarantee st.guarantees; + Format.printf "@]@." + end; + + if List.exists (fun (p, _, _) -> p) st.all_vars then begin + Format.printf "Probes:@[<v>"; + List.iter (fun (p, id, _) -> + if p then Format.printf " %a ∊ %a@ " + Formula_printer.print_id id + E.print_itv (E.var_itv final id)) + st.all_vars; + Format.printf "@]@." + end end |