mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 12:23:38 +00:00
Code Activity

Bugfix for hwf::round_to_integral

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-05-22 11:39:58 +01:00
parent 759d9f2dda
commit 54cde7cabb
1 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/util/hwf.cpp
View file

@ -340,7 +340,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
// According to the Intel Architecture manual, the x87-instrunction FRNDINT is the // 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. // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
#ifdef _WINDOWS
#ifdef USE_INTRINSICS #ifdef USE_INTRINSICS
switch (rm) { switch (rm) {
case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break; case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break;
@ -354,10 +354,6 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
UNREACHABLE(); // Unknown rounding mode. UNREACHABLE(); // Unknown rounding mode.
} }
#else #else
NOT_IMPLEMENTED_YET();
#endif
#if 0
double xv = x.value; double xv = x.value;
double & ov = o.value; double & ov = o.value;
@ -366,7 +362,10 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
frndint frndint
fstp ov // Store result away. fstp ov // Store result away.
} }
#endif
#else
// Linux, OSX.
o.value = nearbyint(x.value);
#endif #endif
} }