From a52085a7187ba16345b8ac40b4b893a92c5064b3 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 2 Mar 2020 08:43:11 -0800
Subject: [PATCH] [sledge] Fix Equality.canon to handle changing term
 classification

Summary:
It can happen that canonizing subterms can change the classification
of a term e.g. to the literal true. In such cases, it is not useful or
correct use `Equality.lookup` (which expects to only be used on
uninterpreted applications) to search for some other equation equal to
the literal and use its representative instead.

Reviewed By: ngorogiannis

Differential Revision: D20120279

fbshipit-source-id: 3e2160233
---
 sledge/src/symbheap/equality.ml | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

diff --git a/sledge/src/symbheap/equality.ml b/sledge/src/symbheap/equality.ml
index b9d630391..57fe19f2e 100644
--- a/sledge/src/symbheap/equality.ml
+++ b/sledge/src/symbheap/equality.ml
@@ -401,7 +401,9 @@ let congruent r a b =
 
 (** [lookup r a] is [b'] if [a ~ b = b'] for some equation [b = b'] in rep *)
 let lookup r a =
-  With_return.with_return
+  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp a pp r]
+  ;
+  ( With_return.with_return
   @@ fun {return} ->
   (* congruent specialized to assume [a] canonized and [b] non-interpreted *)
   let semi_congruent r a b =
@@ -409,15 +411,26 @@ let lookup r a =
   in
   Subst.iteri r.rep ~f:(fun ~key ~data ->
       if semi_congruent r a key then return data ) ;
-  a
+  a )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" Term.pp]
 
-(** rewrite a term into canonical form using rep and, for uninterpreted
+(** rewrite a term into canonical form using rep and, for non-interpreted
     terms, congruence composed with rep *)
 let rec canon r a =
-  match classify a with
-  | Interpreted -> Term.map ~f:(canon r) a
-  | Simplified | Uninterpreted -> lookup r (Term.map ~f:(canon r) a)
+  [%Trace.call fun {pf} -> pf "%a@ %a" Term.pp a pp r]
+  ;
+  ( match classify a with
   | Atomic -> Subst.apply r.rep a
+  | Interpreted -> Term.map ~f:(canon r) a
+  | Simplified | Uninterpreted -> (
+      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'
+      | Simplified | Uninterpreted -> lookup r a' ) )
+  |>
+  [%Trace.retn fun {pf} -> pf "%a" Term.pp]
 
 (** add a term to the carrier *)
 let rec extend a r =