From 01825598f7439ad9f3acc79fd66e5e37cc75e3db Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 8 Jan 2020 08:03:35 -0800 Subject: [PATCH] [sledge] Equality.and_eq is part of the exposed interface Summary: So trace it and check invariant on return. Reviewed By: ngorogiannis Differential Revision: D19221878 fbshipit-source-id: ce05da740 --- sledge/src/symbheap/equality.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml index b1e34fcb2..ad540b638 100644 --- a/sledge/src/symbheap/equality.ml +++ b/sledge/src/symbheap/equality.ml @@ -200,16 +200,22 @@ let close r = pf "%a" pp_diff (r, r') ; invariant r'] +(** Exposed interface *) + let and_eq a b r = - if not r.sat then r + [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp a Term.pp b pp r] + ; + ( if not r.sat then r else let a' = canon r a in let b' = canon r b in let r = extend a' r in let r = extend b' r in - if Term.equal a' b' then r else close (merge a' b' r) - -(** Exposed interface *) + if Term.equal a' b' then r else close (merge a' b' r) ) + |> + [%Trace.retn fun {pf} r' -> + pf "%a" pp_diff (r, r') ; + invariant r'] let is_true {sat; rep} = sat && Map.for_alli rep ~f:(fun ~key:a ~data:a' -> Term.equal a a')