mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Implement RCF external C API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-06 20:06:27 -08:00
parent f1d47f35b2
commit 9fbbdb56e4
6 changed files with 155 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/api_context.cpp
View file

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

134
src/api/api_rcf.cpp
View file

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

1
src/api/api_util.h
View file

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

21
src/api/z3_rcf.h
View file

@ -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

18
src/math/realclosure/realclosure.cpp
View file

@ -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);

10
src/math/realclosure/realclosure.h
View file

@ -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