From 5c4598c2e9383bcbfadd1d81bc3c89105fd6edff Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 15 Aug 2020 02:19:11 -0700 Subject: [PATCH] [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 | 1 - sledge/src/fol.mli | 5 ----- sledge/src/fol_test.ml | 1 + sledge/src/solver.ml | 13 +++++++------ 4 files changed, 8 insertions(+), 12 deletions(-) diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 79d9bb29c..693d33fd9 100644 --- a/sledge/src/fol.ml +++ b/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)) diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index eb6bd7c37..1c9364341 100644 --- a/sledge/src/fol.mli +++ b/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 *) diff --git a/sledge/src/fol_test.ml b/sledge/src/fol_test.ml index 0c16a5f55..bdd9a60c1 100644 --- a/sledge/src/fol_test.ml +++ b/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)) diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml index 615b920e7..bb0e15740 100644 --- a/sledge/src/solver.ml +++ b/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) *)