From 123d3ec3a765ff57b449526f49808efef3a9f36b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 17:55:29 +0100 Subject: [PATCH] New FPA operators added. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 11 ++++++++++- src/ast/float_decl_plugin.h | 8 +++++++- 2 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 2a090fc39..21d4d6a86 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -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 & 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)); diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 5c18e1241..fd632a8a1 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -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); }