mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

FPA: added is_nan

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-07 18:34:31 +01:00
parent d7639557d2
commit 455618bb2b
7 changed files with 24 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/float_decl_plugin.cpp
View file

@ -256,6 +256,7 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
case OP_FLOAT_IS_NZERO: name = "isNZero"; break;
case OP_FLOAT_IS_PZERO: name = "isPZero"; break;
case OP_FLOAT_IS_SIGN_MINUS: name = "isSignMinus"; break;
case OP_FLOAT_IS_NAN: name = "isNaN"; break;
case OP_FLOAT_IS_INF: name = "isInfinite"; break;
case OP_FLOAT_IS_NORMAL: name = "isNormal"; break;
case OP_FLOAT_IS_SUBNORMAL: name = "isSubnormal"; break;
@ -418,6 +419,7 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_FLOAT_IS_NZERO:
case OP_FLOAT_IS_PZERO:
case OP_FLOAT_IS_SIGN_MINUS:
case OP_FLOAT_IS_NAN:
case OP_FLOAT_IS_INF:
case OP_FLOAT_IS_NORMAL:
case OP_FLOAT_IS_SUBNORMAL:
@ -479,6 +481,7 @@ void float_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol co
op_names.push_back(builtin_name("<=", OP_FLOAT_LE));
op_names.push_back(builtin_name(">=", OP_FLOAT_GE));
op_names.push_back(builtin_name("isNaN", OP_FLOAT_IS_NAN));
op_names.push_back(builtin_name("isInfinite", OP_FLOAT_IS_INF));
op_names.push_back(builtin_name("isZero", OP_FLOAT_IS_ZERO));
op_names.push_back(builtin_name("isNZero", OP_FLOAT_IS_NZERO));

2
src/ast/float_decl_plugin.h
View file

@ -61,6 +61,7 @@ enum float_op_kind {
OP_FLOAT_GT,
OP_FLOAT_LE,
OP_FLOAT_GE,
OP_FLOAT_IS_NAN,
OP_FLOAT_IS_INF,
OP_FLOAT_IS_ZERO,
OP_FLOAT_IS_NORMAL,
@ -240,6 +241,7 @@ public:
app * mk_le(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_LE, arg1, arg2); }
app * mk_ge(expr * arg1, expr * arg2) { return m().mk_app(m_fid, OP_FLOAT_GE, arg1, arg2); }
app * mk_is_nan(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NAN, arg1); }
app * mk_is_inf(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_INF, arg1); }
app * mk_is_zero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_ZERO, arg1); }
app * mk_is_normal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NORMAL, arg1); }

11
src/ast/rewriter/float_rewriter.cpp
View file

@ -58,6 +58,7 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
case OP_FLOAT_IS_ZERO: SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
case OP_FLOAT_IS_NZERO: SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
case OP_FLOAT_IS_PZERO: SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
case OP_FLOAT_IS_NAN: SASSERT(num_args == 1); st = mk_is_nan(args[0], result); break;
case OP_FLOAT_IS_INF: SASSERT(num_args == 1); st = mk_is_inf(args[0], result); break;
case OP_FLOAT_IS_NORMAL: SASSERT(num_args == 1); st = mk_is_normal(args[0], result); break;
case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break;
@ -431,6 +432,16 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
return BR_FAILED;
}
br_status float_rewriter::mk_is_nan(expr * arg1, expr_ref & result) {
scoped_mpf v(m_util.fm());
if (m_util.is_value(arg1, v)) {
result = (m_util.fm().is_nan(v)) ? m().mk_true() : m().mk_false();
return BR_DONE;
}
return BR_FAILED;
}
br_status float_rewriter::mk_is_inf(expr * arg1, expr_ref & result) {
scoped_mpf v(m_util.fm());
if (m_util.is_value(arg1, v)) {

1
src/ast/rewriter/float_rewriter.h
View file

@ -66,6 +66,7 @@ public:
br_status mk_is_zero(expr * arg1, expr_ref & result);
br_status mk_is_nzero(expr * arg1, expr_ref & result);
br_status mk_is_pzero(expr * arg1, expr_ref & result);
br_status mk_is_nan(expr * arg1, expr_ref & result);
br_status mk_is_inf(expr * arg1, expr_ref & result);
br_status mk_is_normal(expr * arg1, expr_ref & result);
br_status mk_is_subnormal(expr * arg1, expr_ref & result);

5
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -1621,6 +1621,11 @@ void fpa2bv_converter::mk_is_pzero(func_decl * f, unsigned num, expr * const * a
m_simp.mk_and(a0_is_pos, a0_is_zero, result);
}
void fpa2bv_converter::mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_nan(args[0], result);
}
void fpa2bv_converter::mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_inf(args[0], result);

1
src/tactic/fpa/fpa2bv_converter.h
View file

@ -116,6 +116,7 @@ public:
void mk_is_nzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_pzero(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result);

1
src/tactic/fpa/fpa2bv_rewriter.h
View file

@ -132,6 +132,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
case OP_FLOAT_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NZERO: m_conv.mk_is_nzero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_PZERO: m_conv.mk_is_pzero(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE;
case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE;