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

Add constants(Pi, 1/2Pi, 2Pi) to double, float, and mpq

Browse source
This commit is contained in:
Soonho Kong 2013-08-07 19:26:10 -07:00
parent 3bdfdcc36c
commit 93b99cf1ec
6 changed files with 58 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -10,7 +10,7 @@ Author: Soonho Kong
namespace lean {
mpfr_rnd_t numeric_traits<double>::rnd = MPFR_RNDN;
thread_local mpfr_rnd_t numeric_traits<double>::rnd = MPFR_RNDN;
void double_power(double & v, unsigned k) {
v = std::pow(v, k);

23
src/util/numerics/double.h
View file

@ -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<double> {
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); }

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

@ -10,7 +10,7 @@ Author: Soonho Kong
namespace lean {
mpfr_rnd_t numeric_traits<float>::rnd = MPFR_RNDN;
thread_local mpfr_rnd_t numeric_traits<float>::rnd = MPFR_RNDN;
void float_power(double & v, unsigned k) {
v = std::pow(v, k);

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

@ -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<float> {
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); }

4
src/util/numerics/mpq.cpp
View file

@ -9,6 +9,10 @@ Author: Leonardo de Moura
namespace lean {
const mpq numeric_traits<mpq>::pi_l((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
const mpq numeric_traits<mpq>::pi_n((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
const mpq numeric_traits<mpq>::pi_u((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
mpq & mpq::operator=(mpbq const & b) {
*this = 2;
power(*this, *this, b.get_k());

14
src/util/numerics/mpq.h
View file

@ -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 */ }