From 05121e25d45319c22d976bacdfb82502c9a89333 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 28 Dec 2014 19:28:48 +0000 Subject: [PATCH] FPA theory support for conversion functions Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 64 +++++++++++++++++++++++++++++++- src/ast/float_decl_plugin.h | 24 +++++++++--- src/ast/fpa/fpa2bv_converter.cpp | 12 ++++-- src/ast/fpa/fpa2bv_converter.h | 4 ++ src/smt/theory_fpa.cpp | 22 ++++++----- 5 files changed, 107 insertions(+), 19 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index a861865f5..b019c7359 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -655,6 +655,45 @@ func_decl * float_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_p return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * float_decl_plugin::mk_internal_to_ubv_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.to_ubv_unspecified"); + if (num_parameters != 1) + m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 1"); + if (!parameters[0].is_int()) + m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting an integer"); + + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + +func_decl * float_decl_plugin::mk_internal_to_sbv_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 internal_to_sbv_unspecified"); + if (!is_sort_of(domain[0], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismatch, expected argument of bitvector sort"); + if (!is_sort_of(range, m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + + sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, parameters); + return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + +func_decl * float_decl_plugin::mk_internal_to_real_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 internal_to_real_unspecified"); + if (!is_sort_of(range, m_arith_fid, REAL_SORT)) + m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); + + return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -726,6 +765,12 @@ func_decl * float_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_FLOAT_INTERNAL_BVUNWRAP: return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED: + return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED: + return mk_internal_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED: + return mk_internal_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -864,7 +909,8 @@ bool float_decl_plugin::is_unique_value(app* e) const { float_util::float_util(ast_manager & m): m_manager(m), m_fid(m.mk_family_id("float")), - m_a_util(m) { + m_a_util(m), + m_bv_util(m) { m_plugin = static_cast(m.get_plugin(m_fid)); } @@ -916,3 +962,19 @@ app * float_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } +app * float_util::mk_internal_to_ubv_unspecified(unsigned width) { + parameter ps[] = { parameter(width) }; + sort * range = m_bv_util.mk_sort(width); + return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED, 1, ps, 0, 0, range); +} + +app * float_util::mk_internal_to_sbv_unspecified(unsigned width) { + parameter ps[] = { parameter(width) }; + sort * range = m_bv_util.mk_sort(width); + return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED, 1, ps, 0, 0, range); +} + +app * float_util::mk_internal_to_real_unspecified() { + sort * range = m_a_util.mk_real(); + return m().mk_app(get_family_id(), OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED, 0, 0, 0, 0, range); +} \ No newline at end of file diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 01daab8e3..3403665a9 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -47,7 +47,7 @@ enum float_op_kind { OP_FLOAT_NAN, OP_FLOAT_PLUS_ZERO, OP_FLOAT_MINUS_ZERO, - + OP_FLOAT_ADD, OP_FLOAT_SUB, OP_FLOAT_NEG, @@ -70,7 +70,7 @@ enum float_op_kind { OP_FLOAT_IS_INF, OP_FLOAT_IS_ZERO, OP_FLOAT_IS_NORMAL, - OP_FLOAT_IS_SUBNORMAL, + OP_FLOAT_IS_SUBNORMAL, OP_FLOAT_IS_PZERO, OP_FLOAT_IS_NZERO, OP_FLOAT_IS_NEGATIVE, @@ -85,10 +85,13 @@ enum float_op_kind { /* Extensions */ OP_FLOAT_TO_IEEE_BV, - + /* Internal use only */ OP_FLOAT_INTERNAL_BVWRAP, OP_FLOAT_INTERNAL_BVUNWRAP, + OP_FLOAT_INTERNAL_TO_UBV_UNSPECIFIED, + OP_FLOAT_INTERNAL_TO_SBV_UNSPECIFIED, + OP_FLOAT_INTERNAL_TO_REAL_UNSPECIFIED, LAST_FLOAT_OP }; @@ -155,9 +158,15 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); + 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); + 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, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_internal_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); @@ -203,6 +212,7 @@ class float_util { float_decl_plugin * m_plugin; family_id m_fid; arith_util m_a_util; + bv_util m_bv_util; public: float_util(ast_manager & m); ~float_util(); @@ -292,6 +302,10 @@ public: bool is_neg(expr * a) { return is_app_of(a, m_fid, OP_FLOAT_NEG); } app * mk_float_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FLOAT_TO_IEEE_BV, arg1); } + + app * mk_internal_to_ubv_unspecified(unsigned width); + app * mk_internal_to_sbv_unspecified(unsigned width); + app * mk_internal_to_real_unspecified(); }; #endif diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 88e738041..bd8240b31 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2487,10 +2487,13 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg mk_is_neg(x, x_is_neg); mk_is_nzero(x, x_is_nzero); + expr_ref undef(m); + undef = m_util.mk_internal_to_ubv_unspecified(bv_sz); + // NaN, Inf, or negative (except -0) -> undefined expr_ref c1(m), v1(m); c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); - v1 = mk_fresh_const(0, bv_sz); + v1 = undef; dbg_decouple("fpa2bv_to_ubv_c1", c1); // +-Zero -> 0 @@ -2546,9 +2549,10 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg dbg_decouple("fpa2bv_to_ubv_shifted_sig", shifted_sig); expr_ref rounded(m); - rounded = shifted_sig; // TODO. + // TODO: Rounding. + rounded = shifted_sig; - result = m.mk_ite(c_in_limits, rounded, mk_fresh_const(0, bv_sz)); + result = m.mk_ite(c_in_limits, rounded, undef); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); @@ -2658,7 +2662,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); expr_ref undef(m); - undef = m.mk_fresh_const(0, rs); + undef = m_util.mk_internal_to_real_unspecified(); result = m.mk_ite(x_is_zero, zero, res); result = m.mk_ite(x_is_inf, undef, result); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index cd92a6ab2..ee7ffa192 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -149,6 +149,10 @@ public: void mk_internal_bvwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_internal_bvunwrap(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + void mk_internal_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_internal_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_internal_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); protected: void mk_is_nan(expr * e, expr_ref & result); diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index f05bca4a1..b63073893 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -291,7 +291,7 @@ namespace smt { SASSERT(m_bv_util.get_bv_size(res) == 3); ctx.internalize(res, false); } - else { + else if (m_float_util.is_float(e)) { SASSERT(to_app(res)->get_family_id() == get_family_id()); decl_kind k = to_app(res)->get_decl_kind(); if (k == OP_FLOAT_TO_FP) { @@ -314,6 +314,9 @@ namespace smt { SASSERT(is_sort_of(m.get_sort(res), m_bv_util.get_family_id(), BV_SORT)); } } + else { + /* ignore; these are the conversion functions fp.to_* */ + } TRACE("t_fpa_detail", tout << "converted term:" << std::endl; tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << @@ -339,6 +342,8 @@ namespace smt { res = convert_atom(e); else if (m_float_util.is_float(e) || m_float_util.is_rm(e)) res = convert_term(e); + else if (m_arith_util.is_real(e)) + res = convert_term(e); else UNREACHABLE(); @@ -508,12 +513,10 @@ namespace smt { c = m.mk_and(m.mk_eq(x_sgn, y_sgn), m.mk_eq(x_sig, y_sig), - m.mk_eq(x_exp, y_exp)); + m.mk_eq(x_exp, y_exp)); } - else if (fu.is_rm(xe) && fu.is_rm(ye)) - c = m.mk_eq(xc, yc); else - UNREACHABLE(); + c = m.mk_eq(xc, yc); // assert_cnstr(m.mk_iff(m.mk_eq(xe, ye), c)); assert_cnstr(c); @@ -556,12 +559,10 @@ namespace smt { c = m.mk_or(m.mk_not(m.mk_eq(x_sgn, y_sgn)), m.mk_not(m.mk_eq(x_sig, y_sig)), - m.mk_not(m.mk_eq(x_exp, y_exp))); + m.mk_not(m.mk_eq(x_exp, y_exp))); } - else if (m_float_util.is_rm(xe) && m_float_util.is_rm(ye)) - c = m.mk_not(m.mk_eq(xc, yc)); else - UNREACHABLE(); + c = m.mk_not(m.mk_eq(xc, yc)); // assert_cnstr(m.mk_iff(m.mk_not(m.mk_eq(xe, ye)), c)); assert_cnstr(c); @@ -638,6 +639,9 @@ namespace smt { } } } + else { + // These are the conversion functions fp.to_* */ + } } void theory_fpa::reset_eh() {