Add basic mpq tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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 ()

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)

src/tests/numerics/mpq.cpp

@@ -7,10 +7,95 @@ Author: Leonardo de Moura
 #include <iostream>
 #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);
+    continue_on_violation(true);
-    lean_assert(false);
+    tst1();
-    std::cout << "PASSED\n";
+    tst2();
-    return 0;
+    tst3();
+    tst4();
+    return has_violations() ? 1 : 0;
 }

src/util/debug.cpp

@@ -19,12 +19,17 @@ Author: Leonardo de Moura
 
 namespace lean {
 
-static bool                                   g_abort_on_violation = false;
+static volatile bool                          g_continue_on_violation = false;
-static bool                                   g_enable_assertions = true;
+static volatile bool                          g_has_violations = false;
+static volatile bool                          g_enable_assertions = true;
 static std::unique_ptr<std::set<std::string>> g_enabled_debug_tags;
 
-void abort_on_violation(bool f) {
+bool has_violations() {
-    g_abort_on_violation = f;
+    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)
+    g_has_violations = true;
-        exit(1);
+    if (g_continue_on_violation)
+        return;
     int * x = 0;
     for (;;) {
         #ifdef _WINDOWS

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