[sledge] Refactor: Move difference from Equality to Context

Summary:
There is nothing specific to the Ses representation in the
implementation, and no uses within Ses.

Reviewed By: jvillard

Differential Revision: D22571150

fbshipit-source-id: 8952f0301

sledge/src/fol.ml

@@ -1215,7 +1215,7 @@ module Context = struct
   let entails_eq x e f = Ses.Equality.entails_eq x (to_ses e) (to_ses f)
   let normalize x e = ses_map (Ses.Equality.normalize x) e
   let normalizef x e = f_ses_map (Ses.Equality.normalize x) e
-  let difference x e f = Ses.Equality.difference x (to_ses e) (to_ses f)
+  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_test.ml

@@ -0,0 +1,116 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+let%test_module _ =
+  ( module struct
+    open Fol
+    open Context
+
+    let () = Trace.init ~margin:68 ()
+
+    (* let () =
+     *   Trace.init ~margin:160
+     *     ~config:(Result.ok_exn (Trace.parse "+Fol"))
+     *     ()
+     *
+     * [@@@warning "-32"] *)
+
+    let printf pp = Format.printf "@\n%a@." pp
+    let pp = printf pp
+    let pp_classes = Format.printf "@\n@[<hv>  %a@]@." pp_classes
+    let ( ! ) i = Term.integer (Z.of_int i)
+    let ( + ) = Term.add
+    let ( - ) = Term.sub
+
+    (* let ( * ) i e = Term.mulq (Q.of_int i) e *)
+    let wrt = Var.Set.empty
+    let t_, wrt = Var.fresh "t" ~wrt
+
+    (* let u_, wrt = Var.fresh "u" ~wrt *)
+    (* let v_, wrt = Var.fresh "v" ~wrt *)
+    let w_, wrt = Var.fresh "w" ~wrt
+    let x_, wrt = Var.fresh "x" ~wrt
+    let y_, wrt = Var.fresh "y" ~wrt
+    let z_, wrt = Var.fresh "z" ~wrt
+    let t = Term.var t_
+
+    (* let u = Term.var u_ *)
+    (* let v = Term.var v_ *)
+    let w = Term.var w_
+    let x = Term.var x_
+    let y = Term.var y_
+    let z = Term.var z_
+    let f = Term.mul t
+
+    (* let g = Term.mul u *)
+
+    let of_eqs l =
+      List.fold ~init:(wrt, true_)
+        ~f:(fun (us, r) (a, b) -> and_formula us (Formula.eq a b) r)
+        l
+      |> snd
+
+    (* 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 r0 = true_
+
+    let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0))
+    let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1))
+
+    let r1 = of_eqs [(x, y)]
+    let r2 = of_eqs [(x, y); (f x, y); (f y, z)]
+
+    let%test _ = difference (or_ r1 r2) x z |> Poly.equal None
+
+    let r4 = of_eqs [(w + !2, x - !3); (x - !5, y + !7); (y, z - !4)]
+
+    let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
+
+    let r9 = of_eqs [(x, z - !16)]
+
+    let%expect_test _ =
+      pp_classes r9 ;
+      pp r9 ;
+      [%expect
+        {|
+        (-16 + %z_5) = %x_3
+    
+      {sat= true;
+       rep= [[%x_3 ↦ (%z_5 + -16)]; [%z_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
+
+    let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
+
+    let r10 = of_eqs [(!16, z - x)]
+
+    let%expect_test _ =
+      pp_classes r10 ;
+      pp r10 ;
+      Format.printf "@.%a@." Term.pp (z - (x + !8)) ;
+      Format.printf "@.%a@." Term.pp (normalize r10 (z - (x + !8))) ;
+      Format.printf "@.%a@." Term.pp (x + !8 - z) ;
+      Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ;
+      [%expect
+        {|
+          (-16 + %z_5) = %x_3
+    
+        {sat= true;
+         rep= [[%x_3 ↦ (%z_5 + -16)]; [%z_5 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
+
+        (%z_5 - (%x_3 + 8))
+
+        8
+
+        ((%x_3 + 8) - %z_5)
+
+        -8 |}]
+
+    let%test _ = difference r10 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
+
+    let%test _ =
+      difference r10 (x + !8) z |> Poly.equal (Some (Z.of_int (-8)))
+  end )

sledge/src/fol_test.mli

@@ -0,0 +1,6 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)

sledge/src/ses/equality.ml

@@ -588,20 +588,6 @@ let fold_uses_of r t ~init ~f =
       let f trm s = fold_ trm ~init:s ~f in
       f trm (f rep s) )
 
-let difference r a b =
-  [%Trace.call fun {pf} -> pf "%a@ %a@ %a" Term.pp a Term.pp b pp r]
-  ;
-  let a = canon r a in
-  let b = canon r b in
-  ( if Term.equal a b then Some Z.zero
-  else
-    match normalize r (Term.sub a b) with
-    | Integer {data} -> Some data
-    | _ -> None )
-  |>
-  [%Trace.retn fun {pf} ->
-    function Some d -> pf "%a" Z.pp_print d | None -> pf ""]
-
 let apply_subst us s r =
   [%Trace.call fun {pf} -> pf "%a@ %a" Subst.pp s pp r]
   ;

sledge/src/ses/equality.mli

@@ -68,11 +68,6 @@ val normalize : t -> Term.t -> Term.t
     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 : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
 
 (** Solution Substitutions *)

sledge/src/ses/equality_test.ml

@@ -111,9 +111,6 @@ let%test_module _ =
       pp_classes r0 ;
       [%expect {||}]
 
-    let%test _ = difference r0 (f x) (f x) |> Poly.equal (Some (Z.of_int 0))
-    let%test _ = difference r0 !4 !3 |> Poly.equal (Some (Z.of_int 1))
-
     let r1 = of_eqs [(x, y)]
 
     let%expect_test _ =
@@ -152,7 +149,6 @@ let%test_module _ =
     let%test _ = entails_eq r2 (f y) y
     let%test _ = entails_eq r2 (f x) (f z)
     let%test _ = entails_eq r2 (g x y) (g z y)
-    let%test _ = difference (or_ r1 r2) x z |> Poly.equal None
 
     let%expect_test _ =
       let r = of_eqs [(w, y); (y, z)] in
@@ -222,7 +218,6 @@ let%test_module _ =
              [0 ↦ ]]} |}]
 
     let%test _ = entails_eq r4 x (w + !5)
-    let%test _ = difference r4 x w |> Poly.equal (Some (Z.of_int 5))
 
     let r5 = of_eqs [(x, y); (g w x, y); (g w y, f z)]
 
@@ -324,49 +319,6 @@ let%test_module _ =
 
     let%test _ = entails_eq r8 y !14
 
-    let r9 = of_eqs [(x, z - !16)]
-
-    let%expect_test _ =
-      pp_classes r9 ;
-      pp r9 ;
-      [%expect
-        {|
-        (%z_7 + -16) = %x_5
-    
-      {sat= true;
-       rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]} |}]
-
-    let%test _ = difference r9 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
-
-    let r10 = of_eqs [(!16, z - x)]
-
-    let%expect_test _ =
-      pp_classes r10 ;
-      pp r10 ;
-      Format.printf "@.%a@." Term.pp (z - (x + !8)) ;
-      Format.printf "@.%a@." Term.pp (normalize r10 (z - (x + !8))) ;
-      Format.printf "@.%a@." Term.pp (x + !8 - z) ;
-      Format.printf "@.%a@." Term.pp (normalize r10 (x + !8 - z)) ;
-      [%expect
-        {|
-          (%z_7 + -16) = %x_5
-    
-        {sat= true;
-         rep= [[%x_5 ↦ (%z_7 + -16)]; [%z_7 ↦ ]; [-1 ↦ ]; [0 ↦ ]]}
-
-        (-1 × %x_5 + %z_7 + -8)
-
-        8
-
-        (%x_5 + -1 × %z_7 + 8)
-
-        -8 |}]
-
-    let%test _ = difference r10 z (x + !8) |> Poly.equal (Some (Z.of_int 8))
-
-    let%test _ =
-      difference r10 (x + !8) z |> Poly.equal (Some (Z.of_int (-8)))
-
     let r11 = of_eqs [(!16, z - x); (x + !8 - z, z - !16 + !8 - z)]
 
     let%expect_test _ =