From 65b4845fbcc8b2e8548ee6e3ac9a2a45880c1434 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Aug 2013 00:28:26 -0700
Subject: [PATCH] Add more tests to improve coverage. Fix bug in mpz.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/frontend/frontend.cpp  | 34 ++++++++++++++++++++++
 src/tests/util/numerics/mpbq.cpp | 50 ++++++++++++++++++++++++++++++++
 src/util/numerics/mpz.h          |  4 +--
 3 files changed, 86 insertions(+), 2 deletions(-)

diff --git a/src/tests/frontend/frontend.cpp b/src/tests/frontend/frontend.cpp
index bfc6eddf0..44d0615e2 100644
--- a/src/tests/frontend/frontend.cpp
+++ b/src/tests/frontend/frontend.cpp
@@ -122,6 +122,39 @@ static void tst8() {
     std::cout << fmt(fe.find_object("Trivial")) << "\n";
 }
 
+static void tst9() {
+    frontend f;
+    lean_assert(!f.has_children());
+    {
+        frontend c = f.mk_child();
+        lean_assert(f.has_children());
+        lean_assert(c.parent().has_children());
+    }
+    lean_assert(!f.has_children());
+    f.add_uvar("l", level()+1);
+    lean_assert(f.get_uvar("l") == level("l"));
+    try { f.get_uvar("l2"); lean_unreachable(); }
+    catch (exception &) {}
+    f.add_definition("x", Bool, True);
+    object const & obj = f.get_object("x");
+    lean_assert(obj.get_name() == "x");
+    lean_assert(obj.get_type() == Bool);
+    lean_assert(obj.get_value() == True);
+    try { f.get_object("y"); lean_unreachable(); }
+    catch (exception &) {}
+    lean_assert(!f.find_object("y"));
+    f.add_definition("y", False);
+    lean_assert(f.find_object("y").get_type() == Bool);
+    lean_assert(f.has_object("y"));
+    lean_assert(!f.has_object("z"));
+    bool found = false;
+    std::for_each(f.begin_objects(), f.end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; });
+    lean_assert(found);
+    f.add_postfix("!", 10, "factorial");
+    name parts[] = {"if", "then", "else"};
+    f.add_mixfixl(3, parts, 10, "if");
+}
+
 int main() {
     tst1();
     tst2();
@@ -131,5 +164,6 @@ int main() {
     tst6();
     tst7();
     tst8();
+    tst9();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/util/numerics/mpbq.cpp b/src/tests/util/numerics/mpbq.cpp
index 6d25c4fe8..6840d660e 100644
--- a/src/tests/util/numerics/mpbq.cpp
+++ b/src/tests/util/numerics/mpbq.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <iostream>
+#include <sstream>
 #include "test.h"
 #include "mpbq.h"
 #include "mpq.h"
@@ -38,7 +39,56 @@ static void tst1() {
     }
 }
 
+static void tst2() {
+    mpbq num(2);
+    std::ostringstream out;
+    out << num;
+    lean_assert(out.str() == "2");
+    mpbq a(-1,2);
+    std::ostringstream out2;
+    display_decimal(out2, a, 10);
+    lean_assert(out2.str() == "-0.25");
+    lean_assert(lt_1div2k(a, 8));
+    mul2(a);
+    lean_assert(a == mpbq(-1,1));
+    mul2k(a, 3);
+    lean_assert(a == mpbq(-4));
+    mul2k(a, 0);
+    lean_assert(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));
+    set(a, mpq(1,4));
+    lean_assert(cmp(a, mpbq(1,2)) == 0);
+    set(a, mpq(0));
+    lean_assert(a.is_zero());
+    a += 3u;
+    lean_assert(a == 3);
+    a += -2;
+    lean_assert(a == 1);
+    div2k(a, 2);
+    lean_assert(a == mpq(1,4));
+    a += 3u;
+    lean_assert(a == mpq(13,4));
+    a += -2;
+    lean_assert(a == mpq(5,4));
+    a -= 1u;
+    lean_assert(a == mpq(1,4));
+    a -= -2;
+    lean_assert(a == mpq(9,4));
+}
+
 int main() {
     tst1();
+    tst2();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h
index d012350d3..49d90c34c 100644
--- a/src/util/numerics/mpz.h
+++ b/src/util/numerics/mpz.h
@@ -113,11 +113,11 @@ public:
 
     mpz & operator+=(mpz const & o) { mpz_add(m_val, m_val, o.m_val); return *this; }
     mpz & operator+=(unsigned u) { mpz_add_ui(m_val, m_val, u); return *this; }
-    mpz & operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, u); return *this; }
+    mpz & operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, -u); return *this; }
 
     mpz & operator-=(mpz const & o) { mpz_sub(m_val, m_val, o.m_val); return *this; }
     mpz & operator-=(unsigned u) { mpz_sub_ui(m_val, m_val, u); return *this; }
-    mpz & operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, u); return *this; }
+    mpz & operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, -u); return *this; }
 
     mpz & operator*=(mpz const & o) { mpz_mul(m_val, m_val, o.m_val); return *this; }
     mpz & operator*=(unsigned u) { mpz_mul_ui(m_val, m_val, u); return *this; }