[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

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

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

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

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 =

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 :