From e6ccd3e497d6cf2c3e0bdb1dd5c75769f2bd7d21 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 10 Mar 2020 02:21:14 -0700
Subject: [PATCH] [sledge] Minor tracing improvements

Reviewed By: jvillard

Differential Revision: D20303062

fbshipit-source-id: afbb621e9
---
 sledge/src/symbheap/sh.ml     | 13 +++++++++----
 sledge/src/symbheap/sh.mli    |  2 +-
 sledge/src/symbheap/solver.ml |  4 +++-
 3 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml
index f6784b7b5..251928e06 100644
--- a/sledge/src/symbheap/sh.ml
+++ b/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
diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli
index 4b104c3f6..386cb72ee 100644
--- a/sledge/src/symbheap/sh.mli
+++ b/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
 
diff --git a/sledge/src/symbheap/solver.ml b/sledge/src/symbheap/solver.ml
index 8d32039aa..337f89290 100644
--- a/sledge/src/symbheap/solver.ml
+++ b/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]