mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

Fixed FP string input conversions.

Browse source 
Fixes #464
This commit is contained in:
Christoph M. Wintersteiger 2016-03-01 15:31:20 +00:00
parent b6e43b6d7b
commit c171170bed
2 changed files with 16 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/api/api_numeral.cpp
View file

@ -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;
}

15
src/util/mpf.cpp
View file

@ -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;);
}