From 10e921bcec4e766454d3c58675439e9f0413c754 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 06:13:40 -0800
Subject: [PATCH] [sledge] Refine Arith.classify to distinguish interpreted and
 uninterpreted
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Summary:
Add a distinction between interpreted and uninterpreted arithmetic
terms, and use it in Context.classify. This enables correctly
classifying non-linear terms such as `x × y` as uninterpreted.

Reviewed By: ngorogiannis

Differential Revision: D24746228

fbshipit-source-id: 1a4b0e3bd
---
 sledge/src/fol/arithmetic.ml      |  9 +++++----
 sledge/src/fol/arithmetic_intf.ml |  7 ++++---
 sledge/src/fol/context.ml         | 10 ++++++++--
 sledge/src/fol/trm.ml             |  6 +++---
 4 files changed, 20 insertions(+), 12 deletions(-)

diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index 963a80985..734ba63de 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -165,7 +165,7 @@ struct
 
     (* projections and embeddings *)
 
-    type view = Trm of trm | Const of Q.t | Compound
+    type kind = Trm of trm | Const of Q.t | Interpreted | Uninterpreted
 
     let classify poly =
       match Sum.classify poly with
@@ -173,9 +173,10 @@ struct
       | `One (mono, coeff) -> (
         match Prod.classify mono with
         | `Zero -> Const coeff
-        | `One (trm, 1) when Q.equal Q.one coeff -> Trm trm
-        | _ -> Compound )
-      | `Many -> Compound
+        | `One (trm, 1) ->
+            if Q.equal Q.one coeff then Trm trm else Interpreted
+        | _ -> Uninterpreted )
+      | `Many -> Interpreted
 
     let get_const poly =
       match Sum.classify poly with
diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index d0592c73c..de7d564d8 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/sledge/src/fol/arithmetic_intf.ml
@@ -28,11 +28,12 @@ module type S = sig
   val get_trm : t -> trm option
   (** [get_trm a] is [Some x] iff [equal a (trm x)] *)
 
-  type view = Trm of trm | Const of Q.t | Compound
+  type kind = Trm of trm | Const of Q.t | Interpreted | Uninterpreted
 
-  val classify : t -> view
+  val classify : t -> kind
   (** [classify a] is [Trm x] iff [get_trm a] is [Some x], [Const q] iff
-      [get_const a] is [Some q], and [Compound] otherwise *)
+      [get_const a] is [Some q], [Interpreted] if the principal operation of
+      [a] is interpreted, and [Uninterpreted] otherwise *)
 
   (** Construct compound terms *)
 
diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 195c20835..3c7799175 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -14,9 +14,15 @@ open Exp
 type kind = Interpreted | Atomic | Uninterpreted
 [@@deriving compare, equal]
 
-let classify e =
+let rec classify e =
   match (e : Trm.t) with
-  | Arith _ | Sized _ | Extract _ | Concat _ -> Interpreted
+  | Arith a -> (
+    match Trm.Arith.classify a with
+    | Trm t -> classify t
+    | Const _ -> Atomic
+    | Interpreted -> Interpreted
+    | Uninterpreted -> Uninterpreted )
+  | Sized _ | Extract _ | Concat _ -> Interpreted
   | Var _ | Z _ | Q _ | Ancestor _ -> Atomic
   | Splat _ | Select _ | Update _ | Record _ | Apply _ -> Uninterpreted
 
diff --git a/sledge/src/fol/trm.ml b/sledge/src/fol/trm.ml
index 019e16d39..ca78a9ebe 100644
--- a/sledge/src/fol/trm.ml
+++ b/sledge/src/fol/trm.ml
@@ -199,8 +199,8 @@ end = struct
     | Q q -> assert (not (Z.equal Z.one (Q.den q)))
     | Arith a -> (
       match Arith.classify a with
-      | Compound -> ()
-      | Trm _ | Const _ -> assert false )
+      | Trm _ | Const _ -> assert false
+      | _ -> () )
     | _ -> ()
 
   (** Destruct *)
@@ -228,7 +228,7 @@ end = struct
     ( match Arith.classify a with
     | Trm e -> e
     | Const q -> _Q q
-    | Compound -> Arith a )
+    | _ -> Arith a )
     |> check invariant
 
   let add x y = _Arith Arith.(add (trm x) (trm y))