From 08f2d87c5676de76dca641673f96cec6116730f9 Mon Sep 17 00:00:00 2001
From: Josh Berdine <josh@berdine.net>
Date: Thu, 10 Apr 2025 10:38:44 +0100
Subject: [PATCH] Add Z3_fpa_is_numeral to the API

This is analogous to Z3_fpa_is_numeral_nan, Z3_fpa_is_numeral_inf, etc. and
can be needed to check that inputs are valid before calling those functions.

Signed-off-by: Josh Berdine <josh@berdine.net>
---
 src/api/api_fpa.cpp | 14 ++++++++++++++
 src/api/z3_fpa.h    | 16 ++++++++++++++++
 2 files changed, 30 insertions(+)

diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 3c350ed18..9f0bc564f 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -1224,6 +1224,20 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    bool Z3_API Z3_fpa_is_numeral(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        LOG_Z3_fpa_is_numeral(c, t);
+        RESET_ERROR_CODE();
+        api::context * ctx = mk_c(c);
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            return false;
+        }
+        return fu.is_numeral(to_expr(t));
+        Z3_CATCH_RETURN(false);
+    }
+
     bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
         Z3_TRY;
         LOG_Z3_fpa_is_numeral_nan(c, t);
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 9c4b22153..525b59814 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -1089,6 +1089,22 @@ extern "C" {
     */
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
 
+    /**
+        \brief Checks whether a given ast is a floating-point numeral.
+
+        \param c logical context
+        \param t an ast
+
+        \sa Z3_fpa_is_numeral_nan
+        \sa Z3_fpa_is_numeral_inf
+        \sa Z3_fpa_is_numeral_normal
+        \sa Z3_fpa_is_numeral_subnormal
+        \sa Z3_fpa_is_numeral_zero
+
+        def_API('Z3_fpa_is_numeral', BOOL, (_in(CONTEXT), _in(AST)))
+    */
+    bool Z3_API Z3_fpa_is_numeral(Z3_context c, Z3_ast t);
+
     /**
         \brief Checks whether a given floating-point numeral is a NaN.