[sledge] Optimize variable renaming in symbolic heaps

Summary:
Add shortcut code paths to return early in some cases guaranteed to be
the identity function.

Reviewed By: ngorogiannis

Differential Revision: D15468704

fbshipit-source-id: f137049c6

sledge/src/llair/exp.ml

@@ -596,6 +596,9 @@ module Var = struct
     let exclude sub vs =
       Set.fold vs ~init:sub ~f:Map.remove |> check invariant
 
+    let restrict sub vs =
+      Map.filter_keys ~f:(Set.mem vs) sub |> check invariant
+
     let domain sub =
       Map.fold sub ~init:Set.empty ~f:(fun ~key ~data:_ domain ->
           Set.add domain key )

sledge/src/llair/exp.mli

@@ -121,6 +121,7 @@ module Var : sig
     val extend : t -> replace:var -> with_:var -> t
     val invert : t -> t
     val exclude : t -> Set.t -> t
+    val restrict : t -> Set.t -> t
     val is_empty : t -> bool
     val domain : t -> Set.t
     val range : t -> Set.t

sledge/src/symbheap/sh.ml

@@ -195,10 +195,13 @@ let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
 and rename sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
   ;
-  let sub = Var.Subst.exclude sub q.xs in
+  let sub = Var.Subst.restrict sub q.us in
-  let us = Var.Subst.apply_set sub q.us in
+  ( if Var.Subst.is_empty sub then q
-  let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Subst.range sub)) in
+  else
-  (if us == q.us && q' == q then q else {q' with us})
+    let us = Var.Subst.apply_set sub q.us in
+    assert (not (Set.equal us q.us)) ;
+    let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Subst.range sub)) in
+    {q' with us} )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
@@ -210,9 +213,11 @@ and freshen_xs q ~wrt =
   [%Trace.call fun {pf} -> pf "{@[%a@]}@ %a" Var.Set.pp wrt pp q]
   ;
   let sub = Var.Subst.freshen q.xs ~wrt in
-  let xs = Var.Subst.apply_set sub q.xs in
+  ( if Var.Subst.is_empty sub then q
-  let q' = apply_subst sub q in
+  else
-  (if xs == q.xs && q' == q then q else {q' with xs})
+    let xs = Var.Subst.apply_set sub q.xs in
+    let q' = apply_subst sub q in
+    if xs == q.xs && q' == q then q else {q' with xs} )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;