test(util/numerics): more tests to improve coverage

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)

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;
+}

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;
+}

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;
 }

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_eq(r, 3);
-    lean_assert(mpz(10) % mpz(3) == mpz(1));
+    lean_assert_eq(mpz(10) % mpz(3), mpz(1));
-    lean_assert(mpz(10) % mpz(-3) == 1);
+    lean_assert_eq(mpz(10) % mpz(-3), 1);
-    lean_assert(mpz(-10) % mpz(-3) == 2);
+    lean_assert_eq(mpz(-10) % mpz(-3), 2);
-    lean_assert(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_eq(s.size(), 10001);
-    lean_assert(s[0] == '1');
+    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;
 }
-

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<mpq>(x1, neg_inf);
+    inv<mpq>(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;
+}

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<typename T>