Add tests

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

src/test/algebraic.cpp

@@ -176,11 +176,11 @@ static void tst1() {
     display_anums(std::cout, rs1);
 }
 
-void tst_refine_mpbq() {
+void tst_refine_mpbq(int n, int d) {
     unsynch_mpq_manager qm;
     mpbq_manager        bqm(qm);
     scoped_mpq q1(qm);
-    qm.set(q1, 5, 7);
+    qm.set(q1, n, d);
     scoped_mpbq l(bqm);
     scoped_mpbq u(bqm);
     std::cout << "using refine upper...\n";
@@ -207,6 +207,10 @@ void tst_refine_mpbq() {
     }
 }
 
+void tst_refine_mpbq() {
+    tst_refine_mpbq(-5, 7);
+}
+
 void tst_mpbq_root() {
     unsynch_mpq_manager qm;
     mpbq_manager        bqm(qm);

src/test/main.cpp

@@ -206,6 +206,7 @@ int main(int argc, char ** argv) {
     TST(mpff);
     TST(horn_subsume_model_converter);
     TST(model2expr);
+    TST(rcf);
 }
 
 void initialize_mam() {}

src/test/rcf.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    rcf.cpp
+
+Abstract:
+
+    Testing RCF module
+
+Author:
+
+    Leonardo (leonardo) 2013-01-04
+
+Notes:
+
+--*/
+#include"realclosure.h"
+
+static void tst1() {
+    unsynch_mpq_manager qm;
+    rcmanager m(qm);
+    scoped_rcnumeral a(m);
+    a = 10;
+    std::cout << sym_pp(a) << std::endl;
+    scoped_rcnumeral eps(m);
+    m.mk_infinitesimal("eps", eps);
+    std::cout << sym_pp(eps) << std::endl;
+}
+
+void tst_rcf() {
+    tst1();
+}