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

FPA: Added core C API.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-07 19:09:41 +01:00
parent dd6dc5e165
commit 573ec293dc
3 changed files with 469 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

253
src/api/api_fpa.cpp
View file

@ -33,7 +33,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
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)
{
Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
@ -44,7 +44,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
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)
{
Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
@ -55,7 +55,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
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)
{
Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
@ -66,7 +66,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
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)
{
Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
@ -77,7 +77,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
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)
{
Z3_TRY;
LOG_Z3_mk_fpa_round_nearest_ties_to_even(c);
@ -102,6 +102,249 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s) {
Z3_TRY;
LOG_Z3_mk_fpa_nan(c, s);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_nan(to_sort(s)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, Z3_bool negative) {
Z3_TRY;
LOG_Z3_mk_fpa_inf(c, s, negative);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
float_util fu(ctx->m());
Z3_ast r = of_ast(negative != 0 ? fu.mk_minus_inf(to_sort(s)) : fu.mk_plus_inf(to_sort(s)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_abs(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_abs(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_abs(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_neg(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_neg(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_uminus(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_add(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_add(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_sub(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_sub(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_mul(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_mul(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_div(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_add(c, rm, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_div(to_expr(rm), to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_fma(Z3_context c, Z3_ast rm, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
Z3_TRY;
LOG_Z3_mk_fpa_fma(c, rm, t1, t2, t3);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_fused_ma(to_expr(rm), to_expr(t1), to_expr(t2), to_expr(t3)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_sqrt(Z3_context c, Z3_ast rm, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_sqrt(c, rm, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_sqrt(to_expr(rm), to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_rem(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_rem(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_rem(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_eq(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_float_eq(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_leq(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_leq(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_le(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_lt(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_lt(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_lt(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_geq(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_geq(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_ge(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_gt(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_gt(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_gt(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_is_normal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_is_normal(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_is_subnormal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_is_subnormal(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_is_zero(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_is_zero(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_is_inf(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_is_inf(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_is_inf(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_is_nan(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_is_nan(to_expr(t)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_min(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_min(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_min(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_max(Z3_context c, Z3_ast t1, Z3_ast t2) {
Z3_TRY;
LOG_Z3_mk_fpa_max(c, t1, t2);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
Z3_ast r = of_ast(float_util(ctx->m()).mk_max(to_expr(t1), to_expr(t2)));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
Z3_ast Z3_API Z3_mk_fpa_convert(Z3_context c, Z3_sort s, Z3_ast rm, Z3_ast t) {
Z3_TRY;
LOG_Z3_mk_fpa_convert(c, s, rm, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
float_util fu(ctx->m());
expr * args [2] = { to_expr(rm), to_expr(t) };
Z3_ast r = of_ast(ctx->m().mk_app(fu.get_family_id(), OP_TO_FLOAT,
to_sort(s)->get_num_parameters(), to_sort(s)->get_parameters(),
2, args));
RETURN_Z3(r);
Z3_CATCH_RETURN(0);
}
};

220
src/api/z3_fpa.h
View file

@ -65,7 +65,6 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_fpa_round_toward_zero(__in Z3_context c);
/**
\brief Create a floating point sort.
@ -74,7 +73,226 @@ extern "C" {
\remark ebits must be larger than 1 and sbits must be larger than 2.
*/
Z3_sort Z3_API Z3_mk_fpa_sort(__in Z3_context c, __in unsigned ebits, __in unsigned sbits);
/**
\brief Create a NaN of sort s.
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);
/**
\brief Create a floating point infinity of sort s.
When \c negative is true, -Inf will be generated instead of +Inf.
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);
/**
\brief Floating-point absolute value
t must have floating point sort.
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);
/**
\brief Floating-point negation
t must have floating point sort.
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);
/**
\brief Floating-point addition
rm must be of FPA rounding mode sort, t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point subtraction
rm must be of FPA rounding mode sort, t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point multiplication
rm must be of FPA rounding mode sort, t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point division
The nodes rm must be of FPA rounding mode sort t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point fused multiply-add.
The result is round((t1 * t2) + t3)
rm must be of FPA rounding mode sort, t1, t2, and t3 must have floating point sort.
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);
/**
\brief Floating-point square root
rm must be of FPA rounding mode sort, t must have floating point sort.
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);
/**
\brief Floating-point remainder
t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point equality
Note that this is IEEE 754 equality (as opposed to SMT-LIB =).
t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point less-than or equal
t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point less-than
t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point greater-than or equal
t1 and t2 must have floating point sort.
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);
/**
\brief Floating-point greater-than
t1 and t2 must have floating point sort.
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);
/**
\brief Predicate indicating whether t is a normal floating point number
t must have floating point sort.
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);
/**
\brief Predicate indicating whether t is a subnormal floating point number
t must have floating point sort.
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);
/**
\brief Predicate indicating whether t is a floating point number with zero value, i.e., +0 or -0.
t must have floating point sort.
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);
/**
\brief Predicate indicating whether t is a floating point number representing +Inf or -Inf
t must have floating point sort.
def_API('Z3_mk_fpa_is_inf', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_inf(__in Z3_context c, __in Z3_ast t);
/**
\brief Predicate indicating whether t is a NaN
t must have floating point sort.
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);
/**
\brief Minimum of floating point numbers
t1, t2 must have floating point sort.
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);
/**
\brief Maximum of floating point numbers
t1, t2 must have floating point sort.
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);
/**
\brief Conversion of a floating point number to sort s.
s must be a floating point sort, rm must have rounding mode sort, and t must have floating point sort.
def_API('Z3_mk_fpa_convert', AST, (_in(CONTEXT),_in(SORT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_convert(__in Z3_context c, __in Z3_sort s, __in Z3_ast rm, __in Z3_ast t);
#ifdef __cplusplus
};
#endif // __cplusplus

3
src/ast/float_decl_plugin.h
View file

@ -178,6 +178,7 @@ public:
family_id get_fid() const { return m_fid; }
family_id get_family_id() const { return m_fid; }
arith_util & au() { return m_a_util; }
float_decl_plugin & plugin() { return *m_plugin; }
sort * mk_float_sort(unsigned ebits, unsigned sbits);
sort * mk_rm_sort() { return m().mk_sort(m_fid, ROUNDING_MODE_SORT); }
@ -211,7 +212,7 @@ public:
bool is_nan(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nan(v); }
bool is_plus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pinf(v); }
bool is_minus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); }
bool is_minus_inf(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_ninf(v); }
bool is_zero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_zero(v); }
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_pzero(v); }
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_value(n, v) && fm().is_nzero(v); }