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

Numeral API: added floating-point numeral cases.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-14 13:12:44 +01:00
parent 4af39b432c
commit 165da842b7
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_numeral.cpp
View file

@ -58,6 +58,8 @@ extern "C" {
SET_ERROR_CODE(Z3_INVALID_ARG); SET_ERROR_CODE(Z3_INVALID_ARG);
RETURN_Z3(0); RETURN_Z3(0);
} }
sort * _ty = to_sort(ty);
bool is_float = mk_c(c)->float_util().is_float(_ty);
std::string fixed_num; std::string fixed_num;
char const* m = n; char const* m = n;
while (*m) { while (*m) {
@ -65,14 +67,15 @@ extern "C" {
('/' == *m) || ('-' == *m) || ('/' == *m) || ('-' == *m) ||
(' ' == *m) || ('\n' == *m) || (' ' == *m) || ('\n' == *m) ||
('.' == *m) || ('e' == *m) || ('.' == *m) || ('e' == *m) ||
('E' == *m))) { ('E' == *m) ||
(('p' == *m) && is_float) ||
(('P' == *m)) && is_float)) {
SET_ERROR_CODE(Z3_PARSER_ERROR); SET_ERROR_CODE(Z3_PARSER_ERROR);
return 0; return 0;
} }
++m; ++m;
} }
ast * a = 0; ast * a = 0;
sort * _ty = to_sort(ty);
if (_ty->get_family_id() == mk_c(c)->get_fpa_fid()) if (_ty->get_family_id() == mk_c(c)->get_fpa_fid())
{ {
// avoid expanding floats into huge rationals. // avoid expanding floats into huge rationals.