[sledge] Strengthen Solver's treatment of existentials using Equality

Summary:
Equality.solve_for_var_contexts can produce solution substitutions
that witness existentials in more cases than the
single-existential-occurrence heuristic, and is more conservative in
cases where the latter is incomplete.

Reviewed By: ngorogiannis

Differential Revision: D19282634

fbshipit-source-id: f86f0a9cb

sledge/src/symbheap/equality.mli

@@ -66,6 +66,12 @@ val fold_terms : t -> init:'a -> f:('a -> Term.t -> 'a) -> 'a
 (** Solution Substitutions *)
 module Subst : sig
   type t [@@deriving compare, equal, sexp]
+
+  val pp : t pp
+  val is_empty : t -> bool
+  val fold : t -> init:'a -> f:(key:Term.t -> data:Term.t -> 'a -> 'a) -> 'a
+  val norm : t -> Term.t -> Term.t
+  val trim : bound:Var.Set.t -> Var.Set.t -> t -> t
 end
 
 val solve_for_vars : Var.Set.t list -> t -> Subst.t

sledge/src/symbheap/sh.ml

@@ -576,3 +576,12 @@ let dnf q =
   fold_dnf ~conj ~disj q (Var.Set.empty, []) []
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp_djn]
+
+(** Simplify *)
+
+let rec norm s q =
+  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Equality.Subst.pp s pp q]
+  ;
+  map q ~f_sjn:(norm s) ~f_cong:Fn.id ~f_trm:(Equality.Subst.norm s)
+  |>
+  [%Trace.retn fun {pf} q' -> pf "%a" pp q' ; invariant q']

sledge/src/symbheap/sh.mli

@@ -79,6 +79,10 @@ val rem_seg : seg -> t -> t
 val filter_heap : f:(seg -> bool) -> t -> t
 (** [filter_heap q f] Remove all segments in [q] for which [f] returns false *)
 
+val norm : Equality.Subst.t -> t -> t
+(** [norm s q] is [q] where subterms have been normalized with a
+    substitution. *)
+
 (** Quantification and Vocabulary *)
 
 val exists : Var.Set.t -> t -> t

sledge/src/symbheap/solver.ml

@@ -44,40 +44,48 @@ let fresh_var name vs zs ~wrt =
 let excise k = [%Trace.infok k]
 let trace k = [%Trace.infok k]
 
-type occurrences = Zero | One of Var.t | Many
-
-let single_existential_occurrence xs term =
-  let exception Multiple_existential_occurrences in
-  try
-    Term.fold_vars term ~init:Zero ~f:(fun seen var ->
-        if not (Set.mem xs var) then seen
-        else
-          match seen with
-          | Zero -> One var
-          | _ -> raise Multiple_existential_occurrences )
-  with Multiple_existential_occurrences -> Many
+let excise_exists goal =
+  trace (fun {pf} -> pf "@[<2>excise_exists@ %a@]" pp goal) ;
+  if Set.is_empty goal.xs then goal
+  else
+    let solutions_for_xs =
+      Equality.solve_for_vars [goal.us; goal.xs] goal.sub.cong
+    in
+    if Equality.Subst.is_empty solutions_for_xs then goal
+    else
+      let sub = Sh.norm solutions_for_xs goal.sub in
+      let removed, survived = Set.diff_inter goal.xs (Sh.fv sub) in
+      if Set.is_empty removed then goal
+      else
+        let witnesses =
+          Equality.Subst.trim ~bound:goal.xs survived solutions_for_xs
+        in
+        if Equality.Subst.is_empty witnesses then goal
+        else (
+          excise (fun {pf} ->
+              pf "@[<2>excise_exists @[%a%a@]@]" Var.Set.pp_xs removed
+                Equality.Subst.pp witnesses ) ;
+          let us = Set.union goal.us removed in
+          let xs = survived in
+          let min =
+            Equality.Subst.fold
+              ~f:(fun ~key ~data -> Sh.and_ (Term.eq key data))
+              witnesses ~init:goal.min
+          in
+          {goal with us; min; xs; sub; pgs= true} )
 
 let special_cases xs = function
   | Term.Ap2 (Eq, Var _, Var _) as e ->
       if Set.is_subset (Term.fv e) ~of_:xs then Term.true_ else e
   | e -> e
 
-let excise_term ({us; min; xs} as goal) pure term =
+let excise_term ({min; xs} as goal) pure term =
   let term' = Equality.normalize min.cong term in
   let term' = special_cases xs term' in
-  if Term.is_true term' then Some ({goal with pgs= true}, pure)
-  else
-    match single_existential_occurrence xs term' with
-    | Zero -> None
-    | One x ->
-        Some
-          ( { goal with
-              us= Set.add us x
-            ; min= Sh.and_ term' min
-            ; xs= Set.remove xs x
-            ; pgs= true }
-          , pure )
-    | Many -> Some (goal, term' :: pure)
+  if Term.is_true term' then (
+    excise (fun {pf} -> pf "excise_pure %a" Term.pp term) ;
+    Some ({goal with pgs= true}, pure) )
+  else Some (goal, term' :: pure)
 
 let excise_pure ({sub} as goal) =
   trace (fun {pf} -> pf "@[<2>excise_pure@ %a@]" pp goal) ;
@@ -546,7 +554,8 @@ let rec excise ({min; xs; sub; zs; pgs} as goal) =
   else if Sh.is_emp sub then Some (Sh.exists zs (Sh.extend_us xs min))
   else if Sh.is_false sub then None
   else if pgs then
-    {goal with pgs= false} |> excise_pure >>= excise_heap >>= excise
+    {goal with pgs= false} |> excise_exists |> excise_pure >>= excise_heap
+    >>= excise
   else None $> fun _ -> [%Trace.info "@[<2>excise fail@ %a@]" pp goal]
 
 let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =

sledge/src/symbheap/solver_test.ml

@@ -267,5 +267,9 @@ let%test_module _ =
           * %l_6 -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩
           \- ∃ %a_1, %m_8 .
               %l_6 -[ %l_6, %m_8 )-> ⟨%m_8,%a_1⟩
-        ) infer_frame: |}]
+        ) infer_frame:
+            %a_1 = %a_2
+          ∧ 2 = %n_9
+          ∧ 16 = %m_8
+          ∧ (%l_6 + 16) -[ %l_6, 16 )-> ⟨0,%a_3⟩ |}]
   end )