michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix cygwin error caused by the use of thread_local in numerics/float class

Browse source
This commit is contained in:
Soonho Kong 2013-08-15 13:49:15 -07:00
parent 96c4343b0c
commit a6f3122146
3 changed files with 34 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/numerics/double.cpp
View file

@ -11,12 +11,10 @@ Author: Soonho Kong
namespace lean { namespace lean {
static thread_local mpfr_rnd_t g_rnd; static thread_local mpfr_rnd_t g_rnd;
void set_double_rnd(bool plus_inf) { void set_double_rnd(bool plus_inf) {
g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD;
} }
mpfr_rnd_t get_double_rnd() { mpfr_rnd_t get_double_rnd() {
return g_rnd; return g_rnd;
} }

9
src/util/numerics/float.cpp
View file

@ -10,7 +10,14 @@ Author: Soonho Kong
namespace lean { namespace lean {
thread_local mpfr_rnd_t numeric_traits<float>::rnd = MPFR_RNDN; static thread_local mpfr_rnd_t g_rnd;
void set_float_rnd(bool plus_inf) {
g_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD;
}
mpfr_rnd_t get_float_rnd() {
return g_rnd;
}
void float_power(float & v, unsigned k) { v = std::pow(v, k); } void float_power(float & v, unsigned k) { v = std::pow(v, k); }
void float_abs(float & v) { v = std::abs(v); } void float_abs(float & v) { v = std::abs(v); }

49
src/util/numerics/float.h
View file

@ -26,15 +26,18 @@ void float_floor(float & v);
t.f(rnd); \ t.f(rnd); \
v = t.get_float(rnd); v = t.get_float(rnd);
void set_float_rnd(bool plus_inf);
mpfr_rnd_t get_float_rnd();
template<> template<>
class numeric_traits<float> { class numeric_traits<float> {
public: public:
static thread_local mpfr_rnd_t rnd;
static bool precise() { return false; } static bool precise() { return false; }
static bool is_zero(float v) { return v == 0.0; } static bool is_zero(float v) { return v == 0.0; }
static bool is_pos(float v) { return v > 0.0; } static bool is_pos(float v) { return v > 0.0; }
static bool is_neg(float v) { return v < 0.0; } static bool is_neg(float v) { return v < 0.0; }
static void set_rounding(bool plus_inf) { rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; } static mpfr_rnd_t rnd() { return get_float_rnd(); }
static void set_rounding(bool plus_inf) { set_float_rnd(plus_inf); }
static void neg(float & v) { v = -v; } static void neg(float & v) { v = -v; }
static void inv(float & v) { v = 1.0/v; } static void inv(float & v) { v = 1.0/v; }
static void reset(float & v) { v = 0.0; } static void reset(float & v) { v = 0.0; }
@ -66,26 +69,26 @@ public:
static inline float pi_twice_upper() { return pi_u * 2; } static inline float pi_twice_upper() { return pi_u * 2; }
// Transcendental functions using MPFR // Transcendental functions using MPFR
static void exp(float & v) { LEAN_TRANS_FLOAT_FUNC(exp, v, rnd); } static void exp(float & v) { LEAN_TRANS_FLOAT_FUNC(exp, v, rnd()); }
static void exp2(float & v) { LEAN_TRANS_FLOAT_FUNC(exp2, v, rnd); } static void exp2(float & v) { LEAN_TRANS_FLOAT_FUNC(exp2, v, rnd()); }
static void exp10(float & v) { LEAN_TRANS_FLOAT_FUNC(exp10, v, rnd); } static void exp10(float & v) { LEAN_TRANS_FLOAT_FUNC(exp10, v, rnd()); }
static void log(float & v) { LEAN_TRANS_FLOAT_FUNC(log, v, rnd); } static void log(float & v) { LEAN_TRANS_FLOAT_FUNC(log, v, rnd()); }
static void log2(float & v) { LEAN_TRANS_FLOAT_FUNC(log2, v, rnd); } static void log2(float & v) { LEAN_TRANS_FLOAT_FUNC(log2, v, rnd()); }
static void log10(float & v) { LEAN_TRANS_FLOAT_FUNC(log10, v, rnd); } static void log10(float & v) { LEAN_TRANS_FLOAT_FUNC(log10, v, rnd()); }
static void sin(float & v) { LEAN_TRANS_FLOAT_FUNC(sin, v, rnd); } static void sin(float & v) { LEAN_TRANS_FLOAT_FUNC(sin, v, rnd()); }
static void cos(float & v) { LEAN_TRANS_FLOAT_FUNC(cos, v, rnd); } static void cos(float & v) { LEAN_TRANS_FLOAT_FUNC(cos, v, rnd()); }
static void tan(float & v) { LEAN_TRANS_FLOAT_FUNC(tan, v, rnd); } static void tan(float & v) { LEAN_TRANS_FLOAT_FUNC(tan, v, rnd()); }
static void sec(float & v) { LEAN_TRANS_FLOAT_FUNC(sec, v, rnd); } static void sec(float & v) { LEAN_TRANS_FLOAT_FUNC(sec, v, rnd()); }
static void csc(float & v) { LEAN_TRANS_FLOAT_FUNC(csc, v, rnd); } static void csc(float & v) { LEAN_TRANS_FLOAT_FUNC(csc, v, rnd()); }
static void cot(float & v) { LEAN_TRANS_FLOAT_FUNC(cot, v, rnd); } static void cot(float & v) { LEAN_TRANS_FLOAT_FUNC(cot, v, rnd()); }
static void asin(float & v) { LEAN_TRANS_FLOAT_FUNC(asin, v, rnd); } static void asin(float & v) { LEAN_TRANS_FLOAT_FUNC(asin, v, rnd()); }
static void acos(float & v) { LEAN_TRANS_FLOAT_FUNC(acos, v, rnd); } static void acos(float & v) { LEAN_TRANS_FLOAT_FUNC(acos, v, rnd()); }
static void atan(float & v) { LEAN_TRANS_FLOAT_FUNC(atan, v, rnd); } static void atan(float & v) { LEAN_TRANS_FLOAT_FUNC(atan, v, rnd()); }
static void sinh(float & v) { LEAN_TRANS_FLOAT_FUNC(sinh, v, rnd); } static void sinh(float & v) { LEAN_TRANS_FLOAT_FUNC(sinh, v, rnd()); }
static void cosh(float & v) { LEAN_TRANS_FLOAT_FUNC(cosh, v, rnd); } static void cosh(float & v) { LEAN_TRANS_FLOAT_FUNC(cosh, v, rnd()); }
static void tanh(float & v) { LEAN_TRANS_FLOAT_FUNC(tanh, v, rnd); } static void tanh(float & v) { LEAN_TRANS_FLOAT_FUNC(tanh, v, rnd()); }
static void asinh(float & v) { LEAN_TRANS_FLOAT_FUNC(asinh, v, rnd); } static void asinh(float & v) { LEAN_TRANS_FLOAT_FUNC(asinh, v, rnd()); }
static void acosh(float & v) { LEAN_TRANS_FLOAT_FUNC(acosh, v, rnd); } static void acosh(float & v) { LEAN_TRANS_FLOAT_FUNC(acosh, v, rnd()); }
static void atanh(float & v) { LEAN_TRANS_FLOAT_FUNC(atanh, v, rnd); } static void atanh(float & v) { LEAN_TRANS_FLOAT_FUNC(atanh, v, rnd()); }
}; };
} }