From e0bc704106e15595856ec81419fb299dcb51aa87 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 11 Jan 2015 18:29:12 +0000 Subject: [PATCH] FPA API bugfixes Signed-off-by: Christoph M. Wintersteiger --- src/api/api_fpa.cpp | 26 +++++++++++++++++++------- src/api/z3_fpa.h | 6 +++--- src/ast/fpa_decl_plugin.cpp | 16 +++++++++++++++- src/util/mpf.h | 17 +++++++++++++++++ 4 files changed, 54 insertions(+), 11 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 219f9b166..67ffe12d9 100644 --- a/src/api/api_fpa.cpp +++ b/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); - if (!plugin->is_numeral(to_expr(t), val)) { + scoped_mpf val(mpfm); + 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; diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h index 7457ed9a3..75002e1a5 100644 --- a/src/api/z3_fpa.h +++ b/src/api/z3_fpa.h @@ -273,13 +273,13 @@ extern "C" { of the arguments. \params c logical context. - \params sgn sign - \params sig significand + \params sgn sign \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. diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index a8e805066..9900812dd 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/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) { diff --git a/src/util/mpf.h b/src/util/mpf.h index b919e0371..599e8e743 100644 --- a/src/util/mpf.h +++ b/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);