[sledge] Minor tracing improvements

Reviewed By: jvillard

Differential Revision: D20303062

fbshipit-source-id: afbb621e9

sledge/src/symbheap/sh.ml

@@ -122,7 +122,13 @@ let rec var_strength_ xs m q =
   in
   (m_stem, m)
 
-let var_strength_full q = var_strength_ Var.Set.empty Var.Map.empty q
+let var_strength_full ?(xs = Var.Set.empty) q =
+  let m =
+    Set.fold xs ~init:Var.Map.empty ~f:(fun m x ->
+        Map.set m ~key:x ~data:`Existential )
+  in
+  var_strength_ xs m q
+
 let var_strength q = snd (var_strength_full q)
 let pp_memory x fs (siz, arr) = Term.ppx x fs (Term.memory ~siz ~arr)
 
@@ -263,9 +269,8 @@ and pp_djn ?var_strength vs xs cong fs = function
                sjn ))
         djn
 
-let pp_diff_eq cong fs q =
-  pp_ ~var_strength:(var_strength_full q) Var.Set.empty Var.Set.empty cong
-    fs q
+let pp_diff_eq ?(us = Var.Set.empty) ?(xs = Var.Set.empty) cong fs q =
+  pp_ ~var_strength:(var_strength_full ~xs q) us xs cong fs q
 
 let pp fs q = pp_diff_eq Equality.true_ fs q
 let pp_djn fs d = pp_djn Var.Set.empty Var.Set.empty Equality.true_ fs d

sledge/src/symbheap/sh.mli

@@ -29,7 +29,7 @@ val pp_seg_norm : Equality.t -> seg pp
 val pp_us : ?pre:('a, 'a) fmt -> ?vs:Var.Set.t -> unit -> Var.Set.t pp
 val pp : t pp
 val pp_raw : t pp
-val pp_diff_eq : Equality.t -> t pp
+val pp_diff_eq : ?us:Var.Set.t -> ?xs:Var.Set.t -> Equality.t -> t pp
 val pp_djn : disjunction pp
 val simplify : t -> t
 

sledge/src/symbheap/solver.ml

@@ -68,7 +68,9 @@ end = struct
   let pp fs {com; min; xs; sub; pgs} =
     Format.fprintf fs "@[<hv>%s %a@ | %a@ @[\\- %a%a@]@]"
       (if pgs then "t" else "f")
-      Sh.pp com Sh.pp min Var.Set.pp_xs xs (Sh.pp_diff_eq min.cong) sub
+      Sh.pp com Sh.pp min Var.Set.pp_xs xs
+      (Sh.pp_diff_eq ~us:(Set.union min.us sub.us) ~xs min.cong)
+      sub
 
   let invariant g =
     Invariant.invariant [%here] g [%sexp_of: t]