[sledge] Fix existential mishandling in Sh.simplify

Summary:
It was possible for the scope of existentials to be violated. In
particular, before this diff the order of re-quantifying the
existentials and conjoining the non-eliminated equations from the
solution of solving for existentials was wrong.

Reviewed By: ngorogiannis

Differential Revision: D24746231

fbshipit-source-id: d96cc60a6

sledge/src/sh.ml

@@ -741,34 +741,45 @@ let remove_absent_xs ks q =
 let rec simplify_ us rev_xss q =
   [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q]
   ;
-  let rev_xss = q.xs :: rev_xss in
+  (* bind existentials *)
+  let xs, q = bind_exists ~wrt:emp.us q in
+  let rev_xss = xs :: rev_xss in
   (* recursively simplify subformulas *)
   let q =
-    exists q.xs
-      (starN
-         ( {q with us= Var.Set.union q.us q.xs; xs= emp.xs; djns= []}
-         :: List.map q.djns ~f:(fun djn ->
-                orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) )
-         ))
+    starN
+      ( {q with djns= []}
+      :: List.map q.djns ~f:(fun djn ->
+             orN (List.map djn ~f:(fun sjn -> simplify_ us rev_xss sjn)) )
+      )
   in
   (* try to solve equations in ctx for variables in xss *)
   let subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
-  (* simplification can reveal inconsistency *)
-  ( if is_false q then false_ q.us
-  else if Context.Subst.is_empty subst then q
-  else
-    (* normalize wrt solutions *)
-    let q = norm subst q in
-    (* reconjoin only non-redundant equations *)
-    let removed =
-      Var.Set.diff
-        (Var.Set.union_list rev_xss)
-        (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
-    (* remove the eliminated variables from xs and subformulas' us *)
-    remove_absent_xs removed q )
+  let removed, q =
+    (* simplification can reveal inconsistency *)
+    if is_false q then (Var.Set.empty, false_ q.us)
+    else if Context.Subst.is_empty subst then (Var.Set.empty, 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)
+  in
+  (* re-quantify existentials *)
+  let q = exists xs q in
+  (* remove the eliminated variables from xs and subformulas' us *)
+  remove_absent_xs removed q
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a@ %a" Context.Subst.pp subst pp_raw q' ;