From 93c6dcc480d755b807b0a5702dfe1dd43c90e140 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 4 Sep 2020 13:37:23 -0700
Subject: [PATCH] [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      |  2 --
 sledge/src/sh.ml     | 25 +++++++++++--------------
 sledge/src/sh.mli    |  8 +-------
 sledge/src/solver.ml |  3 +--
 4 files changed, 13 insertions(+), 25 deletions(-)

diff --git a/sledge/TODO.org b/sledge/TODO.org
index 63dea1344..6cd074506 100644
--- a/sledge/TODO.org
+++ b/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.
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index b86120d7e..302d8b6ef 100644
--- a/sledge/src/sh.ml
+++ b/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= _}
-    ~init ~f =
-  List.fold ~init heap ~f:(fun init -> fold_vars_seg ~f ~init)
-  |> fun init ->
-  Term.fold_vars ~f ~init (Formula.inject pure)
-  |> fun init ->
-  if Option.is_some ignore_ctx then init else Context.fold_vars ~f ~init ctx
-
-let fold_vars ?ignore_ctx fold_vars q ~init ~f =
-  fold_vars_stem ?ignore_ctx ~init ~f q
+let fold_vars_stem ?ignore_ctx ?ignore_pure
+    {us= _; xs= _; ctx; pure; heap; djns= _} ~init ~f =
+  let unless flag f init = if Option.is_some flag then init else f ~init in
+  List.fold ~f:(fun init -> fold_vars_seg ~f ~init) heap ~init
+  |> unless ignore_pure (Term.fold_vars ~f (Formula.inject pure))
+  |> unless ignore_ctx (Context.fold_vars ~f ctx)
+
+let fold_vars ?ignore_ctx ?ignore_pure fold_vars q ~init ~f =
+  fold_vars_stem ?ignore_ctx ?ignore_pure ~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
 
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index 9935cab2e..6677deb91 100644
--- a/sledge/src/sh.mli
+++ b/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 :
diff --git a/sledge/src/solver.ml b/sledge/src/solver.ml
index bb0e15740..79ad4c65c 100644
--- a/sledge/src/solver.ml
+++ b/sledge/src/solver.ml
@@ -154,8 +154,7 @@ let excise_exists goal =
   else
     let solutions_for_xs =
       let xs =
-        Var.Set.diff goal.xs
-          (Sh.fv ~ignore_ctx:() (Sh.with_pure Formula.tt goal.sub))
+        Var.Set.diff goal.xs (Sh.fv ~ignore_ctx:() ~ignore_pure:() goal.sub)
       in
       Context.solve_for_vars [Var.Set.empty; goal.us; xs] goal.sub.ctx
     in