From dd3645820f74c7962bce65c8ee863f98d903213f Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Thu, 7 May 2020 16:53:50 -0700 Subject: [PATCH] [sledge] Remove Sh.var_strength, no longer used by Solver Summary: Now only used internally for printing. Reviewed By: jvillard Differential Revision: D21441534 fbshipit-source-id: 1e6e484c8 --- sledge/src/sh.ml | 5 ++--- sledge/src/sh.mli | 5 ----- 2 files changed, 2 insertions(+), 8 deletions(-) diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 59cb1c03b..1391a29ba 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -120,14 +120,13 @@ let rec var_strength_ xs m q = in (m_stem, m) -let var_strength_full ?(xs = Var.Set.empty) q = +let var_strength ?(xs = Var.Set.empty) q = let m = Var.Set.fold xs ~init:Var.Map.empty ~f:(fun m x -> Var.Map.set m ~key:x ~data:`Existential ) in var_strength_ xs m q -let var_strength q = snd (var_strength_full q) let pp_memory x fs (siz, arr) = Term.ppx x fs (Term.memory ~siz ~arr) let pp_seg x fs {loc; bas; len; siz; arr} = @@ -269,7 +268,7 @@ and pp_djn ?var_strength vs xs cong fs = function djn let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q = - pp_ ~var_strength:(var_strength_full ~xs q) us xs cong fs q + pp_ ~var_strength:(var_strength ~xs q) us xs cong fs q let pp fs q = pp_diff_eq Equality.true_ fs q let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli index b0578c035..c99d38dfe 100644 --- a/sledge/src/sh.mli +++ b/sledge/src/sh.mli @@ -124,11 +124,6 @@ val is_false : t -> bool val fv : ?ignore_cong:unit -> t -> Var.Set.t (** Free variables, a subset of vocabulary. *) -val var_strength : t -> [`Anonymous | `Existential | `Universal] Var.Map.t -(** Classify each variable in a formula as either [Universal], - [Existential], or [Anonymous], meaning existential but with only one - occurrence. *) - val pure_approx : t -> t (** [pure_approx q] is inconsistent only if [q] is inconsistent. *)