From 9d8ff0eadb4847bdb8f8b89aeadb39edd19b5d30 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 Sep 2013 19:56:12 -0700
Subject: [PATCH] test(mpz): add unit tests for mpz

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/numerics/CMakeLists.txt |  3 ++
 src/tests/util/numerics/mpz.cpp        | 45 ++++++++++++++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 src/tests/util/numerics/mpz.cpp

diff --git a/src/tests/util/numerics/CMakeLists.txt b/src/tests/util/numerics/CMakeLists.txt
index 1ccdc92a8..3f3323fb7 100644
--- a/src/tests/util/numerics/CMakeLists.txt
+++ b/src/tests/util/numerics/CMakeLists.txt
@@ -7,3 +7,6 @@ add_test(mpbq ${CMAKE_CURRENT_BINARY_DIR}/mpbq)
 add_executable(mpfp mpfp.cpp)
 target_link_libraries(mpfp ${EXTRA_LIBS})
 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)
diff --git a/src/tests/util/numerics/mpz.cpp b/src/tests/util/numerics/mpz.cpp
new file mode 100644
index 000000000..1e890202d
--- /dev/null
+++ b/src/tests/util/numerics/mpz.cpp
@@ -0,0 +1,45 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include <sstream>
+#include <string>
+#include "util/test.h"
+#include "util/numerics/mpz.h"
+using namespace lean;
+
+static void tst1() {
+    mpz a(-10);
+    lean_assert_eq(a.log2(), 0);
+    lean_assert_eq(a.mlog2(), 3);
+    lean_assert_eq(a.is_power_of_two(), false);
+    lean_assert_eq(mpz(10).mlog2(), 0);
+    mpz r;
+    lean_assert(root(r, mpz(4), 2));
+    lean_assert(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);
+    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');
+    for (unsigned i = 1; i < 10001; i++) {
+        lean_assert(s[i] == '0');
+    }
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}
+