From c91e09031f0d61238bd4b73e72a0fa09cf42deae Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 16 Apr 2020 03:39:04 -0700
Subject: [PATCH] [sledge] Strengthen Equality normalization

Summary:
It is possible for the canonical form of a term in (the carrier set
of) a relation to be a term that is not in the relation. It is also
possible for this term to be equal to a term in the relation. It is
the job of the lookup subroutine of normalization to find these
equations.

The current implementation of entails_eq is incomplete in this case,
in particular, when an uninterpreted term has an interpreted subterm,
which itself has a subterm that is not a representative.

This diff strengthens normalization (and hence it's callers such as
entails_eq) to handle such cases. This makes lookup work slightly
harder. An alternative would be to extend the carrier with new terms
from normalization to the carrier and closing the relation, and then
re-normalizing. That would lead to much inflated representation sizes,
and is inefficient.

Reviewed By: jvillard

Differential Revision: D20612565

fbshipit-source-id: 3b7534a62
---
 sledge/lib/equality.ml      | 6 +++---
 sledge/lib/equality_test.ml | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/sledge/lib/equality.ml b/sledge/lib/equality.ml
index 733d42f28..139310180 100644
--- a/sledge/lib/equality.ml
+++ b/sledge/lib/equality.ml
@@ -456,7 +456,7 @@ let lookup r a =
   @@ fun {return} ->
   (* congruent specialized to assume [a] canonized and [b] non-interpreted *)
   let semi_congruent r a b =
-    Term.equal a (Term.map ~f:(Subst.apply r.rep) b)
+    Term.equal a (Term.map ~f:(Subst.norm r.rep) b)
   in
   Subst.iteri r.rep ~f:(fun ~key ~data ->
       if semi_congruent r a key then return data ) ;
@@ -476,7 +476,7 @@ let rec canon r a =
       let a' = Term.map ~f:(canon r) a in
       match classify a' with
       | Atomic -> Subst.apply r.rep a'
-      | Interpreted -> Term.map ~f:(canon r) a'
+      | Interpreted -> a'
       | Simplified | Uninterpreted -> lookup r a' ) )
   |>
   [%Trace.retn fun {pf} -> pf "%a" Term.pp]
@@ -557,7 +557,7 @@ let is_false {sat} = not sat
 let entails_eq r d e =
   [%Trace.call fun {pf} -> pf "%a = %a@ %a" Term.pp d Term.pp e pp r]
   ;
-  Term.is_true (canon r (Term.eq d e))
+  Term.is_true (Term.eq (canon r d) (canon r e))
   |>
   [%Trace.retn fun {pf} -> pf "%b"]
 
diff --git a/sledge/lib/equality_test.ml b/sledge/lib/equality_test.ml
index 9a03bfa06..0e620605a 100644
--- a/sledge/lib/equality_test.ml
+++ b/sledge/lib/equality_test.ml
@@ -345,7 +345,8 @@ let%test_module _ =
     let%expect_test _ =
       pp r14 ;
       [%expect
-        {| {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
+        {|
+          {sat= true; rep= [[%x_5 ↦ 1]; [(%y_6 ≠ 0) ↦ -1]]} |}]
 
     let%test _ = entails_eq r14 a Term.true_
     let%test _ = entails_eq r14 b Term.true_