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

Update interval tests to reduce compile-time

Browse source
This commit is contained in:
Soonho Kong 2013-08-15 11:10:50 -07:00
parent 7059836e21
commit 25bfb58f17
4 changed files with 74 additions and 63 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

115
src/tests/interval/check.h
View file

@ -1,44 +1,77 @@
// Check F(I.lower()) \in F(I) and F(I.upper()) \in F(I).
#define check_bop(T, f, i, c) { \
cout << #f << "(" << #i << " " << i << ", " << c << ") = "; \
interval<T> tmp = f(i, c); \
cout << tmp << endl; \
if(!i.is_lower_inf()) { \
numeric_traits<T>::set_rounding(false); \
T l = i.lower(); \
numeric_traits<T>::f(l, c); \
cout << "\t" << #f << "(" << i.lower() << ", " << c << ") = " << l << endl; \
lean_assert(tmp.is_lower_inf() || \
((tmp.lower() <= l) && (tmp.is_upper_inf() || (l <= tmp.upper())))); \
} \
if(!i.is_upper_inf()) { \
numeric_traits<T>::set_rounding(true); \
T u = i.upper(); \
numeric_traits<T>::f(u, c); \
cout << "\t" << #f << "(" << i.upper() << ", " << c << ") = " << u << endl; \
lean_assert(tmp.is_upper_inf() || \
((tmp.is_lower_inf() || (tmp.lower() <= u)) && (u <= tmp.upper()))); \
} \
using std::cout;
using std::endl;
using namespace lean;
template <typename T1, typename T2, typename F>
void check_interval_bop(std::string const & fname, std::string const & varname, interval<T1> i, T2 c, interval<T1> r, F f) {
cout << fname << "(" << varname << " " << i << ", " << c << ") = ";
cout << r << endl;
if(!i.is_lower_inf()) {
T1 ll = i.lower();
T1 lu = i.lower();
numeric_traits<T1>::set_rounding(false);
f(ll, c);
numeric_traits<T1>::set_rounding(true);
f(lu, c);
cout << "\t" << fname << "(" << i.lower() << ", " << c << ") = [" << ll << ", " << lu << "]"<< endl;
lean_assert(r.is_lower_inf() ||
((r.lower() <= ll) && (r.is_upper_inf() || (ll <= r.upper()))));
lean_assert(r.is_lower_inf() ||
((r.lower() <= lu) && (r.is_upper_inf() || (lu <= r.upper()))));
}
if(!i.is_upper_inf()) {
T1 ul = i.upper();
T1 uu = i.upper();
numeric_traits<T1>::set_rounding(false);
f(ul, c);
numeric_traits<T1>::set_rounding(true);
f(uu, c);
cout << "\t" << fname << "(" << i.upper() << ", " << c << ") = [" << ul << ", " << uu << "]" << endl;
lean_assert(r.is_upper_inf() ||
((r.is_lower_inf() || (r.lower() <= ul)) && (ul <= r.upper())));
lean_assert(r.is_upper_inf() ||
((r.is_lower_inf() || (r.lower() <= uu)) && (uu <= r.upper())));
}
}
#define check_uop(T, f, i) { \
cout << #f << "(" << #i << " " << i << ") = "; \
interval<T> tmp = f(i); \
cout << tmp << endl; \
if(!i.is_lower_inf()) { \
numeric_traits<T>::set_rounding(false); \
T l = i.lower(); \
numeric_traits<T>::f(l); \
cout << "\t" << #f << "(" << i.lower() << ") = " << l << endl; \
lean_assert(tmp.is_lower_inf() || \
((tmp.lower() <= l) && (tmp.is_upper_inf() || (l <= tmp.upper())))); \
} \
if(!i.is_upper_inf()) { \
numeric_traits<T>::set_rounding(true); \
T u = i.upper(); \
numeric_traits<T>::f(u); \
cout << "\t" << #f << "(" << i.upper() << ") = " << u << endl; \
lean_assert(tmp.is_upper_inf() || \
((tmp.is_lower_inf() || (tmp.lower() <= u)) && (u <= tmp.upper()))); \
} \
template <typename T, typename F>
void check_interval_uop(std::string const & fname, std::string const & varname, interval<T> i, interval<T> r, F f) {
cout << fname << "(" << varname << " " << i << ") = ";
cout << r << endl;
if(!i.is_lower_inf()) {
T ll = i.lower();
T lu = i.lower();
numeric_traits<T>::set_rounding(false);
f(ll);
numeric_traits<T>::set_rounding(true);
f(lu);
cout << "\t" << fname << "(" << i.lower() << ") = [" << ll << ", " << lu << "]"<< endl;
lean_assert(r.is_lower_inf() ||
((r.lower() <= ll) && (r.is_upper_inf() || (ll <= r.upper()))));
lean_assert(r.is_lower_inf() ||
((r.lower() <= lu) && (r.is_upper_inf() || (lu <= r.upper()))));
}
if(!i.is_upper_inf()) {
T ul = i.upper();
T uu = i.upper();
numeric_traits<T>::set_rounding(false);
f(ul);
numeric_traits<T>::set_rounding(true);
f(uu);
cout << "\t" << fname << "(" << i.upper() << ") = [" << ul << ", " << uu << "]" << endl;
lean_assert(r.is_upper_inf() ||
((r.is_lower_inf() || (r.lower() <= ul)) && (ul <= r.upper())));
lean_assert(r.is_upper_inf() ||
((r.is_lower_inf() || (r.lower() <= uu)) && (uu <= r.upper())));
}
}
#define print_result(a, op, b, r) \
cout << a << " " << op << " " << b << " = " << r << endl;
#define check_bop(T, f, i, c) \
check_interval_bop(#f, #i, i, c, f(i, c), numeric_traits<T>::f)
#define check_uop(T, f, i) \
check_interval_uop(#f, #i, i, f(i), numeric_traits<T>::f)

7
src/tests/interval/double_interval.cpp
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Soonho Kong
*/
#include <vector>
#include "test.h"
#include "trace.h"
#include "double.h"
@ -17,12 +16,6 @@ using std::cout;
using std::endl;
typedef interval<double> di;
typedef interval<mpfp> fi;
template<typename T1, typename T2, typename T3>
void print_result(T1 a, std::string const & op, T2 b, T3 r) {
cout << a << " " << op << " " << b << " = " << r << endl;
}
static void double_interval_arith() {
di i1(1.0, 2.0);

7
src/tests/interval/float_interval.cpp
View file

@ -4,13 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Soonho Kong
*/
#include <vector>
#include "test.h"
#include "trace.h"
#include "float.h"
#include "interval_def.h"
#include "check.h"
#include <cmath>
using namespace lean;
@ -19,11 +17,6 @@ using std::endl;
typedef interval<float> flti;
template<typename T1, typename T2, typename T3>
void print_result(T1 a, std::string const & op, T2 b, T3 r) {
cout << a << " " << op << " " << b << " = " << r << endl;
}
static void float_interval_arith() {
flti i1(1.0, 2.0);
flti i2(3.0, 4.0);

8
src/tests/interval/mpfp_interval.cpp
View file

@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Soonho Kong
*/
#include <vector>
#include "test.h"
#include "trace.h"
#include "double.h"
#include "mpfp.h"
#include "interval_def.h"
#include "check.h"
@ -17,14 +15,8 @@ using namespace lean;
using std::cout;
using std::endl;
typedef interval<double> di;
typedef interval<mpfp> fi;
template<typename T1, typename T2, typename T3>
void print_result(T1 a, std::string const & op, T2 b, T3 r) {
cout << a << " " << op << " " << b << " = " << r << endl;
}
static void mpfp_interval_arith() {
fi i1(1.0, 2.0);
fi i2(3.0, 4.0);