From 5c07232ea3cc46e9ad4024f8b3556aecc1b70f7a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 8 Feb 2021 13:11:13 -0800
Subject: [PATCH] [sledge] Fix handling of existentials in Sh.and_
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
`Sh.and_ b q` normalizes `b` using the equality context of `q` and
then conjoins the result to `q`. This is incorrect in case normalizing
`b` results in expressing it using existentials of `q`, which takes
the existentials out of their scope. So this diff changes from
essentially

    `(∃x.Q) ∧ B = (∃x.Q) ∧ (∃x.Bρ)`
to
    `(∃x.Q) ∧ B = (∃x'.Q[x'/x] ∧ Bρ)`

where `ρ` is the substitution that normalizes with respect to the
equality context.

Reviewed By: jvillard

Differential Revision: D26250536

fbshipit-source-id: 05f5c48c0
---
 sledge/src/sh.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index fa646b481..c18cbece7 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -555,7 +555,13 @@ let pure (p : Formula.t) =
     invariant q]
 
 let and_ b q =
-  star (pure (Formula.map_terms ~f:(Context.normalize q.ctx) b)) q
+  [%trace]
+    ~call:(fun {pf} -> pf "@ (%a)@ (%a)" Formula.pp b pp q)
+    ~retn:(fun {pf} -> pf "%a" pp)
+  @@ fun () ->
+  let xs, q = bind_exists q ~wrt:(Formula.fv b) in
+  let b = Formula.map_terms ~f:(Context.normalize q.ctx) b in
+  exists xs (star (pure b) q)
 
 let and_subst subst q =
   [%Trace.call fun {pf} -> pf "@ %a@ %a" Context.Subst.pp subst pp q]