From 8353181fd1a71c24246be4da9984bf04d48c911c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Jul 2013 11:10:15 -0700 Subject: [PATCH] Add basic mpq tests Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 4 +- src/tests/numerics/CMakeLists.txt | 3 +- src/tests/numerics/mpq.cpp | 93 +++++++++++++++++++++++++++++-- src/util/debug.cpp | 18 ++++-- src/util/debug.h | 4 +- 5 files changed, 107 insertions(+), 15 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 36b652103..26aca9560 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -8,7 +8,7 @@ enable_testing() # Initialize CXXFLAGS. set(CMAKE_CXX_FLAGS "-Wall -std=c++11") -set(CMAKE_CXX_FLAGS_DEBUG "-O0 -g -DLEAN_DEBUG -DLEAN_TRACE") +set(CMAKE_CXX_FLAGS_DEBUG "-g -DLEAN_DEBUG -DLEAN_TRACE") set(CMAKE_CXX_FLAGS_MINSIZEREL "-Os -DNDEBUG") set(CMAKE_CXX_FLAGS_RELEASE "-O3 -DNDEBUG") set(CMAKE_CXX_FLAGS_RELWITHDEBINFO "-O2 -g") @@ -21,7 +21,7 @@ if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") message(FATAL_ERROR "${PROJECT_NAME} requires g++ 4.8 or greater.") endif () elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") - set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -stdlib=libc++") + # Do nothing else () message(FATAL_ERROR "Your C++ compiler does not support C++11.") endif () diff --git a/src/tests/numerics/CMakeLists.txt b/src/tests/numerics/CMakeLists.txt index bb742045a..19fd29e0e 100644 --- a/src/tests/numerics/CMakeLists.txt +++ b/src/tests/numerics/CMakeLists.txt @@ -1,4 +1,3 @@ -include_directories(${LEAN_SOURCE_DIR}/numerics) add_executable(mpq mpq.cpp) -add_test(mpq ${CMAKE_CURRENT_BINARY_DIR}/mpq) target_link_libraries(mpq ${EXTRA_LIBS}) +add_test(mpq ${CMAKE_CURRENT_BINARY_DIR}/mpq) diff --git a/src/tests/numerics/mpq.cpp b/src/tests/numerics/mpq.cpp index f77e99e13..ad9977e8f 100644 --- a/src/tests/numerics/mpq.cpp +++ b/src/tests/numerics/mpq.cpp @@ -7,10 +7,95 @@ Author: Leonardo de Moura #include #include "test.h" #include "mpq.h" +using namespace lean; + +static void tst1() { + mpq a(2,3), b(4,3); + b = a / b; + lean_assert(b == mpq(1,2)); + a = mpq(2); + a.inv(); + lean_assert(a == b); + a = -2; + b = mpq(-1, 2); + a.inv(); + lean_assert(a == b); +} + +static void tst2() { + mpq a(2,3); + lean_assert(floor(a) == 0); + lean_assert(ceil(a) == 1); + mpq b(-2, 3); + lean_assert(floor(b) == -1); + lean_assert(ceil(b) == 0); + mpq c; + lean_assert(floor(c) == 0); + lean_assert(ceil(c) == 0); + mpq d(3); + lean_assert(d > 0); + lean_assert(d.is_pos()); + lean_assert(floor(d) == d); + lean_assert(ceil(d) == d); + mpq e(-3); + lean_assert(e < 0); + lean_assert(e.is_neg()); + lean_assert(floor(e) == e); + lean_assert(ceil(e) == e); +} + +static void tst3() { + mpq a("1"); + mpq b(1); + lean_assert(a == b); +} + +static void tst4() { + mpq a(8,6); + lean_assert(a == mpq(4,3)); + lean_assert(mpq(1,2)+mpq(1,2) == mpq(1)); + lean_assert(mpq("1/2") < mpq("2/3")); + lean_assert(mpq(-1,2).is_neg()); + lean_assert(mpq(-1,2).is_nonpos()); + lean_assert(!mpq(-1,2).is_zero()); + lean_assert(mpq(1,2) > mpq()); + lean_assert(mpq().is_zero()); + lean_assert(mpq(2,3) + mpq(4,3) == mpq(2)); + lean_assert(mpq(1,2) >= mpq(1,3)); + lean_assert(mpq(3,4).get_denominator() == 4); + lean_assert(mpq(3,4).get_numerator() == 3); + lean_assert(mpq(1,2) / mpq(5,4) == mpq(2,5)); + lean_assert(mpq(1,2) - mpq(2,3) == mpq(-1,6)); + lean_assert(mpq(3,4) * mpq(2,3) == mpq(1,2)); + a *= 3; + lean_assert(a == 4); + a /= 2; + lean_assert(a == 2); + lean_assert(a.is_integer()); + a /= 5; + lean_assert(a == mpq(2,5)); + lean_assert(!a.is_integer()); + mpq b(3,7); + a *= b; + lean_assert(a == mpq(6,35)); + a /= b; + lean_assert(a == mpq(2,5)); + mpz c(5); + a *= c; + lean_assert(a == 2); + a += c; + lean_assert(a == 7); + a -= c; + lean_assert(a == 2); + a /= c; + lean_assert(a == mpq(2,5)); +} int main() { - lean::abort_on_violation(true); - lean_assert(false); - std::cout << "PASSED\n"; - return 0; + continue_on_violation(true); + tst1(); + tst2(); + tst3(); + tst4(); + return has_violations() ? 1 : 0; } diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 879ce6cb1..e3f95d72d 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -19,12 +19,17 @@ Author: Leonardo de Moura namespace lean { -static bool g_abort_on_violation = false; -static bool g_enable_assertions = true; +static volatile bool g_continue_on_violation = false; +static volatile bool g_has_violations = false; +static volatile bool g_enable_assertions = true; static std::unique_ptr> g_enabled_debug_tags; -void abort_on_violation(bool f) { - g_abort_on_violation = f; +bool has_violations() { + return g_has_violations; +} + +void continue_on_violation(bool f) { + g_continue_on_violation = f; } void enable_assertions(bool f) { @@ -59,8 +64,9 @@ bool is_debug_enabled(const char * tag) { } void invoke_debugger() { - if (g_abort_on_violation) - exit(1); + g_has_violations = true; + if (g_continue_on_violation) + return; int * x = 0; for (;;) { #ifdef _WINDOWS diff --git a/src/util/debug.h b/src/util/debug.h index fdcaa8e8b..7d9697550 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -33,11 +33,13 @@ Author: Leonardo de Moura namespace lean { -void abort_on_violation(bool flag); void notify_assertion_violation(char const * file_name, int line, char const * condition); void enable_debug(char const * tag); void disable_debug(char const * tag); bool is_debug_enabled(char const * tag); void invoke_debugger(); +// support for testing +void continue_on_violation(bool flag); +bool has_violations(); }