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

Add more tests to improve coverage. Fix bug in mpz.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-18 00:28:26 -07:00
parent ecd8eb7912
commit 65b4845fbc
3 changed files with 86 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/tests/frontend/frontend.cpp
View file

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

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

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

4
src/util/numerics/mpz.h
View file

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