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

Added Z3_fpa_is_numeral_negative to FPA API

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-27 15:06:24 +01:00
parent 23c58a1ef6
commit e4f7ff9881
3 changed files with 35 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/api/api_fpa.cpp
View file

@ -1087,7 +1087,7 @@ extern "C" {
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val));
if (mpfm.is_normal(val) && !biased)
if (mpfm.is_normal(val) && !biased)
exp = mpfm.exp(val);
std::stringstream ss;
ss << exp;
@ -1122,7 +1122,7 @@ extern "C" {
mpfm.is_denormal(val) ? mpfm.mk_min_exp(ebits) :
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val));
if (mpfm.is_normal(val) && !biased)
if (mpfm.is_normal(val) && !biased)
*n = mpfm.exp(val);
return 1;
Z3_CATCH_RETURN(0);
@ -1155,10 +1155,10 @@ extern "C" {
mpfm.is_inf(val) ? mpfm.mk_top_exp(ebits) :
mpfm.bias_exp(ebits, mpfm.exp(val));
if (mpfm.is_normal(val) && !biased) {
std::cout << "unbiassing" << std::endl;
std::cout << "unbiassing" << std::endl;
exp = mpfm.exp(val);
}
app * a = mk_c(c)->bvutil().mk_numeral(exp, ebits);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_expr(a));
@ -1200,7 +1200,7 @@ extern "C" {
Z3_bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_nan(c, t);
LOG_Z3_fpa_is_numeral_nan(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
@ -1214,7 +1214,7 @@ extern "C" {
Z3_bool Z3_API Z3_fpa_is_numeral_inf(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_inf(c, t);
LOG_Z3_fpa_is_numeral_inf(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
@ -1228,7 +1228,7 @@ extern "C" {
Z3_bool Z3_API Z3_fpa_is_numeral_zero(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_zero(c, t);
LOG_Z3_fpa_is_numeral_zero(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
@ -1242,7 +1242,7 @@ extern "C" {
Z3_bool Z3_API Z3_fpa_is_numeral_normal(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_normal(c, t);
LOG_Z3_fpa_is_numeral_normal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
@ -1256,7 +1256,7 @@ extern "C" {
Z3_bool Z3_API Z3_fpa_is_numeral_subnormal(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_subnormal(c, t);
LOG_Z3_fpa_is_numeral_subnormal(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
@ -1270,7 +1270,7 @@ extern "C" {
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t) {
Z3_TRY;
Z3_fpa_is_numeral_positive(c, t);
LOG_Z3_fpa_is_numeral_positive(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
@ -1282,4 +1282,18 @@ extern "C" {
Z3_CATCH_RETURN(Z3_FALSE);
}
Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_negative(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
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_negative(to_expr(t));
Z3_CATCH_RETURN(Z3_FALSE);
}
};

10
src/api/z3_fpa.h
View file

@ -882,6 +882,16 @@ extern "C" {
*/
Z3_bool Z3_API Z3_fpa_is_numeral_positive(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is negative.
\param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_is_numeral_negative', BOOL, (_in(CONTEXT), _in(AST)))
*/
Z3_bool Z3_API Z3_fpa_is_numeral_negative(Z3_context c, Z3_ast t);
/**
\brief Retrieves the sign of a floating-point literal as a bit-vector expression.

1
src/ast/fpa_decl_plugin.h
View file

@ -297,6 +297,7 @@ public:
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); }
bool is_negative(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_neg(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);