Add {float,double,mpfp}_interval.cpp in tests/interval
This commit is contained in:
Soonho Kong
parent
840403db42
commit
56f4050932
6 changed files with 1554 additions and 505 deletions
|
|
@ -1080,7 +1080,6 @@ template<typename T> void interval<T>::tan() {
|
|||
|
||||
T const pi = numeric_traits<T>::pi();
|
||||
T const pi_half_lower = numeric_traits<T>::pi_half_lower();
|
||||
T const pi_half_upper = numeric_traits<T>::pi_half_upper();
|
||||
fmod(pi);
|
||||
|
||||
if (m_lower >= pi_half_lower) {
|
||||
|
|
|
|||
|
|
@ -1,3 +1,15 @@
|
|||
add_executable(interval_tst interval.cpp)
|
||||
target_link_libraries(interval_tst ${EXTRA_LIBS})
|
||||
add_test(interval ${CMAKE_CURRENT_BINARY_DIR}/interval_tst)
|
||||
|
||||
add_executable(float_interval_tst float_interval.cpp)
|
||||
target_link_libraries(float_interval_tst ${EXTRA_LIBS})
|
||||
add_test(interval ${CMAKE_CURRENT_BINARY_DIR}/float_interval_tst)
|
||||
|
||||
add_executable(double_interval_tst double_interval.cpp)
|
||||
target_link_libraries(double_interval_tst ${EXTRA_LIBS})
|
||||
add_test(interval ${CMAKE_CURRENT_BINARY_DIR}/double_interval_tst)
|
||||
|
||||
add_executable(mpfp_interval_tst mpfp_interval.cpp)
|
||||
target_link_libraries(mpfp_interval_tst ${EXTRA_LIBS})
|
||||
add_test(interval ${CMAKE_CURRENT_BINARY_DIR}/mpfp_interval_tst)
|
||||
|
|
|
|||
513
src/tests/interval/double_interval.cpp
Normal file
513
src/tests/interval/double_interval.cpp
Normal file
|
|
@ -0,0 +1,513 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
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"
|
||||
|
||||
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() {
|
||||
di i1(1.0, 2.0);
|
||||
di i2(3.0, 4.0);
|
||||
di i3(-10.0, -5.0);
|
||||
di i4(-3.0, +4.0);
|
||||
di i5(5.0, 8.0);
|
||||
|
||||
double c1 = 0.6;
|
||||
double c2 = 3.0;
|
||||
double c3 = 0.0;
|
||||
double c4 = -4.5;
|
||||
double c5 = -0.3;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "+", c1, i1 + c1);
|
||||
print_result(i2, "+", c2, i2 + c2);
|
||||
print_result(i3, "+", c3, i3 + c3);
|
||||
print_result(i4, "+", c4, i4 + c4);
|
||||
print_result(i5, "+", c5, i5 + c5);
|
||||
print_result(i5, "+", c1, i5 + c1);
|
||||
print_result(i4, "+", c2, i4 + c2);
|
||||
print_result(i2, "+", c4, i2 + c4);
|
||||
print_result(i1, "+", c5, i1 + c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "+", i1, c1 + i1);
|
||||
print_result(c2, "+", i2, c2 + i2);
|
||||
print_result(c3, "+", i3, c3 + i3);
|
||||
print_result(c4, "+", i4, c4 + i4);
|
||||
print_result(c5, "+", i5, c5 + i5);
|
||||
print_result(c5, "+", i1, c5 + i1);
|
||||
print_result(c4, "+", i2, c4 + i2);
|
||||
print_result(c2, "+", i4, c2 + i4);
|
||||
print_result(c1, "+", i5, c1 + i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "-", c1, i1 - c1);
|
||||
print_result(i2, "-", c2, i2 - c2);
|
||||
print_result(i3, "-", c3, i3 - c3);
|
||||
print_result(i4, "-", c4, i4 - c4);
|
||||
print_result(i5, "-", c5, i5 - c5);
|
||||
print_result(i5, "-", c1, i5 - c1);
|
||||
print_result(i4, "-", c2, i4 - c2);
|
||||
print_result(i2, "-", c4, i2 - c4);
|
||||
print_result(i1, "-", c5, i1 - c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "-", i1, c1 - i1);
|
||||
print_result(c2, "-", i2, c2 - i2);
|
||||
print_result(c3, "-", i3, c3 - i3);
|
||||
print_result(c4, "-", i4, c4 - i4);
|
||||
print_result(c5, "-", i5, c5 - i5);
|
||||
print_result(c5, "-", i1, c5 - i1);
|
||||
print_result(c4, "-", i2, c4 - i2);
|
||||
print_result(c2, "-", i4, c2 - i4);
|
||||
print_result(c1, "-", i5, c1 - i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "*", c1, i1 * c1);
|
||||
print_result(i2, "*", c2, i2 * c2);
|
||||
print_result(i3, "*", c3, i3 * c3);
|
||||
print_result(i4, "*", c4, i4 * c4);
|
||||
print_result(i5, "*", c5, i5 * c5);
|
||||
print_result(i5, "*", c1, i5 * c1);
|
||||
print_result(i4, "*", c2, i4 * c2);
|
||||
print_result(i2, "*", c4, i2 * c4);
|
||||
print_result(i1, "*", c5, i1 * c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "*", i1, c1 * i1);
|
||||
print_result(c2, "*", i2, c2 * i2);
|
||||
print_result(c3, "*", i3, c3 * i3);
|
||||
print_result(c4, "*", i4, c4 * i4);
|
||||
print_result(c5, "*", i5, c5 * i5);
|
||||
print_result(c5, "*", i1, c5 * i1);
|
||||
print_result(c4, "*", i2, c4 * i2);
|
||||
print_result(c2, "*", i4, c2 * i4);
|
||||
print_result(c1, "*", i5, c1 * i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "/", c1, i1 / c1);
|
||||
print_result(i2, "/", c2, i2 / c2);
|
||||
print_result(i3, "/", c3, i3 / c3);
|
||||
print_result(i4, "/", c4, i4 / c4);
|
||||
print_result(i5, "/", c5, i5 / c5);
|
||||
print_result(i5, "/", c1, i5 / c1);
|
||||
print_result(i4, "/", c2, i4 / c2);
|
||||
print_result(i2, "/", c4, i2 / c4);
|
||||
print_result(i1, "/", c5, i1 / c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "/", i1, c1 / i1);
|
||||
print_result(c2, "/", i2, c2 / i2);
|
||||
print_result(c3, "/", i3, c3 / i3);
|
||||
print_result(c5, "/", i5, c5 / i5);
|
||||
print_result(c5, "/", i1, c5 / i1);
|
||||
print_result(c4, "/", i2, c4 / i2);
|
||||
print_result(c1, "/", i5, c1 / i5);
|
||||
}
|
||||
|
||||
static void mpfp_interval_inf1() {
|
||||
di i1(1.0, 2.0);
|
||||
di inf;
|
||||
di ozero_pinf;
|
||||
di ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
di czero_pinf;
|
||||
di czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
cout << i1 << " * " << ozero_ninf << " = " << i1 * ozero_ninf << endl;
|
||||
cout << i1 << " * " << ozero_pinf << " = " << i1 * ozero_pinf << endl;
|
||||
cout << i1 << " * " << czero_ninf << " = " << i1 * czero_ninf << endl;
|
||||
cout << i1 << " * " << czero_pinf << " = " << i1 * czero_pinf << endl;
|
||||
lean_assert(i1 * ozero_ninf == ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
|
||||
lean_assert(i1 * ozero_pinf == ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
|
||||
lean_assert(i1 * czero_ninf == czero_ninf); lean_assert(czero_ninf * i1 == czero_ninf);
|
||||
lean_assert(i1 * czero_pinf == czero_pinf); lean_assert(czero_pinf * i1 == czero_pinf);
|
||||
|
||||
cout << "=== Addition between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " + " << ozero_ninf << " = " << ozero_ninf + ozero_ninf << endl;
|
||||
cout << ozero_ninf << " + " << ozero_pinf << " = " << ozero_ninf + ozero_pinf << endl;
|
||||
cout << ozero_ninf << " + " << czero_ninf << " = " << ozero_ninf + czero_ninf << endl;
|
||||
cout << ozero_ninf << " + " << czero_pinf << " = " << ozero_ninf + czero_pinf << endl;
|
||||
cout << ozero_pinf << " + " << ozero_ninf << " = " << ozero_pinf + ozero_ninf << endl;
|
||||
cout << ozero_pinf << " + " << ozero_pinf << " = " << ozero_pinf + ozero_pinf << endl;
|
||||
cout << ozero_pinf << " + " << czero_ninf << " = " << ozero_pinf + czero_ninf << endl;
|
||||
cout << ozero_pinf << " + " << czero_pinf << " = " << ozero_pinf + czero_pinf << endl;
|
||||
cout << czero_ninf << " + " << ozero_ninf << " = " << czero_ninf + ozero_ninf << endl;
|
||||
cout << czero_ninf << " + " << ozero_pinf << " = " << czero_ninf + ozero_pinf << endl;
|
||||
cout << czero_ninf << " + " << czero_ninf << " = " << czero_ninf + czero_ninf << endl;
|
||||
cout << czero_ninf << " + " << czero_pinf << " = " << czero_ninf + czero_pinf << endl;
|
||||
cout << czero_pinf << " + " << ozero_ninf << " = " << czero_pinf + ozero_ninf << endl;
|
||||
cout << czero_pinf << " + " << ozero_pinf << " = " << czero_pinf + ozero_pinf << endl;
|
||||
cout << czero_pinf << " + " << czero_ninf << " = " << czero_pinf + czero_ninf << endl;
|
||||
cout << czero_pinf << " + " << czero_pinf << " = " << czero_pinf + czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + ozero_pinf == inf);
|
||||
lean_assert(ozero_ninf + czero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + czero_pinf == inf);
|
||||
lean_assert(ozero_pinf + ozero_ninf == inf);
|
||||
lean_assert(ozero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf + czero_ninf == inf);
|
||||
lean_assert(ozero_pinf + czero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(czero_ninf + ozero_pinf == inf);
|
||||
lean_assert(czero_ninf + czero_ninf == czero_ninf);
|
||||
lean_assert(czero_ninf + czero_pinf == inf);
|
||||
lean_assert(czero_pinf + ozero_ninf == inf);
|
||||
lean_assert(czero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_pinf + czero_ninf == inf);
|
||||
lean_assert(czero_pinf + czero_pinf == czero_pinf);
|
||||
|
||||
cout << "=== Subtraction between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " - " << ozero_ninf << " = " << ozero_ninf - ozero_ninf << endl;
|
||||
cout << ozero_ninf << " - " << ozero_pinf << " = " << ozero_ninf - ozero_pinf << endl;
|
||||
cout << ozero_ninf << " - " << czero_ninf << " = " << ozero_ninf - czero_ninf << endl;
|
||||
cout << ozero_ninf << " - " << czero_pinf << " = " << ozero_ninf - czero_pinf << endl;
|
||||
cout << ozero_pinf << " - " << ozero_ninf << " = " << ozero_pinf - ozero_ninf << endl;
|
||||
cout << ozero_pinf << " - " << ozero_pinf << " = " << ozero_pinf - ozero_pinf << endl;
|
||||
cout << ozero_pinf << " - " << czero_ninf << " = " << ozero_pinf - czero_ninf << endl;
|
||||
cout << ozero_pinf << " - " << czero_pinf << " = " << ozero_pinf - czero_pinf << endl;
|
||||
cout << czero_ninf << " - " << ozero_ninf << " = " << czero_ninf - ozero_ninf << endl;
|
||||
cout << czero_ninf << " - " << ozero_pinf << " = " << czero_ninf - ozero_pinf << endl;
|
||||
cout << czero_ninf << " - " << czero_ninf << " = " << czero_ninf - czero_ninf << endl;
|
||||
cout << czero_ninf << " - " << czero_pinf << " = " << czero_ninf - czero_pinf << endl;
|
||||
cout << czero_pinf << " - " << ozero_ninf << " = " << czero_pinf - ozero_ninf << endl;
|
||||
cout << czero_pinf << " - " << ozero_pinf << " = " << czero_pinf - ozero_pinf << endl;
|
||||
cout << czero_pinf << " - " << czero_ninf << " = " << czero_pinf - czero_ninf << endl;
|
||||
cout << czero_pinf << " - " << czero_pinf << " = " << czero_pinf - czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf - ozero_ninf == inf);
|
||||
lean_assert(ozero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf - czero_ninf == inf);
|
||||
lean_assert(ozero_ninf - czero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - ozero_pinf == inf);
|
||||
lean_assert(ozero_pinf - czero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - czero_pinf == inf);
|
||||
lean_assert(czero_ninf - ozero_ninf == inf);
|
||||
lean_assert(czero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(czero_ninf - czero_ninf == inf);
|
||||
lean_assert(czero_ninf - czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(czero_pinf - ozero_pinf == inf);
|
||||
lean_assert(czero_pinf - czero_ninf == czero_pinf);
|
||||
lean_assert(czero_pinf - czero_pinf == inf);
|
||||
|
||||
cout << "=== Multiplication between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " * " << ozero_ninf << " = " << ozero_ninf * ozero_ninf << endl;
|
||||
cout << ozero_ninf << " * " << ozero_pinf << " = " << ozero_ninf * ozero_pinf << endl;
|
||||
cout << ozero_ninf << " * " << czero_ninf << " = " << ozero_ninf * czero_ninf << endl;
|
||||
cout << ozero_ninf << " * " << czero_pinf << " = " << ozero_ninf * czero_pinf << endl;
|
||||
cout << ozero_pinf << " * " << ozero_ninf << " = " << ozero_pinf * ozero_ninf << endl;
|
||||
cout << ozero_pinf << " * " << ozero_pinf << " = " << ozero_pinf * ozero_pinf << endl;
|
||||
cout << ozero_pinf << " * " << czero_ninf << " = " << ozero_pinf * czero_ninf << endl;
|
||||
cout << ozero_pinf << " * " << czero_pinf << " = " << ozero_pinf * czero_pinf << endl;
|
||||
cout << czero_ninf << " * " << ozero_ninf << " = " << czero_ninf * ozero_ninf << endl;
|
||||
cout << czero_ninf << " * " << ozero_pinf << " = " << czero_ninf * ozero_pinf << endl;
|
||||
cout << czero_ninf << " * " << czero_ninf << " = " << czero_ninf * czero_ninf << endl;
|
||||
cout << czero_ninf << " * " << czero_pinf << " = " << czero_ninf * czero_pinf << endl;
|
||||
cout << czero_pinf << " * " << ozero_ninf << " = " << czero_pinf * ozero_ninf << endl;
|
||||
cout << czero_pinf << " * " << ozero_pinf << " = " << czero_pinf * ozero_pinf << endl;
|
||||
cout << czero_pinf << " * " << czero_ninf << " = " << czero_pinf * czero_ninf << endl;
|
||||
cout << czero_pinf << " * " << czero_pinf << " = " << czero_pinf * czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf * ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf * ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(ozero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(ozero_pinf * czero_pinf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_pinf == czero_pinf);
|
||||
lean_assert(czero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * czero_pinf == czero_pinf);
|
||||
|
||||
cout << "=== Division between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " / " << ozero_ninf << " = " << ozero_ninf / ozero_ninf << endl;
|
||||
cout << ozero_ninf << " / " << ozero_pinf << " = " << ozero_ninf / ozero_pinf << endl;
|
||||
cout << ozero_pinf << " / " << ozero_ninf << " = " << ozero_pinf / ozero_ninf << endl;
|
||||
cout << ozero_pinf << " / " << ozero_pinf << " = " << ozero_pinf / ozero_pinf << endl;
|
||||
cout << czero_ninf << " / " << ozero_ninf << " = " << czero_ninf / ozero_ninf << endl;
|
||||
cout << czero_ninf << " / " << ozero_pinf << " = " << czero_ninf / ozero_pinf << endl;
|
||||
cout << czero_pinf << " / " << ozero_ninf << " = " << czero_pinf / ozero_ninf << endl;
|
||||
cout << czero_pinf << " / " << ozero_pinf << " = " << czero_pinf / ozero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf / ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf / ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf / ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf / ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_pinf == czero_pinf);
|
||||
}
|
||||
|
||||
static void mpfp_interval_inf2() {
|
||||
di i1(1.0, 2.0);
|
||||
di i2(3.0, 4.0);
|
||||
di i3(-10.0, -5.0);
|
||||
di i4(-3.0, +4.0);
|
||||
di i5(5.0, 8.0);
|
||||
di inf;
|
||||
|
||||
double c1 = 0.6;
|
||||
double c2 = 3.0;
|
||||
double c3 = -0.3;
|
||||
double c4 = -4.5;
|
||||
double zero = 0.0;
|
||||
|
||||
lean_assert(i1 + inf == inf); lean_assert(inf + i1 == inf);
|
||||
lean_assert(i2 + inf == inf); lean_assert(inf + i2 == inf);
|
||||
lean_assert(i3 + inf == inf); lean_assert(inf + i3 == inf);
|
||||
lean_assert(i4 + inf == inf); lean_assert(inf + i4 == inf);
|
||||
lean_assert(i5 + inf == inf); lean_assert(inf + i5 == inf);
|
||||
lean_assert(c1 + inf == inf); lean_assert(inf + c1 == inf);
|
||||
lean_assert(c2 + inf == inf); lean_assert(inf + c2 == inf);
|
||||
lean_assert(c3 + inf == inf); lean_assert(inf + c3 == inf);
|
||||
lean_assert(c4 + inf == inf); lean_assert(inf + c4 == inf);
|
||||
lean_assert(zero + inf == inf); lean_assert(inf + zero == inf);
|
||||
|
||||
lean_assert(i1 - inf == inf); lean_assert(inf - i1 == inf);
|
||||
lean_assert(i2 - inf == inf); lean_assert(inf - i2 == inf);
|
||||
lean_assert(i3 - inf == inf); lean_assert(inf - i3 == inf);
|
||||
lean_assert(i4 - inf == inf); lean_assert(inf - i4 == inf);
|
||||
lean_assert(i5 - inf == inf); lean_assert(inf - i5 == inf);
|
||||
lean_assert(c1 - inf == inf); lean_assert(inf - c1 == inf);
|
||||
lean_assert(c2 - inf == inf); lean_assert(inf - c2 == inf);
|
||||
lean_assert(c3 - inf == inf); lean_assert(inf - c3 == inf);
|
||||
lean_assert(c4 - inf == inf); lean_assert(inf - c4 == inf);
|
||||
lean_assert(zero - inf == inf); lean_assert(inf - zero == inf);
|
||||
|
||||
lean_assert(i1 * inf == inf); lean_assert(inf * i1 == inf);
|
||||
lean_assert(i2 * inf == inf); lean_assert(inf * i2 == inf);
|
||||
lean_assert(i3 * inf == inf); lean_assert(inf * i3 == inf);
|
||||
lean_assert(i4 * inf == inf); lean_assert(inf * i4 == inf);
|
||||
lean_assert(i5 * inf == inf); lean_assert(inf * i5 == inf);
|
||||
lean_assert(c1 * inf == inf); lean_assert(inf * c1 == inf);
|
||||
lean_assert(c2 * inf == inf); lean_assert(inf * c2 == inf);
|
||||
lean_assert(c3 * inf == inf); lean_assert(inf * c3 == inf);
|
||||
lean_assert(c4 * inf == inf); lean_assert(inf * c4 == inf);
|
||||
lean_assert(zero * inf == zero);lean_assert(inf * zero == zero);
|
||||
}
|
||||
|
||||
static void mpfp_interval_trans() {
|
||||
di i1(1.0, 2.0);
|
||||
di i2(3.0, 4.0);
|
||||
di i3(-10.0, -5.0);
|
||||
di i4(-3.0, +4.0);
|
||||
di i5(5.0, 8.0);
|
||||
di oi1(1.0, 2.0);
|
||||
di oi2(3.0, 4.0);
|
||||
di oi3(-10.0, -5.0);
|
||||
di oi4(-3.0, +4.0);
|
||||
di oi5(5.0, 8.0);
|
||||
oi1.set_is_lower_open(true); oi1.set_is_upper_open(true);
|
||||
oi2.set_is_lower_open(true); oi2.set_is_upper_open(true);
|
||||
oi3.set_is_lower_open(true); oi3.set_is_upper_open(true);
|
||||
oi4.set_is_lower_open(true); oi4.set_is_upper_open(true);
|
||||
oi5.set_is_lower_open(true); oi5.set_is_upper_open(true);
|
||||
|
||||
di inf;
|
||||
di ozero_pinf;
|
||||
di ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
di czero_pinf;
|
||||
di czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
// double c1 = 0.6;
|
||||
// double c2 = 3.0;
|
||||
// double c3 = 0.0;
|
||||
// double c4 = -4.5;
|
||||
// double c5 = -0.3;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "power" << "(" << i1 << ", " << 3 << ") = " << power(i1, 3) << endl;
|
||||
cout << "power" << "(" << i2 << ", " << 3 << ") = " << power(i2, 3) << endl;
|
||||
cout << "power" << "(" << i3 << ", " << 3 << ") = " << power(i3, 3) << endl;
|
||||
cout << "power" << "(" << i4 << ", " << 3 << ") = " << power(i4, 3) << endl;
|
||||
cout << "power" << "(" << i5 << ", " << 3 << ") = " << power(i5, 3) << endl;
|
||||
cout << "power" << "(" << oi1 << ", " << 3 << ") = " << power(oi1, 3) << endl;
|
||||
cout << "power" << "(" << oi2 << ", " << 3 << ") = " << power(oi2, 3) << endl;
|
||||
cout << "power" << "(" << oi3 << ", " << 3 << ") = " << power(oi3, 3) << endl;
|
||||
cout << "power" << "(" << oi4 << ", " << 3 << ") = " << power(oi4, 3) << endl;
|
||||
cout << "power" << "(" << oi5 << ", " << 3 << ") = " << power(oi5, 3) << endl;
|
||||
cout << "power" << "(" << inf << ", " << 3 << ") = " << power(inf, 3) << endl;
|
||||
cout << "power" << "(" << ozero_ninf << ", " << 3 << ") = " << power(ozero_ninf, 3) << endl;
|
||||
cout << "power" << "(" << ozero_pinf << ", " << 3 << ") = " << power(ozero_pinf, 3) << endl;
|
||||
cout << "power" << "(" << czero_ninf << ", " << 3 << ") = " << power(czero_ninf, 3) << endl;
|
||||
cout << "power" << "(" << czero_pinf << ", " << 3 << ") = " << power(czero_pinf, 3) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp" << "(" << i1 << ") = " << exp(i1) << endl;
|
||||
cout << "exp" << "(" << i2 << ") = " << exp(i2) << endl;
|
||||
cout << "exp" << "(" << i3 << ") = " << exp(i3) << endl;
|
||||
cout << "exp" << "(" << i4 << ") = " << exp(i4) << endl;
|
||||
cout << "exp" << "(" << i5 << ") = " << exp(i5) << endl;
|
||||
cout << "exp" << "(" << oi1 << ") = " << exp(oi1) << endl;
|
||||
cout << "exp" << "(" << oi2 << ") = " << exp(oi2) << endl;
|
||||
cout << "exp" << "(" << oi3 << ") = " << exp(oi3) << endl;
|
||||
cout << "exp" << "(" << oi4 << ") = " << exp(oi4) << endl;
|
||||
cout << "exp" << "(" << oi5 << ") = " << exp(oi5) << endl;
|
||||
cout << "exp" << "(" << ozero_pinf << ") = " << exp(ozero_pinf) << endl;
|
||||
cout << "exp" << "(" << ozero_ninf << ") = " << exp(ozero_ninf) << endl;
|
||||
cout << "exp" << "(" << czero_pinf << ") = " << exp(czero_pinf) << endl;
|
||||
cout << "exp" << "(" << czero_ninf << ") = " << exp(czero_ninf) << endl;
|
||||
cout << "exp" << "(" << inf << ") = " << exp(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp2" << "(" << i1 << ") = " << exp2(i1) << endl;
|
||||
cout << "exp2" << "(" << i2 << ") = " << exp2(i2) << endl;
|
||||
cout << "exp2" << "(" << i3 << ") = " << exp2(i3) << endl;
|
||||
cout << "exp2" << "(" << i4 << ") = " << exp2(i4) << endl;
|
||||
cout << "exp2" << "(" << i5 << ") = " << exp2(i5) << endl;
|
||||
cout << "exp2" << "(" << oi1 << ") = " << exp2(oi1) << endl;
|
||||
cout << "exp2" << "(" << oi2 << ") = " << exp2(oi2) << endl;
|
||||
cout << "exp2" << "(" << oi3 << ") = " << exp2(oi3) << endl;
|
||||
cout << "exp2" << "(" << oi4 << ") = " << exp2(oi4) << endl;
|
||||
cout << "exp2" << "(" << oi5 << ") = " << exp2(oi5) << endl;
|
||||
cout << "exp2" << "(" << ozero_pinf << ") = " << exp2(ozero_pinf) << endl;
|
||||
cout << "exp2" << "(" << ozero_ninf << ") = " << exp2(ozero_ninf) << endl;
|
||||
cout << "exp2" << "(" << czero_pinf << ") = " << exp2(czero_pinf) << endl;
|
||||
cout << "exp2" << "(" << czero_ninf << ") = " << exp2(czero_ninf) << endl;
|
||||
cout << "exp2" << "(" << inf << ") = " << exp2(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp10" << "(" << i1 << ") = " << exp10(i1) << endl;
|
||||
cout << "exp10" << "(" << i2 << ") = " << exp10(i2) << endl;
|
||||
cout << "exp10" << "(" << i3 << ") = " << exp10(i3) << endl;
|
||||
cout << "exp10" << "(" << i4 << ") = " << exp10(i4) << endl;
|
||||
cout << "exp10" << "(" << i5 << ") = " << exp10(i5) << endl;
|
||||
cout << "exp10" << "(" << oi1 << ") = " << exp10(oi1) << endl;
|
||||
cout << "exp10" << "(" << oi2 << ") = " << exp10(oi2) << endl;
|
||||
cout << "exp10" << "(" << oi3 << ") = " << exp10(oi3) << endl;
|
||||
cout << "exp10" << "(" << oi4 << ") = " << exp10(oi4) << endl;
|
||||
cout << "exp10" << "(" << oi5 << ") = " << exp10(oi5) << endl;
|
||||
cout << "exp10" << "(" << ozero_pinf << ") = " << exp10(ozero_pinf) << endl;
|
||||
cout << "exp10" << "(" << ozero_ninf << ") = " << exp10(ozero_ninf) << endl;
|
||||
cout << "exp10" << "(" << czero_pinf << ") = " << exp10(czero_pinf) << endl;
|
||||
cout << "exp10" << "(" << czero_ninf << ") = " << exp10(czero_ninf) << endl;
|
||||
cout << "exp10" << "(" << inf << ") = " << exp10(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log" << "(" << i1 << ") = " << log(i1) << endl;
|
||||
cout << "log" << "(" << i2 << ") = " << log(i2) << endl;
|
||||
cout << "log" << "(" << i5 << ") = " << log(i5) << endl;
|
||||
cout << "log" << "(" << oi1 << ") = " << log(oi1) << endl;
|
||||
cout << "log" << "(" << oi2 << ") = " << log(oi2) << endl;
|
||||
cout << "log" << "(" << oi5 << ") = " << log(oi5) << endl;
|
||||
cout << "log" << "(" << ozero_pinf << ") = " << log(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log2" << "(" << i1 << ") = " << log2(i1) << endl;
|
||||
cout << "log2" << "(" << i2 << ") = " << log2(i2) << endl;
|
||||
cout << "log2" << "(" << i5 << ") = " << log2(i5) << endl;
|
||||
cout << "log2" << "(" << oi1 << ") = " << log2(oi1) << endl;
|
||||
cout << "log2" << "(" << oi2 << ") = " << log2(oi2) << endl;
|
||||
cout << "log2" << "(" << oi5 << ") = " << log2(oi5) << endl;
|
||||
cout << "log2" << "(" << ozero_pinf << ") = " << log2(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log10" << "(" << i1 << ") = " << log10(i1) << endl;
|
||||
cout << "log10" << "(" << i2 << ") = " << log10(i2) << endl;
|
||||
cout << "log10" << "(" << i5 << ") = " << log10(i5) << endl;
|
||||
cout << "log10" << "(" << oi1 << ") = " << log10(oi1) << endl;
|
||||
cout << "log10" << "(" << oi2 << ") = " << log10(oi2) << endl;
|
||||
cout << "log10" << "(" << oi5 << ") = " << log10(oi5) << endl;
|
||||
cout << "log10" << "(" << ozero_pinf << ") = " << log10(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "sin" << "(" << i1 << ") = " << sin(i1) << endl;
|
||||
cout << "sin" << "(" << i2 << ") = " << sin(i2) << endl;
|
||||
cout << "sin" << "(" << i3 << ") = " << sin(i3) << endl;
|
||||
cout << "sin" << "(" << i4 << ") = " << sin(i4) << endl;
|
||||
cout << "sin" << "(" << i5 << ") = " << sin(i5) << endl;
|
||||
cout << "sin" << "(" << oi1 << ") = " << sin(oi1) << endl;
|
||||
cout << "sin" << "(" << oi2 << ") = " << sin(oi2) << endl;
|
||||
cout << "sin" << "(" << oi3 << ") = " << sin(oi3) << endl;
|
||||
cout << "sin" << "(" << oi4 << ") = " << sin(oi4) << endl;
|
||||
cout << "sin" << "(" << oi5 << ") = " << sin(oi5) << endl;
|
||||
cout << "sin" << "(" << ozero_pinf << ") = " << sin(ozero_pinf) << endl;
|
||||
cout << "sin" << "(" << ozero_ninf << ") = " << sin(ozero_ninf) << endl;
|
||||
cout << "sin" << "(" << czero_pinf << ") = " << sin(czero_pinf) << endl;
|
||||
cout << "sin" << "(" << czero_ninf << ") = " << sin(czero_ninf) << endl;
|
||||
cout << "sin" << "(" << inf << ") = " << sin(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "cos" << "(" << i1 << ") = " << cos(i1) << endl;
|
||||
cout << "cos" << "(" << i2 << ") = " << cos(i2) << endl;
|
||||
cout << "cos" << "(" << i3 << ") = " << cos(i3) << endl;
|
||||
cout << "cos" << "(" << i4 << ") = " << cos(i4) << endl;
|
||||
cout << "cos" << "(" << i5 << ") = " << cos(i5) << endl;
|
||||
cout << "cos" << "(" << oi1 << ") = " << cos(oi1) << endl;
|
||||
cout << "cos" << "(" << oi2 << ") = " << cos(oi2) << endl;
|
||||
cout << "cos" << "(" << oi3 << ") = " << cos(oi3) << endl;
|
||||
cout << "cos" << "(" << oi4 << ") = " << cos(oi4) << endl;
|
||||
cout << "cos" << "(" << oi5 << ") = " << cos(oi5) << endl;
|
||||
cout << "cos" << "(" << ozero_pinf << ") = " << cos(ozero_pinf) << endl;
|
||||
cout << "cos" << "(" << ozero_ninf << ") = " << cos(ozero_ninf) << endl;
|
||||
cout << "cos" << "(" << czero_pinf << ") = " << cos(czero_pinf) << endl;
|
||||
cout << "cos" << "(" << czero_ninf << ") = " << cos(czero_ninf) << endl;
|
||||
cout << "cos" << "(" << inf << ") = " << cos(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "tan" << "(" << i1 << ") = " << tan(i1) << endl;
|
||||
cout << "tan" << "(" << i2 << ") = " << tan(i2) << endl;
|
||||
cout << "tan" << "(" << i3 << ") = " << tan(i3) << endl;
|
||||
cout << "tan" << "(" << i4 << ") = " << tan(i4) << endl;
|
||||
cout << "tan" << "(" << i5 << ") = " << tan(i5) << endl;
|
||||
cout << "tan" << "(" << oi1 << ") = " << tan(oi1) << endl;
|
||||
cout << "tan" << "(" << oi2 << ") = " << tan(oi2) << endl;
|
||||
cout << "tan" << "(" << oi3 << ") = " << tan(oi3) << endl;
|
||||
cout << "tan" << "(" << oi4 << ") = " << tan(oi4) << endl;
|
||||
cout << "tan" << "(" << oi5 << ") = " << tan(oi5) << endl;
|
||||
cout << "tan" << "(" << ozero_pinf << ") = " << tan(ozero_pinf) << endl;
|
||||
cout << "tan" << "(" << ozero_ninf << ") = " << tan(ozero_ninf) << endl;
|
||||
cout << "tan" << "(" << czero_pinf << ") = " << tan(czero_pinf) << endl;
|
||||
cout << "tan" << "(" << czero_ninf << ") = " << tan(czero_ninf) << endl;
|
||||
cout << "tan" << "(" << inf << ") = " << tan(inf) << endl;
|
||||
}
|
||||
|
||||
int main() {
|
||||
continue_on_violation(true);
|
||||
enable_trace("numerics");
|
||||
mpfp_interval_arith();
|
||||
mpfp_interval_inf1();
|
||||
mpfp_interval_inf2();
|
||||
mpfp_interval_trans();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
514
src/tests/interval/float_interval.cpp
Normal file
514
src/tests/interval/float_interval.cpp
Normal file
|
|
@ -0,0 +1,514 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
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 "mpfp.h"
|
||||
#include "interval_def.h"
|
||||
|
||||
using namespace lean;
|
||||
|
||||
using std::cout;
|
||||
using std::endl;
|
||||
|
||||
typedef interval<float> flti;
|
||||
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() {
|
||||
flti i1(1.0, 2.0);
|
||||
flti i2(3.0, 4.0);
|
||||
flti i3(-10.0, -5.0);
|
||||
flti i4(-3.0, +4.0);
|
||||
flti i5(5.0, 8.0);
|
||||
|
||||
float c1 = 0.6;
|
||||
float c2 = 3.0;
|
||||
float c3 = 0.0;
|
||||
float c4 = -4.5;
|
||||
float c5 = -0.3;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "+", c1, i1 + c1);
|
||||
print_result(i2, "+", c2, i2 + c2);
|
||||
print_result(i3, "+", c3, i3 + c3);
|
||||
print_result(i4, "+", c4, i4 + c4);
|
||||
print_result(i5, "+", c5, i5 + c5);
|
||||
print_result(i5, "+", c1, i5 + c1);
|
||||
print_result(i4, "+", c2, i4 + c2);
|
||||
print_result(i2, "+", c4, i2 + c4);
|
||||
print_result(i1, "+", c5, i1 + c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "+", i1, c1 + i1);
|
||||
print_result(c2, "+", i2, c2 + i2);
|
||||
print_result(c3, "+", i3, c3 + i3);
|
||||
print_result(c4, "+", i4, c4 + i4);
|
||||
print_result(c5, "+", i5, c5 + i5);
|
||||
print_result(c5, "+", i1, c5 + i1);
|
||||
print_result(c4, "+", i2, c4 + i2);
|
||||
print_result(c2, "+", i4, c2 + i4);
|
||||
print_result(c1, "+", i5, c1 + i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "-", c1, i1 - c1);
|
||||
print_result(i2, "-", c2, i2 - c2);
|
||||
print_result(i3, "-", c3, i3 - c3);
|
||||
print_result(i4, "-", c4, i4 - c4);
|
||||
print_result(i5, "-", c5, i5 - c5);
|
||||
print_result(i5, "-", c1, i5 - c1);
|
||||
print_result(i4, "-", c2, i4 - c2);
|
||||
print_result(i2, "-", c4, i2 - c4);
|
||||
print_result(i1, "-", c5, i1 - c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "-", i1, c1 - i1);
|
||||
print_result(c2, "-", i2, c2 - i2);
|
||||
print_result(c3, "-", i3, c3 - i3);
|
||||
print_result(c4, "-", i4, c4 - i4);
|
||||
print_result(c5, "-", i5, c5 - i5);
|
||||
print_result(c5, "-", i1, c5 - i1);
|
||||
print_result(c4, "-", i2, c4 - i2);
|
||||
print_result(c2, "-", i4, c2 - i4);
|
||||
print_result(c1, "-", i5, c1 - i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "*", c1, i1 * c1);
|
||||
print_result(i2, "*", c2, i2 * c2);
|
||||
print_result(i3, "*", c3, i3 * c3);
|
||||
print_result(i4, "*", c4, i4 * c4);
|
||||
print_result(i5, "*", c5, i5 * c5);
|
||||
print_result(i5, "*", c1, i5 * c1);
|
||||
print_result(i4, "*", c2, i4 * c2);
|
||||
print_result(i2, "*", c4, i2 * c4);
|
||||
print_result(i1, "*", c5, i1 * c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "*", i1, c1 * i1);
|
||||
print_result(c2, "*", i2, c2 * i2);
|
||||
print_result(c3, "*", i3, c3 * i3);
|
||||
print_result(c4, "*", i4, c4 * i4);
|
||||
print_result(c5, "*", i5, c5 * i5);
|
||||
print_result(c5, "*", i1, c5 * i1);
|
||||
print_result(c4, "*", i2, c4 * i2);
|
||||
print_result(c2, "*", i4, c2 * i4);
|
||||
print_result(c1, "*", i5, c1 * i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "/", c1, i1 / c1);
|
||||
print_result(i2, "/", c2, i2 / c2);
|
||||
print_result(i3, "/", c3, i3 / c3);
|
||||
print_result(i4, "/", c4, i4 / c4);
|
||||
print_result(i5, "/", c5, i5 / c5);
|
||||
print_result(i5, "/", c1, i5 / c1);
|
||||
print_result(i4, "/", c2, i4 / c2);
|
||||
print_result(i2, "/", c4, i2 / c4);
|
||||
print_result(i1, "/", c5, i1 / c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "/", i1, c1 / i1);
|
||||
print_result(c2, "/", i2, c2 / i2);
|
||||
print_result(c3, "/", i3, c3 / i3);
|
||||
print_result(c5, "/", i5, c5 / i5);
|
||||
print_result(c5, "/", i1, c5 / i1);
|
||||
print_result(c4, "/", i2, c4 / i2);
|
||||
print_result(c1, "/", i5, c1 / i5);
|
||||
}
|
||||
|
||||
static void mpfp_interval_inf1() {
|
||||
flti i1(1.0, 2.0);
|
||||
flti inf;
|
||||
flti ozero_pinf;
|
||||
flti ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
flti czero_pinf;
|
||||
flti czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
cout << i1 << " * " << ozero_ninf << " = " << i1 * ozero_ninf << endl;
|
||||
cout << i1 << " * " << ozero_pinf << " = " << i1 * ozero_pinf << endl;
|
||||
cout << i1 << " * " << czero_ninf << " = " << i1 * czero_ninf << endl;
|
||||
cout << i1 << " * " << czero_pinf << " = " << i1 * czero_pinf << endl;
|
||||
lean_assert(i1 * ozero_ninf == ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
|
||||
lean_assert(i1 * ozero_pinf == ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
|
||||
lean_assert(i1 * czero_ninf == czero_ninf); lean_assert(czero_ninf * i1 == czero_ninf);
|
||||
lean_assert(i1 * czero_pinf == czero_pinf); lean_assert(czero_pinf * i1 == czero_pinf);
|
||||
|
||||
cout << "=== Adfltition between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " + " << ozero_ninf << " = " << ozero_ninf + ozero_ninf << endl;
|
||||
cout << ozero_ninf << " + " << ozero_pinf << " = " << ozero_ninf + ozero_pinf << endl;
|
||||
cout << ozero_ninf << " + " << czero_ninf << " = " << ozero_ninf + czero_ninf << endl;
|
||||
cout << ozero_ninf << " + " << czero_pinf << " = " << ozero_ninf + czero_pinf << endl;
|
||||
cout << ozero_pinf << " + " << ozero_ninf << " = " << ozero_pinf + ozero_ninf << endl;
|
||||
cout << ozero_pinf << " + " << ozero_pinf << " = " << ozero_pinf + ozero_pinf << endl;
|
||||
cout << ozero_pinf << " + " << czero_ninf << " = " << ozero_pinf + czero_ninf << endl;
|
||||
cout << ozero_pinf << " + " << czero_pinf << " = " << ozero_pinf + czero_pinf << endl;
|
||||
cout << czero_ninf << " + " << ozero_ninf << " = " << czero_ninf + ozero_ninf << endl;
|
||||
cout << czero_ninf << " + " << ozero_pinf << " = " << czero_ninf + ozero_pinf << endl;
|
||||
cout << czero_ninf << " + " << czero_ninf << " = " << czero_ninf + czero_ninf << endl;
|
||||
cout << czero_ninf << " + " << czero_pinf << " = " << czero_ninf + czero_pinf << endl;
|
||||
cout << czero_pinf << " + " << ozero_ninf << " = " << czero_pinf + ozero_ninf << endl;
|
||||
cout << czero_pinf << " + " << ozero_pinf << " = " << czero_pinf + ozero_pinf << endl;
|
||||
cout << czero_pinf << " + " << czero_ninf << " = " << czero_pinf + czero_ninf << endl;
|
||||
cout << czero_pinf << " + " << czero_pinf << " = " << czero_pinf + czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + ozero_pinf == inf);
|
||||
lean_assert(ozero_ninf + czero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + czero_pinf == inf);
|
||||
lean_assert(ozero_pinf + ozero_ninf == inf);
|
||||
lean_assert(ozero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf + czero_ninf == inf);
|
||||
lean_assert(ozero_pinf + czero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(czero_ninf + ozero_pinf == inf);
|
||||
lean_assert(czero_ninf + czero_ninf == czero_ninf);
|
||||
lean_assert(czero_ninf + czero_pinf == inf);
|
||||
lean_assert(czero_pinf + ozero_ninf == inf);
|
||||
lean_assert(czero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_pinf + czero_ninf == inf);
|
||||
lean_assert(czero_pinf + czero_pinf == czero_pinf);
|
||||
|
||||
cout << "=== Subtraction between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " - " << ozero_ninf << " = " << ozero_ninf - ozero_ninf << endl;
|
||||
cout << ozero_ninf << " - " << ozero_pinf << " = " << ozero_ninf - ozero_pinf << endl;
|
||||
cout << ozero_ninf << " - " << czero_ninf << " = " << ozero_ninf - czero_ninf << endl;
|
||||
cout << ozero_ninf << " - " << czero_pinf << " = " << ozero_ninf - czero_pinf << endl;
|
||||
cout << ozero_pinf << " - " << ozero_ninf << " = " << ozero_pinf - ozero_ninf << endl;
|
||||
cout << ozero_pinf << " - " << ozero_pinf << " = " << ozero_pinf - ozero_pinf << endl;
|
||||
cout << ozero_pinf << " - " << czero_ninf << " = " << ozero_pinf - czero_ninf << endl;
|
||||
cout << ozero_pinf << " - " << czero_pinf << " = " << ozero_pinf - czero_pinf << endl;
|
||||
cout << czero_ninf << " - " << ozero_ninf << " = " << czero_ninf - ozero_ninf << endl;
|
||||
cout << czero_ninf << " - " << ozero_pinf << " = " << czero_ninf - ozero_pinf << endl;
|
||||
cout << czero_ninf << " - " << czero_ninf << " = " << czero_ninf - czero_ninf << endl;
|
||||
cout << czero_ninf << " - " << czero_pinf << " = " << czero_ninf - czero_pinf << endl;
|
||||
cout << czero_pinf << " - " << ozero_ninf << " = " << czero_pinf - ozero_ninf << endl;
|
||||
cout << czero_pinf << " - " << ozero_pinf << " = " << czero_pinf - ozero_pinf << endl;
|
||||
cout << czero_pinf << " - " << czero_ninf << " = " << czero_pinf - czero_ninf << endl;
|
||||
cout << czero_pinf << " - " << czero_pinf << " = " << czero_pinf - czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf - ozero_ninf == inf);
|
||||
lean_assert(ozero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf - czero_ninf == inf);
|
||||
lean_assert(ozero_ninf - czero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - ozero_pinf == inf);
|
||||
lean_assert(ozero_pinf - czero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - czero_pinf == inf);
|
||||
lean_assert(czero_ninf - ozero_ninf == inf);
|
||||
lean_assert(czero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(czero_ninf - czero_ninf == inf);
|
||||
lean_assert(czero_ninf - czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(czero_pinf - ozero_pinf == inf);
|
||||
lean_assert(czero_pinf - czero_ninf == czero_pinf);
|
||||
lean_assert(czero_pinf - czero_pinf == inf);
|
||||
|
||||
cout << "=== Multiplication between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " * " << ozero_ninf << " = " << ozero_ninf * ozero_ninf << endl;
|
||||
cout << ozero_ninf << " * " << ozero_pinf << " = " << ozero_ninf * ozero_pinf << endl;
|
||||
cout << ozero_ninf << " * " << czero_ninf << " = " << ozero_ninf * czero_ninf << endl;
|
||||
cout << ozero_ninf << " * " << czero_pinf << " = " << ozero_ninf * czero_pinf << endl;
|
||||
cout << ozero_pinf << " * " << ozero_ninf << " = " << ozero_pinf * ozero_ninf << endl;
|
||||
cout << ozero_pinf << " * " << ozero_pinf << " = " << ozero_pinf * ozero_pinf << endl;
|
||||
cout << ozero_pinf << " * " << czero_ninf << " = " << ozero_pinf * czero_ninf << endl;
|
||||
cout << ozero_pinf << " * " << czero_pinf << " = " << ozero_pinf * czero_pinf << endl;
|
||||
cout << czero_ninf << " * " << ozero_ninf << " = " << czero_ninf * ozero_ninf << endl;
|
||||
cout << czero_ninf << " * " << ozero_pinf << " = " << czero_ninf * ozero_pinf << endl;
|
||||
cout << czero_ninf << " * " << czero_ninf << " = " << czero_ninf * czero_ninf << endl;
|
||||
cout << czero_ninf << " * " << czero_pinf << " = " << czero_ninf * czero_pinf << endl;
|
||||
cout << czero_pinf << " * " << ozero_ninf << " = " << czero_pinf * ozero_ninf << endl;
|
||||
cout << czero_pinf << " * " << ozero_pinf << " = " << czero_pinf * ozero_pinf << endl;
|
||||
cout << czero_pinf << " * " << czero_ninf << " = " << czero_pinf * czero_ninf << endl;
|
||||
cout << czero_pinf << " * " << czero_pinf << " = " << czero_pinf * czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf * ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf * ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(ozero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(ozero_pinf * czero_pinf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_pinf == czero_pinf);
|
||||
lean_assert(czero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * czero_pinf == czero_pinf);
|
||||
|
||||
cout << "=== Fltivision between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " / " << ozero_ninf << " = " << ozero_ninf / ozero_ninf << endl;
|
||||
cout << ozero_ninf << " / " << ozero_pinf << " = " << ozero_ninf / ozero_pinf << endl;
|
||||
cout << ozero_pinf << " / " << ozero_ninf << " = " << ozero_pinf / ozero_ninf << endl;
|
||||
cout << ozero_pinf << " / " << ozero_pinf << " = " << ozero_pinf / ozero_pinf << endl;
|
||||
cout << czero_ninf << " / " << ozero_ninf << " = " << czero_ninf / ozero_ninf << endl;
|
||||
cout << czero_ninf << " / " << ozero_pinf << " = " << czero_ninf / ozero_pinf << endl;
|
||||
cout << czero_pinf << " / " << ozero_ninf << " = " << czero_pinf / ozero_ninf << endl;
|
||||
cout << czero_pinf << " / " << ozero_pinf << " = " << czero_pinf / ozero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf / ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf / ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf / ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf / ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_pinf == czero_pinf);
|
||||
}
|
||||
|
||||
static void mpfp_interval_inf2() {
|
||||
flti i1(1.0, 2.0);
|
||||
flti i2(3.0, 4.0);
|
||||
flti i3(-10.0, -5.0);
|
||||
flti i4(-3.0, +4.0);
|
||||
flti i5(5.0, 8.0);
|
||||
flti inf;
|
||||
|
||||
float c1 = 0.6;
|
||||
float c2 = 3.0;
|
||||
float c3 = -0.3;
|
||||
float c4 = -4.5;
|
||||
float zero = 0.0;
|
||||
|
||||
lean_assert(i1 + inf == inf); lean_assert(inf + i1 == inf);
|
||||
lean_assert(i2 + inf == inf); lean_assert(inf + i2 == inf);
|
||||
lean_assert(i3 + inf == inf); lean_assert(inf + i3 == inf);
|
||||
lean_assert(i4 + inf == inf); lean_assert(inf + i4 == inf);
|
||||
lean_assert(i5 + inf == inf); lean_assert(inf + i5 == inf);
|
||||
lean_assert(c1 + inf == inf); lean_assert(inf + c1 == inf);
|
||||
lean_assert(c2 + inf == inf); lean_assert(inf + c2 == inf);
|
||||
lean_assert(c3 + inf == inf); lean_assert(inf + c3 == inf);
|
||||
lean_assert(c4 + inf == inf); lean_assert(inf + c4 == inf);
|
||||
lean_assert(zero + inf == inf); lean_assert(inf + zero == inf);
|
||||
|
||||
lean_assert(i1 - inf == inf); lean_assert(inf - i1 == inf);
|
||||
lean_assert(i2 - inf == inf); lean_assert(inf - i2 == inf);
|
||||
lean_assert(i3 - inf == inf); lean_assert(inf - i3 == inf);
|
||||
lean_assert(i4 - inf == inf); lean_assert(inf - i4 == inf);
|
||||
lean_assert(i5 - inf == inf); lean_assert(inf - i5 == inf);
|
||||
lean_assert(c1 - inf == inf); lean_assert(inf - c1 == inf);
|
||||
lean_assert(c2 - inf == inf); lean_assert(inf - c2 == inf);
|
||||
lean_assert(c3 - inf == inf); lean_assert(inf - c3 == inf);
|
||||
lean_assert(c4 - inf == inf); lean_assert(inf - c4 == inf);
|
||||
lean_assert(zero - inf == inf); lean_assert(inf - zero == inf);
|
||||
|
||||
lean_assert(i1 * inf == inf); lean_assert(inf * i1 == inf);
|
||||
lean_assert(i2 * inf == inf); lean_assert(inf * i2 == inf);
|
||||
lean_assert(i3 * inf == inf); lean_assert(inf * i3 == inf);
|
||||
lean_assert(i4 * inf == inf); lean_assert(inf * i4 == inf);
|
||||
lean_assert(i5 * inf == inf); lean_assert(inf * i5 == inf);
|
||||
lean_assert(c1 * inf == inf); lean_assert(inf * c1 == inf);
|
||||
lean_assert(c2 * inf == inf); lean_assert(inf * c2 == inf);
|
||||
lean_assert(c3 * inf == inf); lean_assert(inf * c3 == inf);
|
||||
lean_assert(c4 * inf == inf); lean_assert(inf * c4 == inf);
|
||||
lean_assert(zero * inf == zero);lean_assert(inf * zero == zero);
|
||||
}
|
||||
|
||||
static void mpfp_interval_trans() {
|
||||
flti i1(1.0, 2.0);
|
||||
flti i2(3.0, 4.0);
|
||||
flti i3(-10.0, -5.0);
|
||||
flti i4(-3.0, +4.0);
|
||||
flti i5(5.0, 8.0);
|
||||
flti oi1(1.0, 2.0);
|
||||
flti oi2(3.0, 4.0);
|
||||
flti oi3(-10.0, -5.0);
|
||||
flti oi4(-3.0, +4.0);
|
||||
flti oi5(5.0, 8.0);
|
||||
oi1.set_is_lower_open(true); oi1.set_is_upper_open(true);
|
||||
oi2.set_is_lower_open(true); oi2.set_is_upper_open(true);
|
||||
oi3.set_is_lower_open(true); oi3.set_is_upper_open(true);
|
||||
oi4.set_is_lower_open(true); oi4.set_is_upper_open(true);
|
||||
oi5.set_is_lower_open(true); oi5.set_is_upper_open(true);
|
||||
|
||||
flti inf;
|
||||
flti ozero_pinf;
|
||||
flti ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
flti czero_pinf;
|
||||
flti czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
// float c1 = 0.6;
|
||||
// float c2 = 3.0;
|
||||
// float c3 = 0.0;
|
||||
// float c4 = -4.5;
|
||||
// float c5 = -0.3;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "power" << "(" << i1 << ", " << 3 << ") = " << power(i1, 3) << endl;
|
||||
cout << "power" << "(" << i2 << ", " << 3 << ") = " << power(i2, 3) << endl;
|
||||
cout << "power" << "(" << i3 << ", " << 3 << ") = " << power(i3, 3) << endl;
|
||||
cout << "power" << "(" << i4 << ", " << 3 << ") = " << power(i4, 3) << endl;
|
||||
cout << "power" << "(" << i5 << ", " << 3 << ") = " << power(i5, 3) << endl;
|
||||
cout << "power" << "(" << oi1 << ", " << 3 << ") = " << power(oi1, 3) << endl;
|
||||
cout << "power" << "(" << oi2 << ", " << 3 << ") = " << power(oi2, 3) << endl;
|
||||
cout << "power" << "(" << oi3 << ", " << 3 << ") = " << power(oi3, 3) << endl;
|
||||
cout << "power" << "(" << oi4 << ", " << 3 << ") = " << power(oi4, 3) << endl;
|
||||
cout << "power" << "(" << oi5 << ", " << 3 << ") = " << power(oi5, 3) << endl;
|
||||
cout << "power" << "(" << inf << ", " << 3 << ") = " << power(inf, 3) << endl;
|
||||
cout << "power" << "(" << ozero_ninf << ", " << 3 << ") = " << power(ozero_ninf, 3) << endl;
|
||||
cout << "power" << "(" << ozero_pinf << ", " << 3 << ") = " << power(ozero_pinf, 3) << endl;
|
||||
cout << "power" << "(" << czero_ninf << ", " << 3 << ") = " << power(czero_ninf, 3) << endl;
|
||||
cout << "power" << "(" << czero_pinf << ", " << 3 << ") = " << power(czero_pinf, 3) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp" << "(" << i1 << ") = " << exp(i1) << endl;
|
||||
cout << "exp" << "(" << i2 << ") = " << exp(i2) << endl;
|
||||
cout << "exp" << "(" << i3 << ") = " << exp(i3) << endl;
|
||||
cout << "exp" << "(" << i4 << ") = " << exp(i4) << endl;
|
||||
cout << "exp" << "(" << i5 << ") = " << exp(i5) << endl;
|
||||
cout << "exp" << "(" << oi1 << ") = " << exp(oi1) << endl;
|
||||
cout << "exp" << "(" << oi2 << ") = " << exp(oi2) << endl;
|
||||
cout << "exp" << "(" << oi3 << ") = " << exp(oi3) << endl;
|
||||
cout << "exp" << "(" << oi4 << ") = " << exp(oi4) << endl;
|
||||
cout << "exp" << "(" << oi5 << ") = " << exp(oi5) << endl;
|
||||
cout << "exp" << "(" << ozero_pinf << ") = " << exp(ozero_pinf) << endl;
|
||||
cout << "exp" << "(" << ozero_ninf << ") = " << exp(ozero_ninf) << endl;
|
||||
cout << "exp" << "(" << czero_pinf << ") = " << exp(czero_pinf) << endl;
|
||||
cout << "exp" << "(" << czero_ninf << ") = " << exp(czero_ninf) << endl;
|
||||
cout << "exp" << "(" << inf << ") = " << exp(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp2" << "(" << i1 << ") = " << exp2(i1) << endl;
|
||||
cout << "exp2" << "(" << i2 << ") = " << exp2(i2) << endl;
|
||||
cout << "exp2" << "(" << i3 << ") = " << exp2(i3) << endl;
|
||||
cout << "exp2" << "(" << i4 << ") = " << exp2(i4) << endl;
|
||||
cout << "exp2" << "(" << i5 << ") = " << exp2(i5) << endl;
|
||||
cout << "exp2" << "(" << oi1 << ") = " << exp2(oi1) << endl;
|
||||
cout << "exp2" << "(" << oi2 << ") = " << exp2(oi2) << endl;
|
||||
cout << "exp2" << "(" << oi3 << ") = " << exp2(oi3) << endl;
|
||||
cout << "exp2" << "(" << oi4 << ") = " << exp2(oi4) << endl;
|
||||
cout << "exp2" << "(" << oi5 << ") = " << exp2(oi5) << endl;
|
||||
cout << "exp2" << "(" << ozero_pinf << ") = " << exp2(ozero_pinf) << endl;
|
||||
cout << "exp2" << "(" << ozero_ninf << ") = " << exp2(ozero_ninf) << endl;
|
||||
cout << "exp2" << "(" << czero_pinf << ") = " << exp2(czero_pinf) << endl;
|
||||
cout << "exp2" << "(" << czero_ninf << ") = " << exp2(czero_ninf) << endl;
|
||||
cout << "exp2" << "(" << inf << ") = " << exp2(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp10" << "(" << i1 << ") = " << exp10(i1) << endl;
|
||||
cout << "exp10" << "(" << i2 << ") = " << exp10(i2) << endl;
|
||||
cout << "exp10" << "(" << i3 << ") = " << exp10(i3) << endl;
|
||||
cout << "exp10" << "(" << i4 << ") = " << exp10(i4) << endl;
|
||||
cout << "exp10" << "(" << i5 << ") = " << exp10(i5) << endl;
|
||||
cout << "exp10" << "(" << oi1 << ") = " << exp10(oi1) << endl;
|
||||
cout << "exp10" << "(" << oi2 << ") = " << exp10(oi2) << endl;
|
||||
cout << "exp10" << "(" << oi3 << ") = " << exp10(oi3) << endl;
|
||||
cout << "exp10" << "(" << oi4 << ") = " << exp10(oi4) << endl;
|
||||
cout << "exp10" << "(" << oi5 << ") = " << exp10(oi5) << endl;
|
||||
cout << "exp10" << "(" << ozero_pinf << ") = " << exp10(ozero_pinf) << endl;
|
||||
cout << "exp10" << "(" << ozero_ninf << ") = " << exp10(ozero_ninf) << endl;
|
||||
cout << "exp10" << "(" << czero_pinf << ") = " << exp10(czero_pinf) << endl;
|
||||
cout << "exp10" << "(" << czero_ninf << ") = " << exp10(czero_ninf) << endl;
|
||||
cout << "exp10" << "(" << inf << ") = " << exp10(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log" << "(" << i1 << ") = " << log(i1) << endl;
|
||||
cout << "log" << "(" << i2 << ") = " << log(i2) << endl;
|
||||
cout << "log" << "(" << i5 << ") = " << log(i5) << endl;
|
||||
cout << "log" << "(" << oi1 << ") = " << log(oi1) << endl;
|
||||
cout << "log" << "(" << oi2 << ") = " << log(oi2) << endl;
|
||||
cout << "log" << "(" << oi5 << ") = " << log(oi5) << endl;
|
||||
cout << "log" << "(" << ozero_pinf << ") = " << log(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log2" << "(" << i1 << ") = " << log2(i1) << endl;
|
||||
cout << "log2" << "(" << i2 << ") = " << log2(i2) << endl;
|
||||
cout << "log2" << "(" << i5 << ") = " << log2(i5) << endl;
|
||||
cout << "log2" << "(" << oi1 << ") = " << log2(oi1) << endl;
|
||||
cout << "log2" << "(" << oi2 << ") = " << log2(oi2) << endl;
|
||||
cout << "log2" << "(" << oi5 << ") = " << log2(oi5) << endl;
|
||||
cout << "log2" << "(" << ozero_pinf << ") = " << log2(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log10" << "(" << i1 << ") = " << log10(i1) << endl;
|
||||
cout << "log10" << "(" << i2 << ") = " << log10(i2) << endl;
|
||||
cout << "log10" << "(" << i5 << ") = " << log10(i5) << endl;
|
||||
cout << "log10" << "(" << oi1 << ") = " << log10(oi1) << endl;
|
||||
cout << "log10" << "(" << oi2 << ") = " << log10(oi2) << endl;
|
||||
cout << "log10" << "(" << oi5 << ") = " << log10(oi5) << endl;
|
||||
cout << "log10" << "(" << ozero_pinf << ") = " << log10(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "sin" << "(" << i1 << ") = " << sin(i1) << endl;
|
||||
cout << "sin" << "(" << i2 << ") = " << sin(i2) << endl;
|
||||
cout << "sin" << "(" << i3 << ") = " << sin(i3) << endl;
|
||||
cout << "sin" << "(" << i4 << ") = " << sin(i4) << endl;
|
||||
cout << "sin" << "(" << i5 << ") = " << sin(i5) << endl;
|
||||
cout << "sin" << "(" << oi1 << ") = " << sin(oi1) << endl;
|
||||
cout << "sin" << "(" << oi2 << ") = " << sin(oi2) << endl;
|
||||
cout << "sin" << "(" << oi3 << ") = " << sin(oi3) << endl;
|
||||
cout << "sin" << "(" << oi4 << ") = " << sin(oi4) << endl;
|
||||
cout << "sin" << "(" << oi5 << ") = " << sin(oi5) << endl;
|
||||
cout << "sin" << "(" << ozero_pinf << ") = " << sin(ozero_pinf) << endl;
|
||||
cout << "sin" << "(" << ozero_ninf << ") = " << sin(ozero_ninf) << endl;
|
||||
cout << "sin" << "(" << czero_pinf << ") = " << sin(czero_pinf) << endl;
|
||||
cout << "sin" << "(" << czero_ninf << ") = " << sin(czero_ninf) << endl;
|
||||
cout << "sin" << "(" << inf << ") = " << sin(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "cos" << "(" << i1 << ") = " << cos(i1) << endl;
|
||||
cout << "cos" << "(" << i2 << ") = " << cos(i2) << endl;
|
||||
cout << "cos" << "(" << i3 << ") = " << cos(i3) << endl;
|
||||
cout << "cos" << "(" << i4 << ") = " << cos(i4) << endl;
|
||||
cout << "cos" << "(" << i5 << ") = " << cos(i5) << endl;
|
||||
cout << "cos" << "(" << oi1 << ") = " << cos(oi1) << endl;
|
||||
cout << "cos" << "(" << oi2 << ") = " << cos(oi2) << endl;
|
||||
cout << "cos" << "(" << oi3 << ") = " << cos(oi3) << endl;
|
||||
cout << "cos" << "(" << oi4 << ") = " << cos(oi4) << endl;
|
||||
cout << "cos" << "(" << oi5 << ") = " << cos(oi5) << endl;
|
||||
cout << "cos" << "(" << ozero_pinf << ") = " << cos(ozero_pinf) << endl;
|
||||
cout << "cos" << "(" << ozero_ninf << ") = " << cos(ozero_ninf) << endl;
|
||||
cout << "cos" << "(" << czero_pinf << ") = " << cos(czero_pinf) << endl;
|
||||
cout << "cos" << "(" << czero_ninf << ") = " << cos(czero_ninf) << endl;
|
||||
cout << "cos" << "(" << inf << ") = " << cos(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "tan" << "(" << i1 << ") = " << tan(i1) << endl;
|
||||
cout << "tan" << "(" << i2 << ") = " << tan(i2) << endl;
|
||||
cout << "tan" << "(" << i3 << ") = " << tan(i3) << endl;
|
||||
cout << "tan" << "(" << i4 << ") = " << tan(i4) << endl;
|
||||
cout << "tan" << "(" << i5 << ") = " << tan(i5) << endl;
|
||||
cout << "tan" << "(" << oi1 << ") = " << tan(oi1) << endl;
|
||||
cout << "tan" << "(" << oi2 << ") = " << tan(oi2) << endl;
|
||||
cout << "tan" << "(" << oi3 << ") = " << tan(oi3) << endl;
|
||||
cout << "tan" << "(" << oi4 << ") = " << tan(oi4) << endl;
|
||||
cout << "tan" << "(" << oi5 << ") = " << tan(oi5) << endl;
|
||||
cout << "tan" << "(" << ozero_pinf << ") = " << tan(ozero_pinf) << endl;
|
||||
cout << "tan" << "(" << ozero_ninf << ") = " << tan(ozero_ninf) << endl;
|
||||
cout << "tan" << "(" << czero_pinf << ") = " << tan(czero_pinf) << endl;
|
||||
cout << "tan" << "(" << czero_ninf << ") = " << tan(czero_ninf) << endl;
|
||||
cout << "tan" << "(" << inf << ") = " << tan(inf) << endl;
|
||||
}
|
||||
|
||||
int main() {
|
||||
continue_on_violation(true);
|
||||
enable_trace("numerics");
|
||||
mpfp_interval_arith();
|
||||
mpfp_interval_inf1();
|
||||
mpfp_interval_inf2();
|
||||
mpfp_interval_trans();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
@ -14,7 +14,7 @@ Author: Leonardo de Moura
|
|||
|
||||
using namespace lean;
|
||||
|
||||
typedef interval<double> qi;
|
||||
typedef interval<mpq> qi;
|
||||
typedef interval<double> di;
|
||||
typedef interval<mpfp> fi;
|
||||
typedef std::vector<qi> qiv;
|
||||
|
|
@ -90,512 +90,10 @@ static void tst2() {
|
|||
lean_assert(power(qi(),2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo)
|
||||
}
|
||||
|
||||
static void double_interval_trans() {
|
||||
di i1(1.0, 2.0);
|
||||
std::cout << "power(" << i1 << ", 3) = " << power(i1, 3) << std::endl;
|
||||
std::cout << "exp(" << i1 << ") = " << exp(i1) << std::endl;
|
||||
std::cout << "log(" << i1 << ") = " << log(i1) << std::endl;
|
||||
}
|
||||
|
||||
template<typename T1, typename T2, typename T3>
|
||||
void print_result(T1 a, std::string const & op, T2 b, T3 r) {
|
||||
std::cout << a << " " << op << " " << b << " = " << r << std::endl;
|
||||
}
|
||||
|
||||
template<typename T, typename F>
|
||||
void print_result_fun(F f, std::string const & fun, T x) {
|
||||
std::cout << fun << "(" << x << ") = " << f(x) << std::endl;
|
||||
}
|
||||
|
||||
static void mpfr_interval_inf1() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi inf;
|
||||
fi ozero_pinf;
|
||||
fi ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
fi czero_pinf;
|
||||
fi czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
std::cerr << i1 << " * " << ozero_ninf << " = " << i1 * ozero_ninf << std::endl;
|
||||
std::cerr << i1 << " * " << ozero_pinf << " = " << i1 * ozero_pinf << std::endl;
|
||||
std::cerr << i1 << " * " << czero_ninf << " = " << i1 * czero_ninf << std::endl;
|
||||
std::cerr << i1 << " * " << czero_pinf << " = " << i1 * czero_pinf << std::endl;
|
||||
lean_assert(i1 * ozero_ninf == ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
|
||||
lean_assert(i1 * ozero_pinf == ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
|
||||
lean_assert(i1 * czero_ninf == czero_ninf); lean_assert(czero_ninf * i1 == czero_ninf);
|
||||
lean_assert(i1 * czero_pinf == czero_pinf); lean_assert(czero_pinf * i1 == czero_pinf);
|
||||
|
||||
std::cerr << "=== Addition between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << std::endl;
|
||||
std::cerr << ozero_ninf << " + " << ozero_ninf << " = " << ozero_ninf + ozero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " + " << ozero_pinf << " = " << ozero_ninf + ozero_pinf << std::endl;
|
||||
std::cerr << ozero_ninf << " + " << czero_ninf << " = " << ozero_ninf + czero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " + " << czero_pinf << " = " << ozero_ninf + czero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " + " << ozero_ninf << " = " << ozero_pinf + ozero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " + " << ozero_pinf << " = " << ozero_pinf + ozero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " + " << czero_ninf << " = " << ozero_pinf + czero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " + " << czero_pinf << " = " << ozero_pinf + czero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " + " << ozero_ninf << " = " << czero_ninf + ozero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " + " << ozero_pinf << " = " << czero_ninf + ozero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " + " << czero_ninf << " = " << czero_ninf + czero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " + " << czero_pinf << " = " << czero_ninf + czero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " + " << ozero_ninf << " = " << czero_pinf + ozero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " + " << ozero_pinf << " = " << czero_pinf + ozero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " + " << czero_ninf << " = " << czero_pinf + czero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " + " << czero_pinf << " = " << czero_pinf + czero_pinf << std::endl;
|
||||
|
||||
lean_assert(ozero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + ozero_pinf == inf);
|
||||
lean_assert(ozero_ninf + czero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + czero_pinf == inf);
|
||||
lean_assert(ozero_pinf + ozero_ninf == inf);
|
||||
lean_assert(ozero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf + czero_ninf == inf);
|
||||
lean_assert(ozero_pinf + czero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(czero_ninf + ozero_pinf == inf);
|
||||
lean_assert(czero_ninf + czero_ninf == czero_ninf);
|
||||
lean_assert(czero_ninf + czero_pinf == inf);
|
||||
lean_assert(czero_pinf + ozero_ninf == inf);
|
||||
lean_assert(czero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_pinf + czero_ninf == inf);
|
||||
lean_assert(czero_pinf + czero_pinf == czero_pinf);
|
||||
|
||||
std::cerr << "=== Subtraction between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << std::endl;
|
||||
std::cerr << ozero_ninf << " - " << ozero_ninf << " = " << ozero_ninf - ozero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " - " << ozero_pinf << " = " << ozero_ninf - ozero_pinf << std::endl;
|
||||
std::cerr << ozero_ninf << " - " << czero_ninf << " = " << ozero_ninf - czero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " - " << czero_pinf << " = " << ozero_ninf - czero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " - " << ozero_ninf << " = " << ozero_pinf - ozero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " - " << ozero_pinf << " = " << ozero_pinf - ozero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " - " << czero_ninf << " = " << ozero_pinf - czero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " - " << czero_pinf << " = " << ozero_pinf - czero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " - " << ozero_ninf << " = " << czero_ninf - ozero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " - " << ozero_pinf << " = " << czero_ninf - ozero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " - " << czero_ninf << " = " << czero_ninf - czero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " - " << czero_pinf << " = " << czero_ninf - czero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " - " << ozero_ninf << " = " << czero_pinf - ozero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " - " << ozero_pinf << " = " << czero_pinf - ozero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " - " << czero_ninf << " = " << czero_pinf - czero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " - " << czero_pinf << " = " << czero_pinf - czero_pinf << std::endl;
|
||||
|
||||
lean_assert(ozero_ninf - ozero_ninf == inf);
|
||||
lean_assert(ozero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf - czero_ninf == inf);
|
||||
lean_assert(ozero_ninf - czero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - ozero_pinf == inf);
|
||||
lean_assert(ozero_pinf - czero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - czero_pinf == inf);
|
||||
lean_assert(czero_ninf - ozero_ninf == inf);
|
||||
lean_assert(czero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(czero_ninf - czero_ninf == inf);
|
||||
lean_assert(czero_ninf - czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(czero_pinf - ozero_pinf == inf);
|
||||
lean_assert(czero_pinf - czero_ninf == czero_pinf);
|
||||
lean_assert(czero_pinf - czero_pinf == inf);
|
||||
|
||||
std::cerr << "=== Multiplication between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << std::endl;
|
||||
std::cerr << ozero_ninf << " * " << ozero_ninf << " = " << ozero_ninf * ozero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " * " << ozero_pinf << " = " << ozero_ninf * ozero_pinf << std::endl;
|
||||
std::cerr << ozero_ninf << " * " << czero_ninf << " = " << ozero_ninf * czero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " * " << czero_pinf << " = " << ozero_ninf * czero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " * " << ozero_ninf << " = " << ozero_pinf * ozero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " * " << ozero_pinf << " = " << ozero_pinf * ozero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " * " << czero_ninf << " = " << ozero_pinf * czero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " * " << czero_pinf << " = " << ozero_pinf * czero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " * " << ozero_ninf << " = " << czero_ninf * ozero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " * " << ozero_pinf << " = " << czero_ninf * ozero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " * " << czero_ninf << " = " << czero_ninf * czero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " * " << czero_pinf << " = " << czero_ninf * czero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " * " << ozero_ninf << " = " << czero_pinf * ozero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " * " << ozero_pinf << " = " << czero_pinf * ozero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " * " << czero_ninf << " = " << czero_pinf * czero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " * " << czero_pinf << " = " << czero_pinf * czero_pinf << std::endl;
|
||||
|
||||
lean_assert(ozero_ninf * ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf * ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(ozero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(ozero_pinf * czero_pinf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_pinf == czero_pinf);
|
||||
lean_assert(czero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * czero_pinf == czero_pinf);
|
||||
|
||||
std::cerr << "=== Division between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << std::endl;
|
||||
std::cerr << ozero_ninf << " / " << ozero_ninf << " = " << ozero_ninf / ozero_ninf << std::endl;
|
||||
std::cerr << ozero_ninf << " / " << ozero_pinf << " = " << ozero_ninf / ozero_pinf << std::endl;
|
||||
std::cerr << ozero_pinf << " / " << ozero_ninf << " = " << ozero_pinf / ozero_ninf << std::endl;
|
||||
std::cerr << ozero_pinf << " / " << ozero_pinf << " = " << ozero_pinf / ozero_pinf << std::endl;
|
||||
std::cerr << czero_ninf << " / " << ozero_ninf << " = " << czero_ninf / ozero_ninf << std::endl;
|
||||
std::cerr << czero_ninf << " / " << ozero_pinf << " = " << czero_ninf / ozero_pinf << std::endl;
|
||||
std::cerr << czero_pinf << " / " << ozero_ninf << " = " << czero_pinf / ozero_ninf << std::endl;
|
||||
std::cerr << czero_pinf << " / " << ozero_pinf << " = " << czero_pinf / ozero_pinf << std::endl;
|
||||
|
||||
lean_assert(ozero_ninf / ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf / ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf / ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf / ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_pinf == czero_pinf);
|
||||
}
|
||||
|
||||
static void mpfr_interval_inf2() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi i2(3.0, 4.0);
|
||||
fi i3(-10.0, -5.0);
|
||||
fi i4(-3.0, +4.0);
|
||||
fi i5(5.0, 8.0);
|
||||
fi inf;
|
||||
|
||||
mpfp c1(0.6);
|
||||
mpfp c2(3.0);
|
||||
mpfp c3(-0.3);
|
||||
mpfp c4(-4.5);
|
||||
mpfp zero(0.0);
|
||||
|
||||
lean_assert(i1 + inf == inf); lean_assert(inf + i1 == inf);
|
||||
lean_assert(i2 + inf == inf); lean_assert(inf + i2 == inf);
|
||||
lean_assert(i3 + inf == inf); lean_assert(inf + i3 == inf);
|
||||
lean_assert(i4 + inf == inf); lean_assert(inf + i4 == inf);
|
||||
lean_assert(i5 + inf == inf); lean_assert(inf + i5 == inf);
|
||||
lean_assert(c1 + inf == inf); lean_assert(inf + c1 == inf);
|
||||
lean_assert(c2 + inf == inf); lean_assert(inf + c2 == inf);
|
||||
lean_assert(c3 + inf == inf); lean_assert(inf + c3 == inf);
|
||||
lean_assert(c4 + inf == inf); lean_assert(inf + c4 == inf);
|
||||
lean_assert(zero + inf == inf); lean_assert(inf + zero == inf);
|
||||
|
||||
lean_assert(i1 - inf == inf); lean_assert(inf - i1 == inf);
|
||||
lean_assert(i2 - inf == inf); lean_assert(inf - i2 == inf);
|
||||
lean_assert(i3 - inf == inf); lean_assert(inf - i3 == inf);
|
||||
lean_assert(i4 - inf == inf); lean_assert(inf - i4 == inf);
|
||||
lean_assert(i5 - inf == inf); lean_assert(inf - i5 == inf);
|
||||
lean_assert(c1 - inf == inf); lean_assert(inf - c1 == inf);
|
||||
lean_assert(c2 - inf == inf); lean_assert(inf - c2 == inf);
|
||||
lean_assert(c3 - inf == inf); lean_assert(inf - c3 == inf);
|
||||
lean_assert(c4 - inf == inf); lean_assert(inf - c4 == inf);
|
||||
lean_assert(zero - inf == inf); lean_assert(inf - zero == inf);
|
||||
|
||||
lean_assert(i1 * inf == inf); lean_assert(inf * i1 == inf);
|
||||
lean_assert(i2 * inf == inf); lean_assert(inf * i2 == inf);
|
||||
lean_assert(i3 * inf == inf); lean_assert(inf * i3 == inf);
|
||||
lean_assert(i4 * inf == inf); lean_assert(inf * i4 == inf);
|
||||
lean_assert(i5 * inf == inf); lean_assert(inf * i5 == inf);
|
||||
lean_assert(c1 * inf == inf); lean_assert(inf * c1 == inf);
|
||||
lean_assert(c2 * inf == inf); lean_assert(inf * c2 == inf);
|
||||
lean_assert(c3 * inf == inf); lean_assert(inf * c3 == inf);
|
||||
lean_assert(c4 * inf == inf); lean_assert(inf * c4 == inf);
|
||||
lean_assert(zero * inf == zero);lean_assert(inf * zero == zero);
|
||||
|
||||
}
|
||||
|
||||
static void mpfr_interval_arith() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi i2(3.0, 4.0);
|
||||
fi i3(-10.0, -5.0);
|
||||
fi i4(-3.0, +4.0);
|
||||
fi i5(5.0, 8.0);
|
||||
|
||||
mpfp c1(0.6);
|
||||
mpfp c2(3.0);
|
||||
mpfp c3(0.0);
|
||||
mpfp c4(-4.5);
|
||||
mpfp c5(-0.3);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(i1, "+", c1, i1 + c1);
|
||||
print_result(i2, "+", c2, i2 + c2);
|
||||
print_result(i3, "+", c3, i3 + c3);
|
||||
print_result(i4, "+", c4, i4 + c4);
|
||||
print_result(i5, "+", c5, i5 + c5);
|
||||
print_result(i5, "+", c1, i5 + c1);
|
||||
print_result(i4, "+", c2, i4 + c2);
|
||||
print_result(i2, "+", c4, i2 + c4);
|
||||
print_result(i1, "+", c5, i1 + c5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(c1, "+", i1, c1 + i1);
|
||||
print_result(c2, "+", i2, c2 + i2);
|
||||
print_result(c3, "+", i3, c3 + i3);
|
||||
print_result(c4, "+", i4, c4 + i4);
|
||||
print_result(c5, "+", i5, c5 + i5);
|
||||
print_result(c5, "+", i1, c5 + i1);
|
||||
print_result(c4, "+", i2, c4 + i2);
|
||||
print_result(c2, "+", i4, c2 + i4);
|
||||
print_result(c1, "+", i5, c1 + i5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(i1, "-", c1, i1 - c1);
|
||||
print_result(i2, "-", c2, i2 - c2);
|
||||
print_result(i3, "-", c3, i3 - c3);
|
||||
print_result(i4, "-", c4, i4 - c4);
|
||||
print_result(i5, "-", c5, i5 - c5);
|
||||
print_result(i5, "-", c1, i5 - c1);
|
||||
print_result(i4, "-", c2, i4 - c2);
|
||||
print_result(i2, "-", c4, i2 - c4);
|
||||
print_result(i1, "-", c5, i1 - c5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(c1, "-", i1, c1 - i1);
|
||||
print_result(c2, "-", i2, c2 - i2);
|
||||
print_result(c3, "-", i3, c3 - i3);
|
||||
print_result(c4, "-", i4, c4 - i4);
|
||||
print_result(c5, "-", i5, c5 - i5);
|
||||
print_result(c5, "-", i1, c5 - i1);
|
||||
print_result(c4, "-", i2, c4 - i2);
|
||||
print_result(c2, "-", i4, c2 - i4);
|
||||
print_result(c1, "-", i5, c1 - i5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(i1, "*", c1, i1 * c1);
|
||||
print_result(i2, "*", c2, i2 * c2);
|
||||
print_result(i3, "*", c3, i3 * c3);
|
||||
print_result(i4, "*", c4, i4 * c4);
|
||||
print_result(i5, "*", c5, i5 * c5);
|
||||
print_result(i5, "*", c1, i5 * c1);
|
||||
print_result(i4, "*", c2, i4 * c2);
|
||||
print_result(i2, "*", c4, i2 * c4);
|
||||
print_result(i1, "*", c5, i1 * c5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(c1, "*", i1, c1 * i1);
|
||||
print_result(c2, "*", i2, c2 * i2);
|
||||
print_result(c3, "*", i3, c3 * i3);
|
||||
print_result(c4, "*", i4, c4 * i4);
|
||||
print_result(c5, "*", i5, c5 * i5);
|
||||
print_result(c5, "*", i1, c5 * i1);
|
||||
print_result(c4, "*", i2, c4 * i2);
|
||||
print_result(c2, "*", i4, c2 * i4);
|
||||
print_result(c1, "*", i5, c1 * i5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(i1, "/", c1, i1 / c1);
|
||||
print_result(i2, "/", c2, i2 / c2);
|
||||
print_result(i3, "/", c3, i3 / c3);
|
||||
print_result(i4, "/", c4, i4 / c4);
|
||||
print_result(i5, "/", c5, i5 / c5);
|
||||
print_result(i5, "/", c1, i5 / c1);
|
||||
print_result(i4, "/", c2, i4 / c2);
|
||||
print_result(i2, "/", c4, i2 / c4);
|
||||
print_result(i1, "/", c5, i1 / c5);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
print_result(c1, "/", i1, c1 / i1);
|
||||
print_result(c2, "/", i2, c2 / i2);
|
||||
print_result(c3, "/", i3, c3 / i3);
|
||||
print_result(c5, "/", i5, c5 / i5);
|
||||
print_result(c5, "/", i1, c5 / i1);
|
||||
print_result(c4, "/", i2, c4 / i2);
|
||||
print_result(c1, "/", i5, c1 / i5);
|
||||
}
|
||||
|
||||
static void mpfr_interval_trans() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi i2(3.0, 4.0);
|
||||
fi i3(-10.0, -5.0);
|
||||
fi i4(-3.0, +4.0);
|
||||
fi i5(5.0, 8.0);
|
||||
fi oi1(1.0, 2.0);
|
||||
fi oi2(3.0, 4.0);
|
||||
fi oi3(-10.0, -5.0);
|
||||
fi oi4(-3.0, +4.0);
|
||||
fi oi5(5.0, 8.0);
|
||||
oi1.set_is_lower_open(true); oi1.set_is_upper_open(true);
|
||||
oi2.set_is_lower_open(true); oi2.set_is_upper_open(true);
|
||||
oi3.set_is_lower_open(true); oi3.set_is_upper_open(true);
|
||||
oi4.set_is_lower_open(true); oi4.set_is_upper_open(true);
|
||||
oi5.set_is_lower_open(true); oi5.set_is_upper_open(true);
|
||||
|
||||
fi inf;
|
||||
fi ozero_pinf;
|
||||
fi ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
fi czero_pinf;
|
||||
fi czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
mpfp c1(0.6);
|
||||
mpfp c2(3.0);
|
||||
mpfp c3(0.0);
|
||||
mpfp c4(-4.5);
|
||||
mpfp c5(-0.3);
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "power" << "(" << i1 << ", " << 3 << ") = " << power(i1, 3) << std::endl;
|
||||
std::cout << "power" << "(" << i2 << ", " << 3 << ") = " << power(i2, 3) << std::endl;
|
||||
std::cout << "power" << "(" << i3 << ", " << 3 << ") = " << power(i3, 3) << std::endl;
|
||||
std::cout << "power" << "(" << i4 << ", " << 3 << ") = " << power(i4, 3) << std::endl;
|
||||
std::cout << "power" << "(" << i5 << ", " << 3 << ") = " << power(i5, 3) << std::endl;
|
||||
std::cout << "power" << "(" << oi1 << ", " << 3 << ") = " << power(oi1, 3) << std::endl;
|
||||
std::cout << "power" << "(" << oi2 << ", " << 3 << ") = " << power(oi2, 3) << std::endl;
|
||||
std::cout << "power" << "(" << oi3 << ", " << 3 << ") = " << power(oi3, 3) << std::endl;
|
||||
std::cout << "power" << "(" << oi4 << ", " << 3 << ") = " << power(oi4, 3) << std::endl;
|
||||
std::cout << "power" << "(" << oi5 << ", " << 3 << ") = " << power(oi5, 3) << std::endl;
|
||||
std::cout << "power" << "(" << inf << ", " << 3 << ") = " << power(inf, 3) << std::endl;
|
||||
std::cout << "power" << "(" << ozero_ninf << ", " << 3 << ") = " << power(ozero_ninf, 3) << std::endl;
|
||||
std::cout << "power" << "(" << ozero_pinf << ", " << 3 << ") = " << power(ozero_pinf, 3) << std::endl;
|
||||
std::cout << "power" << "(" << czero_ninf << ", " << 3 << ") = " << power(czero_ninf, 3) << std::endl;
|
||||
std::cout << "power" << "(" << czero_pinf << ", " << 3 << ") = " << power(czero_pinf, 3) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "exp" << "(" << i1 << ") = " << exp(i1) << std::endl;
|
||||
std::cout << "exp" << "(" << i2 << ") = " << exp(i2) << std::endl;
|
||||
std::cout << "exp" << "(" << i3 << ") = " << exp(i3) << std::endl;
|
||||
std::cout << "exp" << "(" << i4 << ") = " << exp(i4) << std::endl;
|
||||
std::cout << "exp" << "(" << i5 << ") = " << exp(i5) << std::endl;
|
||||
std::cout << "exp" << "(" << oi1 << ") = " << exp(oi1) << std::endl;
|
||||
std::cout << "exp" << "(" << oi2 << ") = " << exp(oi2) << std::endl;
|
||||
std::cout << "exp" << "(" << oi3 << ") = " << exp(oi3) << std::endl;
|
||||
std::cout << "exp" << "(" << oi4 << ") = " << exp(oi4) << std::endl;
|
||||
std::cout << "exp" << "(" << oi5 << ") = " << exp(oi5) << std::endl;
|
||||
std::cout << "exp" << "(" << ozero_pinf << ") = " << exp(ozero_pinf) << std::endl;
|
||||
std::cout << "exp" << "(" << ozero_ninf << ") = " << exp(ozero_ninf) << std::endl;
|
||||
std::cout << "exp" << "(" << czero_pinf << ") = " << exp(czero_pinf) << std::endl;
|
||||
std::cout << "exp" << "(" << czero_ninf << ") = " << exp(czero_ninf) << std::endl;
|
||||
std::cout << "exp" << "(" << inf << ") = " << exp(inf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "exp2" << "(" << i1 << ") = " << exp2(i1) << std::endl;
|
||||
std::cout << "exp2" << "(" << i2 << ") = " << exp2(i2) << std::endl;
|
||||
std::cout << "exp2" << "(" << i3 << ") = " << exp2(i3) << std::endl;
|
||||
std::cout << "exp2" << "(" << i4 << ") = " << exp2(i4) << std::endl;
|
||||
std::cout << "exp2" << "(" << i5 << ") = " << exp2(i5) << std::endl;
|
||||
std::cout << "exp2" << "(" << oi1 << ") = " << exp2(oi1) << std::endl;
|
||||
std::cout << "exp2" << "(" << oi2 << ") = " << exp2(oi2) << std::endl;
|
||||
std::cout << "exp2" << "(" << oi3 << ") = " << exp2(oi3) << std::endl;
|
||||
std::cout << "exp2" << "(" << oi4 << ") = " << exp2(oi4) << std::endl;
|
||||
std::cout << "exp2" << "(" << oi5 << ") = " << exp2(oi5) << std::endl;
|
||||
std::cout << "exp2" << "(" << ozero_pinf << ") = " << exp2(ozero_pinf) << std::endl;
|
||||
std::cout << "exp2" << "(" << ozero_ninf << ") = " << exp2(ozero_ninf) << std::endl;
|
||||
std::cout << "exp2" << "(" << czero_pinf << ") = " << exp2(czero_pinf) << std::endl;
|
||||
std::cout << "exp2" << "(" << czero_ninf << ") = " << exp2(czero_ninf) << std::endl;
|
||||
std::cout << "exp2" << "(" << inf << ") = " << exp2(inf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "exp10" << "(" << i1 << ") = " << exp10(i1) << std::endl;
|
||||
std::cout << "exp10" << "(" << i2 << ") = " << exp10(i2) << std::endl;
|
||||
std::cout << "exp10" << "(" << i3 << ") = " << exp10(i3) << std::endl;
|
||||
std::cout << "exp10" << "(" << i4 << ") = " << exp10(i4) << std::endl;
|
||||
std::cout << "exp10" << "(" << i5 << ") = " << exp10(i5) << std::endl;
|
||||
std::cout << "exp10" << "(" << oi1 << ") = " << exp10(oi1) << std::endl;
|
||||
std::cout << "exp10" << "(" << oi2 << ") = " << exp10(oi2) << std::endl;
|
||||
std::cout << "exp10" << "(" << oi3 << ") = " << exp10(oi3) << std::endl;
|
||||
std::cout << "exp10" << "(" << oi4 << ") = " << exp10(oi4) << std::endl;
|
||||
std::cout << "exp10" << "(" << oi5 << ") = " << exp10(oi5) << std::endl;
|
||||
std::cout << "exp10" << "(" << ozero_pinf << ") = " << exp10(ozero_pinf) << std::endl;
|
||||
std::cout << "exp10" << "(" << ozero_ninf << ") = " << exp10(ozero_ninf) << std::endl;
|
||||
std::cout << "exp10" << "(" << czero_pinf << ") = " << exp10(czero_pinf) << std::endl;
|
||||
std::cout << "exp10" << "(" << czero_ninf << ") = " << exp10(czero_ninf) << std::endl;
|
||||
std::cout << "exp10" << "(" << inf << ") = " << exp10(inf) << std::endl;
|
||||
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "log" << "(" << i1 << ") = " << log(i1) << std::endl;
|
||||
std::cout << "log" << "(" << i2 << ") = " << log(i2) << std::endl;
|
||||
std::cout << "log" << "(" << i5 << ") = " << log(i5) << std::endl;
|
||||
std::cout << "log" << "(" << oi1 << ") = " << log(oi1) << std::endl;
|
||||
std::cout << "log" << "(" << oi2 << ") = " << log(oi2) << std::endl;
|
||||
std::cout << "log" << "(" << oi5 << ") = " << log(oi5) << std::endl;
|
||||
std::cout << "log" << "(" << ozero_pinf << ") = " << log(ozero_pinf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "log2" << "(" << i1 << ") = " << log2(i1) << std::endl;
|
||||
std::cout << "log2" << "(" << i2 << ") = " << log2(i2) << std::endl;
|
||||
std::cout << "log2" << "(" << i5 << ") = " << log2(i5) << std::endl;
|
||||
std::cout << "log2" << "(" << oi1 << ") = " << log2(oi1) << std::endl;
|
||||
std::cout << "log2" << "(" << oi2 << ") = " << log2(oi2) << std::endl;
|
||||
std::cout << "log2" << "(" << oi5 << ") = " << log2(oi5) << std::endl;
|
||||
std::cout << "log2" << "(" << ozero_pinf << ") = " << log2(ozero_pinf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "log10" << "(" << i1 << ") = " << log10(i1) << std::endl;
|
||||
std::cout << "log10" << "(" << i2 << ") = " << log10(i2) << std::endl;
|
||||
std::cout << "log10" << "(" << i5 << ") = " << log10(i5) << std::endl;
|
||||
std::cout << "log10" << "(" << oi1 << ") = " << log10(oi1) << std::endl;
|
||||
std::cout << "log10" << "(" << oi2 << ") = " << log10(oi2) << std::endl;
|
||||
std::cout << "log10" << "(" << oi5 << ") = " << log10(oi5) << std::endl;
|
||||
std::cout << "log10" << "(" << ozero_pinf << ") = " << log10(ozero_pinf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "sin" << "(" << i1 << ") = " << sin(i1) << std::endl;
|
||||
std::cout << "sin" << "(" << i2 << ") = " << sin(i2) << std::endl;
|
||||
std::cout << "sin" << "(" << i3 << ") = " << sin(i3) << std::endl;
|
||||
std::cout << "sin" << "(" << i4 << ") = " << sin(i4) << std::endl;
|
||||
std::cout << "sin" << "(" << i5 << ") = " << sin(i5) << std::endl;
|
||||
std::cout << "sin" << "(" << oi1 << ") = " << sin(oi1) << std::endl;
|
||||
std::cout << "sin" << "(" << oi2 << ") = " << sin(oi2) << std::endl;
|
||||
std::cout << "sin" << "(" << oi3 << ") = " << sin(oi3) << std::endl;
|
||||
std::cout << "sin" << "(" << oi4 << ") = " << sin(oi4) << std::endl;
|
||||
std::cout << "sin" << "(" << oi5 << ") = " << sin(oi5) << std::endl;
|
||||
std::cout << "sin" << "(" << ozero_pinf << ") = " << sin(ozero_pinf) << std::endl;
|
||||
std::cout << "sin" << "(" << ozero_ninf << ") = " << sin(ozero_ninf) << std::endl;
|
||||
std::cout << "sin" << "(" << czero_pinf << ") = " << sin(czero_pinf) << std::endl;
|
||||
std::cout << "sin" << "(" << czero_ninf << ") = " << sin(czero_ninf) << std::endl;
|
||||
std::cout << "sin" << "(" << inf << ") = " << sin(inf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "cos" << "(" << i1 << ") = " << cos(i1) << std::endl;
|
||||
std::cout << "cos" << "(" << i2 << ") = " << cos(i2) << std::endl;
|
||||
std::cout << "cos" << "(" << i3 << ") = " << cos(i3) << std::endl;
|
||||
std::cout << "cos" << "(" << i4 << ") = " << cos(i4) << std::endl;
|
||||
std::cout << "cos" << "(" << i5 << ") = " << cos(i5) << std::endl;
|
||||
std::cout << "cos" << "(" << oi1 << ") = " << cos(oi1) << std::endl;
|
||||
std::cout << "cos" << "(" << oi2 << ") = " << cos(oi2) << std::endl;
|
||||
std::cout << "cos" << "(" << oi3 << ") = " << cos(oi3) << std::endl;
|
||||
std::cout << "cos" << "(" << oi4 << ") = " << cos(oi4) << std::endl;
|
||||
std::cout << "cos" << "(" << oi5 << ") = " << cos(oi5) << std::endl;
|
||||
std::cout << "cos" << "(" << ozero_pinf << ") = " << cos(ozero_pinf) << std::endl;
|
||||
std::cout << "cos" << "(" << ozero_ninf << ") = " << cos(ozero_ninf) << std::endl;
|
||||
std::cout << "cos" << "(" << czero_pinf << ") = " << cos(czero_pinf) << std::endl;
|
||||
std::cout << "cos" << "(" << czero_ninf << ") = " << cos(czero_ninf) << std::endl;
|
||||
std::cout << "cos" << "(" << inf << ") = " << cos(inf) << std::endl;
|
||||
|
||||
std::cout << "=====================" << std::endl;
|
||||
std::cout << "tan" << "(" << i1 << ") = " << tan(i1) << std::endl;
|
||||
std::cout << "tan" << "(" << i2 << ") = " << tan(i2) << std::endl;
|
||||
std::cout << "tan" << "(" << i3 << ") = " << tan(i3) << std::endl;
|
||||
std::cout << "tan" << "(" << i4 << ") = " << tan(i4) << std::endl;
|
||||
std::cout << "tan" << "(" << i5 << ") = " << tan(i5) << std::endl;
|
||||
std::cout << "tan" << "(" << oi1 << ") = " << tan(oi1) << std::endl;
|
||||
std::cout << "tan" << "(" << oi2 << ") = " << tan(oi2) << std::endl;
|
||||
std::cout << "tan" << "(" << oi3 << ") = " << tan(oi3) << std::endl;
|
||||
std::cout << "tan" << "(" << oi4 << ") = " << tan(oi4) << std::endl;
|
||||
std::cout << "tan" << "(" << oi5 << ") = " << tan(oi5) << std::endl;
|
||||
std::cout << "tan" << "(" << ozero_pinf << ") = " << tan(ozero_pinf) << std::endl;
|
||||
std::cout << "tan" << "(" << ozero_ninf << ") = " << tan(ozero_ninf) << std::endl;
|
||||
std::cout << "tan" << "(" << czero_pinf << ") = " << tan(czero_pinf) << std::endl;
|
||||
std::cout << "tan" << "(" << czero_ninf << ") = " << tan(czero_ninf) << std::endl;
|
||||
std::cout << "tan" << "(" << inf << ") = " << tan(inf) << std::endl;
|
||||
}
|
||||
|
||||
int main() {
|
||||
continue_on_violation(false);
|
||||
continue_on_violation(true);
|
||||
enable_trace("numerics");
|
||||
tst1();
|
||||
tst2();
|
||||
double_interval_trans();
|
||||
mpfr_interval_arith();
|
||||
mpfr_interval_inf1();
|
||||
mpfr_interval_inf2();
|
||||
mpfr_interval_trans();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
|
|
|
|||
513
src/tests/interval/mpfp_interval.cpp
Normal file
513
src/tests/interval/mpfp_interval.cpp
Normal file
|
|
@ -0,0 +1,513 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
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"
|
||||
|
||||
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);
|
||||
fi i3(-10.0, -5.0);
|
||||
fi i4(-3.0, +4.0);
|
||||
fi i5(5.0, 8.0);
|
||||
|
||||
mpfp c1(0.6);
|
||||
mpfp c2(3.0);
|
||||
mpfp c3(0.0);
|
||||
mpfp c4(-4.5);
|
||||
mpfp c5(-0.3);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "+", c1, i1 + c1);
|
||||
print_result(i2, "+", c2, i2 + c2);
|
||||
print_result(i3, "+", c3, i3 + c3);
|
||||
print_result(i4, "+", c4, i4 + c4);
|
||||
print_result(i5, "+", c5, i5 + c5);
|
||||
print_result(i5, "+", c1, i5 + c1);
|
||||
print_result(i4, "+", c2, i4 + c2);
|
||||
print_result(i2, "+", c4, i2 + c4);
|
||||
print_result(i1, "+", c5, i1 + c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "+", i1, c1 + i1);
|
||||
print_result(c2, "+", i2, c2 + i2);
|
||||
print_result(c3, "+", i3, c3 + i3);
|
||||
print_result(c4, "+", i4, c4 + i4);
|
||||
print_result(c5, "+", i5, c5 + i5);
|
||||
print_result(c5, "+", i1, c5 + i1);
|
||||
print_result(c4, "+", i2, c4 + i2);
|
||||
print_result(c2, "+", i4, c2 + i4);
|
||||
print_result(c1, "+", i5, c1 + i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "-", c1, i1 - c1);
|
||||
print_result(i2, "-", c2, i2 - c2);
|
||||
print_result(i3, "-", c3, i3 - c3);
|
||||
print_result(i4, "-", c4, i4 - c4);
|
||||
print_result(i5, "-", c5, i5 - c5);
|
||||
print_result(i5, "-", c1, i5 - c1);
|
||||
print_result(i4, "-", c2, i4 - c2);
|
||||
print_result(i2, "-", c4, i2 - c4);
|
||||
print_result(i1, "-", c5, i1 - c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "-", i1, c1 - i1);
|
||||
print_result(c2, "-", i2, c2 - i2);
|
||||
print_result(c3, "-", i3, c3 - i3);
|
||||
print_result(c4, "-", i4, c4 - i4);
|
||||
print_result(c5, "-", i5, c5 - i5);
|
||||
print_result(c5, "-", i1, c5 - i1);
|
||||
print_result(c4, "-", i2, c4 - i2);
|
||||
print_result(c2, "-", i4, c2 - i4);
|
||||
print_result(c1, "-", i5, c1 - i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "*", c1, i1 * c1);
|
||||
print_result(i2, "*", c2, i2 * c2);
|
||||
print_result(i3, "*", c3, i3 * c3);
|
||||
print_result(i4, "*", c4, i4 * c4);
|
||||
print_result(i5, "*", c5, i5 * c5);
|
||||
print_result(i5, "*", c1, i5 * c1);
|
||||
print_result(i4, "*", c2, i4 * c2);
|
||||
print_result(i2, "*", c4, i2 * c4);
|
||||
print_result(i1, "*", c5, i1 * c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "*", i1, c1 * i1);
|
||||
print_result(c2, "*", i2, c2 * i2);
|
||||
print_result(c3, "*", i3, c3 * i3);
|
||||
print_result(c4, "*", i4, c4 * i4);
|
||||
print_result(c5, "*", i5, c5 * i5);
|
||||
print_result(c5, "*", i1, c5 * i1);
|
||||
print_result(c4, "*", i2, c4 * i2);
|
||||
print_result(c2, "*", i4, c2 * i4);
|
||||
print_result(c1, "*", i5, c1 * i5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(i1, "/", c1, i1 / c1);
|
||||
print_result(i2, "/", c2, i2 / c2);
|
||||
print_result(i3, "/", c3, i3 / c3);
|
||||
print_result(i4, "/", c4, i4 / c4);
|
||||
print_result(i5, "/", c5, i5 / c5);
|
||||
print_result(i5, "/", c1, i5 / c1);
|
||||
print_result(i4, "/", c2, i4 / c2);
|
||||
print_result(i2, "/", c4, i2 / c4);
|
||||
print_result(i1, "/", c5, i1 / c5);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
print_result(c1, "/", i1, c1 / i1);
|
||||
print_result(c2, "/", i2, c2 / i2);
|
||||
print_result(c3, "/", i3, c3 / i3);
|
||||
print_result(c5, "/", i5, c5 / i5);
|
||||
print_result(c5, "/", i1, c5 / i1);
|
||||
print_result(c4, "/", i2, c4 / i2);
|
||||
print_result(c1, "/", i5, c1 / i5);
|
||||
}
|
||||
|
||||
static void mpfp_interval_inf1() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi inf;
|
||||
fi ozero_pinf;
|
||||
fi ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
fi czero_pinf;
|
||||
fi czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
cout << i1 << " * " << ozero_ninf << " = " << i1 * ozero_ninf << endl;
|
||||
cout << i1 << " * " << ozero_pinf << " = " << i1 * ozero_pinf << endl;
|
||||
cout << i1 << " * " << czero_ninf << " = " << i1 * czero_ninf << endl;
|
||||
cout << i1 << " * " << czero_pinf << " = " << i1 * czero_pinf << endl;
|
||||
lean_assert(i1 * ozero_ninf == ozero_ninf); lean_assert(ozero_ninf * i1 == ozero_ninf);
|
||||
lean_assert(i1 * ozero_pinf == ozero_pinf); lean_assert(ozero_pinf * i1 == ozero_pinf);
|
||||
lean_assert(i1 * czero_ninf == czero_ninf); lean_assert(czero_ninf * i1 == czero_ninf);
|
||||
lean_assert(i1 * czero_pinf == czero_pinf); lean_assert(czero_pinf * i1 == czero_pinf);
|
||||
|
||||
cout << "=== Addition between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " + " << ozero_ninf << " = " << ozero_ninf + ozero_ninf << endl;
|
||||
cout << ozero_ninf << " + " << ozero_pinf << " = " << ozero_ninf + ozero_pinf << endl;
|
||||
cout << ozero_ninf << " + " << czero_ninf << " = " << ozero_ninf + czero_ninf << endl;
|
||||
cout << ozero_ninf << " + " << czero_pinf << " = " << ozero_ninf + czero_pinf << endl;
|
||||
cout << ozero_pinf << " + " << ozero_ninf << " = " << ozero_pinf + ozero_ninf << endl;
|
||||
cout << ozero_pinf << " + " << ozero_pinf << " = " << ozero_pinf + ozero_pinf << endl;
|
||||
cout << ozero_pinf << " + " << czero_ninf << " = " << ozero_pinf + czero_ninf << endl;
|
||||
cout << ozero_pinf << " + " << czero_pinf << " = " << ozero_pinf + czero_pinf << endl;
|
||||
cout << czero_ninf << " + " << ozero_ninf << " = " << czero_ninf + ozero_ninf << endl;
|
||||
cout << czero_ninf << " + " << ozero_pinf << " = " << czero_ninf + ozero_pinf << endl;
|
||||
cout << czero_ninf << " + " << czero_ninf << " = " << czero_ninf + czero_ninf << endl;
|
||||
cout << czero_ninf << " + " << czero_pinf << " = " << czero_ninf + czero_pinf << endl;
|
||||
cout << czero_pinf << " + " << ozero_ninf << " = " << czero_pinf + ozero_ninf << endl;
|
||||
cout << czero_pinf << " + " << ozero_pinf << " = " << czero_pinf + ozero_pinf << endl;
|
||||
cout << czero_pinf << " + " << czero_ninf << " = " << czero_pinf + czero_ninf << endl;
|
||||
cout << czero_pinf << " + " << czero_pinf << " = " << czero_pinf + czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + ozero_pinf == inf);
|
||||
lean_assert(ozero_ninf + czero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_ninf + czero_pinf == inf);
|
||||
lean_assert(ozero_pinf + ozero_ninf == inf);
|
||||
lean_assert(ozero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf + czero_ninf == inf);
|
||||
lean_assert(ozero_pinf + czero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf + ozero_ninf == ozero_ninf);
|
||||
lean_assert(czero_ninf + ozero_pinf == inf);
|
||||
lean_assert(czero_ninf + czero_ninf == czero_ninf);
|
||||
lean_assert(czero_ninf + czero_pinf == inf);
|
||||
lean_assert(czero_pinf + ozero_ninf == inf);
|
||||
lean_assert(czero_pinf + ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_pinf + czero_ninf == inf);
|
||||
lean_assert(czero_pinf + czero_pinf == czero_pinf);
|
||||
|
||||
cout << "=== Subtraction between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " - " << ozero_ninf << " = " << ozero_ninf - ozero_ninf << endl;
|
||||
cout << ozero_ninf << " - " << ozero_pinf << " = " << ozero_ninf - ozero_pinf << endl;
|
||||
cout << ozero_ninf << " - " << czero_ninf << " = " << ozero_ninf - czero_ninf << endl;
|
||||
cout << ozero_ninf << " - " << czero_pinf << " = " << ozero_ninf - czero_pinf << endl;
|
||||
cout << ozero_pinf << " - " << ozero_ninf << " = " << ozero_pinf - ozero_ninf << endl;
|
||||
cout << ozero_pinf << " - " << ozero_pinf << " = " << ozero_pinf - ozero_pinf << endl;
|
||||
cout << ozero_pinf << " - " << czero_ninf << " = " << ozero_pinf - czero_ninf << endl;
|
||||
cout << ozero_pinf << " - " << czero_pinf << " = " << ozero_pinf - czero_pinf << endl;
|
||||
cout << czero_ninf << " - " << ozero_ninf << " = " << czero_ninf - ozero_ninf << endl;
|
||||
cout << czero_ninf << " - " << ozero_pinf << " = " << czero_ninf - ozero_pinf << endl;
|
||||
cout << czero_ninf << " - " << czero_ninf << " = " << czero_ninf - czero_ninf << endl;
|
||||
cout << czero_ninf << " - " << czero_pinf << " = " << czero_ninf - czero_pinf << endl;
|
||||
cout << czero_pinf << " - " << ozero_ninf << " = " << czero_pinf - ozero_ninf << endl;
|
||||
cout << czero_pinf << " - " << ozero_pinf << " = " << czero_pinf - ozero_pinf << endl;
|
||||
cout << czero_pinf << " - " << czero_ninf << " = " << czero_pinf - czero_ninf << endl;
|
||||
cout << czero_pinf << " - " << czero_pinf << " = " << czero_pinf - czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf - ozero_ninf == inf);
|
||||
lean_assert(ozero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf - czero_ninf == inf);
|
||||
lean_assert(ozero_ninf - czero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - ozero_pinf == inf);
|
||||
lean_assert(ozero_pinf - czero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_pinf - czero_pinf == inf);
|
||||
lean_assert(czero_ninf - ozero_ninf == inf);
|
||||
lean_assert(czero_ninf - ozero_pinf == ozero_ninf);
|
||||
lean_assert(czero_ninf - czero_ninf == inf);
|
||||
lean_assert(czero_ninf - czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf - ozero_ninf == ozero_pinf);
|
||||
lean_assert(czero_pinf - ozero_pinf == inf);
|
||||
lean_assert(czero_pinf - czero_ninf == czero_pinf);
|
||||
lean_assert(czero_pinf - czero_pinf == inf);
|
||||
|
||||
cout << "=== Multiplication between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " * " << ozero_ninf << " = " << ozero_ninf * ozero_ninf << endl;
|
||||
cout << ozero_ninf << " * " << ozero_pinf << " = " << ozero_ninf * ozero_pinf << endl;
|
||||
cout << ozero_ninf << " * " << czero_ninf << " = " << ozero_ninf * czero_ninf << endl;
|
||||
cout << ozero_ninf << " * " << czero_pinf << " = " << ozero_ninf * czero_pinf << endl;
|
||||
cout << ozero_pinf << " * " << ozero_ninf << " = " << ozero_pinf * ozero_ninf << endl;
|
||||
cout << ozero_pinf << " * " << ozero_pinf << " = " << ozero_pinf * ozero_pinf << endl;
|
||||
cout << ozero_pinf << " * " << czero_ninf << " = " << ozero_pinf * czero_ninf << endl;
|
||||
cout << ozero_pinf << " * " << czero_pinf << " = " << ozero_pinf * czero_pinf << endl;
|
||||
cout << czero_ninf << " * " << ozero_ninf << " = " << czero_ninf * ozero_ninf << endl;
|
||||
cout << czero_ninf << " * " << ozero_pinf << " = " << czero_ninf * ozero_pinf << endl;
|
||||
cout << czero_ninf << " * " << czero_ninf << " = " << czero_ninf * czero_ninf << endl;
|
||||
cout << czero_ninf << " * " << czero_pinf << " = " << czero_ninf * czero_pinf << endl;
|
||||
cout << czero_pinf << " * " << ozero_ninf << " = " << czero_pinf * ozero_ninf << endl;
|
||||
cout << czero_pinf << " * " << ozero_pinf << " = " << czero_pinf * ozero_pinf << endl;
|
||||
cout << czero_pinf << " * " << czero_ninf << " = " << czero_pinf * czero_ninf << endl;
|
||||
cout << czero_pinf << " * " << czero_pinf << " = " << czero_pinf * czero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf * ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf * ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(ozero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf * ozero_pinf == ozero_pinf);
|
||||
lean_assert(ozero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(ozero_pinf * czero_pinf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_ninf * czero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf * czero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * ozero_pinf == czero_pinf);
|
||||
lean_assert(czero_pinf * czero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf * czero_pinf == czero_pinf);
|
||||
|
||||
cout << "=== Division between [0, +oo), (-oo, 0], (0, +oo), (-oo, 0) ===" << endl;
|
||||
cout << ozero_ninf << " / " << ozero_ninf << " = " << ozero_ninf / ozero_ninf << endl;
|
||||
cout << ozero_ninf << " / " << ozero_pinf << " = " << ozero_ninf / ozero_pinf << endl;
|
||||
cout << ozero_pinf << " / " << ozero_ninf << " = " << ozero_pinf / ozero_ninf << endl;
|
||||
cout << ozero_pinf << " / " << ozero_pinf << " = " << ozero_pinf / ozero_pinf << endl;
|
||||
cout << czero_ninf << " / " << ozero_ninf << " = " << czero_ninf / ozero_ninf << endl;
|
||||
cout << czero_ninf << " / " << ozero_pinf << " = " << czero_ninf / ozero_pinf << endl;
|
||||
cout << czero_pinf << " / " << ozero_ninf << " = " << czero_pinf / ozero_ninf << endl;
|
||||
cout << czero_pinf << " / " << ozero_pinf << " = " << czero_pinf / ozero_pinf << endl;
|
||||
|
||||
lean_assert(ozero_ninf / ozero_ninf == ozero_pinf);
|
||||
lean_assert(ozero_ninf / ozero_pinf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_ninf == ozero_ninf);
|
||||
lean_assert(ozero_pinf / ozero_pinf == ozero_pinf);
|
||||
lean_assert(czero_ninf / ozero_ninf == czero_pinf);
|
||||
lean_assert(czero_ninf / ozero_pinf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_ninf == czero_ninf);
|
||||
lean_assert(czero_pinf / ozero_pinf == czero_pinf);
|
||||
}
|
||||
|
||||
static void mpfp_interval_inf2() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi i2(3.0, 4.0);
|
||||
fi i3(-10.0, -5.0);
|
||||
fi i4(-3.0, +4.0);
|
||||
fi i5(5.0, 8.0);
|
||||
fi inf;
|
||||
|
||||
mpfp c1(0.6);
|
||||
mpfp c2(3.0);
|
||||
mpfp c3(-0.3);
|
||||
mpfp c4(-4.5);
|
||||
mpfp zero(0.0);
|
||||
|
||||
lean_assert(i1 + inf == inf); lean_assert(inf + i1 == inf);
|
||||
lean_assert(i2 + inf == inf); lean_assert(inf + i2 == inf);
|
||||
lean_assert(i3 + inf == inf); lean_assert(inf + i3 == inf);
|
||||
lean_assert(i4 + inf == inf); lean_assert(inf + i4 == inf);
|
||||
lean_assert(i5 + inf == inf); lean_assert(inf + i5 == inf);
|
||||
lean_assert(c1 + inf == inf); lean_assert(inf + c1 == inf);
|
||||
lean_assert(c2 + inf == inf); lean_assert(inf + c2 == inf);
|
||||
lean_assert(c3 + inf == inf); lean_assert(inf + c3 == inf);
|
||||
lean_assert(c4 + inf == inf); lean_assert(inf + c4 == inf);
|
||||
lean_assert(zero + inf == inf); lean_assert(inf + zero == inf);
|
||||
|
||||
lean_assert(i1 - inf == inf); lean_assert(inf - i1 == inf);
|
||||
lean_assert(i2 - inf == inf); lean_assert(inf - i2 == inf);
|
||||
lean_assert(i3 - inf == inf); lean_assert(inf - i3 == inf);
|
||||
lean_assert(i4 - inf == inf); lean_assert(inf - i4 == inf);
|
||||
lean_assert(i5 - inf == inf); lean_assert(inf - i5 == inf);
|
||||
lean_assert(c1 - inf == inf); lean_assert(inf - c1 == inf);
|
||||
lean_assert(c2 - inf == inf); lean_assert(inf - c2 == inf);
|
||||
lean_assert(c3 - inf == inf); lean_assert(inf - c3 == inf);
|
||||
lean_assert(c4 - inf == inf); lean_assert(inf - c4 == inf);
|
||||
lean_assert(zero - inf == inf); lean_assert(inf - zero == inf);
|
||||
|
||||
lean_assert(i1 * inf == inf); lean_assert(inf * i1 == inf);
|
||||
lean_assert(i2 * inf == inf); lean_assert(inf * i2 == inf);
|
||||
lean_assert(i3 * inf == inf); lean_assert(inf * i3 == inf);
|
||||
lean_assert(i4 * inf == inf); lean_assert(inf * i4 == inf);
|
||||
lean_assert(i5 * inf == inf); lean_assert(inf * i5 == inf);
|
||||
lean_assert(c1 * inf == inf); lean_assert(inf * c1 == inf);
|
||||
lean_assert(c2 * inf == inf); lean_assert(inf * c2 == inf);
|
||||
lean_assert(c3 * inf == inf); lean_assert(inf * c3 == inf);
|
||||
lean_assert(c4 * inf == inf); lean_assert(inf * c4 == inf);
|
||||
lean_assert(zero * inf == zero);lean_assert(inf * zero == zero);
|
||||
}
|
||||
|
||||
static void mpfp_interval_trans() {
|
||||
fi i1(1.0, 2.0);
|
||||
fi i2(3.0, 4.0);
|
||||
fi i3(-10.0, -5.0);
|
||||
fi i4(-3.0, +4.0);
|
||||
fi i5(5.0, 8.0);
|
||||
fi oi1(1.0, 2.0);
|
||||
fi oi2(3.0, 4.0);
|
||||
fi oi3(-10.0, -5.0);
|
||||
fi oi4(-3.0, +4.0);
|
||||
fi oi5(5.0, 8.0);
|
||||
oi1.set_is_lower_open(true); oi1.set_is_upper_open(true);
|
||||
oi2.set_is_lower_open(true); oi2.set_is_upper_open(true);
|
||||
oi3.set_is_lower_open(true); oi3.set_is_upper_open(true);
|
||||
oi4.set_is_lower_open(true); oi4.set_is_upper_open(true);
|
||||
oi5.set_is_lower_open(true); oi5.set_is_upper_open(true);
|
||||
|
||||
fi inf;
|
||||
fi ozero_pinf;
|
||||
fi ozero_ninf;
|
||||
ozero_pinf.set_is_lower_inf(false);
|
||||
ozero_ninf.set_is_upper_inf(false);
|
||||
fi czero_pinf;
|
||||
fi czero_ninf;
|
||||
czero_pinf.set_is_lower_inf(false);
|
||||
czero_pinf.set_is_lower_open(false);
|
||||
czero_ninf.set_is_upper_inf(false);
|
||||
czero_ninf.set_is_upper_open(false);
|
||||
|
||||
mpfp c1(0.6);
|
||||
mpfp c2(3.0);
|
||||
mpfp c3(0.0);
|
||||
mpfp c4(-4.5);
|
||||
mpfp c5(-0.3);
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "power" << "(" << i1 << ", " << 3 << ") = " << power(i1, 3) << endl;
|
||||
cout << "power" << "(" << i2 << ", " << 3 << ") = " << power(i2, 3) << endl;
|
||||
cout << "power" << "(" << i3 << ", " << 3 << ") = " << power(i3, 3) << endl;
|
||||
cout << "power" << "(" << i4 << ", " << 3 << ") = " << power(i4, 3) << endl;
|
||||
cout << "power" << "(" << i5 << ", " << 3 << ") = " << power(i5, 3) << endl;
|
||||
cout << "power" << "(" << oi1 << ", " << 3 << ") = " << power(oi1, 3) << endl;
|
||||
cout << "power" << "(" << oi2 << ", " << 3 << ") = " << power(oi2, 3) << endl;
|
||||
cout << "power" << "(" << oi3 << ", " << 3 << ") = " << power(oi3, 3) << endl;
|
||||
cout << "power" << "(" << oi4 << ", " << 3 << ") = " << power(oi4, 3) << endl;
|
||||
cout << "power" << "(" << oi5 << ", " << 3 << ") = " << power(oi5, 3) << endl;
|
||||
cout << "power" << "(" << inf << ", " << 3 << ") = " << power(inf, 3) << endl;
|
||||
cout << "power" << "(" << ozero_ninf << ", " << 3 << ") = " << power(ozero_ninf, 3) << endl;
|
||||
cout << "power" << "(" << ozero_pinf << ", " << 3 << ") = " << power(ozero_pinf, 3) << endl;
|
||||
cout << "power" << "(" << czero_ninf << ", " << 3 << ") = " << power(czero_ninf, 3) << endl;
|
||||
cout << "power" << "(" << czero_pinf << ", " << 3 << ") = " << power(czero_pinf, 3) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp" << "(" << i1 << ") = " << exp(i1) << endl;
|
||||
cout << "exp" << "(" << i2 << ") = " << exp(i2) << endl;
|
||||
cout << "exp" << "(" << i3 << ") = " << exp(i3) << endl;
|
||||
cout << "exp" << "(" << i4 << ") = " << exp(i4) << endl;
|
||||
cout << "exp" << "(" << i5 << ") = " << exp(i5) << endl;
|
||||
cout << "exp" << "(" << oi1 << ") = " << exp(oi1) << endl;
|
||||
cout << "exp" << "(" << oi2 << ") = " << exp(oi2) << endl;
|
||||
cout << "exp" << "(" << oi3 << ") = " << exp(oi3) << endl;
|
||||
cout << "exp" << "(" << oi4 << ") = " << exp(oi4) << endl;
|
||||
cout << "exp" << "(" << oi5 << ") = " << exp(oi5) << endl;
|
||||
cout << "exp" << "(" << ozero_pinf << ") = " << exp(ozero_pinf) << endl;
|
||||
cout << "exp" << "(" << ozero_ninf << ") = " << exp(ozero_ninf) << endl;
|
||||
cout << "exp" << "(" << czero_pinf << ") = " << exp(czero_pinf) << endl;
|
||||
cout << "exp" << "(" << czero_ninf << ") = " << exp(czero_ninf) << endl;
|
||||
cout << "exp" << "(" << inf << ") = " << exp(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp2" << "(" << i1 << ") = " << exp2(i1) << endl;
|
||||
cout << "exp2" << "(" << i2 << ") = " << exp2(i2) << endl;
|
||||
cout << "exp2" << "(" << i3 << ") = " << exp2(i3) << endl;
|
||||
cout << "exp2" << "(" << i4 << ") = " << exp2(i4) << endl;
|
||||
cout << "exp2" << "(" << i5 << ") = " << exp2(i5) << endl;
|
||||
cout << "exp2" << "(" << oi1 << ") = " << exp2(oi1) << endl;
|
||||
cout << "exp2" << "(" << oi2 << ") = " << exp2(oi2) << endl;
|
||||
cout << "exp2" << "(" << oi3 << ") = " << exp2(oi3) << endl;
|
||||
cout << "exp2" << "(" << oi4 << ") = " << exp2(oi4) << endl;
|
||||
cout << "exp2" << "(" << oi5 << ") = " << exp2(oi5) << endl;
|
||||
cout << "exp2" << "(" << ozero_pinf << ") = " << exp2(ozero_pinf) << endl;
|
||||
cout << "exp2" << "(" << ozero_ninf << ") = " << exp2(ozero_ninf) << endl;
|
||||
cout << "exp2" << "(" << czero_pinf << ") = " << exp2(czero_pinf) << endl;
|
||||
cout << "exp2" << "(" << czero_ninf << ") = " << exp2(czero_ninf) << endl;
|
||||
cout << "exp2" << "(" << inf << ") = " << exp2(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "exp10" << "(" << i1 << ") = " << exp10(i1) << endl;
|
||||
cout << "exp10" << "(" << i2 << ") = " << exp10(i2) << endl;
|
||||
cout << "exp10" << "(" << i3 << ") = " << exp10(i3) << endl;
|
||||
cout << "exp10" << "(" << i4 << ") = " << exp10(i4) << endl;
|
||||
cout << "exp10" << "(" << i5 << ") = " << exp10(i5) << endl;
|
||||
cout << "exp10" << "(" << oi1 << ") = " << exp10(oi1) << endl;
|
||||
cout << "exp10" << "(" << oi2 << ") = " << exp10(oi2) << endl;
|
||||
cout << "exp10" << "(" << oi3 << ") = " << exp10(oi3) << endl;
|
||||
cout << "exp10" << "(" << oi4 << ") = " << exp10(oi4) << endl;
|
||||
cout << "exp10" << "(" << oi5 << ") = " << exp10(oi5) << endl;
|
||||
cout << "exp10" << "(" << ozero_pinf << ") = " << exp10(ozero_pinf) << endl;
|
||||
cout << "exp10" << "(" << ozero_ninf << ") = " << exp10(ozero_ninf) << endl;
|
||||
cout << "exp10" << "(" << czero_pinf << ") = " << exp10(czero_pinf) << endl;
|
||||
cout << "exp10" << "(" << czero_ninf << ") = " << exp10(czero_ninf) << endl;
|
||||
cout << "exp10" << "(" << inf << ") = " << exp10(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log" << "(" << i1 << ") = " << log(i1) << endl;
|
||||
cout << "log" << "(" << i2 << ") = " << log(i2) << endl;
|
||||
cout << "log" << "(" << i5 << ") = " << log(i5) << endl;
|
||||
cout << "log" << "(" << oi1 << ") = " << log(oi1) << endl;
|
||||
cout << "log" << "(" << oi2 << ") = " << log(oi2) << endl;
|
||||
cout << "log" << "(" << oi5 << ") = " << log(oi5) << endl;
|
||||
cout << "log" << "(" << ozero_pinf << ") = " << log(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log2" << "(" << i1 << ") = " << log2(i1) << endl;
|
||||
cout << "log2" << "(" << i2 << ") = " << log2(i2) << endl;
|
||||
cout << "log2" << "(" << i5 << ") = " << log2(i5) << endl;
|
||||
cout << "log2" << "(" << oi1 << ") = " << log2(oi1) << endl;
|
||||
cout << "log2" << "(" << oi2 << ") = " << log2(oi2) << endl;
|
||||
cout << "log2" << "(" << oi5 << ") = " << log2(oi5) << endl;
|
||||
cout << "log2" << "(" << ozero_pinf << ") = " << log2(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "log10" << "(" << i1 << ") = " << log10(i1) << endl;
|
||||
cout << "log10" << "(" << i2 << ") = " << log10(i2) << endl;
|
||||
cout << "log10" << "(" << i5 << ") = " << log10(i5) << endl;
|
||||
cout << "log10" << "(" << oi1 << ") = " << log10(oi1) << endl;
|
||||
cout << "log10" << "(" << oi2 << ") = " << log10(oi2) << endl;
|
||||
cout << "log10" << "(" << oi5 << ") = " << log10(oi5) << endl;
|
||||
cout << "log10" << "(" << ozero_pinf << ") = " << log10(ozero_pinf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "sin" << "(" << i1 << ") = " << sin(i1) << endl;
|
||||
cout << "sin" << "(" << i2 << ") = " << sin(i2) << endl;
|
||||
cout << "sin" << "(" << i3 << ") = " << sin(i3) << endl;
|
||||
cout << "sin" << "(" << i4 << ") = " << sin(i4) << endl;
|
||||
cout << "sin" << "(" << i5 << ") = " << sin(i5) << endl;
|
||||
cout << "sin" << "(" << oi1 << ") = " << sin(oi1) << endl;
|
||||
cout << "sin" << "(" << oi2 << ") = " << sin(oi2) << endl;
|
||||
cout << "sin" << "(" << oi3 << ") = " << sin(oi3) << endl;
|
||||
cout << "sin" << "(" << oi4 << ") = " << sin(oi4) << endl;
|
||||
cout << "sin" << "(" << oi5 << ") = " << sin(oi5) << endl;
|
||||
cout << "sin" << "(" << ozero_pinf << ") = " << sin(ozero_pinf) << endl;
|
||||
cout << "sin" << "(" << ozero_ninf << ") = " << sin(ozero_ninf) << endl;
|
||||
cout << "sin" << "(" << czero_pinf << ") = " << sin(czero_pinf) << endl;
|
||||
cout << "sin" << "(" << czero_ninf << ") = " << sin(czero_ninf) << endl;
|
||||
cout << "sin" << "(" << inf << ") = " << sin(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "cos" << "(" << i1 << ") = " << cos(i1) << endl;
|
||||
cout << "cos" << "(" << i2 << ") = " << cos(i2) << endl;
|
||||
cout << "cos" << "(" << i3 << ") = " << cos(i3) << endl;
|
||||
cout << "cos" << "(" << i4 << ") = " << cos(i4) << endl;
|
||||
cout << "cos" << "(" << i5 << ") = " << cos(i5) << endl;
|
||||
cout << "cos" << "(" << oi1 << ") = " << cos(oi1) << endl;
|
||||
cout << "cos" << "(" << oi2 << ") = " << cos(oi2) << endl;
|
||||
cout << "cos" << "(" << oi3 << ") = " << cos(oi3) << endl;
|
||||
cout << "cos" << "(" << oi4 << ") = " << cos(oi4) << endl;
|
||||
cout << "cos" << "(" << oi5 << ") = " << cos(oi5) << endl;
|
||||
cout << "cos" << "(" << ozero_pinf << ") = " << cos(ozero_pinf) << endl;
|
||||
cout << "cos" << "(" << ozero_ninf << ") = " << cos(ozero_ninf) << endl;
|
||||
cout << "cos" << "(" << czero_pinf << ") = " << cos(czero_pinf) << endl;
|
||||
cout << "cos" << "(" << czero_ninf << ") = " << cos(czero_ninf) << endl;
|
||||
cout << "cos" << "(" << inf << ") = " << cos(inf) << endl;
|
||||
|
||||
cout << "=====================" << endl;
|
||||
cout << "tan" << "(" << i1 << ") = " << tan(i1) << endl;
|
||||
cout << "tan" << "(" << i2 << ") = " << tan(i2) << endl;
|
||||
cout << "tan" << "(" << i3 << ") = " << tan(i3) << endl;
|
||||
cout << "tan" << "(" << i4 << ") = " << tan(i4) << endl;
|
||||
cout << "tan" << "(" << i5 << ") = " << tan(i5) << endl;
|
||||
cout << "tan" << "(" << oi1 << ") = " << tan(oi1) << endl;
|
||||
cout << "tan" << "(" << oi2 << ") = " << tan(oi2) << endl;
|
||||
cout << "tan" << "(" << oi3 << ") = " << tan(oi3) << endl;
|
||||
cout << "tan" << "(" << oi4 << ") = " << tan(oi4) << endl;
|
||||
cout << "tan" << "(" << oi5 << ") = " << tan(oi5) << endl;
|
||||
cout << "tan" << "(" << ozero_pinf << ") = " << tan(ozero_pinf) << endl;
|
||||
cout << "tan" << "(" << ozero_ninf << ") = " << tan(ozero_ninf) << endl;
|
||||
cout << "tan" << "(" << czero_pinf << ") = " << tan(czero_pinf) << endl;
|
||||
cout << "tan" << "(" << czero_ninf << ") = " << tan(czero_ninf) << endl;
|
||||
cout << "tan" << "(" << inf << ") = " << tan(inf) << endl;
|
||||
}
|
||||
|
||||
int main() {
|
||||
continue_on_violation(true);
|
||||
enable_trace("numerics");
|
||||
mpfp_interval_arith();
|
||||
mpfp_interval_inf1();
|
||||
mpfp_interval_inf2();
|
||||
mpfp_interval_trans();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
||||
Loading…
Reference in a new issue