[sledge] Filter out trivial pure constraints in Sh.map

Summary:
The function transforming terms passed to Sh.map might produce trivial
constraints, filter them out.

Reviewed By: ngorogiannis

Differential Revision: D19286628

fbshipit-source-id: e3d9926ce

sledge/src/import/import.ml

@@ -137,6 +137,18 @@ let map_preserving_phys_equal map t ~f =
   in
   if !change then t' else t
 
+let filter_map_preserving_phys_equal filter_map t ~f =
+  let change = ref false in
+  let t' =
+    filter_map t ~f:(fun x ->
+        let x'_opt = f x in
+        ( match x'_opt with
+        | Some x' when x' == x -> ()
+        | _ -> change := true ) ;
+        x'_opt )
+  in
+  if !change then t' else t
+
 module type Applicative_syntax = sig
   type 'a t
 
@@ -205,6 +217,9 @@ module List = struct
       (fold xs ~init ~f:(fun acc elt ->
            match f acc elt with Some res -> res | None -> return None ))
 
+  let filter_map_preserving_phys_equal t ~f =
+    filter_map_preserving_phys_equal filter_map t ~f
+
   let map_preserving_phys_equal t ~f = map_preserving_phys_equal map t ~f
 
   let remove_exn ?(equal = phys_equal) xs x =

sledge/src/import/import.mli

@@ -172,6 +172,10 @@ module List : sig
   (** Like map, but preserves [phys_equal] if [f] preserves [phys_equal] of
       every element. *)
 
+  val filter_map_preserving_phys_equal : 'a t -> f:('a -> 'a option) -> 'a t
+  (** Like filter_map, but preserves [phys_equal] if [f] preserves
+      [phys_equal] of every element. *)
+
   val remove_exn : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list
   (** Returns the input list without the first element [equal] to the
       argument, or raise [Not_found] if no such element exists. [equal]

sledge/src/symbheap/sh.ml

@@ -42,7 +42,11 @@ let map_seg ~f h =
 let map ~f_sjn ~f_cong ~f_trm ({us= _; xs= _; cong; pure; heap; djns} as q)
     =
   let cong = f_cong cong in
-  let pure = List.map_preserving_phys_equal pure ~f:f_trm in
+  let pure =
+    List.filter_map_preserving_phys_equal pure ~f:(fun e ->
+        let e' = f_trm e in
+        if Term.is_true e' then None else Some e' )
+  in
   let heap = List.map_preserving_phys_equal heap ~f:(map_seg ~f:f_trm) in
   let djns =
     List.map_preserving_phys_equal djns