From cdc8e1303ae488c35904f8a43b6cb8ba0e00673b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 16 Mar 2016 16:16:29 +0000 Subject: [PATCH] Bugfix for fp.to_*_unspecified. Fixes #507 --- src/api/api_ast.cpp | 3 +- src/ast/fpa/fpa2bv_converter.cpp | 80 ++++++++++++---- src/ast/fpa/fpa2bv_converter.h | 2 +- src/ast/rewriter/fpa_rewriter.cpp | 37 ++------ src/tactic/fpa/fpa2bv_model_converter.cpp | 110 +++++++++------------- src/tactic/fpa/fpa2bv_model_converter.h | 9 -- 6 files changed, 121 insertions(+), 120 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index e30da1aa1..3e094e082 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1129,7 +1129,7 @@ extern "C" { case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; - + case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS; case Z3_OP_RE_STAR: return Z3_OP_RE_STAR; case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION; @@ -1189,6 +1189,7 @@ extern "C" { case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_UNINTERPRETED; default: UNREACHABLE(); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 20d04ebe6..c958fb67f 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2944,17 +2944,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), m_bv_util.mk_numeral(1, 1)))); - else { - app_ref unspec(m), mask(m); - unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); - mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), - m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), - m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits-2), - m_bv_util.mk_numeral(1, 1)))); - expr * args[2] = { unspec, mask }; - nanv = m_bv_util.mk_bv_or(2, args); - } + else + nanv = mk_to_ieee_bv_unspecified(ebits, sbits); result = m.mk_ite(x_is_nan, nanv, m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s)); @@ -3120,8 +3111,17 @@ expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, else { app_ref unspec(m); unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); - result = unspec; + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); } return result; } @@ -3133,8 +3133,17 @@ expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, else { app_ref unspec(m); unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); - result = unspec; + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); } return result; } @@ -3146,12 +3155,51 @@ expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits else { app_ref unspec(m); unspec = m_util.mk_internal_to_real_unspecified(ebits, sbits); - m_unspecified_ufs.insert_if_not_there(unspec->get_decl()); + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); result = unspec; } return result; } +expr_ref fpa2bv_converter::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) { + expr_ref result(m); + + app_ref unspec(m); + unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + func_decl * unspec_fd = unspec->get_decl(); + func_decl * fd; + if (!m_uf2bvuf.find(unspec_fd, fd)) { + app_ref bvc(m); + bvc = m.mk_fresh_const(0, unspec_fd->get_range()); + fd = bvc->get_decl(); + m_uf2bvuf.insert(unspec_fd, fd); + m.inc_ref(unspec_fd); + m.inc_ref(fd); + } + result = m.mk_const(fd); + + app_ref mask(m), extra(m); + mask = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits), + m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), + m_bv_util.mk_numeral(1, 1)))); + expr * args[2] = { result, mask }; + extra = m.mk_eq(m.mk_app(m_bv_util.get_fid(), OP_BAND, 2, args), mask); + m_extra_assertions.push_back(extra); + + return result; +} + void fpa2bv_converter::mk_rm(expr * bv3, expr_ref & result) { SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); result = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_RM, 0, 0, 1, &bv3, m_util.mk_rm_sort()); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 2414b2110..f69351cb2 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -41,7 +41,6 @@ protected: obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; - obj_hashtable m_unspecified_ufs; obj_map > m_specials; @@ -138,6 +137,7 @@ public: expr_ref mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); expr_ref mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); expr_ref mk_to_real_unspecified(unsigned ebits, unsigned sbits); + expr_ref mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); void reset(void); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index b5d8f6754..83372bcf4 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -102,13 +102,10 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_RM: SASSERT(num_args == 1); st = mk_rm(args[0], result); 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: - SASSERT(num_args == 0); st = mk_to_sbv_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_real_unspecified(f, result); break; case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: - SASSERT(num_args == 0); st = mk_to_ieee_bv_unspecified(f, result); break; + st = BR_FAILED; case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVUNWRAP: @@ -859,27 +856,6 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ return BR_FAILED; } -br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 2); - SASSERT(f->get_parameter(0).is_int()); - SASSERT(f->get_parameter(1).is_int()); - unsigned ebits = f->get_parameter(0).get_int(); - unsigned sbits = f->get_parameter(1).get_int(); - - bv_util bu(m()); - - if (m_hi_fp_unspecified) - // The "hardware interpretation" is 01...10...01. - result = bu.mk_concat(bu.mk_numeral(0, 1), - bu.mk_concat(bu.mk_numeral(-1, ebits), - bu.mk_concat(bu.mk_numeral(0, sbits - 2), - bu.mk_numeral(1, 1)))); - else - result = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); - - return BR_DONE; -} - br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { scoped_mpf v(m_fm); @@ -888,8 +864,15 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu const mpf & x = v.get(); if (m_fm.is_nan(v)) { - result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); - return BR_REWRITE1; + if (m_hi_fp_unspecified) { + result = bu.mk_concat(bu.mk_numeral(0, 1), + bu.mk_concat(bu.mk_numeral(-1, x.get_ebits()), + bu.mk_concat(bu.mk_numeral(0, x.get_sbits() - 2), + bu.mk_numeral(1, 1)))); + } + else + result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + return BR_REWRITE_FULL; } else { scoped_mpz rz(m_fm.mpq_manager()); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 61f6c8549..627e33a7b 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -54,15 +54,6 @@ void fpa2bv_model_converter::display(std::ostream & out) { out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << mk_ismt2_pp(it->m_value.second, m, indent) << ")"; } - for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); - it != m_unspecified_ufs.end(); - it++) - { - const symbol & n = (*it)->get_name(); - unsigned indent = n.size() + 4; - out << n << " "; - } - out << ")" << std::endl; } model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { @@ -107,14 +98,6 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(v1); translator.to().inc_ref(v2); } - for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); - it != m_unspecified_ufs.end(); - it++) - { - func_decl * k = translator(*it); - res->m_unspecified_ufs.insert(k); - translator.to().inc_ref(k); - } return res; } @@ -337,66 +320,61 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { func_decl * f = it->m_key; unsigned arity = f->get_arity(); sort * rng = f->get_range(); - func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); - func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value); - SASSERT(bv_fi->args_are_values()); + if (arity > 0) { + func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); - for (unsigned i = 0; i < bv_fi->num_entries(); i++) { - func_entry const * bv_fe = bv_fi->get_entry(i); - expr * const * bv_args = bv_fe->get_args(); - expr_ref_buffer new_args(m); + func_interp * bv_fi = bv_mdl->get_func_interp(it->m_value); + SASSERT(bv_fi->args_are_values()); - for (unsigned j = 0; j < arity; j++) { - sort * dj = f->get_domain(j); - expr * aj = bv_args[j]; - if (fu.is_float(dj)) - new_args.push_back(convert_bv2fp(bv_mdl, dj, aj)); - else if (fu.is_rm(dj)) { - expr_ref fv(m); - fv = convert_bv2rm(aj); - new_args.push_back(fv); + for (unsigned i = 0; i < bv_fi->num_entries(); i++) { + func_entry const * bv_fe = bv_fi->get_entry(i); + expr * const * bv_args = bv_fe->get_args(); + expr_ref_buffer new_args(m); + + for (unsigned j = 0; j < arity; j++) { + sort * dj = f->get_domain(j); + expr * aj = bv_args[j]; + if (fu.is_float(dj)) + new_args.push_back(convert_bv2fp(bv_mdl, dj, aj)); + else if (fu.is_rm(dj)) { + expr_ref fv(m); + fv = convert_bv2rm(aj); + new_args.push_back(fv); + } + else + new_args.push_back(aj); } - else - new_args.push_back(aj); + + expr_ref ret(m); + ret = bv_fe->get_result(); + if (fu.is_float(rng)) + ret = convert_bv2fp(bv_mdl, rng, ret); + else if (fu.is_rm(rng)) + ret = convert_bv2rm(ret); + + flt_fi->insert_new_entry(new_args.c_ptr(), ret); } - expr_ref ret(m); - ret = bv_fe->get_result(); + expr_ref els(m); + els = bv_fi->get_else(); if (fu.is_float(rng)) - ret = convert_bv2fp(bv_mdl, rng, ret); + els = convert_bv2fp(bv_mdl, rng, els); else if (fu.is_rm(rng)) - ret = convert_bv2rm(ret); + els = convert_bv2rm(els); - flt_fi->insert_new_entry(new_args.c_ptr(), ret); + flt_fi->set_else(els); + + float_mdl->register_decl(f, flt_fi); } - - expr_ref els(m); - els = bv_fi->get_else(); - if (fu.is_float(rng)) - els = convert_bv2fp(bv_mdl, rng, els); - else if (fu.is_rm(rng)) - els = convert_bv2rm(els); - - flt_fi->set_else(els); - - float_mdl->register_decl(f, flt_fi); - } - - // fp.to_*_unspecified UFs. - for (obj_hashtable::iterator it = m_unspecified_ufs.begin(); - it != m_unspecified_ufs.end(); - it++) - { - func_decl * f = *it; - - if (bv_mdl->has_interpretation(f)) { - func_interp * val = bv_mdl->get_func_interp(f)->copy(); - TRACE("fpa2bv_mc", tout << "Keeping interpretation for " << mk_ismt2_pp(f, m) << std::endl;); - float_mdl->register_decl(f, val); + else { + func_decl * bvf = it->m_value; + expr_ref c(m), e(m); + c = m.mk_const(bvf); + bv_mdl->eval(c, e, true); + float_mdl->register_decl(f, e); + TRACE("fpa2bv_mc", tout << "model value for " << mk_ismt2_pp(f, m) << " is " << mk_ismt2_pp(e, m) << std::endl;); } - else - TRACE("fpa2bv_mc", tout << "No interpretation for " << mk_ismt2_pp(f, m) << std::endl;); } // Keep all the non-float constants. diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index 589d3c201..854543f24 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -28,7 +28,6 @@ class fpa2bv_model_converter : public model_converter { obj_map m_rm_const2bv; obj_map m_uf2bvuf; obj_map > m_specials; - obj_hashtable m_unspecified_ufs; public: fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) { @@ -64,13 +63,6 @@ public: m.inc_ref(it->m_value.first); m.inc_ref(it->m_value.second); } - for (obj_hashtable::iterator it = conv.m_unspecified_ufs.begin(); - it != conv.m_unspecified_ufs.end(); - it++) - { - m_unspecified_ufs.insert(*it); - m.inc_ref(*it); - } } virtual ~fpa2bv_model_converter() { @@ -84,7 +76,6 @@ public: m.dec_ref(it->m_value.first); m.dec_ref(it->m_value.second); } - dec_ref_collection_values(m, m_unspecified_ufs); } virtual void operator()(model_ref & md, unsigned goal_idx) {