From 914cd06e4d5ba82c51ebee3b5dc8103c58bfc5a6 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 9 Jan 2020 05:06:04 -0800
Subject: [PATCH] [sledge] Close Equality.classes under one-step congruence

Summary:
Equality.classes was assuming a simpler representation, and was
incomplete as a result.

The 'representative' map is not kept in a normalized form, where
subterms are necessarily representatives. Therefore, applying the
representative map to subterms of terms in a class can reveal new
elements of the class. This mirrors how the `lookup` function in
`normalize` works.

Reviewed By: ngorogiannis

Differential Revision: D19221868

fbshipit-source-id: 4a2ed6d3f
---
 sledge/src/symbheap/equality.ml      | 16 +++++++++++-----
 sledge/src/symbheap/equality_test.ml | 11 +++++------
 sledge/src/symbheap/solver_test.ml   |  1 +
 3 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index ad540b638..550841549 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -22,10 +22,19 @@ type t =
             'rep(resentative)' of [a] *) }
 [@@deriving compare, equal, sexp]
 
+(** apply a subst to a term *)
+let apply s a = Map.find s a |> Option.value ~default:a
+
 let classes r =
+  let add key data cls =
+    if Term.equal key data then cls
+    else Map.add_multi cls ~key:data ~data:key
+  in
   Map.fold r.rep ~init:empty_map ~f:(fun ~key ~data cls ->
-      if Term.equal key data then cls
-      else Map.add_multi cls ~key:data ~data:key )
+      match Term.classify key with
+      | `Interpreted | `Atomic -> add key data cls
+      | `Simplified | `Uninterpreted ->
+          add (Term.map ~f:(apply r.rep) key) data cls )
 
 (** Pretty-printing *)
 
@@ -106,9 +115,6 @@ let invariant r =
 
 let true_ = {sat= true; rep= empty_map} |> check invariant
 
-(** apply a subst to a term *)
-let apply s a = Map.find s a |> Option.value ~default:a
-
 (** apply a subst to maximal non-interpreted subterms *)
 let rec norm s a =
   match Term.classify a with
diff --git a/sledge/src/symbheap/equality_test.ml b/sledge/src/symbheap/equality_test.ml
index fdccd60bc..d0e5563ff 100644
--- a/sledge/src/symbheap/equality_test.ml
+++ b/sledge/src/symbheap/equality_test.ml
@@ -140,8 +140,8 @@ let%test_module _ =
       pp r3 ;
       [%expect
         {|
-      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %v_3)
-      = (%y_6 rem %z_7)
+      %t_1 = %u_2 = %v_3 = %w_4 = %x_5 = %z_7 = (%y_6 rem %t_1)
+      = (%y_6 rem %t_1)
 
       {sat= true;
        rep= [[%u_2 ↦ %t_1];
@@ -343,8 +343,7 @@ let%test_module _ =
     let r15 = of_eqs [(b, b); (x, !1)]
 
     let%expect_test _ =
-      pp r15 ; [%expect {|
-          {sat= true; rep= [[%x_5 ↦ 1]]} |}]
+      pp r15 ; [%expect {| {sat= true; rep= [[%x_5 ↦ 1]]} |}]
 
     let%test _ = entails_eq r15 b (Term.signed 1 !1)
     let%test _ = entails_eq r15 (Term.unsigned 1 b) !1
@@ -391,6 +390,6 @@ let%test_module _ =
                [((u8) %x_5) ↦ %x_5];
                [((u8) %y_6) ↦ ]]}
 
-        (((u8) %y_6) + 1) = %y_6
-        ∧ %x_5 = ((u8) %x_5) |}]
+        (((u8) %y_6) + 1) = %y_6 ∧ %x_5 = ((u8) %x_5)
+        ∧ ((u8) %y_6) = ((u8) (((u8) %y_6) + 1)) |}]
   end )
diff --git a/sledge/src/symbheap/solver_test.ml b/sledge/src/symbheap/solver_test.ml
index edc1bb65c..75f57f32a 100644
--- a/sledge/src/symbheap/solver_test.ml
+++ b/sledge/src/symbheap/solver_test.ml
@@ -196,6 +196,7 @@ let%test_module _ =
         ) infer_frame:
           ∃ %a0_10, %a1_11 .
             %a_2 = %a0_10
+          ∧ ⟨%n_9,%a0_10⟩ = ⟨16,%a_2⟩
           ∧ ⟨32,%a_1⟩ = ⟨%n_9,%a0_10⟩^⟨16,%a1_11⟩
           ∧ 16 = %m_8 = %n_9
           ∧ (%k_5 + 16) -[ %k_5, 16 )-> ⟨16,%a1_11⟩ |}]