From de39173f6fe750b1fb6115f5516ebc7208e7c546 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 7 Oct 2015 20:29:36 +0100 Subject: [PATCH] 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 {