From fb41a4f5a37dc79c95ec69a99dd9370d28f333f9 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Tue, 6 Aug 2013 19:52:53 -0700 Subject: [PATCH] Add numeric_traits for double and float --- src/util/numerics/double.cpp | 18 ++++++ src/util/numerics/double.h | 63 ++++++++++++++++++ src/util/numerics/float.cpp | 18 ++++++ src/util/numerics/float.h | 63 ++++++++++++++++++ src/util/numerics/numeric_traits.cpp | 10 --- src/util/numerics/numeric_traits.h | 97 ---------------------------- 6 files changed, 162 insertions(+), 107 deletions(-) create mode 100644 src/util/numerics/double.cpp create mode 100644 src/util/numerics/double.h create mode 100644 src/util/numerics/float.cpp create mode 100644 src/util/numerics/float.h diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp new file mode 100644 index 000000000..532489df9 --- /dev/null +++ b/src/util/numerics/double.cpp @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "numeric_traits.h" +#include "double.h" +#include + +namespace lean { + +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 new file mode 100644 index 000000000..3cce1720d --- /dev/null +++ b/src/util/numerics/double.h @@ -0,0 +1,63 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#pragma once +#include +#include "mpfp.h" + +namespace lean { + +/** + \brief Template specializations define traits for native and lean + numeric types. +*/ +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); \ + v = t.get_double(rnd); + +template<> +class numeric_traits { +public: + static 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; } + static bool is_neg(double v) { return v < 0.0; } + static void set_rounding(bool plus_inf) { rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; } + static void neg(double & v) { v = -v; } + static void inv(double & v) { v = 1.0/v; } + static void reset(double & v) { v = 0.0; } + // v <- v^k + static void power(double & v, unsigned k) { double_power(v, k); } + + // 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); } + static void exp10(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp10, v, rnd); } + static void log(double & v) { LEAN_TRANS_DOUBLE_FUNC(log, v, rnd); } + static void log2(double & v) { LEAN_TRANS_DOUBLE_FUNC(log2, v, rnd); } + static void log10(double & v) { LEAN_TRANS_DOUBLE_FUNC(log10, v, rnd); } + static void sin(double & v) { LEAN_TRANS_DOUBLE_FUNC(sin, v, rnd); } + static void cos(double & v) { LEAN_TRANS_DOUBLE_FUNC(cos, v, rnd); } + static void tan(double & v) { LEAN_TRANS_DOUBLE_FUNC(tan, v, rnd); } + static void sec(double & v) { LEAN_TRANS_DOUBLE_FUNC(sec, v, rnd); } + static void csc(double & v) { LEAN_TRANS_DOUBLE_FUNC(csc, v, rnd); } + static void cot(double & v) { LEAN_TRANS_DOUBLE_FUNC(cot, v, rnd); } + static void asin(double & v) { LEAN_TRANS_DOUBLE_FUNC(asin, v, rnd); } + static void acos(double & v) { LEAN_TRANS_DOUBLE_FUNC(acos, v, rnd); } + static void atan(double & v) { LEAN_TRANS_DOUBLE_FUNC(atan, v, rnd); } + static void sinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(sinh, v, rnd); } + static void cosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(cosh, v, rnd); } + static void tanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(tanh, v, rnd); } + static void asinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(asinh, v, rnd); } + static void acosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(acosh, v, rnd); } + static void atanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(atanh, v, rnd); } +}; +} diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp new file mode 100644 index 000000000..5ab1db0a1 --- /dev/null +++ b/src/util/numerics/float.cpp @@ -0,0 +1,18 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "numeric_traits.h" +#include "float.h" +#include + +namespace lean { + +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 new file mode 100644 index 000000000..71526d2a9 --- /dev/null +++ b/src/util/numerics/float.h @@ -0,0 +1,63 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#pragma once +#include +#include "mpfp.h" + +namespace lean { + +/** + \brief Template specializations define traits for native and lean + numeric types. +*/ +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); \ + v = t.get_float(rnd); + +template<> +class numeric_traits { +public: + static 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; } + 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 void neg(float & v) { v = -v; } + static void inv(float & v) { v = 1.0/v; } + static void reset(float & v) { v = 0.0; } + // v <- v^k + static void power(float & v, unsigned k) { float_power(v, k); } + + // 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); } + 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 log2(float & v) { LEAN_TRANS_FLOAT_FUNC(log2, 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 cos(float & v) { LEAN_TRANS_FLOAT_FUNC(cos, 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 csc(float & v) { LEAN_TRANS_FLOAT_FUNC(csc, 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 acos(float & v) { LEAN_TRANS_FLOAT_FUNC(acos, 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 cosh(float & v) { LEAN_TRANS_FLOAT_FUNC(cosh, 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 acosh(float & v) { LEAN_TRANS_FLOAT_FUNC(acosh, v, rnd); } + static void atanh(float & v) { LEAN_TRANS_FLOAT_FUNC(atanh, v, rnd); } +}; +} diff --git a/src/util/numerics/numeric_traits.cpp b/src/util/numerics/numeric_traits.cpp index ce261f7d4..8a230f2e6 100644 --- a/src/util/numerics/numeric_traits.cpp +++ b/src/util/numerics/numeric_traits.cpp @@ -11,20 +11,10 @@ Author: Leonardo de Moura namespace lean { -mpfr_rnd_t numeric_traits::rnd = MPFR_RNDN; -mpfr_rnd_t numeric_traits::rnd = MPFR_RNDN; void set_processor_rounding(bool plus_inf) { if (plus_inf) std::fesetround(FE_UPWARD); else std::fesetround(FE_DOWNWARD); } - -void double_power(double & v, unsigned k) { - v = std::pow(v, k); -} -void float_power(float & v, unsigned k) { - v = std::pow(v, k); -} - }; diff --git a/src/util/numerics/numeric_traits.h b/src/util/numerics/numeric_traits.h index 1ddc4ba5b..53633c590 100644 --- a/src/util/numerics/numeric_traits.h +++ b/src/util/numerics/numeric_traits.h @@ -6,7 +6,6 @@ Author: Leonardo de Moura Soonho Kong */ #pragma once -#include namespace lean { @@ -19,101 +18,5 @@ class numeric_traits { }; void set_processor_rounding(bool plus_inf); -void double_power(double & v, unsigned k); -void float_power(float & v, unsigned k); - -// Macro to implement transcendental functions using MPFR -#define LEAN_TRANS_FLOAT_FUNC(f, v) mpfr_t t; \ - mpfr_init2(t, 24); /* precision of float = 24bit */ \ - mpfr_set_flt(t, v, rnd); \ - mpfr_##f(t, t, rnd); \ - v = mpfr_get_flt(t, rnd); \ - mpfr_clear (t); \ - -// Macro to implement transcendental functions using MPFR -#define LEAN_TRANS_DOUBLE_FUNC(f, v) mpfr_t t; \ - mpfr_init2(t, 53); /* precision of double = 53bit */ \ - mpfr_set_d(t, v, rnd); \ - mpfr_##f(t, t, rnd); \ - v = mpfr_get_d(t, rnd); \ - mpfr_clear (t); \ - -template<> -class numeric_traits { -public: - static 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; } - static bool is_neg(double v) { return v < 0.0; } - static void set_rounding(bool plus_inf) { rnd = plus_inf ? MPFR_RNDU : MPFR_RNDD; } - static void neg(double & v) { v = -v; } - static void inv(double & v) { v = 1.0/v; } - static void reset(double & v) { v = 0.0; } - // v <- v^k - static void power(double & v, unsigned k) { double_power(v, k); } - - // Transcendental functions using MPFR - static void exp(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp, v); } - static void exp2(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp2, v); } - static void exp10(double & v) { LEAN_TRANS_DOUBLE_FUNC(exp10, v); } - static void log(double & v) { LEAN_TRANS_DOUBLE_FUNC(log, v); } - static void log2(double & v) { LEAN_TRANS_DOUBLE_FUNC(log2, v); } - static void log10(double & v) { LEAN_TRANS_DOUBLE_FUNC(log10, v); } - static void sin(double & v) { LEAN_TRANS_DOUBLE_FUNC(sin, v); } - static void cos(double & v) { LEAN_TRANS_DOUBLE_FUNC(cos, v); } - static void tan(double & v) { LEAN_TRANS_DOUBLE_FUNC(tan, v); } - static void sec(double & v) { LEAN_TRANS_DOUBLE_FUNC(sec, v); } - static void csc(double & v) { LEAN_TRANS_DOUBLE_FUNC(csc, v); } - static void cot(double & v) { LEAN_TRANS_DOUBLE_FUNC(cot, v); } - static void asin(double & v) { LEAN_TRANS_DOUBLE_FUNC(asin, v); } - static void acos(double & v) { LEAN_TRANS_DOUBLE_FUNC(acos, v); } - static void atan(double & v) { LEAN_TRANS_DOUBLE_FUNC(atan, v); } - static void sinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(sinh, v); } - static void cosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(cosh, v); } - static void tanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(tanh, v); } - static void asinh(double & v) { LEAN_TRANS_DOUBLE_FUNC(asinh, v); } - static void acosh(double & v) { LEAN_TRANS_DOUBLE_FUNC(acosh, v); } - static void atanh(double & v) { LEAN_TRANS_DOUBLE_FUNC(atanh, v); } -}; - -template<> -class numeric_traits { -public: - static 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; } - 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 void neg(float & v) { v = -v; } - static void inv(float & v) { v = 1.0/v; } - static void reset(float & v) { v = 0.0; } - // v <- v^k - static void power(float & v, unsigned k) { float_power(v, k); } - - // Transcendental functions using MPFR - static void exp(float & v) { LEAN_TRANS_FLOAT_FUNC(exp, v); } - static void exp2(float & v) { LEAN_TRANS_FLOAT_FUNC(exp2, v); } - static void exp10(float & v) { LEAN_TRANS_FLOAT_FUNC(exp10, v); } - static void log(float & v) { LEAN_TRANS_FLOAT_FUNC(log, v); } - static void log2(float & v) { LEAN_TRANS_FLOAT_FUNC(log2, v); } - static void log10(float & v) { LEAN_TRANS_FLOAT_FUNC(log10, v); } - static void sin(float & v) { LEAN_TRANS_FLOAT_FUNC(sin, v); } - static void cos(float & v) { LEAN_TRANS_FLOAT_FUNC(cos, v); } - static void tan(float & v) { LEAN_TRANS_FLOAT_FUNC(tan, v); } - static void sec(float & v) { LEAN_TRANS_FLOAT_FUNC(sec, v); } - static void csc(float & v) { LEAN_TRANS_FLOAT_FUNC(csc, v); } - static void cot(float & v) { LEAN_TRANS_FLOAT_FUNC(cot, v); } - static void asin(float & v) { LEAN_TRANS_FLOAT_FUNC(asin, v); } - static void acos(float & v) { LEAN_TRANS_FLOAT_FUNC(acos, v); } - static void atan(float & v) { LEAN_TRANS_FLOAT_FUNC(atan, v); } - static void sinh(float & v) { LEAN_TRANS_FLOAT_FUNC(sinh, v); } - static void cosh(float & v) { LEAN_TRANS_FLOAT_FUNC(cosh, v); } - static void tanh(float & v) { LEAN_TRANS_FLOAT_FUNC(tanh, v); } - static void asinh(float & v) { LEAN_TRANS_FLOAT_FUNC(asinh, v); } - static void acosh(float & v) { LEAN_TRANS_FLOAT_FUNC(acosh, v); } - static void atanh(float & v) { LEAN_TRANS_FLOAT_FUNC(atanh, v); } -}; }