[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

@@ -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

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. *)