[sledge] Refactor: Replace Sh.with_pure with ~ignore_pure arg to Sh.fv

Summary:
The only use of the ill-specified Sh.with_pure function is to ignore
the pure part when computing free variables. So add an argument to
Sh.fv to achieve that explicitly and remove Sh.with_pure.

Reviewed By: ngorogiannis

Differential Revision: D23459517

fbshipit-source-id: 8767799ca

sledge/TODO.org

@@ -214,8 +214,6 @@ since they (could) have the same domain
 ** eliminate existentials
 by changing Congruence reps to avoid existentials if possible and then normalizing Sh ito reps
 ** add exps in pure and pto (including memory siz and arr) to carrier
-** Sh.with_pure is an underspeced, tightly coupled, API: replace
-Sh.with_pure assumes that the replaced pure part is defined in the same vocabulary, induces the same congruence, etc. This API is fragile, and ought to be replaced with something that has simpler assumptions without imposing an excessive pessimization.
 ** optimize Sh.and_ with direct implementation
 ** perhaps it would be better to allow us and xs to intersect
 but to rename xs when binding them or otherwise operating under the quantifier. But it might be an unnecessary complication to always have to deal with the potential for shadowing.

sledge/src/sh.ml

@@ -75,16 +75,15 @@ let fold_terms_seg {loc; bas; len; siz; seq} ~init ~f =
 let fold_vars_seg seg ~init ~f =
   fold_terms_seg seg ~init ~f:(fun init -> Term.fold_vars ~f ~init)
 
-let fold_vars_stem ?ignore_ctx {us= _; xs= _; ctx; pure; heap; djns= _}
+let fold_vars_stem ?ignore_ctx ?ignore_pure
-    ~init ~f =
+    {us= _; xs= _; ctx; pure; heap; djns= _} ~init ~f =
-  List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
+  let unless flag f init = if Option.is_some flag then init else f ~init in
-  |> fun init ->
+  List.fold ~f:(fun init -> fold_vars_seg ~f ~init) heap ~init
-  Term.fold_vars ~f ~init (Formula.inject pure)
+  |> unless ignore_pure (Term.fold_vars ~f (Formula.inject pure))
-  |> fun init ->
+  |> unless ignore_ctx (Context.fold_vars ~f ctx)
-  if Option.is_some ignore_ctx then init else Context.fold_vars ~f ~init ctx
+
-
+let fold_vars ?ignore_ctx ?ignore_pure fold_vars q ~init ~f =
-let fold_vars ?ignore_ctx fold_vars q ~init ~f =
+  fold_vars_stem ?ignore_ctx ?ignore_pure ~init ~f q
-  fold_vars_stem ?ignore_ctx ~init ~f q
   |> fun init ->
   List.fold ~init q.djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
 
@@ -266,10 +265,10 @@ let pp_raw fs q =
 
 let fv_seg seg = fold_vars_seg seg ~f:Var.Set.add ~init:Var.Set.empty
 
-let fv ?ignore_ctx q =
+let fv ?ignore_ctx ?ignore_pure q =
   let rec fv_union init q =
     Var.Set.diff
-      (fold_vars ?ignore_ctx fv_union q ~init ~f:Var.Set.add)
+      (fold_vars ?ignore_ctx ?ignore_pure fv_union q ~init ~f:Var.Set.add)
       q.xs
   in
   fv_union Var.Set.empty q
@@ -570,8 +569,6 @@ let seg pt =
 
 (** Update *)
 
-let with_pure pure q = {q with pure} |> check invariant
-
 let rem_seg seg q =
   {q with heap= List.remove_exn q.heap seg} |> check invariant
 

sledge/src/sh.mli

@@ -72,12 +72,6 @@ val and_subst : Context.Subst.t -> t -> t
 
 (** Update *)
 
-val with_pure : Formula.t -> t -> t
-(** [with_pure pure q] is [{q with pure}], which assumes that [q.pure] and
-    [pure] are defined in the same vocabulary. Note that [ctx] is not
-    weakened, so if [pure] and [q.pure] do not induce the same context, then
-    the result will have a stronger [ctx] than induced by its [pure]. *)
-
 val rem_seg : seg -> t -> t
 (** [star (seg s) (rem_seg s q)] is equivalent to [q], assuming that [s] is
     (physically equal to) one of the elements of [q.heap]. Raises if [s] is
@@ -128,7 +122,7 @@ val pure_approx : t -> Formula.t
     [is_empty q], then [pure_approx q] is equivalent to
     [pure (pure_approx q)]. *)
 
-val fv : ?ignore_ctx:unit -> t -> Var.Set.t
+val fv : ?ignore_ctx:unit -> ?ignore_pure:unit -> t -> Var.Set.t
 (** Free variables, a subset of vocabulary. *)
 
 val fold_dnf :

sledge/src/solver.ml

@@ -154,8 +154,7 @@ let excise_exists goal =
   else
     let solutions_for_xs =
       let xs =
-        Var.Set.diff goal.xs
+        Var.Set.diff goal.xs (Sh.fv ~ignore_ctx:() ~ignore_pure:() goal.sub)
-          (Sh.fv ~ignore_ctx:() (Sh.with_pure Formula.tt goal.sub))
       in
       Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx
     in