[sledge] Change Term.rename to preserve sharing in cyclic records

Reviewed By: bennostein

Differential Revision: D17665265

fbshipit-source-id: 50844096a

sledge/src/import/import.ml

@@ -29,6 +29,7 @@ include (
 
 (* undeprecate *)
 external ( == ) : 'a -> 'a -> bool = "%eq"
+external ( != ) : 'a -> 'a -> bool = "%noteq"
 
 include Stdio
 module Command = Core.Command

sledge/src/import/import.mli

@@ -30,6 +30,7 @@ include module type of (
 (* undeprecate *)
 
 external ( == ) : 'a -> 'a -> bool = "%eq"
+external ( != ) : 'a -> 'a -> bool = "%noteq"
 
 include module type of Stdio
 module Command = Core.Command

sledge/src/import/vector.ml

@@ -70,12 +70,14 @@ let map_preserving_phys_equal xs ~f =
 
 let mapi x ~f = v (Array.mapi (a x) ~f)
 let map2_exn x y ~f = v (Array.map2_exn (a x) (a y) ~f)
+let map_inplace x ~f = Array.map_inplace (a x) ~f
 
 let fold_map x ~init ~f =
   let s, x = Array.fold_map (a x) ~init ~f in
   (s, v x)
 
 let concat xs = v (Array.concat (al xs))
+let copy x = v (Array.copy (a x))
 let of_array = v
 let of_list x = v (Array.of_list x)
 let of_list_rev x = v (Array.of_list_rev x)

sledge/src/import/vector.mli

@@ -86,8 +86,8 @@ val init : int -> f:(int -> 'a) -> 'a t
 (* val append : 'a t -> 'a t -> 'a t *)
 
 val concat : 'a t list -> 'a t
+val copy : 'a t -> 'a t
 
-(* val copy : 'a t -> 'a t *)
 (* val sub : ('a t, 'a t) Base__Blit_intf.sub *)
 (* val subo : ('a t, 'a t) Base__Blit_intf.subo *)
 
@@ -153,6 +153,7 @@ val of_list_rev : 'a list -> 'a t
 (* val of_list_map : 'a list -> f:('a -> 'b) -> 'b t *)
 (* val of_list_rev_map : 'a list -> f:('a -> 'b) -> 'b t *)
 
+val map_inplace : 'a t -> f:('a -> 'a) -> unit
 val find_exn : 'a t -> f:('a -> bool) -> 'a
 
 (* val find_map_exn : 'a t -> f:('a -> 'b option) -> 'b *)

sledge/src/symbheap/term.ml

@@ -1046,8 +1046,6 @@ let of_exp e =
 (** Transform *)
 
 let map e ~f =
-  let map_ : (t -> t) -> t -> t =
-   fun map_ e ->
   let map1 op ~f x =
     let x' = f x in
     if x' == x then e else norm1 op x'
@@ -1063,9 +1061,9 @@ let map e ~f =
     let z' = f z in
     if x' == x && y' == y && z' == z then e else norm3 op x' y' z'
   in
-    let mapN op ~f xs =
+  let mapN mk ~f xs =
     let xs' = Vector.map_preserving_phys_equal ~f xs in
-      if xs' == xs then e else normN op xs'
+    if xs' == xs then e else mk xs'
   in
   let map_qset mk ~f args =
     let args' = Qset.map ~f:(fun arg q -> (f arg, q)) args in
@@ -1077,19 +1075,47 @@ let map e ~f =
   | Ap1 (op, x) -> map1 op ~f x
   | Ap2 (op, x, y) -> map2 op ~f x y
   | Ap3 (op, x, y, z) -> map3 op ~f x y z
-    | ApN (op, xs) -> mapN op ~f xs
-    | RecN (op, xs) -> RecN (op, Vector.map ~f:map_ xs)
+  | ApN (op, xs) -> mapN (normN op) ~f xs
+  | RecN (_, xs) ->
+      assert (
+        xs == Vector.map_preserving_phys_equal ~f xs
+        || fail "Term.map does not support updating subterms of RecN." ) ;
+      e
   | _ -> e
-  in
-  fix map_ (fun e -> e) e
 
-let rename sub e =
-  let rec rename_ sub e =
+(** Pre-order transformation that preserves cycles. Each subterm [x] from
+    root to leaves is presented to [f]. If [f x = Some x'] then the subterms
+    of [x] are not traversed and [x] is transformed to [x']. Otherwise
+    traversal proceeds to the subterms of [x], followed by rebuilding the
+    term structure on the transformed subterms. Cycles (through terms
+    involving [RecN]) are preserved. *)
+let map_rec_pre ~f e =
+  let rec map_rec_pre_f memo e =
+    match f e with
+    | Some e' -> e'
+    | None -> (
       match e with
-    | Var _ -> Var.Subst.apply sub e
-    | _ -> map ~f:(rename_ sub) e
+      | RecN (op, xs) -> (
+        match List.Assoc.find ~equal:( == ) memo e with
+        | None ->
+            let xs' = Vector.copy xs in
+            let e' = RecN (op, xs') in
+            let memo = List.Assoc.add ~equal:( == ) memo e e' in
+            let changed = ref false in
+            Vector.map_inplace xs' ~f:(fun x ->
+                let x' = map_rec_pre_f memo x in
+                if x' != x then changed := true ;
+                x' ) ;
+            if !changed then e' else e
+        | Some e' -> e' )
+      | _ -> map ~f:(map_rec_pre_f memo) e )
   in
-  rename_ sub e |> check invariant
+  map_rec_pre_f [] e
+
+let rename sub e =
+  map_rec_pre e ~f:(function
+    | Var _ as v -> Some (Var.Subst.apply sub v)
+    | _ -> None )
 
 (** Query *)