[sledge] Add Sh.subst implemented ito and and exists

Reviewed By: bennostein

Differential Revision: D17801943

fbshipit-source-id: 192863296

sledge/src/llair/term.ml

@@ -444,6 +444,9 @@ module Var = struct
           (sub, wrt) )
       |> fst |> check invariant
 
+    let fold sub ~init ~f =
+      Map.fold sub ~init ~f:(fun ~key ~data s -> f key data s)
+
     let invert sub =
       Map.fold sub ~init:empty ~f:(fun ~key ~data sub' ->
           Map.add_exn sub' ~key:data ~data:key )

sledge/src/llair/term.mli

@@ -127,6 +127,7 @@ module Var : sig
     val domain : t -> Set.t
     val range : t -> Set.t
     val apply_set : t -> Set.t -> Set.t
+    val fold : t -> init:'a -> f:(var -> var -> 'a -> 'a) -> 'a
   end
 end
 

sledge/src/symbheap/sh.ml

@@ -403,6 +403,22 @@ let rec pure (e : Term.t) =
 
 let and_ e q = star (pure e) q
 
+let subst sub q =
+  [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
+  ;
+  let dom, eqs =
+    Var.Subst.fold sub ~init:(Var.Set.empty, Term.true_)
+      ~f:(fun var trm (dom, eqs) ->
+        ( Set.add dom var
+        , Term.and_ (Term.eq (Term.var var) (Term.var trm)) eqs ) )
+  in
+  exists dom (and_ eqs q)
+  |>
+  [%Trace.retn fun {pf} q' ->
+    pf "%a" pp q' ;
+    invariant q' ;
+    assert (Set.disjoint q'.us (Var.Subst.domain sub))]
+
 let seg pt =
   let us = fv_seg pt in
   if Term.equal Term.null pt.loc then false_ us

sledge/src/symbheap/sh.mli

@@ -92,6 +92,10 @@ val rename : Var.Subst.t -> t -> t
 (** Apply a substitution, remove its domain from vocabulary and add its
     range. *)
 
+val subst : Var.Subst.t -> t -> t
+(** Apply a substitution, remove its domain from vocabulary and add its
+    range. *)
+
 val freshen : wrt:Var.Set.t -> t -> t * Var.Subst.t
 (** Freshen free variables with respect to [wrt], and extend vocabulary with
     [wrt], renaming bound variables as needed. *)