From df37767a93e503d08e335f13fc18c40de026aa10 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:25:29 -0800
Subject: [PATCH] [sledge] Detect unsat symbolic heaps earlier during
 simplification

Summary:
Simplifying a symbolic heap can reveal inconsistencies, either of
individual disjuncts or (therefore) of toplevel formulas. This is due
to the first-order contexts being propagated from a formula to its
descendents, and for the intersection of the contexts of disjunctions
being propagated to their parent. The later stages of eliminating
redundant quantifiers, etc. do not reveal further
inconsistencies. Therefore this diff moves the inconsistency detection
earlier, to just after the contexts are strengthened. This is clearer,
and also a minor optimization.

Reviewed By: jvillard

Differential Revision: D25756564

fbshipit-source-id: d3acf875b
---
 sledge/src/sh.ml | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index b208705cc..df8d4459b 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -703,20 +703,25 @@ let rec propagate_context_ ancestor_vs ancestor_ctx q =
   (* strengthen context with that from above *)
   let ancestor_stem = and_ctx_ ancestor_ctx stem in
   let ancestor_ctx = ancestor_stem.ctx in
-  exists xs
-    (List.fold djns ancestor_stem ~f:(fun djn q' ->
-         let dj_ctxs, djn =
-           List.rev_map_split djn ~f:(fun dj ->
-               let dj = propagate_context_ ancestor_vs ancestor_ctx dj in
-               (dj.ctx, dj) )
-         in
-         let new_xs, djn_ctx = Context.interN ancestor_vs dj_ctxs in
-         (* hoist xs appearing in disjunction's context *)
-         let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in
-         let djn = List.map ~f:(elim_exists djn_xs) djn in
-         let ctx_djn = and_ctx_ djn_ctx (orN djn) in
-         assert (is_unsat ctx_djn || Var.Set.subset new_xs ~of_:djn_xs) ;
-         star (exists djn_xs ctx_djn) q' ))
+  let q' =
+    List.fold djns ancestor_stem ~f:(fun djn q' ->
+        let dj_ctxs, djn =
+          List.rev_map_split djn ~f:(fun dj ->
+              let dj = propagate_context_ ancestor_vs ancestor_ctx dj in
+              (dj.ctx, dj) )
+        in
+        let new_xs, djn_ctx = Context.interN ancestor_vs dj_ctxs in
+        (* hoist xs appearing in disjunction's context *)
+        let djn_xs = Var.Set.diff (Context.fv djn_ctx) q'.us in
+        let djn = List.map ~f:(elim_exists djn_xs) djn in
+        let ctx_djn = and_ctx_ djn_ctx (orN djn) in
+        assert (is_false ctx_djn || Var.Set.subset new_xs ~of_:djn_xs) ;
+        star (exists djn_xs ctx_djn) q' )
+  in
+  (* requantify existentials *)
+  let q' = exists xs q' in
+  (* strengthening contexts can reveal inconsistency *)
+  (if is_false q' then false_ q'.us else q')
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
@@ -776,9 +781,7 @@ let rec simplify_ us rev_xss q =
   (* try to solve equations in ctx for variables in xss *)
   let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
   let removed, q =
-    (* simplification can reveal inconsistency *)
-    if is_unsat q then (Var.Set.empty, false_ q.us)
-    else if Context.Subst.is_empty subst then (Var.Set.empty, q)
+    if Context.Subst.is_empty subst then (Var.Set.empty, q)
     else
       (* normalize wrt solutions *)
       let q = norm subst q in