From d574b14dc79ec90200d2d265173492ffef290922 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:26:15 -0800
Subject: [PATCH] [sledge] Improve Sh.simplify using stronger Context.elim

Summary:
The implementation of quantifier elimination in Sh.simplify currently
relies on a subtle implementation detail of Context.apply_subst to
remove some identity mappings. Now that Context.elim has been
strengthened and generalized, it can be used to to give a much clearer
implementation, that is also more robust to representation changes in
Context.

Reviewed By: jvillard

Differential Revision: D25756554

fbshipit-source-id: 6be0de2f3
---
 sledge/src/sh.ml | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 8e156e2d7..a9256b372 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -794,20 +794,20 @@ let rec simplify_ us rev_xss q =
     else
       (* normalize wrt solutions *)
       let q = norm subst q in
-      (* reconjoin only non-redundant equations *)
-      let _, ctx =
-        Context.apply_subst
-          (Var.Set.union us (Var.Set.union_list rev_xss))
-          subst q.ctx
-      in
-      let removed =
-        Var.Set.diff
-          (Var.Set.union_list rev_xss)
-          (Var.Set.union (Context.fv ctx)
-             (fv ~ignore_ctx:() (elim_exists q.xs q)))
-      in
-      let keep, removed, _ = Context.Subst.partition_valid removed subst in
-      (removed, and_subst keep {q with ctx})
+      if is_false q then (Var.Set.empty, false_ q.us)
+      else
+        let removed, ctx =
+          Context.elim (Var.Set.union_list rev_xss) q.ctx
+        in
+        let q = {q with ctx} in
+        let removed =
+          Var.Set.diff removed (fv ~ignore_ctx:() (elim_exists q.xs q))
+        in
+        let keep, removed, _ =
+          Context.Subst.partition_valid removed subst
+        in
+        let q = and_subst keep q in
+        (removed, q)
   in
   (* re-quantify existentials *)
   let q = exists xs q in