mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

New FPA operators added.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-06-07 17:55:29 +01:00
parent e5c720de29
commit 123d3ec3a7
2 changed files with 17 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/float_decl_plugin.cpp
View file

@ -255,7 +255,10 @@ func_decl * float_decl_plugin::mk_unary_rel_decl(decl_kind k, unsigned num_param
case OP_FLOAT_IS_ZERO: name = "isZero"; break;
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_SIGN_MINUS: name = "isSignMinus"; 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;
default:
UNREACHABLE();
break;
@ -415,6 +418,9 @@ 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_INF:
case OP_FLOAT_IS_NORMAL:
case OP_FLOAT_IS_SUBNORMAL:
return mk_unary_rel_decl(k, num_parameters, parameters, arity, domain, range);
case OP_FLOAT_ABS:
case OP_FLOAT_UMINUS:
@ -473,9 +479,12 @@ 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("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));
op_names.push_back(builtin_name("isPZero", OP_FLOAT_IS_PZERO));
op_names.push_back(builtin_name("isNormal", OP_FLOAT_IS_NORMAL));
op_names.push_back(builtin_name("isSubnormal", OP_FLOAT_IS_SUBNORMAL));
op_names.push_back(builtin_name("isSignMinus", OP_FLOAT_IS_SIGN_MINUS));
op_names.push_back(builtin_name("min", OP_FLOAT_MIN));

8
src/ast/float_decl_plugin.h
View file

@ -61,9 +61,12 @@ enum float_op_kind {
OP_FLOAT_GT,
OP_FLOAT_LE,
OP_FLOAT_GE,
OP_FLOAT_IS_INF,
OP_FLOAT_IS_ZERO,
OP_FLOAT_IS_NZERO,
OP_FLOAT_IS_NORMAL,
OP_FLOAT_IS_SUBNORMAL,
OP_FLOAT_IS_PZERO,
OP_FLOAT_IS_NZERO,
OP_FLOAT_IS_SIGN_MINUS,
OP_TO_FLOAT,
@ -237,7 +240,10 @@ 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_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); }
app * mk_is_subnormal(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SUBNORMAL, arg1); }
app * mk_is_nzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_NZERO, arg1); }
app * mk_is_pzero(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_PZERO, arg1); }
app * mk_is_sign_minus(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_IS_SIGN_MINUS, arg1); }