From d5de3f78a6804b0428febfdaa3f33eeaab39145a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 15 Jun 2020 15:42:41 -0700
Subject: [PATCH] [sledge] Refactor: split Equality.diff_classes out of
 ppx_classes_diff

Summary:
Refactor `Equality.ppx_classes_diff` into `diff_classes` to construct
the difference between classes maps explicitly, and change
`ppx_classes` to accept such a difference instead of computing it
internally.

This more flexibly composable interface allows elimination of extra
calls to `Equality.entails` to check if the difference is empty.

Reviewed By: jvillard

Differential Revision: D22038488

fbshipit-source-id: c19c18fc8
---
 sledge/src/equality.ml  | 42 ++++++++++++++---------------------------
 sledge/src/equality.mli | 18 ++++++++++--------
 sledge/src/sh.ml        |  5 +++--
 3 files changed, 27 insertions(+), 38 deletions(-)

diff --git a/sledge/src/equality.ml b/sledge/src/equality.ml
index 4dd80b120..9f37c877f 100644
--- a/sledge/src/equality.ml
+++ b/sledge/src/equality.ml
@@ -339,6 +339,8 @@ type t =
             'rep(resentative)' of [a] *) }
 [@@deriving compare, equal, sexp]
 
+type classes = Term.t list Term.Map.t
+
 let classes r =
   let add key data cls =
     if Term.equal key data then cls
@@ -382,14 +384,14 @@ let ppx_cls x = List.pp "@ = " (Term.ppx x)
 let pp_cls = ppx_cls (fun _ -> None)
 let pp_diff_cls = List.pp_diff ~compare:Term.compare "@ = " Term.pp
 
-let ppx_clss x fs cs =
+let ppx_classes x fs clss =
   List.pp "@ @<2>∧ "
-    (fun fs (key, data) ->
-      Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) key (ppx_cls x)
-        (List.sort ~compare:Term.compare data) )
-    fs (Term.Map.to_alist cs)
+    (fun fs (rep, cls) ->
+      Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep (ppx_cls x)
+        (List.sort ~compare:Term.compare cls) )
+    fs (Term.Map.to_alist clss)
 
-let pp_clss fs cs = ppx_clss (fun _ -> None) fs cs
+let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r)
 
 let pp_diff_clss =
   Term.Map.pp_diff ~data_equal:(List.equal Term.equal) Term.pp pp_cls
@@ -566,9 +568,6 @@ let entails_eq r d e =
   |>
   [%Trace.retn fun {pf} -> pf "%b"]
 
-let entails r s =
-  Subst.for_alli s.rep ~f:(fun ~key:e ~data:e' -> entails_eq r e e')
-
 let normalize = canon
 
 let class_of r e =
@@ -710,25 +709,12 @@ let fold_vars r ~init ~f =
   fold_terms r ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
 let fv e = fold_vars e ~f:Var.Set.add ~init:Var.Set.empty
-let pp_classes fs r = pp_clss fs (classes r)
-let ppx_classes x fs r = ppx_clss x fs (classes r)
-
-let ppx_classes_diff x fs (r, s) =
-  let clss = classes s in
-  let clss =
-    Term.Map.filter_mapi clss ~f:(fun ~key:rep ~data:cls ->
-        match
-          List.filter cls ~f:(fun exp -> not (entails_eq r rep exp))
-        with
-        | [] -> None
-        | cls -> Some cls )
-  in
-  List.pp "@ @<2>∧ "
-    (fun fs (rep, cls) ->
-      Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep
-        (List.pp "@ = " (Term.ppx x))
-        (List.dedup_and_sort ~compare:Term.compare cls) )
-    fs (Term.Map.to_alist clss)
+
+let diff_classes r s =
+  Term.Map.filter_mapi (classes r) ~f:(fun ~key:rep ~data:cls ->
+      match List.filter cls ~f:(fun exp -> not (entails_eq s rep exp)) with
+      | [] -> None
+      | cls -> Some cls )
 
 (** Existential Witnessing and Elimination *)
 
diff --git a/sledge/src/equality.mli b/sledge/src/equality.mli
index 8bbb0b806..a536606fc 100644
--- a/sledge/src/equality.mli
+++ b/sledge/src/equality.mli
@@ -14,11 +14,19 @@
     fresh, and the output set is the variables that have been generated. *)
 
 type t [@@deriving compare, equal, sexp]
+type classes = Term.t list Term.Map.t
+
+val classes : t -> classes
+(** [classes r] maps each equivalence class representative to the other
+    terms [r] proves equal to it. *)
+
+val diff_classes : t -> t -> classes
+(** [diff_classes r s] is the equality classes of [r] omitting equalities in
+    [s]. *)
 
 val pp : t pp
 val pp_classes : t pp
-val ppx_classes : Var.strength -> t pp
-val ppx_classes_diff : Var.strength -> (t * t) pp
+val ppx_classes : Var.strength -> classes pp
 
 include Invariant.S with type t := t
 
@@ -55,9 +63,6 @@ val is_false : t -> bool
 val entails_eq : t -> Term.t -> Term.t -> bool
 (** Test if an equation is entailed by a relation. *)
 
-val entails : t -> t -> bool
-(** Test if one relation entails another. *)
-
 val class_of : t -> Term.t -> Term.t list
 (** Equivalence class of [e]: all the terms [f] in the relation such that
     [e = f] is implied by the relation. *)
@@ -74,9 +79,6 @@ val difference : t -> Term.t -> Term.t -> Z.t option
 
 val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
 
-val classes : t -> Term.t list Term.Map.t
-(** The equalities that make up the relation. *)
-
 (** Solution Substitutions *)
 module Subst : sig
   type t [@@deriving compare, equal, sexp]
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index f4cfdf8f1..5cd920669 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -216,9 +216,10 @@ let rec pp_ ?var_strength vs parent_xs parent_cong fs
     if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ;
   if not (Var.Set.is_empty xs_d_vs) then
     Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ;
-  let first = Equality.entails parent_cong cong in
+  let clss = Equality.diff_classes cong parent_cong in
+  let first = Term.Map.is_empty clss in
   if not first then Format.fprintf fs "  " ;
-  Equality.ppx_classes_diff x fs (parent_cong, cong) ;
+  Equality.ppx_classes x fs clss ;
   let pure =
     if Option.is_none var_strength then [pure]
     else