mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
remove __in/__out SAL annotations.
They break the build with recent glibc versions and apparently noone is using them. Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes
parent
d7b3aaffbd
commit
f62a192357
18 changed files with 912 additions and 966 deletions
|
|
@ -47,7 +47,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_real(__in Z3_context c, int num, int den) {
|
||||
Z3_ast Z3_API Z3_mk_real(Z3_context c, int num, int den) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_real(c, num, den);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_map(__in Z3_context c, __in Z3_func_decl f, unsigned n, __in Z3_ast const* args) {
|
||||
Z3_ast Z3_API Z3_mk_map(Z3_context c, Z3_func_decl f, unsigned n, Z3_ast const* args) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_map(c, f, n, args);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -108,7 +108,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_const_array(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v) {
|
||||
Z3_ast Z3_API Z3_mk_const_array(Z3_context c, Z3_sort domain, Z3_ast v) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_const_array(c, domain, v);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -127,7 +127,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_array_default(__in Z3_context c, __in Z3_ast array) {
|
||||
Z3_ast Z3_API Z3_mk_array_default(Z3_context c, Z3_ast array) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_array_default(c, array);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -142,7 +142,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast mk_app_array_core(__in Z3_context c, __in Z3_sort domain, __in Z3_ast v) {
|
||||
Z3_ast mk_app_array_core(Z3_context c, Z3_sort domain, Z3_ast v) {
|
||||
RESET_ERROR_CODE();
|
||||
ast_manager & m = mk_c(c)->m();
|
||||
expr * _v = to_expr(v);
|
||||
|
|
@ -158,13 +158,13 @@ extern "C" {
|
|||
return of_ast(r);
|
||||
}
|
||||
|
||||
Z3_sort Z3_API Z3_mk_set_sort(__in Z3_context c, __in Z3_sort ty) {
|
||||
Z3_sort Z3_API Z3_mk_set_sort(Z3_context c, Z3_sort ty) {
|
||||
Z3_TRY;
|
||||
return Z3_mk_array_sort(c, ty, Z3_mk_bool_sort(c));
|
||||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_empty_set(__in Z3_context c, __in Z3_sort domain) {
|
||||
Z3_ast Z3_API Z3_mk_empty_set(Z3_context c, Z3_sort domain) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_empty_set(c, domain);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -173,7 +173,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_full_set(__in Z3_context c, __in Z3_sort domain) {
|
||||
Z3_ast Z3_API Z3_mk_full_set(Z3_context c, Z3_sort domain) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_mk_full_set(c, domain);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -188,15 +188,15 @@ extern "C" {
|
|||
MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
|
||||
MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
|
||||
|
||||
Z3_ast Z3_mk_set_member(__in Z3_context c, __in Z3_ast elem, __in Z3_ast set) {
|
||||
Z3_ast Z3_mk_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
|
||||
return Z3_mk_select(c, set, elem);
|
||||
}
|
||||
|
||||
Z3_ast Z3_mk_set_add(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem) {
|
||||
Z3_ast Z3_mk_set_add(Z3_context c, Z3_ast set, Z3_ast elem) {
|
||||
return Z3_mk_store(c, set, elem, Z3_mk_true(c));
|
||||
}
|
||||
|
||||
Z3_ast Z3_mk_set_del(__in Z3_context c, __in Z3_ast set, __in Z3_ast elem) {
|
||||
Z3_ast Z3_mk_set_del(Z3_context c, Z3_ast set, Z3_ast elem) {
|
||||
return Z3_mk_store(c, set, elem, Z3_mk_false(c));
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -159,7 +159,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
This function is a shorthand for <tt>shl(1, N-1)</tt>
|
||||
where <tt>N</tt> are the number of bits of \c s.
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_bvmsb(__in Z3_context c, __in Z3_sort s) {
|
||||
Z3_ast Z3_API Z3_mk_bvmsb(Z3_context c, Z3_sort s) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
// Not logging this one, since it is just syntax sugar.
|
||||
|
|
@ -179,19 +179,19 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_mk_bvsmin(__in Z3_context c, __in Z3_sort s) {
|
||||
Z3_ast Z3_mk_bvsmin(Z3_context c, Z3_sort s) {
|
||||
return Z3_mk_bvmsb(c, s);
|
||||
}
|
||||
|
||||
Z3_ast Z3_mk_bvsmax(__in Z3_context c, __in Z3_sort s) {
|
||||
Z3_ast Z3_mk_bvsmax(Z3_context c, Z3_sort s) {
|
||||
return Z3_mk_bvnot(c, Z3_mk_bvmsb(c, s));
|
||||
}
|
||||
|
||||
Z3_ast Z3_mk_bvumax(__in Z3_context c, __in Z3_sort s) {
|
||||
Z3_ast Z3_mk_bvumax(Z3_context c, Z3_sort s) {
|
||||
return Z3_mk_int(c, -1, s);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed) {
|
||||
Z3_ast Z3_API Z3_mk_bvadd_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
if (is_signed) {
|
||||
|
|
@ -235,7 +235,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
}
|
||||
|
||||
// only for signed machine integers
|
||||
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
|
||||
Z3_ast Z3_API Z3_mk_bvadd_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
Z3_ast zero = Z3_mk_int(c, 0, Z3_get_sort(c, t1));
|
||||
|
|
@ -263,7 +263,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
}
|
||||
|
||||
// only for signed machine integers
|
||||
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
|
||||
Z3_ast Z3_API Z3_mk_bvsub_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
Z3_ast minus_t2 = Z3_mk_bvneg(c, t2);
|
||||
|
|
@ -291,7 +291,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2, Z3_bool is_signed) {
|
||||
Z3_ast Z3_API Z3_mk_bvsub_no_underflow(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_bool is_signed) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
if (is_signed) {
|
||||
|
|
@ -316,7 +316,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(__in Z3_context c, __in Z3_ast n1, __in Z3_ast n2, Z3_bool is_signed) {
|
||||
Z3_ast Z3_API Z3_mk_bvmul_no_overflow(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_bool is_signed) {
|
||||
LOG_Z3_mk_bvmul_no_overflow(c, n1, n2, is_signed);
|
||||
RESET_ERROR_CODE();
|
||||
if (is_signed) {
|
||||
|
|
@ -328,13 +328,13 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
}
|
||||
|
||||
// only for signed machine integers
|
||||
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(__in Z3_context c, __in Z3_ast n1, __in Z3_ast n2) {
|
||||
Z3_ast Z3_API Z3_mk_bvmul_no_underflow(Z3_context c, Z3_ast n1, Z3_ast n2) {
|
||||
LOG_Z3_mk_bvmul_no_underflow(c, n1, n2);
|
||||
MK_BINARY_BODY(Z3_mk_bvmul_no_underflow, mk_c(c)->get_bv_fid(), OP_BSMUL_NO_UDFL, SKIP);
|
||||
}
|
||||
|
||||
// only for signed machine integers
|
||||
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(__in Z3_context c, __in Z3_ast t) {
|
||||
Z3_ast Z3_API Z3_mk_bvneg_no_overflow(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
Z3_ast min = Z3_mk_bvsmin(c, Z3_get_sort(c, t));
|
||||
|
|
@ -346,7 +346,7 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \
|
|||
}
|
||||
|
||||
// only for signed machine integers
|
||||
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2) {
|
||||
Z3_ast Z3_API Z3_mk_bvsdiv_no_overflow(Z3_context c, Z3_ast t1, Z3_ast t2) {
|
||||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
Z3_sort s = Z3_get_sort(c, t1);
|
||||
|
|
|
|||
|
|
@ -532,7 +532,7 @@ extern "C" {
|
|||
// [Leo]: using exception handling, we don't need global error handlers anymore
|
||||
}
|
||||
|
||||
void Z3_API Z3_set_error(__in Z3_context c, __in Z3_error_code e) {
|
||||
void Z3_API Z3_set_error(Z3_context c, Z3_error_code e) {
|
||||
SET_ERROR_CODE(e);
|
||||
}
|
||||
|
||||
|
|
@ -584,7 +584,7 @@ extern "C" {
|
|||
|
||||
};
|
||||
|
||||
Z3_API ast_manager& Z3_get_manager(__in Z3_context c) {
|
||||
Z3_API ast_manager& Z3_get_manager(Z3_context c) {
|
||||
return mk_c(c)->m();
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -304,8 +304,8 @@ extern "C" {
|
|||
}
|
||||
|
||||
Z3_lbool Z3_API Z3_fixedpoint_query_relations(
|
||||
__in Z3_context c,__in Z3_fixedpoint d,
|
||||
__in unsigned num_relations, Z3_func_decl const relations[]) {
|
||||
Z3_context c,Z3_fixedpoint d,
|
||||
unsigned num_relations, Z3_func_decl const relations[]) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fixedpoint_query_relations(c, d, num_relations, relations);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
|
|||
|
|
@ -619,7 +619,7 @@ extern "C" {
|
|||
}
|
||||
|
||||
Z3_ast Z3_datatype_update_field(
|
||||
__in Z3_context c, __in Z3_func_decl f, __in Z3_ast t, __in Z3_ast v) {
|
||||
Z3_context c, Z3_func_decl f, Z3_ast t, Z3_ast v) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_datatype_update_field(c, f, t, v);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
|
|||
|
|
@ -737,7 +737,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t) {
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_string(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -767,7 +767,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n) {
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -791,7 +791,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t) {
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_string(c, t);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -815,7 +815,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN("");
|
||||
}
|
||||
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n) {
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
|
|||
|
|
@ -207,7 +207,7 @@ extern "C" {
|
|||
opts->map[name] = value;
|
||||
}
|
||||
|
||||
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p){
|
||||
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p){
|
||||
Z3_TRY;
|
||||
LOG_Z3_get_interpolant(c, pf, pat, p);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -240,7 +240,7 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c, __in Z3_ast pat, __in Z3_params p, __out Z3_ast_vector *out_interp, __out Z3_model *model){
|
||||
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c, Z3_ast pat, Z3_params p, Z3_ast_vector *out_interp, Z3_model *model){
|
||||
Z3_TRY;
|
||||
LOG_Z3_compute_interpolant(c, pat, p, out_interp, model);
|
||||
RESET_ERROR_CODE();
|
||||
|
|
@ -708,15 +708,15 @@ extern "C" {
|
|||
def_API('Z3_interpolate', BOOL, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(PARAMS), _out_array(1, AST), _out(MODEL), _out(LITERALS), _in(UINT), _in(UINT), _in_array(9, AST)))
|
||||
*/
|
||||
|
||||
Z3_lbool Z3_API Z3_interpolate(__in Z3_context ctx,
|
||||
__in unsigned num,
|
||||
__in_ecount(num) Z3_ast *cnsts,
|
||||
__in_ecount(num) unsigned *parents,
|
||||
__in Z3_params options,
|
||||
__out_ecount(num - 1) Z3_ast *interps,
|
||||
__out Z3_model *model,
|
||||
__out Z3_literals *labels,
|
||||
__in unsigned incremental,
|
||||
__in unsigned num_theory,
|
||||
__in_ecount(num_theory) Z3_ast *theory);
|
||||
Z3_lbool Z3_API Z3_interpolate(Z3_context ctx,
|
||||
unsigned num,
|
||||
Z3_ast *cnsts,
|
||||
unsigned *parents,
|
||||
Z3_params options,
|
||||
Z3_ast *interps,
|
||||
Z3_model *model,
|
||||
Z3_literals *labels,
|
||||
unsigned incremental,
|
||||
unsigned num_theory,
|
||||
Z3_ast *theory);
|
||||
#endif
|
||||
|
|
|
|||
10
src/api/z3.h
10
src/api/z3.h
|
|
@ -30,15 +30,5 @@ Notes:
|
|||
#include"z3_interp.h"
|
||||
#include"z3_fpa.h"
|
||||
|
||||
#undef __in
|
||||
#undef __out
|
||||
#undef __inout
|
||||
#undef __in_z
|
||||
#undef __out_z
|
||||
#undef __ecount
|
||||
#undef __in_ecount
|
||||
#undef __out_ecount
|
||||
#undef __inout_ecount
|
||||
|
||||
#endif
|
||||
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_value(__in Z3_context c, __in Z3_ast a);
|
||||
Z3_bool Z3_API Z3_algebraic_is_value(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the Z3_TRUE if \c a is positive, and Z3_FALSE otherwise.
|
||||
|
|
@ -52,7 +52,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_is_pos', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_pos(__in Z3_context c, __in Z3_ast a);
|
||||
Z3_bool Z3_API Z3_algebraic_is_pos(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the Z3_TRUE if \c a is negative, and Z3_FALSE otherwise.
|
||||
|
|
@ -61,7 +61,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_is_neg', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_neg(__in Z3_context c, __in Z3_ast a);
|
||||
Z3_bool Z3_API Z3_algebraic_is_neg(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the Z3_TRUE if \c a is zero, and Z3_FALSE otherwise.
|
||||
|
|
@ -70,7 +70,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_is_zero', BOOL, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_is_zero(__in Z3_context c, __in Z3_ast a);
|
||||
Z3_bool Z3_API Z3_algebraic_is_zero(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return 1 if \c a is positive, 0 if \c a is zero, and -1 if \c a is negative.
|
||||
|
|
@ -79,7 +79,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_sign', INT, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
int Z3_API Z3_algebraic_sign(__in Z3_context c, __in Z3_ast a);
|
||||
int Z3_API Z3_algebraic_sign(Z3_context c, Z3_ast a);
|
||||
|
||||
/**
|
||||
\brief Return the value a + b.
|
||||
|
|
@ -90,7 +90,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_add', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_add(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_ast Z3_API Z3_algebraic_add(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the value a - b.
|
||||
|
|
@ -101,7 +101,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_sub', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_sub(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_ast Z3_API Z3_algebraic_sub(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the value a * b.
|
||||
|
|
@ -112,7 +112,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_mul', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_mul(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_ast Z3_API Z3_algebraic_mul(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the value a / b.
|
||||
|
|
@ -124,7 +124,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_div', AST, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_div(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_ast Z3_API Z3_algebraic_div(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return the a^(1/k)
|
||||
|
|
@ -135,7 +135,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_root', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_root(__in Z3_context c, __in Z3_ast a, __in unsigned k);
|
||||
Z3_ast Z3_API Z3_algebraic_root(Z3_context c, Z3_ast a, unsigned k);
|
||||
|
||||
/**
|
||||
\brief Return the a^k
|
||||
|
|
@ -145,7 +145,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_power', AST, (_in(CONTEXT), _in(AST), _in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_algebraic_power(__in Z3_context c, __in Z3_ast a, __in unsigned k);
|
||||
Z3_ast Z3_API Z3_algebraic_power(Z3_context c, Z3_ast a, unsigned k);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a < b, and Z3_FALSE otherwise.
|
||||
|
|
@ -155,7 +155,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_lt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_lt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_bool Z3_API Z3_algebraic_lt(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a > b, and Z3_FALSE otherwise.
|
||||
|
|
@ -165,7 +165,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_gt', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_gt(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_bool Z3_API Z3_algebraic_gt(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a <= b, and Z3_FALSE otherwise.
|
||||
|
|
@ -175,7 +175,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_le', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_le(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_bool Z3_API Z3_algebraic_le(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a >= b, and Z3_FALSE otherwise.
|
||||
|
|
@ -185,7 +185,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_ge', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_ge(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_bool Z3_API Z3_algebraic_ge(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a == b, and Z3_FALSE otherwise.
|
||||
|
|
@ -195,7 +195,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_eq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_eq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_bool Z3_API Z3_algebraic_eq(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Return Z3_TRUE if a != b, and Z3_FALSE otherwise.
|
||||
|
|
@ -205,7 +205,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_neq', BOOL, (_in(CONTEXT), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_algebraic_neq(__in Z3_context c, __in Z3_ast a, __in Z3_ast b);
|
||||
Z3_bool Z3_API Z3_algebraic_neq(Z3_context c, Z3_ast a, Z3_ast b);
|
||||
|
||||
/**
|
||||
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
|
||||
|
|
@ -217,7 +217,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_roots', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_algebraic_roots(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
|
||||
Z3_ast_vector Z3_API Z3_algebraic_roots(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
|
||||
|
||||
/**
|
||||
\brief Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the
|
||||
|
|
@ -228,7 +228,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_algebraic_eval', INT, (_in(CONTEXT), _in(AST), _in(UINT), _in_array(2, AST)))
|
||||
*/
|
||||
int Z3_API Z3_algebraic_eval(__in Z3_context c, __in Z3_ast p, __in unsigned n, __in Z3_ast a[]);
|
||||
int Z3_API Z3_algebraic_eval(Z3_context c, Z3_ast p, unsigned n, Z3_ast a[]);
|
||||
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
|
|
|||
1442
src/api/z3_api.h
1442
src/api/z3_api.h
File diff suppressed because it is too large
Load diff
140
src/api/z3_fpa.h
140
src/api/z3_fpa.h
|
|
@ -42,7 +42,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_rounding_mode_sort(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
|
||||
|
|
@ -51,7 +51,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_even(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
|
||||
|
|
@ -60,7 +60,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rne(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_rne(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
|
||||
|
|
@ -69,7 +69,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_nearest_ties_to_away(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
|
||||
|
|
@ -78,7 +78,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rna(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_rna(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
|
||||
|
|
@ -87,7 +87,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_positive(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
|
||||
|
|
@ -96,7 +96,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtp(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtp(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
|
||||
|
|
@ -105,7 +105,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_negative(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
|
||||
|
|
@ -114,7 +114,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtn(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtn(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
|
||||
|
|
@ -123,7 +123,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
|
||||
|
|
@ -132,7 +132,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtz(__in Z3_context c);
|
||||
Z3_ast Z3_API Z3_mk_fpa_rtz(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a FloatingPoint sort.
|
||||
|
|
@ -145,7 +145,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort(Z3_context c, unsigned ebits, unsigned sbits);
|
||||
|
||||
/**
|
||||
\brief Create the half-precision (16-bit) FloatingPoint sort.
|
||||
|
|
@ -154,7 +154,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_half(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_half(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the half-precision (16-bit) FloatingPoint sort.
|
||||
|
|
@ -163,7 +163,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_16(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_16(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the single-precision (32-bit) FloatingPoint sort.
|
||||
|
|
@ -172,7 +172,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_single', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_single(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_single(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the single-precision (32-bit) FloatingPoint sort.
|
||||
|
|
@ -181,7 +181,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_32(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_32(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the double-precision (64-bit) FloatingPoint sort.
|
||||
|
|
@ -190,7 +190,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_double(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_double(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the double-precision (64-bit) FloatingPoint sort.
|
||||
|
|
@ -199,7 +199,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_64(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_64(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the quadruple-precision (128-bit) FloatingPoint sort.
|
||||
|
|
@ -208,7 +208,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_quadruple(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create the quadruple-precision (128-bit) FloatingPoint sort.
|
||||
|
|
@ -217,7 +217,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
|
||||
*/
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_128(__in Z3_context c);
|
||||
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Create a floating-point NaN of sort s.
|
||||
|
|
@ -227,7 +227,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_nan(__in Z3_context c, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Create a floating-point infinity of sort s.
|
||||
|
|
@ -240,7 +240,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_inf', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_inf(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
|
||||
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative);
|
||||
|
||||
/**
|
||||
\brief Create a floating-point zero of sort s.
|
||||
|
|
@ -253,7 +253,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_zero', AST, (_in(CONTEXT),_in(SORT),_in(BOOL)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_zero(__in Z3_context c, __in Z3_sort s, __in Z3_bool negative);
|
||||
Z3_ast Z3_API Z3_mk_fpa_zero(Z3_context c, Z3_sort s, Z3_bool negative);
|
||||
|
||||
/**
|
||||
\brief Create an expression of FloatingPoint sort from three bit-vector expressions.
|
||||
|
|
@ -271,7 +271,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_fp(__in Z3_context c, __in Z3_ast sgn, __in Z3_ast exp, __in Z3_ast sig);
|
||||
Z3_ast Z3_API Z3_mk_fpa_fp(Z3_context c, Z3_ast sgn, Z3_ast exp, Z3_ast sig);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a float.
|
||||
|
|
@ -289,7 +289,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_numeral_float', AST, (_in(CONTEXT), _in(FLOAT), _in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_float(__in Z3_context c, __in float v, __in Z3_sort ty);
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_float(Z3_context c, float v, Z3_sort ty);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a double.
|
||||
|
|
@ -307,7 +307,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_numeral_double', AST, (_in(CONTEXT), _in(DOUBLE), _in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_double(__in Z3_context c, __in double v, __in Z3_sort ty);
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_double(Z3_context c, double v, Z3_sort ty);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a signed integer.
|
||||
|
|
@ -322,7 +322,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_numeral_int', AST, (_in(CONTEXT), _in(INT), _in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_int(__in Z3_context c, __in signed v, Z3_sort ty);
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_int(Z3_context c, signed v, Z3_sort ty);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a sign bit and two integers.
|
||||
|
|
@ -339,7 +339,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_numeral_int_uint', AST, (_in(CONTEXT), _in(BOOL), _in(INT), _in(UINT), _in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(__in Z3_context c, __in Z3_bool sgn, __in signed exp, __in unsigned sig, Z3_sort ty);
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_int_uint(Z3_context c, Z3_bool sgn, signed exp, unsigned sig, Z3_sort ty);
|
||||
|
||||
/**
|
||||
\brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
|
||||
|
|
@ -356,7 +356,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_numeral_int64_uint64', AST, (_in(CONTEXT), _in(BOOL), _in(INT64), _in(UINT64), _in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(__in Z3_context c, __in Z3_bool sgn, __in __int64 exp, __in __uint64 sig, Z3_sort ty);
|
||||
Z3_ast Z3_API Z3_mk_fpa_numeral_int64_uint64(Z3_context c, Z3_bool sgn, __int64 exp, __uint64 sig, Z3_sort ty);
|
||||
|
||||
/**
|
||||
\brief Floating-point absolute value
|
||||
|
|
@ -366,7 +366,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_abs(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Floating-point negation
|
||||
|
|
@ -376,7 +376,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_neg(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Floating-point addition
|
||||
|
|
@ -390,7 +390,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_add(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point subtraction
|
||||
|
|
@ -404,7 +404,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_sub(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point multiplication
|
||||
|
|
@ -418,7 +418,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_mul(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point division
|
||||
|
|
@ -432,7 +432,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_div(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point fused multiply-add.
|
||||
|
|
@ -449,7 +449,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_fma(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t1, __in Z3_ast t2, __in Z3_ast t3);
|
||||
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3);
|
||||
|
||||
/**
|
||||
\brief Floating-point square root
|
||||
|
|
@ -462,7 +462,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_sqrt(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Floating-point remainder
|
||||
|
|
@ -475,7 +475,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_rem(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point roundToIntegral. Rounds a floating-point number to
|
||||
|
|
@ -489,7 +489,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_round_to_integral(Z3_context c, Z3_ast rm, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Minimum of floating-point numbers.
|
||||
|
|
@ -502,7 +502,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_min(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Maximum of floating-point numbers.
|
||||
|
|
@ -515,7 +515,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_max(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point less than or equal.
|
||||
|
|
@ -528,7 +528,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_leq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point less than.
|
||||
|
|
@ -541,7 +541,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_lt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point greater than or equal.
|
||||
|
|
@ -554,7 +554,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_geq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point greater than.
|
||||
|
|
@ -567,7 +567,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_gt(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Floating-point equality.
|
||||
|
|
@ -582,7 +582,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_eq(__in Z3_context c, __in Z3_ast t1, __in Z3_ast t2);
|
||||
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a normal floating-point number.
|
||||
|
|
@ -594,7 +594,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_normal(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a subnormal floating-point number.
|
||||
|
|
@ -606,7 +606,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
|
||||
|
|
@ -618,7 +618,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_zero(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a floating-point number representing +oo or -oo.
|
||||
|
|
@ -630,7 +630,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_infinite(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a NaN.
|
||||
|
|
@ -642,7 +642,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_nan(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a negative floating-point number.
|
||||
|
|
@ -654,7 +654,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_negative(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Predicate indicating whether t is a positive floating-point number.
|
||||
|
|
@ -666,7 +666,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_positive(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_is_positive(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
|
||||
|
|
@ -684,7 +684,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(__in Z3_context c, __in Z3_ast bv, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_bv(Z3_context c, Z3_ast bv, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
|
||||
|
|
@ -702,7 +702,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_float(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Conversion of a term of real sort into a term of FloatingPoint sort.
|
||||
|
|
@ -720,7 +720,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_real(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
|
||||
|
|
@ -739,7 +739,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_signed(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
|
||||
|
|
@ -758,7 +758,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_unsigned(Z3_context c, Z3_ast rm, Z3_ast t, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Conversion of a floating-point term into an unsigned bit-vector.
|
||||
|
|
@ -774,7 +774,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ubv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ubv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);
|
||||
|
||||
/**
|
||||
\brief Conversion of a floating-point term into a signed bit-vector.
|
||||
|
|
@ -790,7 +790,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_sbv(__in Z3_context c, __in Z3_ast rm, __in Z3_ast t, __in unsigned sz);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_sbv(Z3_context c, Z3_ast rm, Z3_ast t, unsigned sz);
|
||||
|
||||
/**
|
||||
\brief Conversion of a floating-point term into a real-numbered term.
|
||||
|
|
@ -804,7 +804,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_real(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_real(Z3_context c, Z3_ast t);
|
||||
|
||||
|
||||
/**
|
||||
|
|
@ -820,7 +820,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_fpa_get_ebits(__in Z3_context c, __in Z3_sort s);
|
||||
unsigned Z3_API Z3_fpa_get_ebits(Z3_context c, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
|
||||
|
|
@ -830,7 +830,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
|
||||
*/
|
||||
unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
|
||||
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
|
||||
|
||||
/**
|
||||
\brief Retrieves the sign of a floating-point literal.
|
||||
|
|
@ -843,7 +843,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
|
||||
|
||||
/**
|
||||
\brief Return the significand value of a floating-point numeral as a string.
|
||||
|
|
@ -856,7 +856,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Return the significand value of a floating-point numeral as a uint64.
|
||||
|
|
@ -870,7 +870,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(__in Z3_context c, __in Z3_ast t, __out __uint64 * n);
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_significand_uint64(Z3_context c, Z3_ast t, __uint64 * n);
|
||||
|
||||
/**
|
||||
\brief Return the exponent value of a floating-point numeral as a string
|
||||
|
|
@ -880,7 +880,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_string Z3_API Z3_fpa_get_numeral_exponent_string(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
|
||||
|
|
@ -891,7 +891,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
|
||||
*/
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(__in Z3_context c, __in Z3_ast t, __out __int64 * n);
|
||||
Z3_bool Z3_API Z3_fpa_get_numeral_exponent_int64(Z3_context c, Z3_ast t, __int64 * n);
|
||||
|
||||
/**
|
||||
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
|
||||
|
|
@ -908,7 +908,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(__in Z3_context c, __in Z3_ast t);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_ieee_bv(Z3_context c, Z3_ast t);
|
||||
|
||||
/**
|
||||
\brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
|
||||
|
|
@ -927,7 +927,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(__in Z3_context c, __in Z3_ast rm, __in Z3_ast exp, __in Z3_ast sig, __in Z3_sort s);
|
||||
Z3_ast Z3_API Z3_mk_fpa_to_fp_int_real(Z3_context c, Z3_ast rm, Z3_ast exp, Z3_ast sig, Z3_sort s);
|
||||
|
||||
/*@}*/
|
||||
|
||||
|
|
|
|||
|
|
@ -43,7 +43,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_mk_interpolant', AST, (_in(CONTEXT), _in(AST)))
|
||||
*/
|
||||
Z3_ast Z3_API Z3_mk_interpolant(__in Z3_context c, __in Z3_ast a);
|
||||
Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a);
|
||||
|
||||
|
||||
/** \brief This function generates a Z3 context suitable for generation of
|
||||
|
|
@ -62,7 +62,7 @@ extern "C" {
|
|||
|
||||
*/
|
||||
|
||||
Z3_context Z3_API Z3_mk_interpolation_context(__in Z3_config cfg);
|
||||
Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg);
|
||||
|
||||
/** Compute an interpolant from a refutation. This takes a proof of
|
||||
"false" from a set of formulas C, and an interpolation
|
||||
|
|
@ -130,7 +130,7 @@ extern "C" {
|
|||
def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
|
||||
*/
|
||||
|
||||
Z3_ast_vector Z3_API Z3_get_interpolant(__in Z3_context c, __in Z3_ast pf, __in Z3_ast pat, __in Z3_params p);
|
||||
Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p);
|
||||
|
||||
/* Compute an interpolant for an unsatisfiable conjunction of formulas.
|
||||
|
||||
|
|
@ -164,11 +164,11 @@ extern "C" {
|
|||
def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
|
||||
*/
|
||||
|
||||
Z3_lbool Z3_API Z3_compute_interpolant(__in Z3_context c,
|
||||
__in Z3_ast pat,
|
||||
__in Z3_params p,
|
||||
__out Z3_ast_vector *interp,
|
||||
__out Z3_model *model);
|
||||
Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
|
||||
Z3_ast pat,
|
||||
Z3_params p,
|
||||
Z3_ast_vector *interp,
|
||||
Z3_model *model);
|
||||
|
||||
/** Return a string summarizing cumulative time used for
|
||||
interpolation. This string is purely for entertainment purposes
|
||||
|
|
@ -180,7 +180,7 @@ extern "C" {
|
|||
def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
|
||||
*/
|
||||
|
||||
Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
|
||||
Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx);
|
||||
|
||||
/**
|
||||
\brief Read an interpolation problem from file.
|
||||
|
|
@ -219,14 +219,14 @@ extern "C" {
|
|||
|
||||
*/
|
||||
|
||||
int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
|
||||
__out unsigned *num,
|
||||
__out Z3_ast *cnsts[],
|
||||
__out unsigned *parents[],
|
||||
__in Z3_string filename,
|
||||
__out_opt Z3_string_ptr error,
|
||||
__out unsigned *num_theory,
|
||||
__out Z3_ast *theory[]);
|
||||
int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
|
||||
unsigned *num,
|
||||
Z3_ast *cnsts[],
|
||||
unsigned *parents[],
|
||||
Z3_string filename,
|
||||
Z3_string_ptr error,
|
||||
unsigned *num_theory,
|
||||
Z3_ast *theory[]);
|
||||
|
||||
|
||||
|
||||
|
|
@ -250,14 +250,14 @@ extern "C" {
|
|||
def_API('Z3_check_interpolant', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in_array(1, AST), _out(STRING), _in(UINT), _in_array(6, AST)))
|
||||
*/
|
||||
|
||||
int Z3_API Z3_check_interpolant(__in Z3_context ctx,
|
||||
__in unsigned num,
|
||||
__in_ecount(num) Z3_ast cnsts[],
|
||||
__in_ecount(num) unsigned parents[],
|
||||
__in_ecount(num - 1) Z3_ast *interps,
|
||||
__out_opt Z3_string_ptr error,
|
||||
__in unsigned num_theory,
|
||||
__in_ecount(num_theory) Z3_ast theory[]);
|
||||
int Z3_API Z3_check_interpolant(Z3_context ctx,
|
||||
unsigned num,
|
||||
Z3_ast cnsts[],
|
||||
unsigned parents[],
|
||||
Z3_ast *interps,
|
||||
Z3_string_ptr error,
|
||||
unsigned num_theory,
|
||||
Z3_ast theory[]);
|
||||
|
||||
/** Write an interpolation problem to file suitable for reading with
|
||||
Z3_read_interpolation_problem. The output file is a sequence
|
||||
|
|
@ -275,13 +275,13 @@ extern "C" {
|
|||
def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST)))
|
||||
*/
|
||||
|
||||
void Z3_API Z3_write_interpolation_problem(__in Z3_context ctx,
|
||||
__in unsigned num,
|
||||
__in_ecount(num) Z3_ast cnsts[],
|
||||
__in_ecount(num) unsigned parents[],
|
||||
__in Z3_string filename,
|
||||
__in unsigned num_theory,
|
||||
__in_ecount(num_theory) Z3_ast theory[]);
|
||||
void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
|
||||
unsigned num,
|
||||
Z3_ast cnsts[],
|
||||
unsigned parents[],
|
||||
Z3_string filename,
|
||||
unsigned num_theory,
|
||||
Z3_ast theory[]);
|
||||
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
|
|
|||
|
|
@ -4,38 +4,6 @@ Copyright (c) 2015 Microsoft Corporation
|
|||
|
||||
--*/
|
||||
|
||||
#ifndef __in
|
||||
#define __in
|
||||
#endif
|
||||
|
||||
#ifndef __out
|
||||
#define __out
|
||||
#endif
|
||||
|
||||
#ifndef __out_opt
|
||||
#define __out_opt __out
|
||||
#endif
|
||||
|
||||
#ifndef __ecount
|
||||
#define __ecount(num_args)
|
||||
#endif
|
||||
|
||||
#ifndef __in_ecount
|
||||
#define __in_ecount(num_args) __in __ecount(num_args)
|
||||
#endif
|
||||
|
||||
#ifndef __out_ecount
|
||||
#define __out_ecount(num_args) __out __ecount(num_args)
|
||||
#endif
|
||||
|
||||
#ifndef __inout_ecount
|
||||
#define __inout_ecount(num_args) __in __out __ecount(num_args)
|
||||
#endif
|
||||
|
||||
#ifndef __inout
|
||||
#define __inout __in __out
|
||||
#endif
|
||||
|
||||
#ifndef Z3_bool_opt
|
||||
#define Z3_bool_opt Z3_bool
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
|
||||
*/
|
||||
Z3_ast_vector Z3_API Z3_polynomial_subresultants(__in Z3_context c, __in Z3_ast p, __in Z3_ast q, __in Z3_ast x);
|
||||
Z3_ast_vector Z3_API Z3_polynomial_subresultants(Z3_context c, Z3_ast p, Z3_ast q, Z3_ast x);
|
||||
|
||||
|
||||
/*@}*/
|
||||
|
|
|
|||
|
|
@ -34,7 +34,7 @@ extern "C" {
|
|||
[pointer_default(ref)] interface Z3 {
|
||||
#endif // CAMLIDL
|
||||
|
||||
Z3_bool Z3_API Z3_get_numeral_rational(__in Z3_context c, __in Z3_ast a, rational& r);
|
||||
Z3_bool Z3_API Z3_get_numeral_rational(Z3_context c, Z3_ast a, rational& r);
|
||||
|
||||
#ifndef CAMLIDL
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
|
|
@ -43,42 +43,42 @@ extern "C" {
|
|||
|
||||
def_API('Z3_rcf_del', VOID, (_in(CONTEXT), _in(RCF_NUM)))
|
||||
*/
|
||||
void Z3_API Z3_rcf_del(__in Z3_context c, __in Z3_rcf_num a);
|
||||
void Z3_API Z3_rcf_del(Z3_context c, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_mk_rational(Z3_context c, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_mk_small_int(Z3_context c, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_mk_pi(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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_mk_e(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),))
|
||||
*/
|
||||
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c);
|
||||
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
|
||||
|
||||
/**
|
||||
\brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
|
||||
|
|
@ -89,112 +89,112 @@ extern "C" {
|
|||
|
||||
def_API('Z3_rcf_mk_roots', UINT, (_in(CONTEXT), _in(UINT), _in_array(1, RCF_NUM), _out_array(1, RCF_NUM)))
|
||||
*/
|
||||
unsigned Z3_API Z3_rcf_mk_roots(__in Z3_context c, __in unsigned n, __in_ecount(n) Z3_rcf_num const a[], __out_ecount(n) Z3_rcf_num roots[]);
|
||||
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
|
||||
|
||||
/**
|
||||
\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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, 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);
|
||||
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
|
||||
|
||||
/**
|
||||
\brief Return the value a^k
|
||||
|
||||
def_API('Z3_rcf_power', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
|
||||
*/
|
||||
Z3_rcf_num Z3_API Z3_rcf_power(__in Z3_context c, __in Z3_rcf_num a, __in unsigned k);
|
||||
Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
|
||||
|
||||
/**
|
||||
\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);
|
||||
Z3_bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, 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);
|
||||
Z3_bool Z3_API Z3_rcf_neq(Z3_context c, Z3_rcf_num a, 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), _in(BOOL), _in(BOOL)))
|
||||
*/
|
||||
Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html);
|
||||
Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact, Z3_bool html);
|
||||
|
||||
/**
|
||||
\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);
|
||||
Z3_string Z3_API Z3_rcf_num_to_decimal_string(Z3_context c, Z3_rcf_num a, unsigned prec);
|
||||
|
||||
/**
|
||||
\brief Extract the "numerator" and "denominator" of the given RCF numeral.
|
||||
|
|
@ -202,7 +202,7 @@ extern "C" {
|
|||
|
||||
def_API('Z3_rcf_get_numerator_denominator', VOID, (_in(CONTEXT), _in(RCF_NUM), _out(RCF_NUM), _out(RCF_NUM)))
|
||||
*/
|
||||
void Z3_API Z3_rcf_get_numerator_denominator(__in Z3_context c, __in Z3_rcf_num a, __out Z3_rcf_num * n, __out Z3_rcf_num * d);
|
||||
void Z3_API Z3_rcf_get_numerator_denominator(Z3_context c, Z3_rcf_num a, Z3_rcf_num * n, Z3_rcf_num * d);
|
||||
|
||||
/*@}*/
|
||||
/*@}*/
|
||||
|
|
|
|||
|
|
@ -273,18 +273,6 @@ bool has_duplicates(const IT & begin, const IT & end) {
|
|||
return false;
|
||||
}
|
||||
|
||||
#ifndef __out
|
||||
#define __out
|
||||
#endif
|
||||
|
||||
#ifndef __in
|
||||
#define __in
|
||||
#endif
|
||||
|
||||
#ifndef __inout
|
||||
#define __inout
|
||||
#endif
|
||||
|
||||
#ifndef __fallthrough
|
||||
#define __fallthrough
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue