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

Added functions to test FP numerals for special values.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-17 13:31:07 +01:00
parent 6b474adc8a
commit 89d38385db
3 changed files with 160 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

96
src/api/api_fpa.cpp
View file

@ -1183,4 +1183,100 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_nan(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
api::context * ctx = mk_c(c);
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_nan(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_inf(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
api::context * ctx = mk_c(c);
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_inf(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_zero(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
api::context * ctx = mk_c(c);
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_zero(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_normal(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
api::context * ctx = mk_c(c);
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_normal(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_subnormal(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
api::context * ctx = mk_c(c);
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_subnormal(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_positive(c, t);
RESET_ERROR_CODE();
ast_manager & m = mk_c(c)->m();
api::context * ctx = mk_c(c);
mpf_manager & mpfm = mk_c(c)->fpautil().fm();
fpa_util & fu = ctx->fpautil();
if (!is_expr(t) || !fu.is_numeral(to_expr(t))) {
SET_ERROR_CODE(Z3_INVALID_ARG);
return 0;
}
return fu.is_positive(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
};

60
src/api/z3_fpa.h
View file

@ -822,6 +822,66 @@ extern "C" {
*/
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
/**
\brief Checks whether a given floating-point numeral is a NaN.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_nan', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is a +oo or -oo.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_inf', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is +zero or -zero.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_zero', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is normal.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_normal', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is subnormal.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_subnormal', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is positive.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_positive', AST, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
/**
\brief Retrieves the sign of a floating-point literal as a bit-vector expression.

4
src/ast/fpa_decl_plugin.h
View file

@ -288,11 +288,15 @@ public:
app * mk_nzero(sort * s) { return mk_nzero(get_ebits(s), get_sbits(s)); }
bool is_nan(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nan(v); }
bool is_inf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_inf(v); }
bool is_pinf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pinf(v); }
bool is_ninf(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_ninf(v); }
bool is_zero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_zero(v); }
bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); }
bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); }
bool is_normal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_normal(v); }
bool is_subnormal(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_denormal(v); }
bool is_positive(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pos(v); }
app * mk_fp(expr * sgn, expr * exp, expr * sig) {
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);