From 28e4c74426dfcd7e5e9f87bc8ae614c13075d1e1 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 15 Nov 2019 03:31:35 -0800
Subject: [PATCH] [sledge] Fix bug in Equality.or_

Summary:
Equality.or_ assumed a simpler representation of equality relations,
and was incomplete as a result.

Reviewed By: jvillard

Differential Revision: D18298138

fbshipit-source-id: cf91229f6
---
 sledge/src/symbheap/equality.ml      | 18 ++++++++++++++----
 sledge/src/symbheap/equality_test.ml | 21 +++++++++++++++++++++
 2 files changed, 35 insertions(+), 4 deletions(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index 6bdff160b..f911211b6 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -250,17 +250,27 @@ let and_ r s =
     Map.fold s.rep ~init:r ~f:(fun ~key:e ~data:e' r -> and_eq e e' r)
 
 let or_ r s =
-  if not s.sat then r
+  [%Trace.call fun {pf} -> pf "@[<hv 1>   %a@ @<2>∨ %a@]" pp r pp s]
+  ;
+  ( if not s.sat then r
   else if not r.sat then s
   else
     let merge_mems rs r s =
-      Map.fold s.rep ~init:rs ~f:(fun ~key:e ~data:e' rs ->
-          if entails_eq r e e' then and_eq e e' rs else rs )
+      Map.fold (classes s) ~init:rs ~f:(fun ~key:rep ~data:cls rs ->
+          List.fold cls
+            ~init:([rep], rs)
+            ~f:(fun (reps, rs) exp ->
+              match List.find ~f:(entails_eq r exp) reps with
+              | Some rep -> (reps, and_eq exp rep rs)
+              | None -> (exp :: reps, rs) )
+          |> snd )
     in
     let rs = true_ in
     let rs = merge_mems rs r s in
     let rs = merge_mems rs s r in
-    rs
+    rs )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" pp]
 
 (* assumes that f is injective and for any set of terms E, f[E] is disjoint
    from E *)
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index 7bfe28327..a4053dc8b 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -112,6 +112,27 @@ let%test_module _ =
     let%test _ = entails_eq r2 (g x y) (g z y)
     let%test _ = difference (or_ r1 r2) x z |> Poly.equal None
 
+    let%expect_test _ =
+      let r = of_eqs [(w, y); (y, z)] in
+      let s = of_eqs [(x, y); (y, z)] in
+      let rs = or_ r s in
+      pp r ;
+      pp s ;
+      pp rs ;
+      [%expect
+        {|
+        {sat= true; rep= [[%y_6 ↦ %w_4]; [%z_7 ↦ %w_4]]}
+
+        {sat= true; rep= [[%y_6 ↦ %x_5]; [%z_7 ↦ %x_5]]}
+
+        {sat= true; rep= [[%z_7 ↦ %y_6]]} |}]
+
+    let%test _ =
+      let r = of_eqs [(w, y); (y, z)] in
+      let s = of_eqs [(x, y); (y, z)] in
+      let rs = or_ r s in
+      entails_eq rs y z
+
     let r3 = of_eqs [(g y z, w); (v, w); (g y w, t); (x, v); (x, u); (u, z)]
 
     let%expect_test _ =