[sledge] Refactor: Context.difference to Solver

Summary:
`Context.difference` is now just a convenience function that does not
need to be defined internally.

Reviewed By: jvillard

Differential Revision: D22571141

fbshipit-source-id: 58aea9488

sledge/src/fol.ml

@@ -1220,7 +1220,6 @@ module Context = struct
     Ses.Term.is_false (Ses.Equality.normalize x (f_to_ses b))
 
   let normalize x e = ses_map (Ses.Equality.normalize x) e
-  let difference x e f = Term.d_int (normalize x (Term.sub e f))
 
   let fold_terms ~init x ~f =
     Ses.Equality.fold_terms x ~init ~f:(fun s e -> f s (of_ses e))

sledge/src/fol.mli

@@ -230,11 +230,6 @@ module Context : sig
       relation, where [e'] and its subterms are expressed in terms of the
       relation's canonical representatives of each equivalence class. *)
 
-  val difference : t -> Term.t -> Term.t -> Z.t option
-  (** The difference as an offset. [difference r a b = Some k] if [r]
-      implies [a = b+k], or [None] if [a] and [b] are not equal up to an
-      integer offset. *)
-
   val fold_terms : init:'a -> t -> f:('a -> Term.t -> 'a) -> 'a
 
   (** Solution Substitutions *)

sledge/src/fol_test.ml

@@ -57,6 +57,7 @@ let%test_module _ =
     (* let and_eq a b r = and_formula wrt (Formula.eq a b) r |> snd *)
     (* let and_ r s = and_ wrt r s |> snd *)
     let or_ r s = orN wrt [r; s] |> snd
+    let difference x e f = Term.d_int (Context.normalize x (Term.sub e f))
     let r0 = true_
 
     let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0))

sledge/src/solver.ml

@@ -144,6 +144,7 @@ let fresh_var name vs zs ~wrt =
   let v = Term.var v in
   (v, vs, zs, wrt)
 
+let difference x e f = Term.d_int (Context.normalize x (Term.sub e f))
 let excise (k : Trace.pf -> _) = [%Trace.infok k]
 let trace (k : Trace.pf -> _) = [%Trace.infok k]
 
@@ -555,7 +556,7 @@ let excise_seg ({sub} as goal) msg ssg =
         (Sh.pp_seg_norm sub.ctx) ssg ) ;
   let {Sh.loc= k; bas= b; len= m; siz= o} = msg in
   let {Sh.loc= l; bas= b'; len= m'; siz= n} = ssg in
-  let* k_l = Context.difference sub.ctx k l in
+  let* k_l = difference sub.ctx k l in
   if
     (not (Context.implies sub.ctx (Formula.eq b b')))
     || not (Context.implies sub.ctx (Formula.eq m m'))
@@ -572,11 +573,11 @@ let excise_seg ({sub} as goal) msg ssg =
     | Neg -> (
         let ko = Term.add k o in
         let ln = Term.add l n in
-        let* ko_ln = Context.difference sub.ctx ko ln in
+        let* ko_ln = difference sub.ctx ko ln in
         match Int.sign (Z.sign ko_ln) with
         (* k+o-(l+n) < 0 so k+o < l+n *)
         | Neg -> (
-            let* l_ko = Context.difference sub.ctx l ko in
+            let* l_ko = difference sub.ctx l ko in
             match Int.sign (Z.sign l_ko) with
             (* l-(k+o) < 0     [k;   o)
              * so l < k+o    ⊢    [l;  n) *)
@@ -594,7 +595,7 @@ let excise_seg ({sub} as goal) msg ssg =
         )
     (* k-l = 0 so k = l *)
     | Zero -> (
-        let* o_n = Context.difference sub.ctx o n in
+        let* o_n = difference sub.ctx o n in
         match Int.sign (Z.sign o_n) with
         (* o-n < 0      [k; o)
          * so o < n   ⊢ [l;   n) *)
@@ -609,7 +610,7 @@ let excise_seg ({sub} as goal) msg ssg =
     | Pos -> (
         let ko = Term.add k o in
         let ln = Term.add l n in
-        let* ko_ln = Context.difference sub.ctx ko ln in
+        let* ko_ln = difference sub.ctx ko ln in
         match Int.sign (Z.sign ko_ln) with
         (* k+o-(l+n) < 0        [k; o)
          * so k+o < l+n    ⊢ [l;      n) *)
@@ -619,7 +620,7 @@ let excise_seg ({sub} as goal) msg ssg =
         | Zero -> Some (excise_seg_min_suffix goal msg ssg k_l)
         (* k+o-(l+n) > 0 so k+o > l+n *)
         | Pos -> (
-            let* k_ln = Context.difference sub.ctx k ln in
+            let* k_ln = difference sub.ctx k ln in
             match Int.sign (Z.sign k_ln) with
             (* k-(l+n) < 0        [k;  o)
              * so k < l+n    ⊢ [l;   n) *)