From 9fbbdb56e4bb185e39885dec31883f820c46e485 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Jan 2013 20:06:27 -0800 Subject: [PATCH] Implement RCF external C API Signed-off-by: Leonardo de Moura --- src/api/api_context.cpp | 2 + src/api/api_rcf.cpp | 134 ++++++++++++++++++++------- src/api/api_util.h | 1 + src/api/z3_rcf.h | 21 +++++ src/math/realclosure/realclosure.cpp | 18 ++++ src/math/realclosure/realclosure.h | 10 ++ 6 files changed, 155 insertions(+), 31 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 6b3fba6ae..441190ba5 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -139,6 +139,8 @@ namespace api { if (m_interruptable) (*m_interruptable)(); m().set_cancel(true); + if (m_rcf_manager.get() == 0) + m_rcf_manager->set_cancel(true); } } diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp index 681cb814e..4ba440266 100644 --- a/src/api/api_rcf.cpp +++ b/src/api/api_rcf.cpp @@ -39,16 +39,38 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_dec_ref(c, a); RESET_ERROR_CODE(); + if (to_rcf_num(a)->ref_count() == 1) { + mk_c(c)->rcfm().del(to_rcnumeral(a)); + } to_rcf_num(a)->dec_ref(); Z3_CATCH; } + static rcmanager & rcfm(Z3_context c) { + return mk_c(c)->rcfm(); + } + + static void reset_rcf_cancel(Z3_context c) { + rcfm(c).reset_cancel(); + } + + static Z3_rcf_num mk_rcf_num(Z3_context c, rcnumeral & a) { + Z3_rcf_num_ref * r = alloc(Z3_rcf_num_ref); + rcfm(c).swap(r->m_num, a); + mk_c(c)->save_object(r); + return of_rcf_num(r); + } + Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, Z3_string val) { Z3_TRY; LOG_Z3_rcf_mk_rational(c, val); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_mpq q(rcfm(c).qm()); + rcfm(c).qm().set(q, val); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).set(r, q); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -56,8 +78,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_mk_small_int(c, val); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).set(r, val); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -65,8 +89,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_mk_pi(c); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).mk_pi(r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -74,8 +100,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_mk_e(c); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).mk_e(r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -83,8 +111,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_mk_infinitesimal(c, name); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).mk_infinitesimal(name, r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -92,8 +122,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_add(c, a, b); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).add(to_rcnumeral(a), to_rcnumeral(b), r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -101,8 +133,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_sub(c, a, b); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).sub(to_rcnumeral(a), to_rcnumeral(b), r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -110,8 +144,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_mul(c, a, b); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).mul(to_rcnumeral(a), to_rcnumeral(b), r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -119,8 +155,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_div(c, a, b); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).div(to_rcnumeral(a), to_rcnumeral(b), r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -128,8 +166,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_neg(c, a); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).neg(to_rcnumeral(a), r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -137,8 +177,10 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_inv(c, a); RESET_ERROR_CODE(); - // TODO - RETURN_Z3(0); + reset_rcf_cancel(c); + scoped_rcnumeral r(rcfm(c)); + rcfm(c).inv(to_rcnumeral(a), r); + RETURN_Z3(mk_rcf_num(c, r)); Z3_CATCH_RETURN(0); } @@ -146,8 +188,8 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_lt(c, a, b); RESET_ERROR_CODE(); - // TODO - return Z3_FALSE; + reset_rcf_cancel(c); + return rcfm(c).lt(to_rcnumeral(a), to_rcnumeral(b)); Z3_CATCH_RETURN(Z3_FALSE); } @@ -155,8 +197,8 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_gt(c, a, b); RESET_ERROR_CODE(); - // TODO - return Z3_FALSE; + reset_rcf_cancel(c); + return rcfm(c).gt(to_rcnumeral(a), to_rcnumeral(b)); Z3_CATCH_RETURN(Z3_FALSE); } @@ -164,8 +206,8 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_le(c, a, b); RESET_ERROR_CODE(); - // TODO - return Z3_FALSE; + reset_rcf_cancel(c); + return rcfm(c).le(to_rcnumeral(a), to_rcnumeral(b)); Z3_CATCH_RETURN(Z3_FALSE); } @@ -173,8 +215,26 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_ge(c, a, b); RESET_ERROR_CODE(); - // TODO - return Z3_FALSE; + reset_rcf_cancel(c); + return rcfm(c).ge(to_rcnumeral(a), to_rcnumeral(b)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_eq(c, a, b); + RESET_ERROR_CODE(); + reset_rcf_cancel(c); + return rcfm(c).eq(to_rcnumeral(a), to_rcnumeral(b)); + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_neq(c, a, b); + RESET_ERROR_CODE(); + reset_rcf_cancel(c); + return rcfm(c).eq(to_rcnumeral(a), to_rcnumeral(b)); Z3_CATCH_RETURN(Z3_FALSE); } @@ -182,8 +242,20 @@ extern "C" { Z3_TRY; LOG_Z3_rcf_num_to_string(c, a); RESET_ERROR_CODE(); + reset_rcf_cancel(c); std::ostringstream buffer; - // TODO + rcfm(c).display(buffer, to_rcnumeral(a)); + return mk_c(c)->mk_external_string(buffer.str()); + Z3_CATCH_RETURN(""); + } + + Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec) { + Z3_TRY; + LOG_Z3_rcf_num_to_string(c, a); + RESET_ERROR_CODE(); + reset_rcf_cancel(c); + std::ostringstream buffer; + rcfm(c).display_decimal(buffer, to_rcnumeral(a), prec); return mk_c(c)->mk_external_string(buffer.str()); Z3_CATCH_RETURN(""); } diff --git a/src/api/api_util.h b/src/api/api_util.h index b08592cb7..c81384f2f 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -37,6 +37,7 @@ namespace api { public: object():m_ref_count(0) {} virtual ~object() {} + unsigned ref_count() const { return m_ref_count; } void inc_ref() { m_ref_count++; } void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); } }; diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h index 5b5cc112d..877ae7c64 100644 --- a/src/api/z3_rcf.h +++ b/src/api/z3_rcf.h @@ -145,6 +145,20 @@ extern "C" { */ Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + /** + \brief Return Z3_TRUE if a == b + + def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_bool Z3_API Z3_rcf_eq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + + /** + \brief Return Z3_TRUE if a != b + + def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_bool Z3_API Z3_rcf_neq(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + /** \brief Convert the RCF numeral into a string. @@ -152,6 +166,13 @@ extern "C" { */ Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a); + /** + \brief Convert the RCF numeral into a string in decimal notation. + + def_API('Z3_rcf_num_to_decimal_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(UINT))) + */ + Z3_string Z3_API Z3_rcf_num_to_decimal_string(__in Z3_context c, __in Z3_rcf_num a, __in unsigned prec); + #ifdef __cplusplus }; #endif // __cplusplus diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp index 856a87ec8..a1b110cc1 100644 --- a/src/math/realclosure/realclosure.cpp +++ b/src/math/realclosure/realclosure.cpp @@ -2464,10 +2464,18 @@ namespace realclosure { set(a, neg(a.m_value)); } + void neg(numeral const & a, numeral & b) { + set(b, neg(a.m_value)); + } + void inv(numeral & a) { set(a, inv(a.m_value)); } + void inv(numeral const & a, numeral & b) { + set(b, inv(a.m_value)); + } + void add(numeral const & a, numeral const & b, numeral & c) { set(c, add(a.m_value, b.m_value)); } @@ -2879,11 +2887,21 @@ namespace realclosure { m_imp->neg(a); } + void manager::neg(numeral const & a, numeral & b) { + save_interval_ctx ctx(this); + m_imp->neg(a, b); + } + void manager::inv(numeral & a) { save_interval_ctx ctx(this); m_imp->inv(a); } + void manager::inv(numeral const & a, numeral & b) { + save_interval_ctx ctx(this); + m_imp->inv(a, b); + } + void manager::div(numeral const & a, numeral const & b, numeral & c) { save_interval_ctx ctx(this); m_imp->div(a, b, c); diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h index 72e0da2aa..d3b39fcb5 100644 --- a/src/math/realclosure/realclosure.h +++ b/src/math/realclosure/realclosure.h @@ -181,11 +181,21 @@ namespace realclosure { \brief a <- -a */ void neg(numeral & a); + + /** + \brief b <- -a + */ + void neg(numeral const & a, numeral & b); /** \brief a <- 1/a if a != 0 */ void inv(numeral & a); + + /** + \brief b <- 1/a if a != 0 + */ + void inv(numeral const & a, numeral & b); /** \brief c <- a/b if b != 0