mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Add RCF external API skeletons

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-05 22:24:56 -08:00
parent ecb58091f7
commit 47c6a73e19
9 changed files with 427 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_project.py
View file

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

14
src/api/api_context.cpp
View file

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

19
src/api/api_context.h
View file

@ -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<realclosure::manager> m_rcf_manager;
public:
realclosure::manager & rcfm();
// ------------------------
//
// Solver interface for backward compatibility

191
src/api/api_rcf.cpp Normal file
View file

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

38
src/api/api_rcf.h Normal file
View file

@ -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<Z3_rcf_num_ref *>(n); }
inline Z3_rcf_num of_rcf_num(Z3_rcf_num_ref * n) { return reinterpret_cast<Z3_rcf_num>(n); }
inline rcnumeral & to_rcnumeral(Z3_rcf_num n) { SASSERT(n != 0); return to_rcf_num(n)->m_num; }
#endif

3
src/api/python/z3types.py
View file

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

1
src/api/z3.h
View file

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

2
src/api/z3_api.h
View file

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

159
src/api/z3_rcf.h Normal file
View file

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