From 93b99cf1ec74edbed8ad81490d40cacc4e727722 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Wed, 7 Aug 2013 19:26:10 -0700 Subject: [PATCH] Add constants(Pi, 1/2Pi, 2Pi) to double, float, and mpq --- src/util/numerics/double.cpp | 2 +- src/util/numerics/double.h | 23 +++++++++++++++++++---- src/util/numerics/float.cpp | 2 +- src/util/numerics/float.h | 23 +++++++++++++++++++---- src/util/numerics/mpq.cpp | 4 ++++ src/util/numerics/mpq.h | 14 ++++++++++++++ 6 files changed, 58 insertions(+), 10 deletions(-) diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp index 532489df94..3b52d43b7a 100644 --- a/src/util/numerics/double.cpp +++ b/src/util/numerics/double.cpp @@ -10,7 +10,7 @@ Author: Soonho Kong namespace lean { -mpfr_rnd_t numeric_traits::rnd = MPFR_RNDN; +thread_local mpfr_rnd_t numeric_traits::rnd = MPFR_RNDN; void double_power(double & v, unsigned k) { v = std::pow(v, k); diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h index 3cce1720df..d1f6be2f3d 100644 --- a/src/util/numerics/double.h +++ b/src/util/numerics/double.h @@ -17,15 +17,16 @@ namespace lean { void double_power(double & v, unsigned k); // Macro to implement transcendental functions using MPFR -#define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \ - static thread_local mpfp t(v, 53); \ - t.f(rnd); \ +#define LEAN_TRANS_DOUBLE_FUNC(f, v, rnd) \ + static thread_local mpfp t(v, 53); \ + t = v; \ + t.f(rnd); \ v = t.get_double(rnd); template<> class numeric_traits { public: - static mpfr_rnd_t rnd; + static thread_local mpfr_rnd_t rnd; static bool precise() { return false; } static bool is_zero(double v) { return v == 0.0; } static bool is_pos(double v) { return v > 0.0; } @@ -37,6 +38,20 @@ public: // v <- v^k static void power(double & v, unsigned k) { double_power(v, k); } + // constants + static const double constexpr pi_l = (3373259426.0 + 273688.0 / (1<<21)) / (1<<30); + static const double constexpr pi_n = (3373259426.0 + 273688.0 / (1<<21)) / (1<<30); + static const double constexpr pi_u = (3373259426.0 + 273689.0 / (1<<21)) / (1<<30); + static inline double pi_lower() { return pi_l; } + static inline double pi() { return pi_n; } + static inline double pi_upper() { return pi_u; } + static inline double pi_half_lower() { return pi_l / 2; } + static inline double pi_half() { return pi_n / 2; } + static inline double pi_half_upper() { return pi_u / 2; } + static inline double pi_twice_lower() { return pi_l * 2; } + static inline double pi_twice() { return pi_n * 2; } + static inline double pi_twice_upper() { return pi_u * 2; } + // Transcendental functions using MPFR static void exp(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp, v, rnd); } static void exp2(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp2, v, rnd); } diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp index 5ab1db0a17..ee85bd349f 100644 --- a/src/util/numerics/float.cpp +++ b/src/util/numerics/float.cpp @@ -10,7 +10,7 @@ Author: Soonho Kong namespace lean { -mpfr_rnd_t numeric_traits::rnd = MPFR_RNDN; +thread_local mpfr_rnd_t numeric_traits::rnd = MPFR_RNDN; void float_power(double & v, unsigned k) { v = std::pow(v, k); diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h index 71526d2a90..4e396d1d83 100644 --- a/src/util/numerics/float.h +++ b/src/util/numerics/float.h @@ -17,15 +17,16 @@ namespace lean { void float_power(float & v, unsigned k); // Macro to implement transcendental functions using MPFR -#define LEAN_TRANS_FLOAT_FUNC(f, v, rnd) \ - static thread_local mpfp t(v, 24); \ - t.f(rnd); \ +#define LEAN_TRANS_FLOAT_FUNC(f, v, rnd) \ + static thread_local mpfp t(v, 24); \ + t = v; \ + t.f(rnd); \ v = t.get_float(rnd); template<> class numeric_traits { public: - static mpfr_rnd_t rnd; + static thread_local mpfr_rnd_t rnd; static bool precise() { return false; } static bool is_zero(float v) { return v == 0.0; } static bool is_pos(float v) { return v > 0.0; } @@ -37,6 +38,20 @@ public: // v <- v^k static void power(float & v, unsigned k) { float_power(v, k); } + // constants + static const float constexpr pi_l = 13176794.0f/(1<<22); + static const float constexpr pi_n = 13176795.0f/(1<<22); + static const float constexpr pi_u = 13176795.0f/(1<<22); + static inline float pi_lower() { return pi_l; } + static inline float pi() { return pi_n; } + static inline float pi_upper() { return pi_u; } + static inline float pi_half_lower() { return pi_l / 2; } + static inline float pi_half() { return pi_n / 2; } + static inline float pi_half_upper() { return pi_u / 2; } + static inline float pi_twice_lower() { return pi_l * 2; } + static inline float pi_twice() { return pi_n * 2; } + static inline float pi_twice_upper() { return pi_u * 2; } + // Transcendental functions using MPFR static void exp(float & v) { LEAN_TRANS_FLOAT_FUNC(exp, v, rnd); } static void exp2(float & v) { LEAN_TRANS_FLOAT_FUNC(exp2, v, rnd); } diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp index f439bf3156..2419cd09d1 100644 --- a/src/util/numerics/mpq.cpp +++ b/src/util/numerics/mpq.cpp @@ -9,6 +9,10 @@ Author: Leonardo de Moura namespace lean { +const mpq numeric_traits::pi_l((3373259426.0 + 273688.0 / (1<<21)) / (1<<30)); +const mpq numeric_traits::pi_n((3373259426.0 + 273688.0 / (1<<21)) / (1<<30)); +const mpq numeric_traits::pi_u((3373259426.0 + 273688.0 / (1<<21)) / (1<<30)); + mpq & mpq::operator=(mpbq const & b) { *this = 2; power(*this, *this, b.get_k()); diff --git a/src/util/numerics/mpq.h b/src/util/numerics/mpq.h index 0b82690797..30ee70c1a8 100644 --- a/src/util/numerics/mpq.h +++ b/src/util/numerics/mpq.h @@ -224,6 +224,20 @@ public: // v <- v^k static void power(mpq & v, unsigned k) { _power(v, v, k); } + // constants + static const mpq pi_l; + static const mpq pi_n; + static const mpq pi_u; + static inline mpq pi_lower() { return pi_l; } + static inline mpq pi() { return pi_n; } + static inline mpq pi_upper() { return pi_u; } + static inline mpq pi_half_lower() { return pi_l / 2; } + static inline mpq pi_half() { return pi_n / 2; } + static inline mpq pi_half_upper() { return pi_u / 2; } + static inline mpq pi_twice_lower() { return pi_l * 2; } + static inline mpq pi_twice() { return pi_n * 2; } + static inline mpq pi_twice_upper() { return pi_u * 2; } + // Transcendental functions static void exp(mpq & v) { lean_unreachable(); /* TODO */ } static void exp2(mpq & v) { lean_unreachable(); /* TODO */ }