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

Removed hwf.mul/hwf.div test code.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-05-26 15:11:21 +01:00
parent 9752888704
commit ec270acd32
1 changed files with 0 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
src/util/hwf.cpp
View file

@ -239,35 +239,6 @@ void hwf_manager::mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
#else
o.value = x.value * y.value;
#endif
#if 0
// On the x86 FPU (x87), we use custom assembly routines because
// the code generated for x*y and x/y suffers from the double
// rounding on underflow problem. The scaling trick is described
// in Roger Golliver: `Efficiently producing default orthogonal IEEE
// double results using extended IEEE hardware', see
// http://www.open-std.org/JTC1/SC22/JSG/docs/m3/docs/jsgn326.pdf
// CMW: Tthis is not really needed if we use only the SSE2 FPU,
// it shouldn't hurt the performance too much though.
static const int const1 = -DBL_SCALE;
static const int const2 = +DBL_SCALE;
double xv = x.value;
double yv = y.value;
double & ov = o.value;
__asm {
fild const1;
fld xv;
fscale;
fstp st(1);
fmul yv;
fild const2;
fxch st(1);
fscale;
fstp ov;
}
#endif
}
void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o) {
@ -277,28 +248,6 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
#else
o.value = x.value / y.value;
#endif
#if 0
// see mul(...)
static const int const1 = -DBL_SCALE;
static const int const2 = +DBL_SCALE;
double xv = x.value;
double yv = y.value;
double & ov = o.value;
__asm {
fild const1;
fld xv;
fscale;
fstp st(1);
fdiv yv;
fild const2;
fxch st(1);
fscale;
fstp ov;
}
#endif
}
#ifdef _M_IA64