From f606ac0915a03bd86f9179b434f9f9249f0828ac Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sat, 15 Aug 2020 02:18:51 -0700
Subject: [PATCH] [sledge] Change: Sh.pure_approx to a Formula

Summary: instead of an Sh with empty heap for each starjunction.

Reviewed By: jvillard

Differential Revision: D22571133

fbshipit-source-id: c2ce4bc5d
---
 sledge/src/exec.ml |  4 +++-
 sledge/src/fol.ml  |  2 ++
 sledge/src/fol.mli |  2 ++
 sledge/src/sh.ml   | 14 ++++++--------
 sledge/src/sh.mli  |  2 +-
 5 files changed, 14 insertions(+), 10 deletions(-)

diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml
index 951f78b24..b9e99fbd6 100644
--- a/sledge/src/exec.ml
+++ b/sledge/src/exec.ml
@@ -696,7 +696,9 @@ let exec_specs pre =
   let rec exec_specs_ (xs, pre) = function
     | specm :: specs ->
         let gs, spec = gen_spec pre.Sh.us specm in
-        let pre_pure = Sh.(star (exists gs (pure_approx spec.foot)) pre) in
+        let pre_pure =
+          Sh.(star (exists gs (Sh.pure (pure_approx spec.foot))) pre)
+        in
         let* post = exec_spec_ (xs, pre_pure) (gs, spec) in
         let+ posts = exec_specs_ (xs, pre) specs in
         Sh.or_ post posts
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 0ea15f3f8..4abe6cb39 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -787,7 +787,9 @@ module Formula = struct
 
   let not_ = _Not
   let and_ = _And
+  let andN = function [] -> tt | b :: bs -> List.fold ~init:b ~f:and_ bs
   let or_ = _Or
+  let orN = function [] -> ff | b :: bs -> List.fold ~init:b ~f:or_ bs
   let iff = _Iff
   let xor = _Xor
   let imp = _Imp
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 504b6248e..6dfb1701d 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -151,7 +151,9 @@ and Formula : sig
   (* connectives *)
   val not_ : t -> t
   val and_ : t -> t -> t
+  val andN : t list -> t
   val or_ : t -> t -> t
+  val orN : t list -> t
   val cond : cnd:t -> pos:t -> neg:t -> t
 
   (** Query *)
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index b8e23866c..5410fcc23 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -594,20 +594,18 @@ let is_false = function
       || List.exists heap ~f:(fun seg ->
              Context.implies ctx (Formula.eq seg.loc Term.zero) )
 
-let rec pure_approx ({us; xs; ctx; pure; heap= _; djns} as q) =
-  let heap = emp.heap in
-  let djns =
-    List.map_endo djns ~f:(fun djn -> List.map_endo djn ~f:pure_approx)
-  in
-  if heap == q.heap && djns == q.djns then q
-  else {us; xs; ctx; pure; heap; djns} |> check invariant
+let rec pure_approx q =
+  Formula.andN
+    ( q.pure
+    :: List.map q.djns ~f:(fun djn ->
+           Formula.orN (List.map djn ~f:pure_approx) ) )
 
 let pure_approx q =
   [%Trace.call fun {pf} -> pf "%a" pp q]
   ;
   pure_approx q
   |>
-  [%Trace.retn fun {pf} -> pf "%a" pp]
+  [%Trace.retn fun {pf} -> pf "%a" Formula.pp]
 
 let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
   let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
diff --git a/sledge/src/sh.mli b/sledge/src/sh.mli
index ad5dff26b..69113e468 100644
--- a/sledge/src/sh.mli
+++ b/sledge/src/sh.mli
@@ -126,7 +126,7 @@ val is_false : t -> bool
 val fv : ?ignore_ctx:unit -> t -> Var.Set.t
 (** Free variables, a subset of vocabulary. *)
 
-val pure_approx : t -> t
+val pure_approx : t -> Formula.t
 (** [pure_approx q] is inconsistent only if [q] is inconsistent. *)
 
 val fold_dnf :