From 099af312bb380cee1e0075a56d9110f5d394ca8a Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Mon, 28 Jun 2021 03:33:56 -0700
Subject: [PATCH] [sledge] Fix bug in Context.canon_extend

Summary:
It is possible for normalization to change a term from an
uninterpreted application to e.g. an interpreted atom. For instance,
the conversion `(u1)-1` evaluates to `1`. Context.canon_extend was not
taking this into account, and as a result could violate the
representation invariant of Context.t.

Reviewed By: ngorogiannis

Differential Revision: D28907806

fbshipit-source-id: 9b5171e15
---
 sledge/src/fol/context.ml | 21 ++++++++++++---------
 sledge/src/fol/theory.ml  |  6 +++++-
 2 files changed, 17 insertions(+), 10 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 187dbc475..1a00261e7 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -508,15 +508,18 @@ let rec canon_extend_ a x =
     | None -> (
         (* norm wrt rep and add subterms *)
         let a_norm, x = Trm.fold_map ~f:canon_extend_ a x in
-        match Trm.Map.find_or_add a_norm a_norm x.rep with
-        | Some a', _ ->
-            (* a_norm already equal to a' *)
-            (a', x)
-        | None, rep ->
-            (* a_norm newly added *)
-            let use = add_uses_of a_norm x.use in
-            let x = {x with rep; use} in
-            (a_norm, x) ) )
+        match Theory.classify a_norm with
+        | InterpAtom | NonInterpAtom | InterpApp -> canon_extend_ a_norm x
+        | UninterpApp -> (
+          match Trm.Map.find_or_add a_norm a_norm x.rep with
+          | Some a', _ ->
+              (* a_norm already equal to a' *)
+              (a', x)
+          | None, rep ->
+              (* a_norm newly added *)
+              let use = add_uses_of a_norm x.use in
+              let x = {x with rep; use} in
+              (a_norm, x) ) ) )
 
 (** normalize and add a term to the carrier *)
 let canon_extend a x =
diff --git a/sledge/src/fol/theory.ml b/sledge/src/fol/theory.ml
index a47ce9592..a5ef78136 100644
--- a/sledge/src/fol/theory.ml
+++ b/sledge/src/fol/theory.ml
@@ -32,9 +32,13 @@ let pp ppf = function
 (* Classification of terms ================================================*)
 
 type kind = InterpApp | NonInterpAtom | InterpAtom | UninterpApp
-[@@deriving compare, equal]
+[@@deriving compare, equal, sexp_of]
 
 let classify e =
+  [%trace]
+    ~call:(fun {pf} -> pf "%a" Trm.pp e)
+    ~retn:(fun {pf} k -> pf "%a" Sexp.pp (sexp_of_kind k))
+  @@ fun () ->
   match (e : Trm.t) with
   | Var _ -> NonInterpAtom
   | Z _ | Q _ -> InterpAtom