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

Fix numeric_traits<mpfp>::pi constants

Browse source
This commit is contained in:
Soonho Kong 2013-08-13 20:06:19 -07:00
parent 8eb87fbeae
commit 5f143f164e
2 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/util/numerics/mpfp.cpp
View file

@ -10,8 +10,12 @@ Author: Soonho Kong
namespace lean {
static thread_local mpfr_rnd_t g_mpfp_rnd = MPFR_RNDN;
mpfp numeric_traits<mpfp>::pi_l;
mpfp numeric_traits<mpfp>::pi_n;
mpfp numeric_traits<mpfp>::pi_u;
void set_mpfp_rnd(bool plus_inf) {
g_mpfp_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD;
g_mpfp_rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD;
}
mpfr_rnd_t get_mpfp_rnd() {

12
src/util/numerics/mpfp.h
View file

@ -526,12 +526,12 @@ public:
mpfr_const_pi(pi_u.m_val, MPFR_RNDU);
return pi_u;
}
static inline mpfp pi_half_lower() { return pi_l / 2lu; }
static inline mpfp pi_half() { return pi_n / 2lu; }
static inline mpfp pi_half_upper() { return pi_u / 2lu; }
static inline mpfp pi_twice_lower() { return pi_l * 2lu; }
static inline mpfp pi_twice() { return pi_n * 2lu; }
static inline mpfp pi_twice_upper() { return pi_u * 2lu; }
static inline mpfp pi_half_lower() { return pi_lower() / 2lu; }
static inline mpfp pi_half() { return pi() / 2lu; }
static inline mpfp pi_half_upper() { return pi_upper() / 2lu; }
static inline mpfp pi_twice_lower() { return pi_lower() * 2lu; }
static inline mpfp pi_twice() { return pi() * 2lu; }
static inline mpfp pi_twice_upper() { return pi_upper() * 2lu; }
// Transcendental functions
static void exp(mpfp & v) { LEAN_TRANS_MPFP_FUNC(exp, v, rnd()); }