[sledge] Add Arith.is_uninterpreted

Reviewed By: jvillard

Differential Revision: D25883733

fbshipit-source-id: eeeea1d4a

sledge/src/fol/arithmetic.ml

@@ -180,6 +180,15 @@ struct
         | _ -> Uninterpreted )
       | `Many -> Interpreted
 
+    let is_uninterpreted poly =
+      match Sum.only_elt poly with
+      | Some (mono, _) -> (
+        match Prod.classify mono with
+        | `Zero -> false
+        | `One (_, 1) -> false
+        | _ -> true )
+      | None -> false
+
     let get_const poly =
       match Sum.classify poly with
       | `Zero -> Some Q.zero

sledge/src/fol/arithmetic_intf.ml

@@ -35,6 +35,9 @@ module type S = sig
       [get_const a] is [Some q], [Interpreted] if the principal operation of
       [a] is interpreted, and [Uninterpreted] otherwise. *)
 
+  val is_uninterpreted : t -> bool
+  (** [is_uninterpreted a] iff [classify a = Uninterpreted] *)
+
   (** Construct compound terms *)
 
   val neg : t -> t