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

Add double/mpfp interval tests

Browse source
This commit is contained in:
Soonho Kong 2013-08-12 12:58:18 -07:00
parent 71e10a0336
commit 6bbe592e2a
1 changed files with 14 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/tests/interval/interval.cpp
View file

@ -5,14 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include <vector> #include <vector>
#include "interval.h"
#include "test.h" #include "test.h"
#include "trace.h" #include "trace.h"
#include "double.h"
#include "mpq.h" #include "mpq.h"
#include "mpfp.h" #include "mpfp.h"
#include "interval_def.h"
using namespace lean; using namespace lean;
typedef interval<mpq> qi; typedef interval<double> qi;
typedef interval<double> di; typedef interval<double> di;
typedef interval<mpfp> fi; typedef interval<mpfp> fi;
typedef std::vector<qi> qiv; typedef std::vector<qi> qiv;
@ -88,18 +90,26 @@ static void tst2() {
lean_assert(power(qi(),2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo) lean_assert(power(qi(),2) == qi(false, 0)); // (-oo, oo)^2 == [0, oo)
} }
static void tst3() { static void double_interval_trans() {
di i1(1.0, 2.0); di i1(1.0, 2.0);
std::cout << "power(" << i1 << ", 3) = " << power(i1, 3) << std::endl; std::cout << "power(" << i1 << ", 3) = " << power(i1, 3) << std::endl;
std::cout << "exp(" << i1 << ") = " << exp(i1) << std::endl; std::cout << "exp(" << i1 << ") = " << exp(i1) << std::endl;
std::cout << "log(" << i1 << ") = " << log(i1) << std::endl; std::cout << "log(" << i1 << ") = " << log(i1) << std::endl;
} }
static void mpfr_interval_trans() {
fi 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;
}
int main() { int main() {
continue_on_violation(true); continue_on_violation(true);
enable_trace("numerics"); enable_trace("numerics");
tst1(); tst1();
tst2(); tst2();
tst3(); double_interval_trans();
mpfr_interval_trans();
return has_violations() ? 1 : 0; return has_violations() ? 1 : 0;
} }