diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp index 064803fe1..d758ee5d8 100644 --- a/src/test/algebraic.cpp +++ b/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); diff --git a/src/test/main.cpp b/src/test/main.cpp index 13ade7714..31d71226c 100644 --- a/src/test/main.cpp +++ b/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() {} diff --git a/src/test/rcf.cpp b/src/test/rcf.cpp new file mode 100644 index 000000000..8cc9dec19 --- /dev/null +++ b/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(); +}