mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Bugfix for hwf_manager::round_to_integral

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-21 15:06:47 +01:00
parent caa616f11b
commit c422b48bf4
1 changed files with 33 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/util/hwf.cpp
View file

@ -338,8 +338,39 @@ void hwf_manager::sqrt(mpf_rounding_mode rm, hwf const & x, hwf & o) {
void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o) {
set_rounding_mode(rm);
modf(x.value, &o.value);
// Note: on x64, this sometimes produces an SNAN instead of a QNAN?
// CMW: modf is not the right function here.
// modf(x.value, &o.value);
// According to the Intel Architecture manual, the x87-instrunction FRNDINT is the
// same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
#ifdef USE_INTRINSICS
switch (rm) {
case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break;
case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break;
case 3: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEG_INF)); break;
case 4: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_ZERO)); break;
case 1:
UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware!
break;
default:
UNREACHABLE(); // Unknown rounding mode.
}
#else
NOT_IMPLEMENTED_YET();
#endif
#if 0
double xv = x.value;
double & ov = o.value;
__asm {
fld xv
frndint
fstp ov // Store result away.
}
#endif
}
void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {