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

test(util/numerics/mpbp): add more tests for improving coverage

Browse source
This commit is contained in:
Soonho Kong 2013-09-28 01:01:23 -07:00
parent 6519d4bb0f
commit fb3635a9ef
1 changed files with 143 additions and 34 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

177
src/tests/util/numerics/mpbq.cpp
View file

@ -3,6 +3,7 @@ Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Soonho Kong
*/
#include <iostream>
#include <sstream>
@ -14,23 +15,23 @@ using namespace lean;
static void tst1() {
mpbq a(1, 1);
std::cout << a << "\n";
lean_assert(a == mpq(1, 2));
lean_assert_eq(a, mpq(1, 2));
std::cout << mpbq(mpq(1, 3)) << "\n";
lean_assert(!set(a, mpq(1, 3)));
lean_assert(a == mpbq(1, 2));
lean_assert_eq(a, mpbq(1, 2));
mpq b;
b = a;
lean_assert(b == mpq(1, 4));
lean_assert(inv(b) == 4);
lean_assert(a/2 == mpbq(1, 3));
lean_assert(a/1 == a);
lean_assert(a/8 == mpbq(1, 5));
lean_assert((3*a)/8 == mpbq(3, 5));
lean_assert_eq(b, mpq(1, 4));
lean_assert_eq(inv(b), 4);
lean_assert_eq(a/2, mpbq(1, 3));
lean_assert_eq(a/1, a);
lean_assert_eq(a/8, mpbq(1, 5));
lean_assert_eq(3*a/8, mpbq(3, 5));
mpbq l(0), u(1);
mpq v(1, 3);
while (true) {
lean_assert(l < v);
lean_assert(v < u);
lean_assert_lt(l, v);
lean_assert_lt(v, u);
std::cout << mpbq::decimal(l, 20) << " " << v << " " << mpbq::decimal(u, 20) << "\n";
if (lt_1div2k((u - l)/2, 50))
break;
@ -43,52 +44,160 @@ static void tst2() {
mpbq num(2);
std::ostringstream out;
out << num;
lean_assert(out.str() == "2");
lean_assert_eq(out.str(), "2");
mpbq a(-1, 2);
std::ostringstream out2;
display_decimal(out2, a, 10);
lean_assert(out2.str() == "-0.25");
lean_assert_eq(out2.str(), "-0.25");
lean_assert(lt_1div2k(a, 8));
mul2(a);
lean_assert(a == mpbq(-1, 1));
lean_assert_eq(a, mpbq(-1, 1));
mul2k(a, 3);
lean_assert(a == mpbq(-4));
lean_assert_eq(a, mpbq(-4));
mul2k(a, 0);
lean_assert(a == mpbq(-4));
lean_assert_eq(a, mpbq(-4));
mul2k(a, 2);
lean_assert(a == mpbq(-16));
lean_assert(cmp(mpbq(1, 2), mpbq(1, 4)) == 1);
lean_assert(cmp(mpbq(1, 2), mpbq(1, 2)) == 0);
lean_assert(cmp(mpbq(1, 2), mpbq(3, 2)) == -1);
lean_assert(cmp(mpbq(3, 2), mpbq(3, 4)) == 1);
lean_assert(cmp(mpbq(15, 2), mpbq(3, 1)) == 1);
lean_assert(cmp(mpbq(7, 1), mpz(3)) == 1);
lean_assert(cmp(mpbq(3, 0), mpz(3)) == 0);
lean_assert(cmp(mpbq(2, 0), mpz(3)) == -1);
lean_assert(cmp(mpbq(7, 4), mpz(10)) == -1);
lean_assert(mpbq(0, 1) == mpz(0));
lean_assert_eq(a, mpbq(-16));
lean_assert_eq(cmp(mpbq(1, 2), mpbq(1, 4)), 1);
lean_assert_eq(cmp(mpbq(1, 2), mpbq(1, 2)), 0);
lean_assert_eq(cmp(mpbq(1, 2), mpbq(3, 2)), -1);
lean_assert_eq(cmp(mpbq(3, 2), mpbq(3, 4)), 1);
lean_assert_eq(cmp(mpbq(15, 2), mpbq(3, 1)), 1);
lean_assert_eq(cmp(mpbq(7, 1), mpz(3)), 1);
lean_assert_eq(cmp(mpbq(3, 0), mpz(3)), 0);
lean_assert_eq(cmp(mpbq(2, 0), mpz(3)), -1);
lean_assert_eq(cmp(mpbq(7, 4), mpz(10)), -1);
lean_assert_eq(mpbq(0, 1), mpz(0));
set(a, mpq(1, 4));
lean_assert(cmp(a, mpbq(1, 2)) == 0);
lean_assert_eq(cmp(a, mpbq(1, 2)), 0);
set(a, mpq(0));
lean_assert(a.is_zero());
a += 3u;
lean_assert(a == 3);
lean_assert_eq(a, 3);
a += -2;
lean_assert(a == 1);
lean_assert_eq(a, 1);
div2k(a, 2);
lean_assert(a == mpq(1, 4));
lean_assert_eq(a, mpq(1, 4));
a += 3u;
lean_assert(a == mpq(13, 4));
lean_assert_eq(a, mpq(13, 4));
a += -2;
lean_assert(a == mpq(5, 4));
lean_assert_eq(a, mpq(5, 4));
a -= 1u;
lean_assert(a == mpq(1, 4));
lean_assert_eq(a, mpq(1, 4));
a -= -2;
lean_assert(a == mpq(9, 4));
lean_assert_eq(a, mpq(9, 4));
}
static void tst3() {
mpbq x1(256, 4);
mpq x2(32, 2);
mpbq x3(1, 4);
mpbq x4(3, 8);
mpbq x5(3, 0);
mpbq x6(3, 2);
mpbq x7(4, 3);
lean_assert_eq(x1, 256 / (2 * 2 * 2 * 2));
lean_assert_eq(x1, x2);
x3-=x4;
lean_assert_eq(x3, mpbq(13, 8));
x5-=2;
lean_assert_eq(x5, mpbq(1, 0));
x6*=x7;
lean_assert_eq(x6, mpbq(3, 3));
}
static void tst4() {
mpbq x1(256, 4);
mpq x2(32, 2);
mpbq x3(1, 4);
mpbq x4(3, 8);
mpbq x5(3, 0);
x1*=3u;
lean_assert_eq(x1, mpbq(48, 0));
x1*=2;
lean_assert_eq(x1, mpbq(96, 0));
x2*=-2;
lean_assert_eq(x2, mpbq(-32, 0));
power(x3, x4, 2); // x3 = (3/2^8)^2 = (9/2^16)
lean_assert_eq(x3, mpbq(9, 16));
power(x4, x5, 3); // x4 = 3^3 = 27
lean_assert_eq(x4, mpbq(27, 0));
}
static void tst5() {
mpbq x1(34, 4);
mpbq x2(3932, 11);
mpbq x3(-68, 9);
mpbq x4(-69048, 15);
mpbq x5(34, -4);
mpbq x6(3932, -11);
mpbq x7(-68, -9);
mpbq x8(-69048, -15);
mpbq x9(0, 4);
lean_assert_eq(x1.magnitude_lb(), 1);
lean_assert_eq(x2.magnitude_lb(), 0);
lean_assert_eq(x3.magnitude_lb(), -2);
lean_assert_eq(x4.magnitude_lb(), 2);
lean_assert_eq(x5.magnitude_lb(), 9);
lean_assert_eq(x6.magnitude_lb(), 22);
lean_assert_eq(x7.magnitude_lb(), 16);
lean_assert_eq(x8.magnitude_lb(), 32);
lean_assert_eq(x9.magnitude_lb(), 0);
}
static void tst6() {
mpbq x1(34, 4);
mpbq x2(3932, 11);
mpbq x3(-68, 9);
mpbq x4(-69048, 15);
mpbq x5(34, -4);
mpbq x6(3932, -11);
mpbq x7(-68, -9);
mpbq x8(-69048, -15);
mpbq x9(0, 4);
lean_assert_eq(x1.magnitude_ub(), x1.magnitude_lb() + 1);
lean_assert_eq(x2.magnitude_ub(), x2.magnitude_lb() + 1);
lean_assert_eq(x3.magnitude_ub(), x3.magnitude_lb() - 1);
lean_assert_eq(x4.magnitude_ub(), x4.magnitude_lb() - 1);
lean_assert_eq(x5.magnitude_ub(), x5.magnitude_lb() + 1);
lean_assert_eq(x6.magnitude_ub(), x6.magnitude_lb() + 1);
lean_assert_eq(x7.magnitude_ub(), x7.magnitude_lb() - 1);
lean_assert_eq(x8.magnitude_ub(), x8.magnitude_lb() - 1);
lean_assert_eq(x9.magnitude_ub(), x9.magnitude_lb());
}
static void tst7() {
mpbq x1(34, 5);
mpbq x2(21, 0);
mpbq x3(-68, 4);
mpbq x4(-67, 8);
mul2(x1);
mul2(x2);
mul2(x3);
mul2k(x4, 3);
lean_assert_eq(x1, mpbq(17, 3));
lean_assert_eq(x2, mpbq(42, 0));
lean_assert_eq(x3, mpbq(-17, 1));
lean_assert_eq(x4, mpbq(-67, 5));
}
static void tst8() {
// TODO(soonhok): root_lower
}
static void tst9() {
// TODO(soonhok): root_upper
}
int main() {
tst1();
tst2();
tst3();
tst4();
tst5();
tst6();
tst7();
tst8();
tst9();
return has_violations() ? 1 : 0;
}