From c9fa894a3184914d1b0400f15d18fbb705624bd2 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 15 Aug 2020 02:18:43 -0700 Subject: [PATCH] [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 | 2 +- sledge/src/fol_test.ml | 116 ++++++++++++++++++++++++++++++++ sledge/src/fol_test.mli | 6 ++ sledge/src/ses/equality.ml | 14 ---- sledge/src/ses/equality.mli | 5 -- sledge/src/ses/equality_test.ml | 48 ------------- 6 files changed, 123 insertions(+), 68 deletions(-) create mode 100644 sledge/src/fol_test.ml create mode 100644 sledge/src/fol_test.mli diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index a491b8ee3..9cb827631 100644 --- a/sledge/src/fol.ml +++ b/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)) diff --git a/sledge/src/fol_test.ml b/sledge/src/fol_test.ml new file mode 100644 index 000000000..0c16a5f55 --- /dev/null +++ b/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@[ %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 ) diff --git a/sledge/src/fol_test.mli b/sledge/src/fol_test.mli new file mode 100644 index 000000000..81857a06f --- /dev/null +++ b/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. + *) diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml index afa8850cb..cd5296fa2 100644 --- a/sledge/src/ses/equality.ml +++ b/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] ; diff --git a/sledge/src/ses/equality.mli b/sledge/src/ses/equality.mli index 6760c4e59..29ddb36c7 100644 --- a/sledge/src/ses/equality.mli +++ b/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 *) diff --git a/sledge/src/ses/equality_test.ml b/sledge/src/ses/equality_test.ml index 86409e1e9..2c67353f1 100644 --- a/sledge/src/ses/equality_test.ml +++ b/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 _ =