mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 11:42:28 +00:00
More see also content in C API docs.
This commit is contained in:
Bruce Mitchener
Nikolaj Bjorner
parent
375c0ff9a9
commit
e89bb37156
3 changed files with 89 additions and 5 deletions
|
|
@ -1456,6 +1456,9 @@ extern "C" {
|
|||
Z3_global_param_set('pp.decimal', 'true')
|
||||
will set the parameter "decimal" in the module "pp" to true.
|
||||
|
||||
\sa Z3_global_param_get
|
||||
\sa Z3_global_param_reset_all
|
||||
|
||||
def_API('Z3_global_param_set', VOID, (_in(STRING), _in(STRING)))
|
||||
*/
|
||||
void Z3_API Z3_global_param_set(Z3_string param_id, Z3_string param_value);
|
||||
|
|
@ -1465,6 +1468,7 @@ extern "C" {
|
|||
\brief Restore the value of all global (and module) parameters.
|
||||
This command will not affect already created objects (such as tactics and solvers).
|
||||
|
||||
\sa Z3_global_param_get
|
||||
\sa Z3_global_param_set
|
||||
|
||||
def_API('Z3_global_param_reset_all', VOID, ())
|
||||
|
|
@ -1476,6 +1480,7 @@ extern "C" {
|
|||
|
||||
Returns \c false if the parameter value does not exist.
|
||||
|
||||
\sa Z3_global_param_reset_all
|
||||
\sa Z3_global_param_set
|
||||
|
||||
\remark This function cannot be invoked simultaneously from different threads without synchronization.
|
||||
|
|
@ -1997,6 +2002,10 @@ extern "C" {
|
|||
sort reference is 0, then the value in sort_refs should be an index referring to
|
||||
one of the recursive datatypes that is declared.
|
||||
|
||||
\sa Z3_del_constructor
|
||||
\sa Z3_mk_constructor_list
|
||||
\sa Z3_query_constructor
|
||||
|
||||
def_API('Z3_mk_constructor', CONSTRUCTOR, (_in(CONTEXT), _in(SYMBOL), _in(SYMBOL), _in(UINT), _in_array(3, SYMBOL), _in_array(3, SORT), _in_array(3, UINT)))
|
||||
*/
|
||||
Z3_constructor Z3_API Z3_mk_constructor(Z3_context c,
|
||||
|
|
@ -2014,6 +2023,8 @@ extern "C" {
|
|||
\param c logical context.
|
||||
\param constr constructor.
|
||||
|
||||
\sa Z3_mk_constructor
|
||||
|
||||
def_API('Z3_del_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR)))
|
||||
*/
|
||||
void Z3_API Z3_del_constructor(Z3_context c, Z3_constructor constr);
|
||||
|
|
@ -2027,6 +2038,10 @@ extern "C" {
|
|||
\param num_constructors number of constructors passed in.
|
||||
\param constructors array of constructor containers.
|
||||
|
||||
\sa Z3_mk_constructor
|
||||
\sa Z3_mk_constructor_list
|
||||
\sa Z3_mk_datatypes
|
||||
|
||||
def_API('Z3_mk_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _inout_array(2, CONSTRUCTOR)))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
|
||||
|
|
@ -2041,6 +2056,9 @@ extern "C" {
|
|||
\param num_constructors number of constructors in list.
|
||||
\param constructors list of constructors.
|
||||
|
||||
\sa Z3_del_constructor_list
|
||||
\sa Z3_mk_constructor
|
||||
|
||||
def_API('Z3_mk_constructor_list', CONSTRUCTOR_LIST, (_in(CONTEXT), _in(UINT), _in_array(1, CONSTRUCTOR)))
|
||||
*/
|
||||
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
|
||||
|
|
@ -2055,6 +2073,8 @@ extern "C" {
|
|||
\param c logical context.
|
||||
\param clist constructor list container.
|
||||
|
||||
\sa Z3_mk_constructor_list
|
||||
|
||||
def_API('Z3_del_constructor_list', VOID, (_in(CONTEXT), _in(CONSTRUCTOR_LIST)))
|
||||
*/
|
||||
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist);
|
||||
|
|
@ -2068,6 +2088,10 @@ extern "C" {
|
|||
\param sorts array of datatype sorts.
|
||||
\param constructor_lists list of constructors, one list per sort.
|
||||
|
||||
\sa Z3_mk_constructor
|
||||
\sa Z3_mk_constructor_list
|
||||
\sa Z3_mk_datatype
|
||||
|
||||
def_API('Z3_mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST)))
|
||||
*/
|
||||
void Z3_API Z3_mk_datatypes(Z3_context c,
|
||||
|
|
@ -2086,6 +2110,8 @@ extern "C" {
|
|||
\param tester constructor test function declaration, allocated by user.
|
||||
\param accessors array of accessor function declarations allocated by user. The array must contain num_fields elements.
|
||||
|
||||
\sa Z3_mk_constructor
|
||||
|
||||
def_API('Z3_query_constructor', VOID, (_in(CONTEXT), _in(CONSTRUCTOR), _in(UINT), _out(FUNC_DECL), _out(FUNC_DECL), _out_array(2, FUNC_DECL)))
|
||||
*/
|
||||
void Z3_API Z3_query_constructor(Z3_context c,
|
||||
|
|
@ -2114,6 +2140,8 @@ extern "C" {
|
|||
application.
|
||||
|
||||
\sa Z3_mk_app
|
||||
\sa Z3_mk_fresh_func_decl
|
||||
\sa Z3_mk_rec_func_decl
|
||||
|
||||
def_API('Z3_mk_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
|
||||
*/
|
||||
|
|
@ -2126,7 +2154,9 @@ extern "C" {
|
|||
/**
|
||||
\brief Create a constant or function application.
|
||||
|
||||
\sa Z3_mk_fresh_func_decl
|
||||
\sa Z3_mk_func_decl
|
||||
\sa Z3_mk_rec_func_decl
|
||||
|
||||
def_API('Z3_mk_app', AST, (_in(CONTEXT), _in(FUNC_DECL), _in(UINT), _in_array(2, AST)))
|
||||
*/
|
||||
|
|
@ -2145,8 +2175,9 @@ extern "C" {
|
|||
Z3_ast n = Z3_mk_app(c, d, 0, 0);
|
||||
\endcode
|
||||
|
||||
\sa Z3_mk_func_decl
|
||||
\sa Z3_mk_app
|
||||
\sa Z3_mk_fresh_const
|
||||
\sa Z3_mk_func_decl
|
||||
|
||||
def_API('Z3_mk_const', AST, (_in(CONTEXT), _in(SYMBOL), _in(SORT)))
|
||||
*/
|
||||
|
|
@ -2176,8 +2207,10 @@ extern "C" {
|
|||
|
||||
\remark If \c prefix is \c NULL, then it is assumed to be the empty string.
|
||||
|
||||
\sa Z3_mk_func_decl
|
||||
\sa Z3_mk_app
|
||||
\sa Z3_mk_const
|
||||
\sa Z3_mk_fresh_func_decl
|
||||
\sa Z3_mk_func_decl
|
||||
|
||||
def_API('Z3_mk_fresh_const', AST, (_in(CONTEXT), _in(STRING), _in(SORT)))
|
||||
*/
|
||||
|
|
@ -2197,8 +2230,9 @@ extern "C" {
|
|||
The function #Z3_mk_app can be used to create a constant or function
|
||||
application.
|
||||
|
||||
\sa Z3_mk_app
|
||||
\sa Z3_add_rec_def
|
||||
\sa Z3_mk_app
|
||||
\sa Z3_mk_func_decl
|
||||
|
||||
def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
|
||||
*/
|
||||
|
|
@ -5557,14 +5591,18 @@ extern "C" {
|
|||
/**
|
||||
\brief Return Z3 version number information.
|
||||
|
||||
\sa Z3_get_full_version
|
||||
|
||||
def_API('Z3_get_version', VOID, (_out(UINT), _out(UINT), _out(UINT), _out(UINT)))
|
||||
*/
|
||||
void Z3_API Z3_get_version(unsigned * major, unsigned * minor, unsigned * build_number, unsigned * revision_number);
|
||||
|
||||
/**
|
||||
\brief Return a string that fully describes the version of Z3 in use.
|
||||
\brief Return a string that fully describes the version of Z3 in use.
|
||||
|
||||
def_API('Z3_get_full_version', STRING, ())
|
||||
\sa Z3_get_version
|
||||
|
||||
def_API('Z3_get_full_version', STRING, ())
|
||||
*/
|
||||
Z3_string Z3_API Z3_get_full_version(void);
|
||||
|
||||
|
|
@ -5572,6 +5610,8 @@ extern "C" {
|
|||
\brief Enable tracing messages tagged as \c tag when Z3 is compiled in debug mode.
|
||||
It is a NOOP otherwise
|
||||
|
||||
\sa Z3_disable_trace
|
||||
|
||||
def_API('Z3_enable_trace', VOID, (_in(STRING),))
|
||||
*/
|
||||
void Z3_API Z3_enable_trace(Z3_string tag);
|
||||
|
|
@ -5580,6 +5620,8 @@ extern "C" {
|
|||
\brief Disable tracing messages tagged as \c tag when Z3 is compiled in debug mode.
|
||||
It is a NOOP otherwise
|
||||
|
||||
\sa Z3_enable_trace
|
||||
|
||||
def_API('Z3_disable_trace', VOID, (_in(STRING),))
|
||||
*/
|
||||
void Z3_API Z3_disable_trace(Z3_string tag);
|
||||
|
|
|
|||
|
|
@ -218,6 +218,9 @@ extern "C" {
|
|||
\param c logical context
|
||||
\param s target sort
|
||||
|
||||
\sa Z3_mk_fpa_inf
|
||||
\sa Z3_mk_fpa_zero
|
||||
|
||||
def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
|
||||
|
|
@ -231,6 +234,9 @@ extern "C" {
|
|||
|
||||
When \c negative is \c true, -oo will be generated instead of +oo.
|
||||
|
||||
\sa Z3_mk_fpa_nan
|
||||
\sa Z3_mk_fpa_zero
|
||||
|
||||
def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);
|
||||
|
|
@ -244,6 +250,9 @@ extern "C" {
|
|||
|
||||
When \c negative is \c true, -zero will be generated instead of +zero.
|
||||
|
||||
\sa Z3_mk_fpa_inf
|
||||
\sa Z3_mk_fpa_nan
|
||||
|
||||
def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, bool negative);
|
||||
|
|
@ -262,6 +271,13 @@ extern "C" {
|
|||
\param exp exponent
|
||||
\param sig significand
|
||||
|
||||
\sa Z3_mk_fpa_numeral_double
|
||||
\sa Z3_mk_fpa_numeral_float
|
||||
\sa Z3_mk_fpa_numeral_int
|
||||
\sa Z3_mk_fpa_numeral_int_uint
|
||||
\sa Z3_mk_fpa_numeral_int64_uint64
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);
|
||||
|
|
@ -278,6 +294,11 @@ extern "C" {
|
|||
|
||||
\c ty must be a FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_fp
|
||||
\sa Z3_mk_fpa_numeral_double
|
||||
\sa Z3_mk_fpa_numeral_int
|
||||
\sa Z3_mk_fpa_numeral_int_uint
|
||||
\sa Z3_mk_fpa_numeral_int64_uint64
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT)))
|
||||
|
|
@ -296,6 +317,11 @@ extern "C" {
|
|||
|
||||
\c ty must be a FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_fp
|
||||
\sa Z3_mk_fpa_numeral_float
|
||||
\sa Z3_mk_fpa_numeral_int
|
||||
\sa Z3_mk_fpa_numeral_int_uint
|
||||
\sa Z3_mk_fpa_numeral_int64_uint64
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
|
||||
|
|
@ -311,6 +337,11 @@ extern "C" {
|
|||
|
||||
\c ty must be a FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_fp
|
||||
\sa Z3_mk_fpa_numeral_double
|
||||
\sa Z3_mk_fpa_numeral_float
|
||||
\sa Z3_mk_fpa_numeral_int_uint
|
||||
\sa Z3_mk_fpa_numeral_int64_uint64
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))
|
||||
|
|
@ -328,6 +359,11 @@ extern "C" {
|
|||
|
||||
\c ty must be a FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_fp
|
||||
\sa Z3_mk_fpa_numeral_double
|
||||
\sa Z3_mk_fpa_numeral_float
|
||||
\sa Z3_mk_fpa_numeral_int
|
||||
\sa Z3_mk_fpa_numeral_int64_uint64
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
|
||||
|
|
@ -345,6 +381,11 @@ extern "C" {
|
|||
|
||||
\c ty must be a FloatingPoint sort
|
||||
|
||||
\sa Z3_mk_fpa_fp
|
||||
\sa Z3_mk_fpa_numeral_double
|
||||
\sa Z3_mk_fpa_numeral_float
|
||||
\sa Z3_mk_fpa_numeral_int
|
||||
\sa Z3_mk_fpa_numeral_int_uint
|
||||
\sa Z3_mk_numeral
|
||||
|
||||
def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))
|
||||
|
|
|
|||
|
|
@ -82,6 +82,7 @@ extern "C" {
|
|||
\param id - optional identifier to group soft constraints
|
||||
|
||||
\sa Z3_optimize_assert
|
||||
\sa Z3_optimize_assert_and_track
|
||||
|
||||
def_API('Z3_optimize_assert_soft', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST), _in(STRING), _in(SYMBOL)))
|
||||
*/
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue