From dbfa63feaa5c1d4504bef15a62d4b36725d0c752 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 2 Feb 2021 04:34:46 -0800
Subject: [PATCH] [sledge] Refine Theory.classify to distinguish
 (un)interpreted atoms

Reviewed By: jvillard

Differential Revision: D25883731

fbshipit-source-id: b63877d43
---
 sledge/src/fol/context.ml | 13 +++++++------
 sledge/src/fol/theory.ml  | 31 +++++++++++++++++++------------
 sledge/src/fol/theory.mli |  2 +-
 3 files changed, 27 insertions(+), 19 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 97b37e05a..d76454a83 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -511,14 +511,15 @@ let rec canon r a =
   [%Trace.call fun {pf} -> pf "@ %a" Trm.pp a]
   ;
   ( match Theory.classify a with
-  | Atomic -> Subst.apply r.rep a
-  | Interpreted -> Trm.map ~f:(canon r) a
-  | Uninterpreted -> (
+  | InterpAtom -> a
+  | NonInterpAtom -> Subst.apply r.rep a
+  | InterpApp -> Trm.map ~f:(canon r) a
+  | UninterpApp -> (
       let a' = Trm.map ~f:(canon r) a in
       match Theory.classify a' with
-      | Atomic -> Subst.apply r.rep a'
-      | Interpreted -> a'
-      | Uninterpreted -> lookup r a' ) )
+      | InterpAtom | InterpApp -> a'
+      | NonInterpAtom -> Subst.apply r.rep a'
+      | UninterpApp -> lookup r a' ) )
   |>
   [%Trace.retn fun {pf} -> pf "%a" Trm.pp]
 
diff --git a/sledge/src/fol/theory.ml b/sledge/src/fol/theory.ml
index f996bc193..56cb7325b 100644
--- a/sledge/src/fol/theory.ml
+++ b/sledge/src/fol/theory.ml
@@ -29,22 +29,29 @@ let pp ppf = function
 
 (* Classification of terms ================================================*)
 
-type kind = Interpreted | Atomic | Uninterpreted
+type kind = InterpApp | NonInterpAtom | InterpAtom | UninterpApp
 [@@deriving compare, equal]
 
 let classify e =
   match (e : Trm.t) with
-  | Var _ | Z _ | Q _ | Concat [||] | Apply (_, [||]) -> Atomic
-  | Arith a -> (
-    match Trm.Arith.classify a with
-    | Trm _ | Const _ -> violates Trm.invariant e
-    | Interpreted -> Interpreted
-    | Uninterpreted -> Uninterpreted )
-  | Splat _ | Sized _ | Extract _ | Concat _ -> Interpreted
-  | Apply _ -> Uninterpreted
-
-let is_interpreted e = equal_kind (classify e) Interpreted
-let is_uninterpreted e = equal_kind (classify e) Uninterpreted
+  | Var _ -> NonInterpAtom
+  | Z _ | Q _ -> InterpAtom
+  | Arith a ->
+      if Trm.Arith.is_uninterpreted a then UninterpApp
+      else (
+        assert (
+          match Trm.Arith.classify a with
+          | Trm _ | Const _ -> violates Trm.invariant e
+          | Interpreted -> true
+          | Uninterpreted -> false ) ;
+        InterpApp )
+  | Concat [||] -> InterpAtom
+  | Splat _ | Sized _ | Extract _ | Concat _ -> InterpApp
+  | Apply (_, [||]) -> NonInterpAtom
+  | Apply _ -> UninterpApp
+
+let is_interpreted e = equal_kind (classify e) InterpApp
+let is_uninterpreted e = equal_kind (classify e) UninterpApp
 
 (* Solving equations ======================================================*)
 
diff --git a/sledge/src/fol/theory.mli b/sledge/src/fol/theory.mli
index 891302213..4de53e50b 100644
--- a/sledge/src/fol/theory.mli
+++ b/sledge/src/fol/theory.mli
@@ -16,7 +16,7 @@ type t =
 
 val pp : t pp
 
-type kind = Interpreted | Atomic | Uninterpreted
+type kind = InterpApp | NonInterpAtom | InterpAtom | UninterpApp
 [@@deriving compare, equal]
 
 val classify : Trm.t -> kind