FPA API bugfixes

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

src/api/api_fpa.cpp

@@ -217,7 +217,7 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast sig, Z3_ast exp) {
+    Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig) {
         Z3_TRY;
         LOG_Z3_mk_fpa_fp(c, sgn, sig, exp);
         RESET_ERROR_CODE();
@@ -680,7 +680,11 @@ extern "C" {
         mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
-        bool r = plugin->is_numeral(to_expr(t), val);        
+        bool r = plugin->is_numeral(to_expr(t), val);
+        if (!r || mpfm.is_nan(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG);
+            return 0;
+        }
         *sgn = (mpfm.is_nan(val)) ? 0 : mpfm.sgn(val);
         return r;
         Z3_CATCH_RETURN(0);
@@ -694,14 +698,18 @@ extern "C" {
         mpf_manager & mpfm = mk_c(c)->fpa_util().fm();
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
-        scoped_mpf val(mpfm);
+        scoped_mpf val(mpfm);        
-        if (!plugin->is_numeral(to_expr(t), val)) {
+        if (!plugin->is_numeral(to_expr(t), val)) {            
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
+        else if (!mpfm.is_regular(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG)
+            return "";
+        }
         unsigned sbits = val.get().get_sbits();
         scoped_mpq q(mpqm);
-        mpqm.set(q, mpfm.sig(val));
+        mpqm.set(q, mpfm.sig_normalized(val));
         mpqm.div(q, mpfm.m_powers2(sbits - 1), q);
         std::stringstream ss;
         mpqm.display_decimal(ss, q, sbits);
@@ -724,7 +732,11 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return "";
         }
-        const mpf_exp_t exp = mpfm.exp(val);        
+        else if (!mpfm.is_normal(val) && !mpfm.is_denormal(val)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG)
+                return "";
+        }
+        mpf_exp_t exp = mpfm.exp_normalized(val);        
         std::stringstream ss;
         ss << exp;
         return mk_c(c)->mk_external_string(ss.str());
@@ -740,7 +752,7 @@ extern "C" {
         unsynch_mpq_manager & mpqm = mpfm.mpq_manager();
         fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid());
         scoped_mpf val(mpfm);
-        bool r = plugin->is_numeral(to_expr(t), val);
+        bool r = plugin->is_numeral(to_expr(t), val);        
         if (!r) {
             SET_ERROR_CODE(Z3_INVALID_ARG);
             return 0;

src/api/z3_fpa.h

@@ -273,13 +273,13 @@ extern "C" {
         of the arguments.
 
         \params c logical context.
-        \params sgn sign 
+        \params sgn sign         
-        \params sig significand
         \params exp exponent
+        \params sig significand
 
         def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
     */
-    Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast sig, __in Z3_ast exp);
+    Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig);
 
     /**
     \brief Create a numeral of FloatingPoint sort from a float.

src/ast/fpa_decl_plugin.cpp

@@ -76,7 +76,21 @@ func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
 }
 
 app * fpa_decl_plugin::mk_numeral(mpf const & v) {
-    return m_manager->mk_const(mk_numeral_decl(v));
+    sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
+    func_decl * d;
+    if (m_fm.is_nan(v))
+        d = m_manager->mk_const_decl(symbol("NaN"), s, func_decl_info(m_family_id, OP_FPA_NAN));
+    else if (m_fm.is_pinf(v))
+        d = m_manager->mk_const_decl(symbol("+oo"), s, func_decl_info(m_family_id, OP_FPA_PLUS_INF));
+    else if (m_fm.is_ninf(v))
+        d = m_manager->mk_const_decl(symbol("-oo"), s, func_decl_info(m_family_id, OP_FPA_MINUS_INF));
+    else if (m_fm.is_pzero(v))
+        d = m_manager->mk_const_decl(symbol("+zero"), s, func_decl_info(m_family_id, OP_FPA_PLUS_ZERO));
+    else if (m_fm.is_nzero(v))
+        d = m_manager->mk_const_decl(symbol("-zero"), s, func_decl_info(m_family_id, OP_FPA_MINUS_ZERO));
+    else
+        d = mk_numeral_decl(v);
+    return m_manager->mk_const(d);
 }
 
 bool fpa_decl_plugin::is_numeral(expr * n, mpf & val) {

src/util/mpf.h

@@ -146,7 +146,24 @@ public:
     
     bool sgn(mpf const & x) const { return x.sign; }
     const mpz & sig(mpf const & x) const { return x.significand; }
+    mpz sig_normalized(mpf const & x) { 
+        mpf t;
+        set(t, x);
+        unpack(t, true);
+        mpz r;
+        mpz_manager().set(r, t.significand);
+        del(t);
+        return r;
+    }
     const mpf_exp_t & exp(mpf const & x) const { return x.exponent; }
+    mpf_exp_t exp_normalized(mpf const & x) { 
+        mpf t;
+        set(t, x);
+        unpack(t, true);
+        mpf_exp_t r = t.exponent;
+        del(t);
+        return r;
+    }
 
     bool is_nan(mpf const & x);
     bool is_inf(mpf const & x);