From 123d3ec3a765ff57b449526f49808efef3a9f36b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 17:55:29 +0100 Subject: [PATCH 1/2] 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); } From d7639557d2867e8cade627237fc686ff76e59580 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 7 Jun 2013 18:03:46 +0100 Subject: [PATCH 2/2] FPA: added rewriting and fpa2bv conversion rules for new operations. Signed-off-by: Christoph M. Wintersteiger --- src/ast/rewriter/float_rewriter.cpp | 33 +++++++++++++++++++++++++++++ src/ast/rewriter/float_rewriter.h | 3 +++ src/tactic/fpa/fpa2bv_converter.cpp | 15 +++++++++++++ src/tactic/fpa/fpa2bv_converter.h | 3 +++ src/tactic/fpa/fpa2bv_rewriter.h | 3 +++ 5 files changed, 57 insertions(+) diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index b43f07b65..bfcfbcbfc 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -58,6 +58,9 @@ 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_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; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; } @@ -428,6 +431,36 @@ br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) { 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)) { + result = (m_util.fm().is_inf(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_normal(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_normal(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_is_subnormal(expr * arg1, expr_ref & result) { + scoped_mpf v(m_util.fm()); + if (m_util.is_value(arg1, v)) { + result = (m_util.fm().is_denormal(v)) ? m().mk_true() : m().mk_false(); + return BR_DONE; + } + + return BR_FAILED; +} + br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) { scoped_mpf v(m_util.fm()); if (m_util.is_value(arg1, v)) { diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 7c86a5bc3..6968d96cf 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -66,6 +66,9 @@ 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_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); br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 02aff67c6..d95709813 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1621,6 +1621,21 @@ 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_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_inf(args[0], result); +} + +void fpa2bv_converter::mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_normal(args[0], result); +} + +void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + mk_is_denormal(args[0], result); +} + void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); mk_is_neg(args[0], result); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 2a68342f8..9f9c74c38 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -116,6 +116,9 @@ 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_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); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index d8a141b62..59d068626 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -132,6 +132,9 @@ 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_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; case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;