[sledge] Simplify the printed symbolic heaps

Summary:
Currently printing symbolic heaps is unreadable, because there are too
many quantified variables, that are mostly just equal to other
variables.

This diff tries to replace all variables in an equivalence class with a
single variable and remove the unneccesary variables.

It also introduces two modes for printing state domains:
`-t +State_domain.pp_full` prints the state domain as is
`-t +State_domain.pp` uses the simplification before printing.

Reviewed By: jberdine

Differential Revision: D15738748

fbshipit-source-id: 7c85b580e

sledge/src/symbheap/sh.ml

@@ -159,6 +159,22 @@ let rec invariant q =
             invariant sjn ) )
   with exc -> [%Trace.info "%a" pp q] ; raise exc
 
+let rec simplify {us; xs; cong; pure; heap; djns} =
+  [%Trace.call fun {pf} -> pf "%a" pp {us; xs; cong; pure; heap; djns}]
+  ;
+  let heap = List.map heap ~f:(map_seg ~f:(Equality.normalize cong)) in
+  let pure = List.map pure ~f:(Equality.normalize cong) in
+  let cong = Equality.true_ in
+  let djns = List.map djns ~f:(List.map ~f:simplify) in
+  let all_vars =
+    fv {us= Set.union us xs; xs= Var.Set.empty; cong; pure; heap; djns}
+  in
+  let xs = Set.inter all_vars xs in
+  let us = Set.inter all_vars us in
+  {us; xs; cong; pure; heap; djns} |> check invariant
+  |>
+  [%Trace.retn fun {pf} s -> pf "%a" pp s]
+
 (** Quantification and Vocabulary *)
 
 let rename_seg sub ({loc; bas; len; siz; arr} as h) =

sledge/src/symbheap/sh.mli

@@ -30,6 +30,7 @@ val pp_seg_norm : Equality.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> Var.Set.t pp
 val pp : t pp
 val pp_djn : disjunction pp
+val simplify : t -> t
 
 include Invariant.S with type t := t
 

sledge/src/symbheap/sh_test.ml

@@ -89,4 +89,30 @@ let%test_module _ =
         ∨ (∃ %x_1, %x_3 .   1 = %y_2 = %x_3 ∧ emp)
         ∨ (∃ %x_1 .   0 = %x_1 ∧ emp)
         ) |}]
+
+    let%expect_test _ =
+      let q =
+        Sh.(
+          exists
+            ~$[x_]
+            (or_
+               (pure (x = !0))
+               (exists
+                  ~$[x_]
+                  (or_
+                     (and_ (x = !1) (pure (y = !1)))
+                     (exists ~$[x_] (pure (x = !2)))))))
+      in
+      pp q ;
+      pp (Sh.simplify q) ;
+      [%expect
+        {|
+        ∃ %x_1 .
+        emp
+        * ( (  0 = %x_1 ∧ emp)
+          ∨ (∃ %x_1 .emp
+             * ( (  1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 .  2 = %x_1 ∧ emp) ))
+          )
+
+        emp * ( (emp) ∨ (emp * ( (emp) ∨ (emp) )) ) |}]
   end )

sledge/src/symbheap/state_domain.ml

@@ -9,7 +9,13 @@
 
 type t = Sh.t [@@deriving equal, sexp_of]
 
-let pp = Sh.pp
+let pp_full fs s = [%Trace.fprintf fs "%a" Sh.pp s]
+let pp fs s = [%Trace.fprintf fs "%a" Sh.pp (Sh.simplify s)]
+let pp fs s = pp_full fs s ; pp fs s
+
+(* I think it would be nice if `-t State_domain.pp` enabled the simplified
+   printing, with `-t State_domain.pp_full` for the more verbose one. So how
+   about this renaming? *)
 
 let init globals =
   Vector.fold globals ~init:Sh.emp ~f:(fun q -> function