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

whitespace

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-04-24 15:11:03 +01:00
parent 643a87cb5b
commit 3131f29816
1 changed files with 38 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

76
src/util/hwf.cpp
View file

@ -38,13 +38,13 @@ Revision History:
// Note:
// Which FPU will be used is determined by compiler settings. On x64 it's always SSE2,
// on x86 we have to chose SSE2 by enabling /arch:SSE2 (otherwise the x87 FPU will be used).
// on x86 we have to chose SSE2 by enabling /arch:SSE2 (otherwise the x87 FPU will be used).
// Christoph has decided that we don't want to use the x87; this makes everything a lot easier.
// For SSE2, it is best to use compiler intrinsics because this makes it completely
// clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
// the x87 FPU, even when /arch:SSE2 is on.
// the x87 FPU, even when /arch:SSE2 is on.
// Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
#ifdef __clang__
#undef USE_INTRINSICS
@ -56,19 +56,19 @@ Revision History:
hwf_manager::hwf_manager() :
m_mpz_manager(m_mpq_manager)
{
{
#ifdef _WINDOWS
#if defined(_AMD64_) || defined(_M_IA64)
// Precision control is not supported on x64.
// Precision control is not supported on x64.
// See: http://msdn.microsoft.com/en-us/library/e9b52ceh(VS.110).aspx
// CMW: I think this is okay though, the compiler will chose the right instructions
// CMW: I think this is okay though, the compiler will chose the right instructions
// (the x64/SSE2 FPU has separate instructions for different precisions).
#else
// Setting the precision should only be required on the x87, but it won't hurt to do it anyways.
// _PC_53 means double precision (53 significand bits). For extended precision use _PC_64.
#ifndef USE_INTRINSICS
__control87_2(_PC_53, _MCW_PC, &x86_state, &sse2_state);
__control87_2(_PC_53, _MCW_PC, &x86_state, &sse2_state);
#endif
#endif
#else
@ -78,7 +78,7 @@ hwf_manager::hwf_manager() :
// We only set the precision of the FPU here in the constructor. At the moment, there are no
// other parts of the code that could overwrite this, and Windows takes care of context switches.
// CMW: I'm not sure what happens on CPUs with hyper-threading (since the FPU is shared).
// CMW: I'm not sure what happens on CPUs with hyper-threading (since the FPU is shared).
// I have yet to discover whether Linux and OSX save the FPU state when switching context.
// As long as we stick to using the SSE2 FPU though, there shouldn't be any problems with respect
// to the precision (not sure about the rounding modes though).
@ -104,7 +104,7 @@ void hwf_manager::set(hwf & o, double value) {
o.value = value;
}
void hwf_manager::set(hwf & o, float value) {
void hwf_manager::set(hwf & o, float value) {
o.value = (double)value;
}
@ -113,7 +113,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & value) {
o.value = m_mpq_manager.get_double(value);
}
void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) {
void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) {
// We expect [i].[f]P[e], where P means that the exponent is interpreted as 2^e instead of 10^e.
std::string v(value);
@ -123,17 +123,17 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) {
std::string f, e;
f = (e_pos != std::string::npos) ? v.substr(0, e_pos) : v;
e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0";
e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0";
TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;);
TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;);
mpq q;
mpq q;
m_mpq_manager.set(q, f.c_str());
mpz ex;
m_mpz_manager.set(ex, e.c_str());
set(o, rm, q, ex);
set(o, rm, q, ex);
TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;);
}
@ -142,7 +142,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp
// Assumption: this represents significand * 2^exponent.
set_rounding_mode(rm);
mpq sig;
mpq sig;
m_mpq_manager.set(sig, significand);
int64 exp = m_mpz_manager.get_int64(exponent);
@ -150,7 +150,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp
o.value = 0.0;
else
{
while (m_mpq_manager.lt(sig, 1))
while (m_mpq_manager.lt(sig, 1))
{
m_mpq_manager.mul(sig, 2, sig);
exp--;
@ -176,7 +176,7 @@ void hwf_manager::set(hwf & o, hwf const & x) {
o.value = x.value;
}
void hwf_manager::abs(hwf & o) {
void hwf_manager::abs(hwf & o) {
o.value = fabs(o.value);
}
@ -244,14 +244,14 @@ void hwf_manager::mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
// 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
// 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;
static const int const2 = +DBL_SCALE;
double xv = x.value;
double yv = y.value;
double & ov = o.value;
@ -266,14 +266,14 @@ void hwf_manager::mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
fxch st(1);
fscale;
fstp ov;
}
}
#endif
}
void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o) {
set_rounding_mode(rm);
#ifdef USE_INTRINSICS
_mm_store_sd(&o.value, _mm_div_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
_mm_store_sd(&o.value, _mm_div_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
#else
o.value = x.value / y.value;
#endif
@ -306,18 +306,18 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
#endif
void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) {
// CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium,
// CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium,
// Intel Sandybridge and AMD Bulldozers support that (via AVX).
set_rounding_mode(rm);
#ifdef _M_IA64
// IA64 (Itanium) will do it, if contractions are on.
// IA64 (Itanium) will do it, if contractions are on.
o.value = x.value * y.value + z.value;
#else
#if defined(_WINDOWS)
#if defined(_WINDOWS)
#if _MSC_VER >= 1800
o.value = ::fma(x.value, y.value, z.value);
o.value = ::fma(x.value, y.value, z.value);
#else // Windows, older than VS 2013
#ifdef USE_INTRINSICS
_mm_store_sd(&o.value, _mm_fmadd_sd(_mm_set_sd(x.value), _mm_set_sd(y.value), _mm_set_sd(z.value)));
@ -351,7 +351,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
// 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
// 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 _WINDOWS
#ifdef USE_INTRINSICS
@ -389,7 +389,7 @@ void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {
o.value = x.value/y.value; // NaN
else if (is_inf(y))
o.value = x.value;
else
else
o.value = fmod(x.value, y.value);
// Here is an x87 alternative if the above makes problems; this may also be faster.
@ -423,7 +423,7 @@ void hwf_manager::maximum(hwf const & x, hwf const & y, hwf & o) {
o.value = x.value;
else if (lt(x, y))
o.value = y.value;
else
else
o.value = x.value;
#endif
}
@ -439,12 +439,12 @@ void hwf_manager::minimum(hwf const & x, hwf const & y, hwf & o) {
o.value = x.value;
else if (lt(x, y))
o.value = x.value;
else
else
o.value = y.value;
#endif
}
std::string hwf_manager::to_string(hwf const & x) {
std::string hwf_manager::to_string(hwf const & x) {
std::stringstream ss("");
ss << std::scientific << x.value;
return ss.str();
@ -488,9 +488,9 @@ void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o)
int e = exp(x);
if (e >= 0)
qm.mul2k(n, (unsigned)e);
else
else
qm.mul2k(d, (unsigned)-e);
qm.set(o, n, d);
qm.set(o, n, d);
}
bool hwf_manager::is_zero(hwf const & x) {
@ -559,13 +559,13 @@ bool hwf_manager::is_denormal(hwf const & x) {
(t & 0x000FFFFFFFFFFFFFull) != 0x0);
}
bool hwf_manager::is_regular(hwf const & x) {
bool hwf_manager::is_regular(hwf const & x) {
// Everything that doesn't have the top-exponent is considered regular.
// Note that +-0.0 and denormal numbers have exponent==0; these are regular.
// All normal numbers are also regular. What remains is +-Inf and NaN, they are
// All normal numbers are also regular. What remains is +-Inf and NaN, they are
// not regular and they are the only numbers that have exponent 7FF.
uint64 e = RAW(x.value) & 0x7FF0000000000000ull; // the exponent
return (e != 0x7FF0000000000000ull);
return (e != 0x7FF0000000000000ull);
}
bool hwf_manager::is_int(hwf const & x) {
@ -596,8 +596,8 @@ void hwf_manager::mk_pzero(hwf & o) {
}
void hwf_manager::mk_zero(bool sign, hwf & o) {
if (sign)
mk_nzero(o);
if (sign)
mk_nzero(o);
else
mk_pzero(o);
}
@ -627,7 +627,7 @@ void hwf_manager::mk_ninf(hwf & o) {
#ifdef USE_INTRINSICS
#define SETRM(RM) _MM_SET_ROUNDING_MODE(RM)
#else
#define SETRM(RM) _controlfp_s(&sse2_state, RM, _MCW_RC);
#define SETRM(RM) _controlfp_s(&sse2_state, RM, _MCW_RC);
#endif
#else
#ifdef USE_INTRINSICS
@ -691,7 +691,7 @@ void hwf_manager::set_rounding_mode(mpf_rounding_mode rm)
#endif
#else // OSX/Linux
switch (rm) {
case MPF_ROUND_NEAREST_TEVEN:
case MPF_ROUND_NEAREST_TEVEN:
SETRM(FE_TONEAREST);
break;
case MPF_ROUND_TOWARD_POSITIVE: