[sledge] Change: Sh.compare to ignore first-order context

Summary:
The first-order context is induced by the pure part, so no need to
compare it.

Reviewed By: jvillard

Differential Revision: D22381645

fbshipit-source-id: 29fff13a3

sledge/src/fol.ml

@@ -1173,7 +1173,7 @@ let f_ses_map : (Ses.Term.t -> Ses.Term.t) -> fml -> fml =
  *)
 
 module Context = struct
-  type t = Ses.Equality.t [@@deriving compare, equal, sexp]
+  type t = Ses.Equality.t [@@deriving sexp]
   type classes = exp list Term.Map.t
 
   let classes_of_ses clss =

sledge/src/fol.mli

@@ -169,7 +169,7 @@ end
 
 (** Inference System *)
 module Context : sig
-  type t [@@deriving compare, equal, sexp]
+  type t [@@deriving sexp]
   type classes = Term.t list Term.Map.t
 
   val classes : t -> classes

sledge/src/sh.ml

@@ -17,7 +17,7 @@ type seg = {loc: Term.t; bas: Term.t; len: Term.t; siz: Term.t; seq: Term.t}
 type starjunction =
   { us: Var.Set.t
   ; xs: Var.Set.t
-  ; ctx: Context.t
+  ; ctx: Context.t [@ignore]
   ; pure: Formula.t
   ; heap: seg list
   ; djns: disjunction list }