[sledge] Refine Arith.classify to distinguish interpreted and uninterpreted

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

@@ -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

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 *)
 

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
 

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))