[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

@@ -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"]
 

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_