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.
This commit is contained in:
Leonardo de Moura
parent
e938a75361
commit
ee3589d99c
9 changed files with 1 additions and 331 deletions
|
|
@ -4,21 +4,12 @@ add_exec_test(mpq "mpq")
|
|||
add_executable(mpz mpz.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(mpz ${EXTRA_LIBS})
|
||||
add_exec_test(mpz "mpz")
|
||||
add_executable(double double.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(double ${EXTRA_LIBS})
|
||||
add_exec_test(double "double")
|
||||
add_executable(float float.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(float ${EXTRA_LIBS})
|
||||
add_exec_test(float "float")
|
||||
add_executable(xnumeral xnumeral.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(xnumeral ${EXTRA_LIBS})
|
||||
add_exec_test(xnumeral "xnumeral")
|
||||
add_executable(primes primes.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(primes ${EXTRA_LIBS})
|
||||
add_exec_test(primes "primes")
|
||||
add_executable(numeric_traits numeric_traits.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(numeric_traits ${EXTRA_LIBS})
|
||||
add_exec_test(numeric_traits "numeric_traits")
|
||||
add_executable(gcd gcd.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:numerics> $<TARGET_OBJECTS:sexpr>)
|
||||
target_link_libraries(gcd ${EXTRA_LIBS})
|
||||
add_exec_test(gcd "gcd")
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
@ -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;
|
||||
}
|
||||
|
|
@ -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<typename T>
|
||||
void tst_num(T const & a) {
|
||||
std::cout << "value: " << a << "\n";
|
||||
std::cout << "is value zero: " << std::boolalpha << numeric_traits<T>::is_zero(a) << "\n";
|
||||
std::cout << "zero: " << numeric_traits<T>::zero() << "\n";
|
||||
std::cout << "is type precise: " << std::boolalpha << numeric_traits<T>::precise() << "\n";
|
||||
std::cout << "typeid: " << typeid(T).name() << "\n";
|
||||
lean_assert(numeric_traits<T>::is_zero(numeric_traits<T>::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<float>(1.0));
|
||||
}
|
||||
|
||||
int main() {
|
||||
initialize_util_module();
|
||||
initialize_numerics_module();
|
||||
tst1();
|
||||
finalize_numerics_module();
|
||||
finalize_util_module();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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 <cmath>
|
||||
#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<double>::g_zero = 0.0;
|
||||
double numeric_traits<double>::g_one = 1.0;
|
||||
|
||||
double numeric_traits<double>::log(double d) {
|
||||
return std::log(d);
|
||||
}
|
||||
};
|
||||
|
|
@ -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 <cstddef>
|
||||
#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<double> {
|
||||
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);
|
||||
};
|
||||
}
|
||||
|
|
@ -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 <cmath>
|
||||
#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<float>::zero() {
|
||||
return g_zero;
|
||||
}
|
||||
|
||||
static float g_one = 1.0;
|
||||
float const & numeric_traits<float>::one() {
|
||||
return g_one;
|
||||
}
|
||||
};
|
||||
|
|
@ -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 <cstddef>
|
||||
#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<float> {
|
||||
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<double>(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; }
|
||||
};
|
||||
}
|
||||
Loading…
Add table
Reference in a new issue