[sledge] Change: Revise Sh handling of empty and pure approximation

Summary:
Make the relationship between Sh.is_empty and Sh.pure_approx stronger
and more precise. In particular:

> If [is_empty q], then [pure_approx q] is equivalent to
> [pure (pure_approx q)].

This enables replacing Solver.excise_pure with a simpler pure_entails
function. In particular, the heavy reliance on normalization of pure
formulas to true or false literals is eliminated, and only pure
entailment is needed.

Reviewed By: jvillard

Differential Revision: D22571146

fbshipit-source-id: 2fca64a61

sledge/src/sh.ml

@@ -583,10 +583,6 @@ let filter_heap ~f q =
 
 (** Query *)
 
-let is_emp = function
-  | {us= _; xs= _; ctx= _; pure; heap= []; djns= []} -> Formula.is_true pure
-  | _ -> false
-
 let is_false = function
   | {djns= [[]]; _} -> true
   | {ctx; pure; heap; _} ->
@@ -594,6 +590,9 @@ let is_false = function
       || List.exists heap ~f:(fun seg ->
              Context.implies ctx (Formula.eq seg.loc Term.zero) )
 
+let rec is_empty q =
+  List.is_empty q.heap && List.for_all ~f:(List.for_all ~f:is_empty) q.djns
+
 let rec pure_approx q =
   Formula.andN
     ( q.pure

sledge/src/sh.mli

@@ -116,18 +116,20 @@ val extend_us : Var.Set.t -> t -> t
 
 (** Query *)
 
-val is_emp : t -> bool
-(** Holds of [emp], with any vocabulary, existentials, and context. *)
-
 val is_false : t -> bool
 (** Holds only of inconsistent formulas, does not hold of all inconsistent
     formulas. *)
 
-val fv : ?ignore_ctx:unit -> t -> Var.Set.t
+val is_empty : t -> bool
-(** Free variables, a subset of vocabulary. *)
+(** Holds only if all satisfying states have empty heap. *)
 
 val pure_approx : t -> Formula.t
-(** [pure_approx q] is inconsistent only if [q] is inconsistent. *)
+(** [pure_approx q] is inconsistent only if [q] is inconsistent. If
+    [is_empty q], then [pure_approx q] is equivalent to
+    [pure (pure_approx q)]. *)
+
+val fv : ?ignore_ctx:unit -> t -> Var.Set.t
+(** Free variables, a subset of vocabulary. *)
 
 val fold_dnf :
      conj:(starjunction -> 'conjuncts -> 'conjuncts)

sledge/src/solver.ml

@@ -179,12 +179,6 @@ let excise_exists goal =
           let min = Sh.and_subst witnesses goal.min in
           goal |> with_ ~us ~min ~xs ~pgs:true )
 
-let excise_pure ({min; sub} as goal) =
-  trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
-  let pure' = Context.normalizef min.ctx sub.pure in
-  if Formula.is_false pure' then None
-  else Some (goal |> with_ ~sub:(Sh.with_pure pure' sub))
-
 (*   [k; o)
  * ⊢ [l; n)
  *
@@ -643,18 +637,16 @@ let excise_heap ({min; sub} as goal) =
   | Some goal -> Some (goal |> with_ ~pgs:true)
   | None -> Some goal
 
+let pure_entails x q = Sh.is_empty q && Context.implies x (Sh.pure_approx q)
+
 let rec excise ({min; xs; sub; zs; pgs} as goal) =
   [%Trace.info "@[<2>excise@ %a@]" pp goal] ;
   if Sh.is_false min then Some (Sh.false_ (Var.Set.diff sub.us zs))
-  else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min))
+  else if pure_entails min.ctx sub then
+    Some (Sh.exists zs (Sh.extend_us xs min))
   else if Sh.is_false sub then None
   else if pgs then
-    goal
+    goal |> with_ ~pgs:false |> excise_exists |> excise_heap >>= excise
-    |> with_ ~pgs:false
-    |> excise_exists
-    |> excise_pure
-    >>= excise_heap
-    >>= excise
   else None $> fun _ -> [%Trace.info "@[<2>excise fail@ %a@]" pp goal]
 
 let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =