[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

@@ -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 *)
+      if is_false q then (Var.Set.empty, false_ q.us)
-      let _, ctx =
+      else
-        Context.apply_subst
+        let removed, ctx =
-          (Var.Set.union us (Var.Set.union_list rev_xss))
+          Context.elim (Var.Set.union_list rev_xss) q.ctx
-          subst q.ctx
+        in
-      in
+        let q = {q with ctx} in
-      let removed =
+        let removed =
-        Var.Set.diff
+          Var.Set.diff removed (fv ~ignore_ctx:() (elim_exists q.xs q))
-          (Var.Set.union_list rev_xss)
+        in
-          (Var.Set.union (Context.fv ctx)
+        let keep, removed, _ =
-             (fv ~ignore_ctx:() (elim_exists q.xs q)))
+          Context.Subst.partition_valid removed subst
-      in
+        in
-      let keep, removed, _ = Context.Subst.partition_valid removed subst in
+        let q = and_subst keep q in
-      (removed, and_subst keep {q with ctx})
+        (removed, q)
   in
   (* re-quantify existentials *)
   let q = exists xs q in