From 8ced6593031fd64a8dc36e296281f501e9047bd0 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sat, 15 Aug 2020 02:19:03 -0700
Subject: [PATCH] [sledge] Change: Strengthen Sh.is_false by defining ito
 pure_approx

Reviewed By: jvillard

Differential Revision: D22571142

fbshipit-source-id: d9dd473da
---
 sledge/src/fol.ml  | 4 ++++
 sledge/src/fol.mli | 3 +++
 sledge/src/sh.ml   | 9 ++-------
 3 files changed, 9 insertions(+), 7 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 4abe6cb39..4f197f2d5 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -1215,6 +1215,10 @@ module Context = struct
   let is_true x = Ses.Equality.is_true x
   let is_false x = Ses.Equality.is_false x
   let implies x b = Ses.Equality.implies x (f_to_ses b)
+
+  let refutes x b =
+    Ses.Term.is_false (Ses.Equality.normalize x (f_to_ses b))
+
   let normalize x e = ses_map (Ses.Equality.normalize x) e
   let normalizef x e = f_ses_map (Ses.Equality.normalize x) e
   let difference x e f = Term.d_int (normalize x (Term.sub e f))
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 6dfb1701d..d52995637 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -225,6 +225,9 @@ module Context : sig
       only checks if [f] is valid in the current state of [x], without doing
       any further logical reasoning or propagation. *)
 
+  val refutes : t -> Formula.t -> bool
+  (** [refutes x f] holds only if [f] is inconsistent with [x]. *)
+
   val class_of : t -> Term.t -> Term.t list
   (** Equivalence class of [e]: all the terms [f] in the relation such that
       [e = f] is implied by the relation. *)
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 4b18e279b..674706281 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -583,13 +583,6 @@ let filter_heap ~f q =
 
 (** Query *)
 
-let is_false = function
-  | {djns= [[]]; _} -> true
-  | {ctx; pure; heap; _} ->
-      Formula.is_false (Context.normalizef ctx pure)
-      || 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
 
@@ -610,6 +603,8 @@ let pure_approx q =
   |>
   [%Trace.retn fun {pf} -> pf "%a" Formula.pp]
 
+let is_false q = Context.refutes q.ctx (pure_approx q)
+
 let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
   let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts =
     let ys, sjn = bind_exists sjn ~wrt:xs in