From ee3589d99ce7b79aad013cd6597e0ec8801927ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Apr 2018 09:31:41 -0700 Subject: [PATCH] chore(util/numerics): remove float/double These two abstractions were added when we planned to have an efficient Simplex module, written in C++, in Lean. We have moved this module to Z3. So, we don't need these abstractions anymore. --- src/tests/util/numerics/CMakeLists.txt | 9 --- src/tests/util/numerics/double.cpp | 51 ----------------- src/tests/util/numerics/float.cpp | 51 ----------------- src/tests/util/numerics/numeric_traits.cpp | 43 --------------- src/util/numerics/CMakeLists.txt | 2 +- src/util/numerics/double.cpp | 24 -------- src/util/numerics/double.h | 64 ---------------------- src/util/numerics/float.cpp | 27 --------- src/util/numerics/float.h | 61 --------------------- 9 files changed, 1 insertion(+), 331 deletions(-) delete mode 100644 src/tests/util/numerics/double.cpp delete mode 100644 src/tests/util/numerics/float.cpp delete mode 100644 src/tests/util/numerics/numeric_traits.cpp delete mode 100644 src/util/numerics/double.cpp delete mode 100644 src/util/numerics/double.h delete mode 100644 src/util/numerics/float.cpp delete mode 100644 src/util/numerics/float.h diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt index 31d2040e6f..a8ea2eb610 100644 --- a/src/tests/util/numerics/CMakeLists.txt +++ b/src/tests/util/numerics/CMakeLists.txt @@ -4,21 +4,12 @@ add_exec_test(mpq "mpq") add_executable(mpz mpz.cpp $ $ $) target_link_libraries(mpz ${EXTRA_LIBS}) add_exec_test(mpz "mpz") -add_executable(double double.cpp $ $ $) -target_link_libraries(double ${EXTRA_LIBS}) -add_exec_test(double "double") -add_executable(float float.cpp $ $ $) -target_link_libraries(float ${EXTRA_LIBS}) -add_exec_test(float "float") add_executable(xnumeral xnumeral.cpp $ $ $) target_link_libraries(xnumeral ${EXTRA_LIBS}) add_exec_test(xnumeral "xnumeral") add_executable(primes primes.cpp $ $ $) target_link_libraries(primes ${EXTRA_LIBS}) add_exec_test(primes "primes") -add_executable(numeric_traits numeric_traits.cpp $ $ $) -target_link_libraries(numeric_traits ${EXTRA_LIBS}) -add_exec_test(numeric_traits "numeric_traits") add_executable(gcd gcd.cpp $ $ $) target_link_libraries(gcd ${EXTRA_LIBS}) add_exec_test(gcd "gcd") diff --git a/src/tests/util/numerics/double.cpp b/src/tests/util/numerics/double.cpp deleted file mode 100644 index d98af88745..0000000000 --- a/src/tests/util/numerics/double.cpp +++ /dev/null @@ -1,51 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Soonho Kong -*/ -#include "util/test.h" -#include "util/numerics/double.h" -using namespace lean; - -static void abs() { - double d1 = -398723.3218937912; - double d2 = -9823.3487729; - double d3 = 0.0; - double d4 = 398.347389; - double d5 = 78398.30912; - double_abs(d1); - double_abs(d2); - double_abs(d3); - double_abs(d4); - double_abs(d5); - lean_assert_eq(d1, 398723.3218937912); - lean_assert_eq(d2, 9823.3487729); - lean_assert_eq(d3, 0.0); - lean_assert_eq(d4, 398.347389); - lean_assert_eq(d5, 78398.30912); -} - -static void ceil() { - double d1 = -398723.3218937912; - double d2 = -9823.3487729; - double d3 = 0.0; - double d4 = 398.347389; - double d5 = 78398.30912; - double_ceil(d1); - double_ceil(d2); - double_ceil(d3); - double_ceil(d4); - double_ceil(d5); - lean_assert_eq(d1, -398723); - lean_assert_eq(d2, -9823); - lean_assert_eq(d3, 0.0); - lean_assert_eq(d4, 399); - lean_assert_eq(d5, 78399); -} - -int main() { - abs(); - ceil(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/util/numerics/float.cpp b/src/tests/util/numerics/float.cpp deleted file mode 100644 index fa71588c21..0000000000 --- a/src/tests/util/numerics/float.cpp +++ /dev/null @@ -1,51 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Soonho Kong -*/ -#include "util/test.h" -#include "util/numerics/float.h" -using namespace lean; - -static void abs() { - float f1 = -398723.3218937912f; - float f2 = -9823.3487729f; - float f3 = 0.0; - float f4 = 398.347389f; - float f5 = 78398.30912f; - float_abs(f1); - float_abs(f2); - float_abs(f3); - float_abs(f4); - float_abs(f5); - lean_assert_eq(f1, 398723.3218937912f); - lean_assert_eq(f2, 9823.3487729f); - lean_assert_eq(f3, 0.0f); - lean_assert_eq(f4, 398.347389f); - lean_assert_eq(f5, 78398.30912f); -} - -static void ceil() { - float f1 = -398723.3218937912f; - float f2 = -9823.3487729f; - float f3 = 0.0; - float f4 = 398.347389f; - float f5 = 78398.30912f; - float_ceil(f1); - float_ceil(f2); - float_ceil(f3); - float_ceil(f4); - float_ceil(f5); - lean_assert_eq(f1, -398723); - lean_assert_eq(f2, -9823); - lean_assert_eq(f3, 0.0); - lean_assert_eq(f4, 399); - lean_assert_eq(f5, 78399); -} - -int main() { - abs(); - ceil(); - return has_violations() ? 1 : 0; -} diff --git a/src/tests/util/numerics/numeric_traits.cpp b/src/tests/util/numerics/numeric_traits.cpp deleted file mode 100644 index 1984c6ae44..0000000000 --- a/src/tests/util/numerics/numeric_traits.cpp +++ /dev/null @@ -1,43 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/test.h" -#include "util/init_module.h" -#include "util/numerics/init_module.h" -#include "util/numerics/mpq.h" -#include "util/numerics/mpz.h" -#include "util/numerics/double.h" -#include "util/numerics/float.h" -using namespace lean; - -template -void tst_num(T const & a) { - std::cout << "value: " << a << "\n"; - std::cout << "is value zero: " << std::boolalpha << numeric_traits::is_zero(a) << "\n"; - std::cout << "zero: " << numeric_traits::zero() << "\n"; - std::cout << "is type precise: " << std::boolalpha << numeric_traits::precise() << "\n"; - std::cout << "typeid: " << typeid(T).name() << "\n"; - lean_assert(numeric_traits::is_zero(numeric_traits::zero())); - std::cout << "\n"; -} - -static void tst1() { - tst_num(mpq(1, 2)); - tst_num(mpq(0)); - tst_num(mpz(3)); - tst_num(mpz(0)); - tst_num(1.0); - tst_num(static_cast(1.0)); -} - -int main() { - initialize_util_module(); - initialize_numerics_module(); - tst1(); - finalize_numerics_module(); - finalize_util_module(); - return has_violations() ? 1 : 0; -} diff --git a/src/util/numerics/CMakeLists.txt b/src/util/numerics/CMakeLists.txt index fb23eb5859..9d46975b29 100644 --- a/src/util/numerics/CMakeLists.txt +++ b/src/util/numerics/CMakeLists.txt @@ -1 +1 @@ -add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp float.cpp double.cpp numeric_traits.cpp primes.cpp zpz.cpp) +add_library(numerics OBJECT init_module.cpp mpz.cpp mpq.cpp numeric_traits.cpp primes.cpp zpz.cpp) diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp deleted file mode 100644 index 727fba68bd..0000000000 --- a/src/util/numerics/double.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Soonho Kong -*/ -#include -#include "util/thread.h" -#include "util/numerics/numeric_traits.h" -#include "util/numerics/double.h" - -namespace lean { -void double_power(double & v, unsigned k) { v = std::pow(v, k); } -void double_abs(double & v) { v = std::abs(v); } -void double_ceil(double & v) { v = std::ceil(v); } -void double_floor(double & v) { v = std::floor(v); } - -double numeric_traits::g_zero = 0.0; -double numeric_traits::g_one = 1.0; - -double numeric_traits::log(double d) { - return std::log(d); -} -}; diff --git a/src/util/numerics/double.h b/src/util/numerics/double.h deleted file mode 100644 index 67719732ad..0000000000 --- a/src/util/numerics/double.h +++ /dev/null @@ -1,64 +0,0 @@ -/* -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 "util/numerics/numeric_traits.h" - -namespace lean { -/** - \brief Template specializations define traits for native and lean - numeric types. -*/ -void double_power(double & v, unsigned k); -void double_abs(double & v); -void double_ceil(double & v); -void double_floor(double & v); - -template<> -class numeric_traits { -public: - 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 neg(double & v) { v = -v; } - static void inv(double & v) { v = 1.0/v; } - static void reset(double & v) { v = 0.0; } - static double g_zero; - static double const & zero() { return g_zero; } - static double g_one; - static double const & one() { return g_one; } - static void power(double & v, unsigned k) { double_power(v, k); } - static void abs(double & v) { double_abs(v); } - static void ceil(double & v) { double_ceil(v); } - static void floor(double & v) { double_floor(v); } - static double const & min(double const & v1, double const & v2) { - return v1 < v2 ? v1 : v2; - } - static double const & max(double const & v1, double const & v2) { - return v1 > v2 ? v1 : v2; - } - - static double const & get_double(double const & d) { return d;} - - // 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; } - - static double log(double d); -}; -} diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp deleted file mode 100644 index 07f96b7800..0000000000 --- a/src/util/numerics/float.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Soonho Kong -*/ -#include -#include "util/thread.h" -#include "util/numerics/numeric_traits.h" -#include "util/numerics/float.h" - -namespace lean { -void float_power(float & v, unsigned k) { v = std::pow(v, k); } -void float_abs(float & v) { v = std::abs(v); } -void float_ceil(float & v) { v = std::ceil(v); } -void float_floor(float & v) { v = std::floor(v); } - -static float g_zero = 0.0; -float const & numeric_traits::zero() { - return g_zero; -} - -static float g_one = 1.0; -float const & numeric_traits::one() { - return g_one; -} -}; diff --git a/src/util/numerics/float.h b/src/util/numerics/float.h deleted file mode 100644 index aaf2c83e7c..0000000000 --- a/src/util/numerics/float.h +++ /dev/null @@ -1,61 +0,0 @@ -/* -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 "util/numerics/numeric_traits.h" - -namespace lean { -/** - \brief Template specializations define traits for native and lean - numeric types. -*/ -void float_power(float & v, unsigned k); -void float_abs(float & v); -void float_ceil(float & v); -void float_floor(float & v); - -template<> -class numeric_traits { -public: - 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 neg(float & v) { v = -v; } - static void inv(float & v) { v = 1.0/v; } - static void reset(float & v) { v = 0.0; } - static float const & zero(); - static float const & one(); - - static void power(float & v, unsigned k) { float_power(v, k); } - static void abs(float & v) { float_abs(v); } - static void ceil(float & v) { float_ceil(v); } - static void floor(float & v) { float_floor(v); } - static double get_double(float const & d) { return static_cast(d); } - - static float const & min(float const & v1, float const & v2) { - return v1 < v2 ? v1 : v2; - } - static float const & max(float const & v1, float const & v2) { - return v1 > v2 ? v1 : v2; - } - - // 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; } -}; -}