From 8a026c355f8f8cd7aaad496ef7097b885b7fef3e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 6 Oct 2015 19:45:05 +0100 Subject: [PATCH 1/2] Corrected unspecified behavior of corner cases in fp.min/fp.max. Partially addresses #68. --- src/ast/fpa/fpa2bv_converter.cpp | 81 ++++++++++++++++++++++- src/ast/fpa/fpa2bv_converter.h | 8 ++- src/ast/fpa/fpa2bv_rewriter_params.pyg | 2 +- src/ast/fpa_decl_plugin.cpp | 34 ++++++++++ src/ast/fpa_decl_plugin.h | 8 +++ src/ast/rewriter/fpa_rewriter.cpp | 66 +++++++++--------- src/tactic/fpa/fpa2bv_model_converter.cpp | 33 ++++++++- src/tactic/fpa/fpa2bv_model_converter.h | 14 +++- src/tactic/fpa/fpa2bv_tactic.cpp | 2 +- src/util/mpf.cpp | 18 ++--- 10 files changed, 211 insertions(+), 55 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b96874667..2d6419d69 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1088,16 +1088,55 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref lt(m); mk_float_lt(f, num, args, lt); + expr_ref zz(m); + zz = mk_min_unspecified(f, x, y); + TRACE("fpa2bv", tout << "min = " << mk_ismt2_pp(zz, m) << std::endl;); + result = y; mk_ite(lt, x, result, result); mk_ite(both_zero, y, result, result); - mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0 + mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); SASSERT(is_well_sorted(m, result)); } +expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) { + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + expr_ref res(m); + + // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. + + if (m_hi_fp_unspecified) + // The hardware interpretation is -0.0. + mk_nzero(f, res); + else { + app_ref pn_nondet(m), np_nondet(m); + pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_decls_to_hide.insert(pn_nondet->get_decl()); + m_decls_to_hide.insert(np_nondet->get_decl()); + + expr_ref pn(m), np(m); + mk_fp(pn_nondet, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + pn); + mk_fp(np_nondet, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + np); + expr_ref x_is_pzero(m), x_is_nzero(m); + mk_is_pzero(x, x_is_pzero); + mk_is_nzero(y, x_is_nzero); + mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res); + } + + return res; +} + void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); @@ -1121,17 +1160,55 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref gt(m); mk_float_gt(f, num, args, gt); + + expr_ref zz(m); + zz = mk_max_unspecified(f, x, y); result = y; mk_ite(gt, x, result, result); mk_ite(both_zero, y, result, result); - mk_ite(m.mk_and(both_zero, sgn_diff), pzero, result, result); // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0 + mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); SASSERT(is_well_sorted(m, result)); } +expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) { + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + expr_ref res(m); + + // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0. + + if (m_hi_fp_unspecified) + // The hardware interpretation is +0.0. + mk_pzero(f, res); + else { + app_ref pn_nondet(m), np_nondet(m); + pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_decls_to_hide.insert(pn_nondet->get_decl()); + m_decls_to_hide.insert(np_nondet->get_decl()); + + expr_ref pn(m), np(m); + mk_fp(pn_nondet, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + pn); + mk_fp(np_nondet, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + np); + expr_ref x_is_pzero(m), x_is_nzero(m); + mk_is_pzero(x, x_is_pzero); + mk_is_nzero(y, x_is_nzero); + mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res); + } + + return res; +} + void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index b91ced404..3cc3d092a 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -55,7 +55,8 @@ protected: obj_map m_const2bv; obj_map m_rm_const2bv; - obj_map m_uf2bvuf; + obj_map m_uf2bvuf; + obj_hashtable m_decls_to_hide; public: fpa2bv_converter(ast_manager & m); @@ -136,13 +137,16 @@ public: void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } + expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); + expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); expr_ref mk_to_ubv_unspecified(unsigned width); expr_ref mk_to_sbv_unspecified(unsigned width); expr_ref mk_to_real_unspecified(); obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } - obj_map const & uf2bvuf() const { return m_uf2bvuf; } + obj_map const & uf2bvuf() const { return m_uf2bvuf; } + obj_hashtable const & decls_to_hide() const { return m_decls_to_hide; } void reset(void); diff --git a/src/ast/fpa/fpa2bv_rewriter_params.pyg b/src/ast/fpa/fpa2bv_rewriter_params.pyg index 91304f143..f8b212546 100644 --- a/src/ast/fpa/fpa2bv_rewriter_params.pyg +++ b/src/ast/fpa/fpa2bv_rewriter_params.pyg @@ -1,5 +1,5 @@ def_module_params(module_name='rewriter', class_name='fpa2bv_rewriter_params', export=True, - params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"), + params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.min, fp.max, fp.to_ubv, fp.to_sbv, and fp.to_real"), )) diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index b7d7dc015..e2e0c6f0a 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -689,6 +689,28 @@ func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_par return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * fpa_decl_plugin::mk_internal_min_unspecified( + decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (arity != 0) + m_manager->raise_exception("invalid number of arguments to fp.min_unspecified"); + if (!is_float_sort(range)) + m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + + return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 0, (sort*)0, range, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + +func_decl * fpa_decl_plugin::mk_internal_max_unspecified( + decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (arity != 0) + m_manager->raise_exception("invalid number of arguments to fp.max_unspecified"); + if (!is_float_sort(range)) + m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + + return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 0, (sort*)0, range, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -796,6 +818,10 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BVUNWRAP: return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: + return mk_internal_min_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: + return mk_internal_max_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: @@ -1001,6 +1027,14 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } +app * fpa_util::mk_internal_min_unspecified(unsigned ebits, unsigned sbits) { + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 0, 0, mk_float_sort(ebits, sbits)); +} + +app * fpa_util::mk_internal_max_unspecified(unsigned ebits, unsigned sbits) { + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 0, 0, mk_float_sort(ebits, sbits)); +} + app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 5ee68797e..5fbecd364 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -87,6 +87,8 @@ enum fpa_op_kind { /* Internal use only */ OP_FPA_INTERNAL_BVWRAP, OP_FPA_INTERNAL_BVUNWRAP, + OP_FPA_INTERNAL_MIN_UNSPECIFIED, + OP_FPA_INTERNAL_MAX_UNSPECIFIED, OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED, OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED, @@ -160,6 +162,10 @@ class fpa_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); + func_decl * mk_internal_min_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_internal_max_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -332,6 +338,8 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } + app * mk_internal_min_unspecified(unsigned ebits, unsigned sbits); + app * mk_internal_max_unspecified(unsigned ebits, unsigned sbits); app * mk_internal_to_ubv_unspecified(unsigned width); app * mk_internal_to_sbv_unspecified(unsigned width); app * mk_internal_to_ieee_bv_unspecified(unsigned width); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 9701e448e..c968bec6f 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -93,6 +93,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: + SASSERT(num_args == 0); st = BR_FAILED; break; + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: @@ -422,29 +426,24 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { result = arg2; return BR_DONE; } - if (m_util.is_nan(arg2)) { + else if (m_util.is_nan(arg2)) { result = arg1; return BR_DONE; } - if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { - result = arg2; - return BR_DONE; + + scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { + if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) + return BR_FAILED; // Result could be +zero or -zero. + else { + scoped_mpf r(m_fm); + m_fm.minimum(v1, v2, r); + result = m_util.mk_value(r); + return BR_DONE; + } } - result = m().mk_ite(mk_eq_nan(arg1), - arg2, - m().mk_ite(mk_eq_nan(arg2), - arg1, - // min(-0.0, +0.0) = min(+0.0, -0.0) = +0.0 - m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), - m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))), - m_util.mk_pzero(m().get_sort(arg1)), - m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), - arg2, - m().mk_ite(m_util.mk_lt(arg1, arg2), - arg1, - arg2))))); - return BR_REWRITE_FULL; + return BR_FAILED; } br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { @@ -452,29 +451,24 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { result = arg2; return BR_DONE; } - if (m_util.is_nan(arg2)) { + else if (m_util.is_nan(arg2)) { result = arg1; return BR_DONE; } - if (m_util.is_zero(arg1) && m_util.is_zero(arg2)) { - result = arg2; - return BR_DONE; + + scoped_mpf v1(m_fm), v2(m_fm); + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { + if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) + return BR_FAILED; // Result could be +zero or -zero. + else { + scoped_mpf r(m_fm); + m_fm.maximum(v1, v2, r); + result = m_util.mk_value(r); + return BR_DONE; + } } - result = m().mk_ite(mk_eq_nan(arg1), - arg2, - m().mk_ite(mk_eq_nan(arg2), - arg1, - // max(-0.0, +0.0) = max(+0.0, -0.0) = +0.0 - m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2), - m().mk_not(m().mk_eq(m_util.mk_is_positive(arg1), m_util.mk_is_positive(arg2)))), - m_util.mk_pzero(m().get_sort(arg1)), - m().mk_ite(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), - arg2, - m().mk_ite(m_util.mk_gt(arg1, arg2), - arg1, - arg2))))); - return BR_REWRITE_FULL; + return BR_FAILED; } br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 91f7bd3d4..f9d2eeed4 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -44,7 +44,12 @@ void fpa2bv_model_converter::display(std::ostream & out) { out << "\n (" << n << " "; unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; - } + } + for (obj_hashtable::iterator it = m_decls_to_hide.begin(); + it != m_decls_to_hide.end(); + it++) { + out << "\n to hide: " << mk_ismt2_pp(*it, m); + } out << ")" << std::endl; } @@ -70,6 +75,22 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(k); translator.to().inc_ref(v); } + for (obj_map::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.end(); + it++) { + func_decl * k = translator(it->m_key); + func_decl * v = translator(it->m_value); + res->m_uf2bvuf.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } + for (obj_hashtable::iterator it = m_decls_to_hide.begin(); + it != m_decls_to_hide.end(); + it++) { + func_decl * k = translator(*it); + res->m_decls_to_hide.insert(k); + translator.to().inc_ref(k); + } return res; } @@ -188,6 +209,11 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { obj_hashtable seen; + for (obj_hashtable::iterator it = m_decls_to_hide.begin(); + it != m_decls_to_hide.end(); + it++) + seen.insert(*it); + for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); it++) @@ -329,6 +355,7 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv, - obj_map const & uf2bvuf) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf); + obj_map const & uf2bvuf, + obj_hashtable const & decls_to_hide) { + return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide); } diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 021538ac1..4cce4bfd1 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -27,11 +27,13 @@ class fpa2bv_model_converter : public model_converter { obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; + obj_hashtable m_decls_to_hide; public: fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv, - obj_map const & uf2bvuf) : + obj_map const & uf2bvuf, + obj_hashtable const & decls_to_hide) : m(m) { // Just create a copy? for (obj_map::iterator it = const2bv.begin(); @@ -58,12 +60,19 @@ public: m.inc_ref(it->m_key); m.inc_ref(it->m_value); } + for (obj_hashtable::iterator it = decls_to_hide.begin(); + it != decls_to_hide.end(); + it++) { + m_decls_to_hide.insert(*it); + m.inc_ref(*it); + } } virtual ~fpa2bv_model_converter() { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); + dec_ref_collection_values(m, m_decls_to_hide); } virtual void operator()(model_ref & md, unsigned goal_idx) { @@ -96,6 +105,7 @@ protected: model_converter * mk_fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, obj_map const & rm_const2bv, - obj_map const & uf2bvuf); + obj_map const & uf2bvuf, + obj_hashtable const & m_decls_to_hide); #endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 07669f513..158bb935e 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -107,7 +107,7 @@ class fpa2bv_tactic : public tactic { } if (g->models_enabled()) - mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf()); + mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.decls_to_hide()); g->inc_depth(); result.push_back(g.get()); diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 855668e5a..a186a492d 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1248,12 +1248,13 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) { void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { if (is_nan(x)) set(o, y); - else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) - mk_pzero(x.ebits, x.sbits, o); - else if (is_zero(x) && is_zero(y)) - set(o, y); else if (is_nan(y)) set(o, x); + else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) { + UNREACHABLE(); // max(+0, -0) and max(-0, +0) are unspecified. + } + else if (is_zero(x) && is_zero(y)) + set(o, y); else if (gt(x, y)) set(o, x); else @@ -1263,12 +1264,13 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) { if (is_nan(x)) set(o, y); - else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) - mk_pzero(x.ebits, x.sbits, o); - else if (is_zero(x) && is_zero(y)) - set(o, y); else if (is_nan(y)) set(o, x); + else if (is_zero(x) && is_zero(y) && sgn(x) != sgn(y)) { + UNREACHABLE(); // min(+0, -0) and min(-0, +0) are unspecified. + } + else if (is_zero(x) && is_zero(y)) + set(o, y); else if (lt(x, y)) set(o, x); else From de39173f6fe750b1fb6115f5516ebc7208e7c546 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 7 Oct 2015 20:29:36 +0100 Subject: [PATCH 2/2] Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa. Fixes #68 --- src/ast/fpa/fpa2bv_converter.h | 6 ++-- src/ast/fpa/fpa2bv_rewriter.h | 4 ++- src/ast/fpa_decl_plugin.cpp | 26 ++++++++++------ src/ast/fpa_decl_plugin.h | 4 +-- src/ast/rewriter/fpa_rewriter.cpp | 16 +++++++--- src/smt/theory_fpa.cpp | 51 ++++++++++++++++++++++++++++++- src/smt/theory_fpa.h | 3 ++ 7 files changed, 90 insertions(+), 20 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 3cc3d092a..819216bd0 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -137,8 +137,10 @@ public: void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } - expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); - expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); + + virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); + virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); + expr_ref mk_to_ubv_unspecified(unsigned width); expr_ref mk_to_sbv_unspecified(unsigned width); expr_ref mk_to_real_unspecified(); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 7d0f4d06b..69c9a6290 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -166,8 +166,10 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE; + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE; case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index e2e0c6f0a..ec410fd18 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -692,23 +692,27 @@ func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_par func_decl * fpa_decl_plugin::mk_internal_min_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (arity != 0) + if (arity != 2) m_manager->raise_exception("invalid number of arguments to fp.min_unspecified"); + if (domain[0] != domain[1] || !is_float_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); if (!is_float_sort(range)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); - return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 0, (sort*)0, range, func_decl_info(m_family_id, k, num_parameters, parameters)); + return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } func_decl * fpa_decl_plugin::mk_internal_max_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { - if (arity != 0) + if (arity != 2) m_manager->raise_exception("invalid number of arguments to fp.max_unspecified"); + if (domain[0] != domain[1] || !is_float_sort(domain[0])) + m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); if (!is_float_sort(range)) m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); - return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 0, (sort*)0, range, func_decl_info(m_family_id, k, num_parameters, parameters)); + return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( @@ -1027,12 +1031,16 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_internal_min_unspecified(unsigned ebits, unsigned sbits) { - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 0, 0, mk_float_sort(ebits, sbits)); +app * fpa_util::mk_internal_min_unspecified(expr * x, expr * y) { + SASSERT(m().get_sort(x) == m().get_sort(y)); + expr * args[] = { x, y }; + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x)); } -app * fpa_util::mk_internal_max_unspecified(unsigned ebits, unsigned sbits) { - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 0, 0, mk_float_sort(ebits, sbits)); +app * fpa_util::mk_internal_max_unspecified(expr * x, expr * y) { + SASSERT(m().get_sort(x) == m().get_sort(y)); + expr * args[] = { x, y }; + return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x)); } app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 5fbecd364..50b388047 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -338,8 +338,8 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } - app * mk_internal_min_unspecified(unsigned ebits, unsigned sbits); - app * mk_internal_max_unspecified(unsigned ebits, unsigned sbits); + app * mk_internal_min_unspecified(expr * x, expr * y); + app * mk_internal_max_unspecified(expr * x, expr * y); app * mk_internal_to_ubv_unspecified(unsigned width); app * mk_internal_to_sbv_unspecified(unsigned width); app * mk_internal_to_ieee_bv_unspecified(unsigned width); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index c968bec6f..d336c3a56 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -95,7 +95,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_MIN_UNSPECIFIED: case OP_FPA_INTERNAL_MAX_UNSPECIFIED: - SASSERT(num_args == 0); st = BR_FAILED; break; + SASSERT(num_args == 2); st = BR_FAILED; break; case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: SASSERT(num_args == 0); st = mk_to_ubv_unspecified(f, result); break; @@ -433,8 +433,11 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { - if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) - return BR_FAILED; // Result could be +zero or -zero. + if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { + // Result could be +zero or -zero. + result = m_util.mk_internal_min_unspecified(arg1, arg2); + return BR_DONE; + } else { scoped_mpf r(m_fm); m_fm.minimum(v1, v2, r); @@ -458,8 +461,11 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { scoped_mpf v1(m_fm), v2(m_fm); if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { - if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) - return BR_FAILED; // Result could be +zero or -zero. + if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { + // Result could be +zero or -zero. + result = m_util.mk_internal_max_unspecified(arg1, arg2); + return BR_REWRITE_FULL; + } else { scoped_mpf r(m_fm); m_fm.maximum(v1, v2, r); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 99ed153fc..0fadc62ca 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -82,7 +82,56 @@ namespace smt { } void theory_fpa::fpa2bv_converter_wrapped::mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - fpa2bv_converter::mk_uninterpreted_function(f, num, args, result); + // TODO: This introduces temporary variables/func_decls that should be filtered in the end. + return fpa2bv_converter::mk_uninterpreted_function(f, num, args, result); + } + + expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_min_unspecified(func_decl * f, expr * x, expr * y) { + // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned bv_sz = ebits + sbits; + expr_ref res(m); + + expr * args[] = { x, y }; + func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, f->get_range()); + expr_ref a(m), wrapped(m); + a = m.mk_app(w, x, y); + wrapped = m_th.wrap(a); + m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped), + m_bv_util.mk_extract(sbits - 2, 0, wrapped), + res); + + expr_ref sc(m); + m_th.m_converter.mk_is_zero(res, sc); + m_extra_assertions.push_back(sc); + //m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a)); + return res; + } + + expr_ref theory_fpa::fpa2bv_converter_wrapped::mk_max_unspecified(func_decl * f, expr * x, expr * y) { + // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0. + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + unsigned bv_sz = ebits + sbits; + expr_ref res(m); + + expr * args[] = { x, y }; + func_decl * w = m.mk_func_decl(m_th.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, f->get_range()); + expr_ref a(m), wrapped(m); + a = m.mk_app(w, x, y); + wrapped = m_th.wrap(a); + m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, wrapped), + m_bv_util.mk_extract(bv_sz - 2, sbits - 1, wrapped), + m_bv_util.mk_extract(sbits - 2, 0, wrapped), + res); + + expr_ref sc(m); + m_th.m_converter.mk_is_zero(res, sc); + m_extra_assertions.push_back(sc); + //m_extra_assertions.push_back(m.mk_eq(m_th.unwrap(wrapped, f->get_range()), a)); + return res; } theory_fpa::theory_fpa(ast_manager & m) : diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 68acb79cd..29bc71bde 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -84,6 +84,9 @@ namespace smt { virtual void mk_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result); virtual void mk_uninterpreted_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); + virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); }; class fpa_value_proc : public model_value_proc {