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

FP: bugfix for get_some_value which couldn't produce rounding-mode values.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-04-25 15:19:48 +01:00
parent 4768a360f8
commit abe73db702
1 changed files with 14 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/ast/fpa_decl_plugin.cpp
View file

@ -879,12 +879,20 @@ void fpa_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
}
expr * fpa_decl_plugin::get_some_value(sort * s) {
SASSERT(s->is_sort_of(m_family_id, FLOATING_POINT_SORT));
mpf tmp;
m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
expr * res = this->mk_numeral(tmp);
m_fm.del(tmp);
return res;
if (s->is_sort_of(m_family_id, FLOATING_POINT_SORT)) {
mpf tmp;
m_fm.mk_nan(s->get_parameter(0).get_int(), s->get_parameter(1).get_int(), tmp);
expr * res = mk_numeral(tmp);
m_fm.del(tmp);
return res;
}
else if (s->is_sort_of(m_family_id, ROUNDING_MODE_SORT)) {
func_decl * f = mk_rm_const_decl(OP_FPA_RM_TOWARD_ZERO, 0, 0, 0, 0, s);
return m_manager->mk_const(f);
}
UNREACHABLE();
return 0;
}
bool fpa_decl_plugin::is_value(app * e) const {