From c171170bedc4d519594aeb2d8415905d0dd10414 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 1 Mar 2016 15:31:20 +0000 Subject: [PATCH] Fixed FP string input conversions. Fixes #464 --- src/api/api_numeral.cpp | 6 ++++-- src/util/mpf.cpp | 15 ++++++++++++--- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 770054870..491d9f597 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -68,8 +68,10 @@ extern "C" { (' ' == *m) || ('\n' == *m) || ('.' == *m) || ('e' == *m) || ('E' == *m) || - ('p' == *m && is_float) || - ('P' == *m && is_float))) { + (is_float && + ('p' == *m) || + ('P' == *m) || + ('+' == *m)))) { SET_ERROR_CODE(Z3_PARSER_ERROR); return 0; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 899b8635b..1d7ed1bb3 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -205,15 +205,23 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode // We expect [i].[f]P[e], where P means that the exponent is interpreted as 2^e instead of 10^e. std::string v(value); - size_t e_pos = v.find('p'); - if (e_pos == std::string::npos) e_pos = v.find('P'); std::string f, e; + bool sgn = false; + if (v.substr(0, 1) == "-") { + sgn = true; + v = v.substr(1); + } + else if (v.substr(0, 1) == "+") + v = v.substr(1); + + size_t e_pos = v.find('p'); + if (e_pos == std::string::npos) e_pos = v.find('P'); f = (e_pos != std::string::npos) ? v.substr(0, e_pos) : v; e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0"; - TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;); + TRACE("mpf_dbg", tout << "sgn = " << sgn << " f = " << f << " e = " << e << std::endl;); scoped_mpq q(m_mpq_manager); m_mpq_manager.set(q, f.c_str()); @@ -222,6 +230,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode m_mpz_manager.set(ex, e.c_str()); set(o, ebits, sbits, rm, ex, q); + o.sign = sgn; TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;); }