diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 3da30683e..d11c5fd30 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -59,7 +59,7 @@ def init_project_def(): add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'muz_qe', 'sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') - API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h'] + API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h'] add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'], includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3') diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 9ebc771f0..6b3fba6ae 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -25,6 +25,7 @@ Revision History: #include"api_log_macros.h" #include"api_util.h" #include"reg_decl_plugins.h" +#include"realclosure.h" // The install_tactics procedure is automatically generated void install_tactics(tactic_manager & ctx); @@ -391,6 +392,19 @@ namespace api { m_smtlib_parser_sorts.reset(); } } + + // ------------------------ + // + // RCF manager + // + // ----------------------- + realclosure::manager & context::rcfm() { + if (m_rcf_manager.get() == 0) { + m_rcf_manager = alloc(realclosure::manager, m_rcf_qm); + } + return *(m_rcf_manager.get()); + } + }; diff --git a/src/api/api_context.h b/src/api/api_context.h index 896011615..e0c95b07b 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -38,6 +38,10 @@ namespace smtlib { class parser; }; +namespace realclosure { + class manager; +}; + namespace api { Z3_search_failure mk_Z3_search_failure(smt::failure f); @@ -83,7 +87,6 @@ namespace api { event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt - pmanager m_pmanager; public: // Scoped obj for setting m_interruptable class set_interruptable { @@ -175,8 +178,22 @@ namespace api { // Polynomial manager & caches // // ----------------------- + private: + pmanager m_pmanager; + public: polynomial::manager & pm() { return m_pmanager.pm(); } + // ------------------------ + // + // RCF manager + // + // ----------------------- + private: + unsynch_mpq_manager m_rcf_qm; + scoped_ptr m_rcf_manager; + public: + realclosure::manager & rcfm(); + // ------------------------ // // Solver interface for backward compatibility diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp new file mode 100644 index 000000000..681cb814e --- /dev/null +++ b/src/api/api_rcf.cpp @@ -0,0 +1,191 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + api_rcf.cpp + +Abstract: + + Additional APIs for handling elements of the Z3 real closed field that contains: + - transcendental extensions + - infinitesimal extensions + - algebraic extensions + +Author: + + Leonardo de Moura (leonardo) 2012-01-05 + +Notes: + +--*/ +#include +#include"z3.h" +#include"api_log_macros.h" +#include"api_context.h" +#include"api_rcf.h" + +extern "C" { + + void Z3_API Z3_rcf_inc_ref(Z3_context c, Z3_rcf_num a) { + Z3_TRY; + LOG_Z3_rcf_inc_ref(c, a); + RESET_ERROR_CODE(); + to_rcf_num(a)->inc_ref(); + Z3_CATCH; + } + + void Z3_API Z3_rcf_dec_ref(Z3_context c, Z3_rcf_num a) { + Z3_TRY; + LOG_Z3_rcf_dec_ref(c, a); + RESET_ERROR_CODE(); + to_rcf_num(a)->dec_ref(); + Z3_CATCH; + } + + 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); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, int val) { + Z3_TRY; + LOG_Z3_rcf_mk_small_int(c, val); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_mk_pi(Z3_context c) { + Z3_TRY; + LOG_Z3_rcf_mk_pi(c); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_mk_e(Z3_context c) { + Z3_TRY; + LOG_Z3_rcf_mk_e(c); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c, Z3_string name) { + Z3_TRY; + LOG_Z3_rcf_mk_infinitesimal(c, name); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_add(c, a, b); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_sub(c, a, b); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_mul(c, a, b); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_div(c, a, b); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a) { + Z3_TRY; + LOG_Z3_rcf_neg(c, a); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a) { + Z3_TRY; + LOG_Z3_rcf_inv(c, a); + RESET_ERROR_CODE(); + // TODO + RETURN_Z3(0); + Z3_CATCH_RETURN(0); + } + + Z3_bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_lt(c, a, b); + RESET_ERROR_CODE(); + // TODO + return Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_gt(c, a, b); + RESET_ERROR_CODE(); + // TODO + return Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_le(c, a, b); + RESET_ERROR_CODE(); + // TODO + return Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b) { + Z3_TRY; + LOG_Z3_rcf_ge(c, a, b); + RESET_ERROR_CODE(); + // TODO + return Z3_FALSE; + Z3_CATCH_RETURN(Z3_FALSE); + } + + Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a) { + Z3_TRY; + LOG_Z3_rcf_num_to_string(c, a); + RESET_ERROR_CODE(); + std::ostringstream buffer; + // TODO + return mk_c(c)->mk_external_string(buffer.str()); + Z3_CATCH_RETURN(""); + } + +}; diff --git a/src/api/api_rcf.h b/src/api/api_rcf.h new file mode 100644 index 000000000..2026fb21e --- /dev/null +++ b/src/api/api_rcf.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + api_rcf.h + +Abstract: + + Additional APIs for handling elements of the Z3 real closed field that contains: + - transcendental extensions + - infinitesimal extensions + - algebraic extensions + +Author: + + Leonardo de Moura (leonardo) 2012-01-05 + +Notes: + +--*/ +#ifndef _API_RCF_H_ +#define _API_RCF_H_ + +#include"api_util.h" +#include"realclosure.h" + +struct Z3_rcf_num_ref : public api::object { + rcnumeral m_num; + virtual ~Z3_rcf_num_ref() {} +}; + + +inline Z3_rcf_num_ref * to_rcf_num(Z3_rcf_num n) { return reinterpret_cast(n); } +inline Z3_rcf_num of_rcf_num(Z3_rcf_num_ref * n) { return reinterpret_cast(n); } +inline rcnumeral & to_rcnumeral(Z3_rcf_num n) { SASSERT(n != 0); return to_rcf_num(n)->m_num; } + +#endif diff --git a/src/api/python/z3types.py b/src/api/python/z3types.py index 3a2449203..a26a958c0 100644 --- a/src/api/python/z3types.py +++ b/src/api/python/z3types.py @@ -106,3 +106,6 @@ class FuncEntryObj(ctypes.c_void_p): def __init__(self, e): self._as_parameter_ = e def from_param(obj): return obj +class RCFNumObj(ctypes.c_void_p): + def __init__(self, e): self._as_parameter_ = e + def from_param(obj): return obj diff --git a/src/api/z3.h b/src/api/z3.h index c3e38e3f1..db8becafd 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -26,6 +26,7 @@ Notes: #include"z3_api.h" #include"z3_algebraic.h" #include"z3_polynomial.h" +#include"z3_rcf.h" #undef __in #undef __out diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 98bde7bcf..410945235 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -47,6 +47,7 @@ DEFINE_TYPE(Z3_func_interp); #define Z3_func_interp_opt Z3_func_interp DEFINE_TYPE(Z3_func_entry); DEFINE_TYPE(Z3_fixedpoint); +DEFINE_TYPE(Z3_rcf_num); DEFINE_VOID(Z3_theory_data); #endif @@ -1190,6 +1191,7 @@ typedef enum def_Type('FUNC_ENTRY', 'Z3_func_entry', 'FuncEntryObj') def_Type('FIXEDPOINT', 'Z3_fixedpoint', 'FixedpointObj') def_Type('PARAM_DESCRS', 'Z3_param_descrs', 'ParamDescrs') + def_Type('RCF_NUM', 'Z3_rcf_num', 'RCFNumObj') */ #ifdef Conly diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h new file mode 100644 index 000000000..5b5cc112d --- /dev/null +++ b/src/api/z3_rcf.h @@ -0,0 +1,159 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + z3_rcf.h + +Abstract: + + Additional APIs for handling elements of the Z3 real closed field that contains: + - transcendental extensions + - infinitesimal extensions + - algebraic extensions + +Author: + + Leonardo de Moura (leonardo) 2012-01-05 + +Notes: + +--*/ +#ifndef _Z3_RCF_H_ +#define _Z3_RCF_H_ + +#ifdef __cplusplus +extern "C" { +#endif // __cplusplus + + /** + \brief Increment the reference counter of a RCF numeral. + + def_API('Z3_rcf_inc_ref', VOID, (_in(CONTEXT), _in(RCF_NUM))) + */ + void Z3_API Z3_rcf_inc_ref(__in Z3_context c, __in Z3_rcf_num a); + + /** + \brief Decrement the reference counter of a RCF numeral. + + def_API('Z3_rcf_dec_ref', VOID, (_in(CONTEXT), _in(RCF_NUM))) + */ + void Z3_API Z3_rcf_dec_ref(__in Z3_context c, __in Z3_rcf_num a); + + /** + \brief Return a RCF rational using the given string. + + def_API('Z3_rcf_mk_rational', RCF_NUM, (_in(CONTEXT), _in(STRING))) + */ + Z3_rcf_num Z3_API Z3_rcf_mk_rational(__in Z3_context c, __in Z3_string val); + + /** + \brief Return a RCF small integer. + + def_API('Z3_rcf_mk_small_int', RCF_NUM, (_in(CONTEXT), _in(INT))) + */ + Z3_rcf_num Z3_API Z3_rcf_mk_small_int(__in Z3_context c, __in int val); + + /** + \brief Return Pi + + def_API('Z3_rcf_mk_pi', RCF_NUM, (_in(CONTEXT),)) + */ + Z3_rcf_num Z3_API Z3_rcf_mk_pi(__in Z3_context c); + + /** + \brief Return e (Euler's constant) + + def_API('Z3_rcf_mk_e', RCF_NUM, (_in(CONTEXT),)) + */ + Z3_rcf_num Z3_API Z3_rcf_mk_e(__in Z3_context c); + + /** + \brief Return a new infinitesimal that is smaller than all elements in the Z3 field. + + def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT), _in(STRING))) + */ + Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c, __in Z3_string name); + + /** + \brief Return the value a + b. + + def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_rcf_num Z3_API Z3_rcf_add(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + + /** + \brief Return the value a - b. + + def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_rcf_num Z3_API Z3_rcf_sub(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + + /** + \brief Return the value a * b. + + def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_rcf_num Z3_API Z3_rcf_mul(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + + /** + \brief Return the value a / b. + + def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_rcf_num Z3_API Z3_rcf_div(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + + /** + \brief Return the value -a + + def_API('Z3_rcf_neg', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM))) + */ + Z3_rcf_num Z3_API Z3_rcf_neg(__in Z3_context c, __in Z3_rcf_num a); + + /** + \brief Return the value 1/a + + def_API('Z3_rcf_inv', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM))) + */ + Z3_rcf_num Z3_API Z3_rcf_inv(__in Z3_context c, __in Z3_rcf_num a); + + /** + \brief Return Z3_TRUE if a < b + + def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_bool Z3_API Z3_rcf_lt(__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_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_bool Z3_API Z3_rcf_gt(__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_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_bool Z3_API Z3_rcf_le(__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_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM))) + */ + Z3_bool Z3_API Z3_rcf_ge(__in Z3_context c, __in Z3_rcf_num a, __in Z3_rcf_num b); + + /** + \brief Convert the RCF numeral into a string. + + def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM))) + */ + Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a); + +#ifdef __cplusplus +}; +#endif // __cplusplus + +#endif