From 548adedc37034fb8c0b45bf73ef86ec7f2b70f5f Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 2 Feb 2021 04:34:39 -0800
Subject: [PATCH] [sledge] Add Arith.is_uninterpreted

Reviewed By: jvillard

Differential Revision: D25883733

fbshipit-source-id: eeeea1d4a
---
 sledge/src/fol/arithmetic.ml      | 9 +++++++++
 sledge/src/fol/arithmetic_intf.ml | 3 +++
 2 files changed, 12 insertions(+)

diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index 532727e68..1e0b82317 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/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
diff --git a/sledge/src/fol/arithmetic_intf.ml b/sledge/src/fol/arithmetic_intf.ml
index 1a092010a..f7d186f8a 100644
--- a/sledge/src/fol/arithmetic_intf.ml
+++ b/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