[sledge] Factor out Sh.and_subst

Reviewed By: ngorogiannis

Differential Revision: D20120278

fbshipit-source-id: 68c170828

sledge/src/symbheap/sh.ml

@@ -513,6 +513,15 @@ let rec pure (e : Term.t) =
 
 let and_ e q = star (pure e) q
 
+let and_subst subst q =
+  [%Trace.call fun {pf} -> pf "%a@ %a" Equality.Subst.pp subst pp q]
+  ;
+  Equality.Subst.fold
+    ~f:(fun ~key ~data -> and_ (Term.eq key data))
+    subst ~init:q
+  |>
+  [%Trace.retn fun {pf} q -> pf "%a" pp q ; invariant q]
+
 let subst sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
   ;

sledge/src/symbheap/sh.mli

@@ -63,6 +63,10 @@ val and_cong : Equality.t -> t -> t
 (** Conjoin constraints of a congruence to a formula, extending to a common
     vocabulary, and avoiding capturing existentials. *)
 
+val and_subst : Equality.Subst.t -> t -> t
+(** Conjoin constraints of a solution substitution to a formula, extending
+    to a common vocabulary, and avoiding capturing existentials. *)
+
 (** Update *)
 
 val with_pure : Term.t list -> t -> t

sledge/src/symbheap/solver.ml

@@ -72,11 +72,7 @@ let excise_exists goal =
                 Equality.Subst.pp witnesses ) ;
           let us = Set.union goal.us removed in
           let xs = Set.diff goal.xs removed in
-          let min =
+          let min = Sh.and_subst witnesses goal.min in
-            Equality.Subst.fold
-              ~f:(fun ~key ~data -> Sh.and_ (Term.eq key data))
-              witnesses ~init:goal.min
-          in
           {goal with us; min; xs; pgs= true} )
 
 (* ad hoc treatment to drop tautologous constraints such as ∃x,y. x = y