From f77608ed884b8233dbba4e434e25845f3a042a9e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 4 Jun 2022 17:53:23 +0100 Subject: [PATCH] Add interpreted versions of unspecified cases of fp.to_ieee_bv and fp.to_real (#6077) --- src/ast/fpa/bv2fpa_converter.cpp | 20 ++++++++++++++++---- src/ast/fpa/fpa2bv_converter.cpp | 19 ++++++++++++++----- src/ast/fpa/fpa2bv_converter.h | 4 +++- src/ast/fpa/fpa2bv_rewriter.cpp | 18 ++++++++++-------- src/ast/fpa_decl_plugin.cpp | 10 ++++++++-- src/ast/fpa_decl_plugin.h | 4 ++++ src/ast/rewriter/fpa_rewriter.cpp | 2 ++ 7 files changed, 57 insertions(+), 20 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 3da45781f90..3611f848ae3 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -312,17 +312,29 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * } } + auto fid = m_fpa_util.get_family_id(); + expr_ref_vector dom(m); + for (unsigned i = 0; i < f->get_arity(); ++i) + dom.push_back(m.mk_var(i, f->get_domain(i))); + if (m_fpa_util.is_to_sbv(f) || m_fpa_util.is_to_ubv(f)) { - auto fid = m_fpa_util.get_family_id(); auto k = m_fpa_util.is_to_sbv(f) ? OP_FPA_TO_SBV_I : OP_FPA_TO_UBV_I; - expr_ref_vector dom(m); - for (unsigned i = 0; i < f->get_arity(); ++i) - dom.push_back(m.mk_var(i, f->get_domain(i))); parameter param = f->get_parameter(0); func_decl_ref to_bv_i(m.mk_func_decl(fid, k, 1, ¶m, dom.size(), dom.data()), m); expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m); result->set_else(else_value); } + else if (m_fpa_util.is_to_real(f)) { + expr_ref_vector dom(m); + func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, NULL, dom.size(), dom.data()), m); + expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m); + result->set_else(else_value); + } + else if (m_fpa_util.is_to_ieee_bv(f)) { + func_decl_ref to_ieee_bv_i(m.mk_func_decl(fid, OP_FPA_TO_IEEE_BV_I, 0, NULL, dom.size(), dom.data()), m); + expr_ref else_value(m.mk_app(to_ieee_bv_i, dom.size(), dom.data()), m); + result->set_else(else_value); + } else if (bv_fi->get_else()) { expr_ref ft_els = rebuild_floats(mc, rng, bv_fi->get_else()); m_th_rw(ft_els); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 0eb784e8c7a..64155d48bd9 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -52,7 +52,6 @@ fpa2bv_converter::~fpa2bv_converter() { void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) { if (is_float(a) && is_float(b)) { - TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl; tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;); @@ -98,12 +97,12 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { expr* c2 = nullptr, *t2 = nullptr, *f2 = nullptr; if (m.is_ite(t, c2, t2, f2)) { mk_ite(c2, t2, f2, result); - mk_ite(c, result, f, result); + mk_ite(c, result, f, result); } else if (m.is_ite(f, c2, t2, f2)) { mk_ite(c2, t2, f2, result); - mk_ite(c, t, result, result); - } + mk_ite(c, t, result, result); + } else if (m_util.is_fp(t) && m_util.is_fp(f)) { expr_ref t_sgn(m), t_sig(m), t_exp(m); expr_ref f_sgn(m), f_sig(m), f_exp(m); @@ -3261,6 +3260,12 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex SASSERT(is_well_sorted(m, result)); } +void fpa2bv_converter::mk_to_ieee_bv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) +{ + func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_IEEE_BV, 0, nullptr, num, args), m); + mk_to_bv(f, num, args, true, result); +} + void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) { TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); @@ -3491,6 +3496,11 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr } } +void fpa2bv_converter::mk_to_real_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + func_decl_ref fu(m.mk_func_decl(f->get_family_id(), OP_FPA_TO_REAL, 0, nullptr, num, args), m); + mk_to_real(f, num, args, result); +} + void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 3); SASSERT(m_bv_util.get_bv_size(args[0]) == 1); @@ -3500,7 +3510,6 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;); } - void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const { expr* e_sgn = nullptr, *e_exp = nullptr, *e_sig = nullptr; VERIFY(m_util.is_fp(e, e_sgn, e_exp, e_sig)); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 471a7c6fccd..d663fda95c0 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -136,6 +136,7 @@ class fpa2bv_converter { void mk_to_fp_unsigned(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); void mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_real_int(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -145,6 +146,7 @@ class fpa2bv_converter { void mk_to_sbv_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } @@ -245,6 +247,6 @@ class fpa2bv_converter_wrapped : public fpa2bv_converter { expr* bv2rm_value(expr* b); expr* bv2fpa_value(sort* s, expr* a, expr* b = nullptr, expr* c = nullptr); - + }; diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 68a5cd784c6..88fde8b673a 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -149,7 +149,9 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_TO_UBV_I: m_conv.mk_to_ubv_i(f, num, args, result); return BR_DONE; case OP_FPA_TO_SBV_I: m_conv.mk_to_sbv_i(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_REAL_I: m_conv.mk_to_real_i(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_TO_IEEE_BV_I: m_conv.mk_to_ieee_bv_i(f, num, args, result); return BR_DONE; case OP_FPA_BVWRAP: case OP_FPA_BV2RM: @@ -290,15 +292,15 @@ expr_ref fpa2bv_rewriter::convert_atom(th_rewriter& rw, expr * e) { expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) { SASSERT(fu().is_rm(e) || fu().is_float(e)); ast_manager& m = m_cfg.m(); - + expr_ref e_conv(m), res(m); proof_ref pr(m); - + (*this)(e, e_conv); - + TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, m) << std::endl; tout << "converted term: " << mk_ismt2_pp(e_conv, m) << std::endl;); - + if (fu().is_rm(e)) { SASSERT(fu().is_bv2rm(e_conv)); expr_ref bv_rm(m); @@ -316,7 +318,7 @@ expr_ref fpa2bv_rewriter::convert_term(th_rewriter& rw, expr * e) { } else UNREACHABLE(); - + return res; } @@ -333,7 +335,7 @@ expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) { ast_manager& m = m_cfg.m(); expr_ref res(m); TRACE("t_fpa", tout << "converting " << mk_ismt2_pp(e, m) << std::endl;); - + if (fu().is_fp(e)) res = e; else if (m.is_bool(e)) @@ -342,10 +344,10 @@ expr_ref fpa2bv_rewriter::convert(th_rewriter& rw, expr * e) { res = convert_term(rw, e); else res = convert_conversion_term(rw, e); - + TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl; tout << mk_ismt2_pp(e, m) << std::endl << " -> " << std::endl << mk_ismt2_pp(res, m) << std::endl;); - + return res; } diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 5062615f27b..78d300ca79c 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -784,12 +784,14 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_TO_SBV_I: return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_REAL: + case OP_FPA_TO_REAL_I: return mk_to_real(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_FP: return mk_to_fp(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_FP_UNSIGNED: return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); case OP_FPA_TO_IEEE_BV: + case OP_FPA_TO_IEEE_BV_I: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); case OP_FPA_BVWRAP: @@ -857,6 +859,7 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("fp.to_ubv_I", OP_FPA_TO_UBV_I)); op_names.push_back(builtin_name("fp.to_sbv_I", OP_FPA_TO_SBV_I)); op_names.push_back(builtin_name("fp.to_real", OP_FPA_TO_REAL)); + op_names.push_back(builtin_name("fp.to_real_I", OP_FPA_TO_REAL_I)); op_names.push_back(builtin_name("to_fp", OP_FPA_TO_FP)); op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED)); @@ -864,6 +867,7 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons /* Extensions */ op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); op_names.push_back(builtin_name("fp.to_ieee_bv", OP_FPA_TO_IEEE_BV)); + op_names.push_back(builtin_name("fp.to_ieee_bv_I", OP_FPA_TO_IEEE_BV_I)); } void fpa_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { @@ -1074,7 +1078,8 @@ bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* cons if (f->get_family_id() != ffid) return false; - if (is_decl_of(f, ffid, OP_FPA_TO_IEEE_BV)) { + if (is_decl_of(f, ffid, OP_FPA_TO_IEEE_BV) || + is_decl_of(f, ffid, OP_FPA_TO_IEEE_BV_I)) { SASSERT(n == 1); expr* x = args[0]; return is_nan(x); @@ -1101,7 +1106,8 @@ bool fpa_util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* cons else return mpqm.is_neg(r) || mpqm.bitsize(r) > bv_sz; } - else if (is_decl_of(f, ffid, OP_FPA_TO_REAL)) { + else if (is_decl_of(f, ffid, OP_FPA_TO_REAL) || + is_decl_of(f, ffid, OP_FPA_TO_REAL_I)) { SASSERT(n == 1); expr* x = args[0]; return is_nan(x) || is_inf(x); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index ef0a1882ce5..0357efa4705 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -83,12 +83,14 @@ enum fpa_op_kind { OP_FPA_TO_UBV, OP_FPA_TO_SBV, OP_FPA_TO_REAL, + OP_FPA_TO_REAL_I, OP_FPA_TO_SBV_I, OP_FPA_TO_UBV_I, /* Extensions */ OP_FPA_TO_IEEE_BV, + OP_FPA_TO_IEEE_BV_I, OP_FPA_BVWRAP, OP_FPA_BV2RM, @@ -353,11 +355,13 @@ class fpa_util { bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BV2RM); } bool is_to_ubv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV); } bool is_to_sbv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV); } + bool is_to_real(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_REAL); } bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; } bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; } bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; } bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; } + bool is_to_real(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_REAL; } bool is_to_ieee_bv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_IEEE_BV; } bool contains_floats(ast * a); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index e135268d690..b7ba20ab78c 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -93,7 +93,9 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_TO_UBV_I: SASSERT(num_args == 2); st = mk_to_ubv(f, args[0], args[1], result); break; case OP_FPA_TO_SBV_I: SASSERT(num_args == 2); st = mk_to_sbv(f, args[0], args[1], result); break; case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; + case OP_FPA_TO_IEEE_BV_I: 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_TO_REAL_I: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break;