From 4602dfd2091a3cdd83551dafc796fc6ecceef766 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Sat, 28 Sep 2013 17:56:49 -0700 Subject: [PATCH] test(util/numerics): more tests to improve coverage --- src/tests/util/numerics/CMakeLists.txt | 9 ++++ src/tests/util/numerics/double.cpp | 51 ++++++++++++++++++++++ src/tests/util/numerics/float.cpp | 51 ++++++++++++++++++++++ src/tests/util/numerics/mpbq.cpp | 59 ++++++++++++++++++++++++-- src/tests/util/numerics/mpz.cpp | 24 ++++++----- src/tests/util/numerics/xnumeral.cpp | 57 +++++++++++++++++++++++++ src/util/numerics/xnumeral.h | 5 +-- 7 files changed, 239 insertions(+), 17 deletions(-) create mode 100644 src/tests/util/numerics/double.cpp create mode 100644 src/tests/util/numerics/float.cpp create mode 100644 src/tests/util/numerics/xnumeral.cpp diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt index 3f3323fb71..c60b11ec11 100644 --- a/src/tests/util/numerics/CMakeLists.txt +++ b/src/tests/util/numerics/CMakeLists.txt @@ -10,3 +10,12 @@ add_test(mpfp ${CMAKE_CURRENT_BINARY_DIR}/mpfp) add_executable(mpz mpz.cpp) target_link_libraries(mpz ${EXTRA_LIBS}) add_test(mpz ${CMAKE_CURRENT_BINARY_DIR}/mpz) +add_executable(double double.cpp) +target_link_libraries(double ${EXTRA_LIBS}) +add_test(double ${CMAKE_CURRENT_BINARY_DIR}/double) +add_executable(float float.cpp) +target_link_libraries(float ${EXTRA_LIBS}) +add_test(float ${CMAKE_CURRENT_BINARY_DIR}/float) +add_executable(xnumeral xnumeral.cpp) +target_link_libraries(xnumeral ${EXTRA_LIBS}) +add_test(xnumeral ${CMAKE_CURRENT_BINARY_DIR}/xnumeral) diff --git a/src/tests/util/numerics/double.cpp b/src/tests/util/numerics/double.cpp new file mode 100644 index 0000000000..d98af88745 --- /dev/null +++ b/src/tests/util/numerics/double.cpp @@ -0,0 +1,51 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "util/test.h" +#include "util/numerics/double.h" +using namespace lean; + +static void abs() { + double d1 = -398723.3218937912; + double d2 = -9823.3487729; + double d3 = 0.0; + double d4 = 398.347389; + double d5 = 78398.30912; + double_abs(d1); + double_abs(d2); + double_abs(d3); + double_abs(d4); + double_abs(d5); + lean_assert_eq(d1, 398723.3218937912); + lean_assert_eq(d2, 9823.3487729); + lean_assert_eq(d3, 0.0); + lean_assert_eq(d4, 398.347389); + lean_assert_eq(d5, 78398.30912); +} + +static void ceil() { + double d1 = -398723.3218937912; + double d2 = -9823.3487729; + double d3 = 0.0; + double d4 = 398.347389; + double d5 = 78398.30912; + double_ceil(d1); + double_ceil(d2); + double_ceil(d3); + double_ceil(d4); + double_ceil(d5); + lean_assert_eq(d1, -398723); + lean_assert_eq(d2, -9823); + lean_assert_eq(d3, 0.0); + lean_assert_eq(d4, 399); + lean_assert_eq(d5, 78399); +} + +int main() { + abs(); + ceil(); + return has_violations() ? 1 : 0; +} diff --git a/src/tests/util/numerics/float.cpp b/src/tests/util/numerics/float.cpp new file mode 100644 index 0000000000..bc960bdc8b --- /dev/null +++ b/src/tests/util/numerics/float.cpp @@ -0,0 +1,51 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "util/test.h" +#include "util/numerics/float.h" +using namespace lean; + +static void abs() { + float f1 = -398723.3218937912; + float f2 = -9823.3487729; + float f3 = 0.0; + float f4 = 398.347389; + float f5 = 78398.30912; + float_abs(f1); + float_abs(f2); + float_abs(f3); + float_abs(f4); + float_abs(f5); + lean_assert_eq(f1, 398723.3218937912f); + lean_assert_eq(f2, 9823.3487729f); + lean_assert_eq(f3, 0.0f); + lean_assert_eq(f4, 398.347389f); + lean_assert_eq(f5, 78398.30912f); +} + +static void ceil() { + float f1 = -398723.3218937912; + float f2 = -9823.3487729; + float f3 = 0.0; + float f4 = 398.347389; + float f5 = 78398.30912; + float_ceil(f1); + float_ceil(f2); + float_ceil(f3); + float_ceil(f4); + float_ceil(f5); + lean_assert_eq(f1, -398723); + lean_assert_eq(f2, -9823); + lean_assert_eq(f3, 0.0); + lean_assert_eq(f4, 399); + lean_assert_eq(f5, 78399); +} + +int main() { + abs(); + ceil(); + return has_violations() ? 1 : 0; +} diff --git a/src/tests/util/numerics/mpbq.cpp b/src/tests/util/numerics/mpbq.cpp index 8ca28efaa1..66e45f4ecc 100644 --- a/src/tests/util/numerics/mpbq.cpp +++ b/src/tests/util/numerics/mpbq.cpp @@ -28,7 +28,7 @@ static void tst1() { 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); + mpq v(21, 91); while (true) { lean_assert_lt(l, v); lean_assert_lt(v, u); @@ -182,11 +182,63 @@ static void tst7() { } static void tst8() { - // TODO(soonhok): root_lower + mpbq x1(36, 4); + mpbq x2(3932, 11); + mpbq x3(-68, 9); + mpbq x4(-69048, 15); + mpbq x5(0, 4); + mpbq x6(74, 5); + mpbq n1; + mpbq n2; + mpbq n3; + mpbq n4; + mpbq n5; + mpbq n6; + lean_assert_eq(root_lower(n1, x1, 2), true); + lean_assert_eq(n1, mpbq(3, 1)); + lean_assert_eq(root_lower(n2, x2, 3), false); + lean_assert_eq(n2, mpbq(1, 0)); + lean_assert_eq(root_lower(n3, x3, 3), false); + lean_assert_eq(n3, mpbq(-3, 2)); + lean_assert_eq(root_lower(n4, x4, 3), false); + lean_assert_eq(n4, mpbq(-21, 4)); + lean_assert_eq(root_lower(n5, x5, 3), true); + lean_assert_eq(n5, mpbq(0, 0)); + lean_assert_eq(root_lower(n6, x6, 3), false); + lean_assert_eq(n6, mpbq(1, 1)); } static void tst9() { - // TODO(soonhok): root_upper + mpbq x1(36, 4); + mpbq x2(3932, 11); + mpbq x3(-68, 9); + mpbq x4(-69048, 15); + mpbq x5(0, 4); + mpbq x6(74, 5); + mpbq n1; + mpbq n2; + mpbq n3; + mpbq n4; + mpbq n5; + mpbq n6; + lean_assert_eq(root_upper(n1, x1, 2), true); + lean_assert_eq(n1, mpbq(3, 1)); + lean_assert_eq(root_upper(n2, x2, 3), false); + lean_assert_eq(n2, mpbq(9, 3)); + lean_assert_eq(root_upper(n3, x3, 3), false); + lean_assert_eq(n3, mpbq(-1, 2)); + lean_assert_eq(root_upper(n4, x4, 3), false); + lean_assert_eq(n4, mpbq(-5, 2)); + lean_assert_eq(root_upper(n5, x5, 3), true); + lean_assert_eq(n5, mpbq(0, 0)); + lean_assert_eq(root_upper(n6, x6, 3), false); + lean_assert_eq(n6, mpbq(3, 1)); +} + +static void tst10() { + mpbq b(4, 5); + b.neg(); + lean_assert_eq(b, mpbq(-4, 5)); } int main() { @@ -199,5 +251,6 @@ int main() { tst7(); tst8(); tst9(); + tst10(); return has_violations() ? 1 : 0; } diff --git a/src/tests/util/numerics/mpz.cpp b/src/tests/util/numerics/mpz.cpp index 1e890202d9..2d01171dfc 100644 --- a/src/tests/util/numerics/mpz.cpp +++ b/src/tests/util/numerics/mpz.cpp @@ -16,25 +16,30 @@ static void tst1() { lean_assert_eq(a.log2(), 0); lean_assert_eq(a.mlog2(), 3); lean_assert_eq(a.is_power_of_two(), false); + unsigned shift = 0; + lean_assert_eq(a.is_power_of_two(shift), false); lean_assert_eq(mpz(10).mlog2(), 0); mpz r; + mpz b(30); + b-=10u; + lean_assert_eq(b, mpz(20)); lean_assert(root(r, mpz(4), 2)); - lean_assert(r == 2); + lean_assert_eq(r, 2); lean_assert(!root(r, mpz(10), 2)); - lean_assert(r == 3); - lean_assert(mpz(10) % mpz(3) == mpz(1)); - lean_assert(mpz(10) % mpz(-3) == 1); - lean_assert(mpz(-10) % mpz(-3) == 2); - lean_assert(mpz(-10) % mpz(3) == 2); + lean_assert_eq(r, 3); + lean_assert_eq(mpz(10) % mpz(3), mpz(1)); + lean_assert_eq(mpz(10) % mpz(-3), 1); + lean_assert_eq(mpz(-10) % mpz(-3), 2); + lean_assert_eq(mpz(-10) % mpz(3), 2); mpz big; big = power(mpz(10), 10000); std::ostringstream out; out << big; std::string s = out.str(); - lean_assert(s.size() == 10001); - lean_assert(s[0] == '1'); + lean_assert_eq(s.size(), 10001); + lean_assert_eq(s[0], '1'); for (unsigned i = 1; i < 10001; i++) { - lean_assert(s[i] == '0'); + lean_assert_eq(s[i], '0'); } } @@ -42,4 +47,3 @@ int main() { tst1(); return has_violations() ? 1 : 0; } - diff --git a/src/tests/util/numerics/xnumeral.cpp b/src/tests/util/numerics/xnumeral.cpp new file mode 100644 index 0000000000..00cbc9d893 --- /dev/null +++ b/src/tests/util/numerics/xnumeral.cpp @@ -0,0 +1,57 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Soonho Kong +*/ +#include "util/test.h" +#include "util/numerics/mpq.h" +#include "util/numerics/xnumeral.h" +using namespace lean; + +static void inv() { + mpq x1(214, 6); + mpq x2(-131, 8); + xnumeral_kind neg_inf = XN_MINUS_INFINITY; + xnumeral_kind pos_inf = XN_PLUS_INFINITY; + inv(x1, neg_inf); + inv(x2, pos_inf); + lean_assert_eq(x1, mpq(0, 1)); + lean_assert_eq(x2, mpq(0, 1)); +} +static void div() { + mpq r1, r2, r3, r4; + xnumeral_kind rk1, rk2, rk3, rk4; + mpq x1(214, 6); + mpq x2(-131, 8); + + // div(T & r, xnumeral_kind & rk, T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { + div(r1, rk1, x1, XN_NUMERAL, x2, XN_PLUS_INFINITY); + lean_assert_eq(r1, mpq(0, 1)); + lean_assert_eq(rk1, XN_NUMERAL); + + div(r2, rk2, x2, XN_NUMERAL, x2, XN_MINUS_INFINITY); + lean_assert_eq(r2, mpq(0, 1)); + lean_assert_eq(rk2, XN_NUMERAL); + + div(r3, rk3, x1, XN_PLUS_INFINITY, x2, XN_NUMERAL); + lean_assert_eq(r3, mpq(0, 1)); + lean_assert_eq(rk3, XN_MINUS_INFINITY); + + div(r4, rk4, x2, XN_MINUS_INFINITY, x2, XN_NUMERAL); + lean_assert_eq(r4, mpq(0, 1)); + lean_assert_eq(rk4, XN_PLUS_INFINITY); +} + +static void lt() { + mpq x1(214, 6); + mpq x2(-131, 8); + lean_assert_eq(lt(x1, XN_NUMERAL, x2, XN_MINUS_INFINITY), false); +} + +int main() { + inv(); + div(); + lt(); + return has_violations() ? 1 : 0; +} diff --git a/src/util/numerics/xnumeral.h b/src/util/numerics/xnumeral.h index 3c9b67415e..6fdddf9e33 100644 --- a/src/util/numerics/xnumeral.h +++ b/src/util/numerics/xnumeral.h @@ -215,14 +215,11 @@ bool lt(T const & a, xnumeral_kind ak, T const & b, xnumeral_kind bk) { return a < b; case XN_PLUS_INFINITY: return true; - default: - lean_unreachable(); } case XN_PLUS_INFINITY: return false; - default: - lean_unreachable(); } + lean_unreachable(); // LCOV_EXEC_LINE } template