[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

@@ -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
+        match Theory.classify a_norm with
-        | Some a', _ ->
+        | InterpAtom | NonInterpAtom | InterpApp -> canon_extend_ a_norm x
-            (* a_norm already equal to a' *)
+        | UninterpApp -> (
-            (a', x)
+          match Trm.Map.find_or_add a_norm a_norm x.rep with
-        | None, rep ->
+          | Some a', _ ->
-            (* a_norm newly added *)
+              (* a_norm already equal to a' *)
-            let use = add_uses_of a_norm x.use in
+              (a', x)
-            let x = {x with rep; use} in
+          | None, rep ->
-            (a_norm, x) ) )
+              (* 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 =

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