[sledge] Revise quantifier elimination of disjunctive formulas

Summary:
The overall operation of the quantifier elimination algorithm in
Sh.simplify is to first descend through the disjunctive structure of a
symbolic heap formula, process the leaves, and then proceed back up
the formula. At each point on the way back up, the first-order solver
is used to compute a solution substitution representing witnesses of
existential variables. This substitution is then used to normalize the
entire subformula at that point. Note that this results in
substituting and normalizing each subformula a number of times
proportional to its depth in the disjunctive structure.

This diff removes this redundancy and substitutes through each
subformula once. This is done by changing from an overall bottom-up to
top-down algorithm, and involves composing solution substitutions
rather than substituting multiple times. This change also heavily
relies on the strengthened Context.apply_and_elim operation, where the
bottom-up many-substitutions approach relies on the internal details
of repeated substitutions.

Reviewed By: jvillard

Differential Revision: D25756549

fbshipit-source-id: ca7cd814a

sledge/src/fol/context.ml

@@ -721,6 +721,9 @@ let fold_uses_of r t s ~f =
   Subst.fold r.rep s ~f:(fun ~key:trm ~data:rep s ->
       fold_ ~f trm (fold_ ~f rep s) )
 
+let iter_uses_of t r ~f = fold_uses_of r t () ~f:(fun use () -> f use)
+let uses_of t r = Iter.from_labelled_iter (iter_uses_of t r)
+
 let apply_subst wrt s r =
   [%Trace.call fun {pf} -> pf "%a@ %a" Subst.pp s pp r]
   ;
@@ -1179,60 +1182,27 @@ let solve_for_vars vss r =
               else `Continue us_xs )
             ~finish:(fun _ -> false) ) )]
 
-(* [elim] removes variables from a context by rearranging the existing
-   equality classes. Non-representative terms that contain a variable to
-   eliminate can be simply dropped. If a representative needs to be removed,
-   a new representative is chosen. This basic approach is insufficient if
-   interpreted terms are to be removed. For example, eliminating x from x +
-   1 = y = z ∧ w = x by just preserving the existing classes between terms
-   that do not mention x would yield y = z. This would lose provability of
-   the equality w = y - 1. So variables with interpreted uses are not
-   eliminated. *)
-let elim xs r =
+let trivial vs r =
   [%trace]
-    ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs xs pp_raw r)
-    ~retn:(fun {pf} (ks, r') ->
-      pf "%a@ %a" Var.Set.pp_xs ks pp_raw r' ;
-      assert (Var.Set.subset ks ~of_:xs) ;
+    ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs vs pp_raw r)
+    ~retn:(fun {pf} ks -> pf "%a" Var.Set.pp_xs ks)
+  @@ fun () ->
+  Var.Set.fold vs Var.Set.empty ~f:(fun v ks ->
+      let x = Trm.var v in
+      match Subst.find x r.rep with
+      | None -> Var.Set.add v ks
+      | Some x' when Trm.equal x x' && Iter.is_empty (uses_of x r) ->
+          Var.Set.add v ks
+      | _ -> ks )
+
+let trim ks r =
+  [%trace]
+    ~call:(fun {pf} -> pf "%a@ %a" Var.Set.pp_xs ks pp_raw r)
+    ~retn:(fun {pf} r' ->
+      pf "%a" pp_raw r' ;
       assert (Var.Set.disjoint ks (fv r')) )
   @@ fun () ->
-  (* add the uninterpreted uses of terms in delta to approx, and the
-     interpreted uses to interp *)
-  let rec add_uninterp_uses approx interp delta =
-    if not (Trm.Set.is_empty delta) then
-      let approx = Trm.Set.union approx delta in
-      let delta, interp =
-        Trm.Set.fold delta
-          (Trm.Set.empty, Trm.Set.empty)
-          ~f:
-            (fold_uses_of r ~f:(fun use (delta, interp) ->
-                 if is_interpreted use then (delta, Trm.Set.add use interp)
-                 else (Trm.Set.add use delta, interp) ))
-      in
-      add_uninterp_uses approx interp delta
-    else
-      (* remove the subterms of interpreted uses from approx *)
-      let rec remove_subtrms misses approx =
-        if not (Trm.Set.is_empty misses) then
-          let approx = Trm.Set.diff approx misses in
-          let misses =
-            Trm.Set.of_iter
-              (Iter.flat_map ~f:Trm.trms (Trm.Set.to_iter misses))
-          in
-          remove_subtrms misses approx
-        else approx
-      in
-      remove_subtrms interp approx
-  in
-  (* compute terms in relation mentioning vars to eliminate *)
-  let kills =
-    add_uninterp_uses Trm.Set.empty Trm.Set.empty
-      (Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter xs)))
-  in
-  let ks =
-    Trm.Set.fold kills Var.Set.empty ~f:(fun kill ks ->
-        match Var.of_trm kill with Some k -> Var.Set.add k ks | None -> ks )
-  in
+  let kills = Trm.Set.of_iter (Iter.map ~f:Trm.var (Var.Set.to_iter ks)) in
   (* compute classes including reps *)
   let reps =
     Subst.fold r.rep Trm.Set.empty ~f:(fun ~key:_ ~data:rep reps ->
@@ -1268,7 +1238,7 @@ let elim xs r =
                   Subst.add ~key:elt ~data:rep' s )
           | None -> s )
   in
-  (ks, {r with rep})
+  {r with rep}
 
 let apply_and_elim ~wrt xs s r =
   [%trace]
@@ -1283,7 +1253,8 @@ let apply_and_elim ~wrt xs s r =
     let zs, r = apply_subst wrt s r in
     if is_unsat r then (Var.Set.empty, unsat, Var.Set.empty)
     else
-      let ks, r = elim xs r in
+      let ks = trivial xs r in
+      let r = trim ks r in
       (zs, r, ks)
 
 (*

sledge/src/fol/context.mli

@@ -85,6 +85,8 @@ module Subst : sig
   type t
 
   val pp : t pp
+  val empty : t
+  val compose : t -> t -> t
   val is_empty : t -> bool
   val fold_eqs : t -> 's -> f:(Formula.t -> 's -> 's) -> 's
 

sledge/src/sh.ml

@@ -767,42 +767,56 @@ let remove_absent_xs ks q =
     in
     {q with xs; djns}
 
-let rec simplify_ us rev_xss q =
-  [%Trace.call fun {pf} -> pf "%a@ %a" pp_vss (List.rev rev_xss) pp_raw q]
+let rec simplify_ us rev_xss ancestor_subst q =
+  [%Trace.call fun {pf} ->
+    pf "%a@ %a@ %a" pp_vss (List.rev rev_xss) Context.Subst.pp
+      ancestor_subst pp_raw q]
   ;
+  assert (not (is_false q)) ;
+  let q0 = q 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 =
-    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 xss = List.rev rev_xss in
-  let subst = Context.solve_for_vars (us :: xss) q.ctx in
-  let union_xss = Var.Set.union_list rev_xss in
-  let wrt = Var.Set.union us union_xss in
-  let fresh, ctx, removed =
-    Context.apply_and_elim ~wrt union_xss subst q.ctx
-  in
-  ( if Context.is_unsat ctx then false_ q.us
-  else if Context.Subst.is_empty subst then exists xs q
+  let stem_subst = Context.solve_for_vars (us :: List.rev rev_xss) q.ctx in
+  let subst = Context.Subst.compose ancestor_subst stem_subst in
+  ( if Context.Subst.is_empty subst then q0
   else
-    (* normalize wrt solutions *)
-    let q = extend_us fresh q in
-    (* opt: ctx already normalized wrt subst, so just preserve it *)
-    let q = {(norm subst {q with ctx= Context.empty}) with ctx} in
+    (* normalize context wrt solutions *)
+    let union_xss = Var.Set.union_list rev_xss in
+    let wrt = Var.Set.union us union_xss in
+    let fresh, ctx, removed =
+      Context.apply_and_elim ~wrt union_xss subst q.ctx
+    in
+    let q = {(extend_us fresh q) with ctx} in
+    (* normalize stem wrt both ancestor and current solutions *)
+    let stem =
+      (* opt: ctx already normalized so just preserve it *)
+      {(norm subst {q with djns= emp.djns; ctx= emp.ctx}) with ctx= q.ctx}
+    in
+    (* recursively simplify subformulas *)
+    let q =
+      starN
+        ( stem
+        :: List.map q.djns ~f:(fun djn ->
+               orN (List.map ~f:(simplify_ us rev_xss subst) djn) ) )
+    in
     if is_false q then false_ q.us
     else
-      (* opt: removed already disjoint from ctx, so ignore it *)
       let removed =
-        Var.Set.diff removed (fv ~ignore_ctx:() (elim_exists q.xs q))
+        if Var.Set.is_empty removed then Var.Set.empty
+        else (
+          (* opt: removed already disjoint from ctx, so ignore_ctx *)
+          assert (Var.Set.disjoint removed (Context.fv q.ctx)) ;
+          Var.Set.diff removed (fv ~ignore_ctx:() (elim_exists q.xs q)) )
+      in
+      (* removed may not contain all variables stem_subst has solutions for,
+         so the equations in [∃ removed. stem_subst] that are not
+         universally valid need to be re-conjoined since they have alredy
+         been normalized out *)
+      let keep, removed, _ =
+        Context.Subst.partition_valid removed stem_subst
       in
-      let keep, removed, _ = Context.Subst.partition_valid removed subst in
       let q = and_subst keep q in
       (* (re)quantify existentials *)
       let q = exists (Var.Set.union fresh xs) q in
@@ -810,7 +824,7 @@ let rec simplify_ us rev_xss q =
       remove_absent_xs removed q )
   |>
   [%Trace.retn fun {pf} q' ->
-    pf "%a@ %a" Context.Subst.pp subst pp_raw q' ;
+    pf "%a@ %a" Context.Subst.pp stem_subst pp_raw q' ;
     invariant q']
 
 let simplify q =
@@ -822,7 +836,7 @@ let simplify q =
     let q = propagate_context Var.Set.empty Context.empty q in
     if is_false q then false_ q.us
     else
-      let q = simplify_ q.us [] q in
+      let q = simplify_ q.us [] Context.Subst.empty q in
       q )
   |>
   [%Trace.retn fun {pf} q' ->