From 89d38385db100947e25229d40e5f2b88909e2891 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 17 Oct 2016 13:31:07 +0100
Subject: [PATCH] Added functions to test FP numerals for special values.

---
 src/api/api_fpa.cpp       | 96 +++++++++++++++++++++++++++++++++++++++
 src/api/z3_fpa.h          | 60 ++++++++++++++++++++++++
 src/ast/fpa_decl_plugin.h |  4 ++
 3 files changed, 160 insertions(+)

diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp
index 048113eca..cc8648c2a 100644
--- a/src/api/api_fpa.cpp
+++ b/src/api/api_fpa.cpp
@@ -1183,4 +1183,100 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        Z3_fpa_is_numeral_nan(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        api::context * ctx = mk_c(c);
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        return fu.is_nan(to_expr(t));
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        Z3_fpa_is_numeral_inf(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        api::context * ctx = mk_c(c);
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        return fu.is_inf(to_expr(t));
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        Z3_fpa_is_numeral_zero(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        api::context * ctx = mk_c(c);
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        return fu.is_zero(to_expr(t));
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        Z3_fpa_is_numeral_normal(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        api::context * ctx = mk_c(c);
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        return fu.is_normal(to_expr(t));
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        Z3_fpa_is_numeral_subnormal(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        api::context * ctx = mk_c(c);
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        return fu.is_subnormal(to_expr(t));
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
+    Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
+        Z3_TRY;
+        Z3_fpa_is_numeral_positive(c, t);
+        RESET_ERROR_CODE();
+        ast_manager & m = mk_c(c)->m();
+        api::context * ctx = mk_c(c);
+        mpf_manager & mpfm = mk_c(c)->fpautil().fm();
+        fpa_util & fu = ctx->fpautil();
+        if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
+        return fu.is_positive(to_expr(t));
+        Z3_CATCH_RETURN(Z3_FALSE);
+    }
+
 };
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 9abbb7b60..d5da90808 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -822,6 +822,66 @@ extern "C" {
     */
     unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
 
+    /**
+        \brief Checks whether a given floating-point numeral is a NaN.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_is_numeral_nan', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
+
+    /**
+        \brief Checks whether a given floating-point numeral is a +oo or -oo.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_is_numeral_inf', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
+
+    /**
+        \brief Checks whether a given floating-point numeral is +zero or -zero.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_is_numeral_zero', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
+
+    /**
+        \brief Checks whether a given floating-point numeral is normal.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_is_numeral_normal', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
+
+    /**
+        \brief Checks whether a given floating-point numeral is subnormal.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_is_numeral_subnormal', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
+
+    /**
+        \brief Checks whether a given floating-point numeral is positive.
+
+        \param c logical context
+        \param t a floating-point numeral
+
+        def_API('Z3_fpa_is_numeral_positive', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
+
     /**
         \brief Retrieves the sign of a floating-point literal as a bit-vector expression.
 
diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h
index c00bed7ae..7c9c311a8 100644
--- a/src/ast/fpa_decl_plugin.h
+++ b/src/ast/fpa_decl_plugin.h
@@ -288,11 +288,15 @@ public:
     app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); }
 
     bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); }
+    bool is_inf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_inf(v); }
     bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); }
     bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); }
     bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); }
     bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
     bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
+    bool is_normal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_normal(v); }
+    bool is_subnormal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_denormal(v); }
+    bool is_positive(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pos(v); }
 
     app * mk_fp(expr * sgn, expr * exp, expr * sig) {
         SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);