diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index 718cb7ffc..6f72cab36 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -430,7 +430,7 @@ let fold_vars r ~init ~f = let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty -let pp_classes x fs r = +let ppx_classes x fs r = List.pp "@ @<2>∧ " (fun fs (key, data) -> Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) key @@ -439,7 +439,9 @@ let pp_classes x fs r = fs (Map.to_alist (classes r)) -let pp_classes_diff x fs (r, s) = +let pp_classes fs r = ppx_classes (fun _ -> None) fs r + +let ppx_classes_diff x fs (r, s) = let clss = classes s in let clss = Map.filter_mapi clss ~f:(fun ~key:rep ~data:cls -> diff --git a/sledge/src/symbheap/equality.mli b/sledge/src/symbheap/equality.mli index 3d78ebda8..4e6ea5ae1 100644 --- a/sledge/src/symbheap/equality.mli +++ b/sledge/src/symbheap/equality.mli @@ -11,8 +11,9 @@ type t [@@deriving compare, equal, sexp] val pp : t pp -val pp_classes : Var.strength -> t pp -val pp_classes_diff : Var.strength -> (t * t) pp +val pp_classes : t pp +val ppx_classes : Var.strength -> t pp +val ppx_classes_diff : Var.strength -> (t * t) pp include Invariant.S with type t := t diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml index 4cf4471c3..18f74a4e6 100644 --- a/sledge/src/symbheap/equality_test.ml +++ b/sledge/src/symbheap/equality_test.ml @@ -14,10 +14,7 @@ let%test_module _ = (* let () = Trace.init ~margin:160 ~config:all () *) let printf pp = Format.printf "@\n%a@." pp let pp = printf pp - - let pp_classes = - Format.printf "@\n@[ %a@]@." (pp_classes (fun _ -> None)) - + let pp_classes = Format.printf "@\n@[ %a@]@." pp_classes let of_eqs = List.fold ~init:true_ ~f:(fun r (a, b) -> and_eq a b r) let ( ! ) i = Term.integer (Z.of_int i) let ( + ) = Term.add diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 5283aa168..b3cff81af 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -150,7 +150,7 @@ let rec pp_ ?var_strength vs parent_cong fs {us; xs; cong; pure; heap; djns} Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; let first = Equality.entails parent_cong cong in if not first then Format.fprintf fs " " ; - Equality.pp_classes_diff x fs (parent_cong, cong) ; + Equality.ppx_classes_diff x fs (parent_cong, cong) ; let pure = List.filter_map pure ~f:(fun e -> let e' = Equality.normalize cong e in