diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6c4d2dc1d..4ee6366f0 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -36,10 +36,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m_mpf_manager(m_util.fm()), m_mpz_manager(m_mpf_manager.mpz_manager()), m_hi_fp_unspecified(true), - m_min_pn_zeros(0, m), - m_min_np_zeros(0, m), - m_max_pn_zeros(0, m), - m_max_np_zeros(0, m), m_extra_assertions(m) { m_plugin = static_cast(m.get_plugin(m.mk_family_id("fpa"))); } @@ -1154,22 +1150,22 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) // The hardware interpretation is -0.0. mk_nzero(f, res); else { - if (m_min_pn_zeros == 0) { - m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_min_pn_zeros->get_decl()); - } - - if (m_min_np_zeros == 0) { - m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl()); + std::pair decls(0, 0); + if (!m_specials.find(f, decls)) { + decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_specials.insert(f, decls); + m.inc_ref(f); + m.inc_ref(decls.first); + m.inc_ref(decls.second); } expr_ref pn(m), np(m); - mk_fp(m_min_pn_zeros, + mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(m_min_np_zeros, + mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); @@ -1243,22 +1239,22 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) // The hardware interpretation is +0.0. mk_pzero(f, res); else { - if (m_max_pn_zeros == 0) { - m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl()); - } - - if (m_max_np_zeros == 0) { - m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_max_np_zeros->get_decl()); + std::pair decls(0, 0); + if (!m_specials.find(f, decls)) { + decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_specials.insert(f, decls); + m.inc_ref(f); + m.inc_ref(decls.first); + m.inc_ref(decls.second); } expr_ref pn(m), np(m); - mk_fp(m_max_pn_zeros, + mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(m_max_np_zeros, + mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); @@ -3839,14 +3835,16 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; ); } - void fpa2bv_converter::reset(void) { 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); - m_min_np_zeros = 0; - m_min_pn_zeros = 0; - m_max_np_zeros = 0; - m_max_pn_zeros = 0; + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + m.dec_ref(it->m_key); + m.dec_ref(it->m_value.first); + m.dec_ref(it->m_value.second); + } m_extra_assertions.reset(); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 95f2ca057..65d99d2c8 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -35,8 +35,8 @@ struct func_decl_triple { f_exp = exp; } func_decl * f_sgn; - func_decl * f_sig; - func_decl * f_exp; + func_decl * f_sig; + func_decl * f_exp; }; class fpa2bv_converter { @@ -47,22 +47,20 @@ protected: bv_util m_bv_util; arith_util m_arith_util; mpf_manager & m_mpf_manager; - unsynch_mpz_manager & m_mpz_manager; + unsynch_mpz_manager & m_mpz_manager; fpa_decl_plugin * m_plugin; bool m_hi_fp_unspecified; obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; - obj_hashtable m_decls_to_hide; - app_ref m_min_pn_zeros; - app_ref m_min_np_zeros; - app_ref m_max_pn_zeros; - app_ref m_max_np_zeros; - + obj_map > m_specials; + + friend class fpa2bv_model_converter; + public: - fpa2bv_converter(ast_manager & m); + fpa2bv_converter(ast_manager & m); ~fpa2bv_converter(); fpa_util & fu() { return m_util; } @@ -83,7 +81,7 @@ public: void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const; void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const; - void mk_eq(expr * a, expr * b, expr_ref & result); + void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -98,7 +96,7 @@ public: void mk_ninf(func_decl * f, expr_ref & result); void mk_nan(func_decl * f, expr_ref & result); void mk_nzero(func_decl *f, expr_ref & result); - void mk_pzero(func_decl *f, expr_ref & result); + void mk_pzero(func_decl *f, expr_ref & result); void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -106,7 +104,7 @@ public: void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -125,10 +123,10 @@ public: void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); + void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result); 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); @@ -137,7 +135,7 @@ public: void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_sbv(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(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } @@ -145,7 +143,7 @@ public: void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); - void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); @@ -153,11 +151,6 @@ public: 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_hashtable const & decls_to_hide() const { return m_decls_to_hide; } - void reset(void); void dbg_decouple(const char * prefix, expr_ref & e); @@ -191,7 +184,7 @@ protected: void mk_unbias(expr * e, expr_ref & result); void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize); - void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); + void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); expr_ref mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky); void add_core(unsigned sbits, unsigned ebits, diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index cc3ba81a3..63af356c8 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -439,7 +439,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { 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)) { result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); - return BR_DONE; + return BR_REWRITE1; } else { scoped_mpf r(m_fm); @@ -474,7 +474,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { 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)) { result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); - return BR_DONE; + return BR_REWRITE1; } else { scoped_mpf r(m_fm); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 78c79dd11..90b2827b2 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -45,6 +45,15 @@ void fpa2bv_model_converter::display(std::ostream & out) { unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; } + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + const symbol & n = it->m_key->get_name(); + out << "\n (" << n << " "; + unsigned indent = n.size() + 4; + out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << + mk_ismt2_pp(it->m_value.second, m, indent) << ")"; + } out << ")" << std::endl; } @@ -79,12 +88,16 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator 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(); + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); it++) { - func_decl * k = translator(*it); - res->m_decls_to_hide.insert(k); + func_decl * k = translator(it->m_key); + app * v1 = translator(it->m_value.first); + app * v2 = translator(it->m_value.second); + res->m_specials.insert(k, std::pair(v1, v2)); translator.to().inc_ref(k); + translator.to().inc_ref(v1); + translator.to().inc_ref(v2); } return res; } @@ -217,10 +230,29 @@ 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_specials.begin(); + it != m_specials.end(); + it++) { + func_decl * f = it->m_key; + expr_ref pzero(m), nzero(m); + pzero = fu.mk_pzero(f->get_range()); + nzero = fu.mk_nzero(f->get_range()); + + expr_ref pn(m), np(m); + bv_mdl->eval(it->m_value.first, pn, true); + bv_mdl->eval(it->m_value.second, np, true); + seen.insert(it->m_value.first->get_decl()); + seen.insert(it->m_value.second->get_decl()); + + func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); + expr * pn_args[2] = { pzero, nzero }; + if (pn != np) flt_fi->insert_new_entry(pn_args, (m.is_true(pn) ? nzero : pzero)); + flt_fi->set_else(m.is_true(np) ? nzero : pzero); + + float_mdl->register_decl(f, flt_fi); + TRACE("fpa2bv_mc", tout << "fp.min/fp.max special: " << std::endl << + mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;); + } for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); @@ -362,10 +394,6 @@ 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, - obj_hashtable const & decls_to_hide) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide); +model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) { + return alloc(fpa2bv_model_converter, m, conv); } diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index a864f753a..534fb6e1c 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -27,44 +27,41 @@ 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; + obj_map > m_specials; public: - fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_hashtable const & decls_to_hide) : - m(m) { - for (obj_map::iterator it = const2bv.begin(); - it != const2bv.end(); + fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) { + for (obj_map::iterator it = conv.m_const2bv.begin(); + it != conv.m_const2bv.end(); it++) { m_const2bv.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_map::iterator it = rm_const2bv.begin(); - it != rm_const2bv.end(); + for (obj_map::iterator it = conv.m_rm_const2bv.begin(); + it != conv.m_rm_const2bv.end(); it++) { m_rm_const2bv.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_map::iterator it = uf2bvuf.begin(); - it != uf2bvuf.end(); + for (obj_map::iterator it = conv.m_uf2bvuf.begin(); + it != conv.m_uf2bvuf.end(); it++) { m_uf2bvuf.insert(it->m_key, it->m_value); 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); + for (obj_map >::iterator it = conv.m_specials.begin(); + it != conv.m_specials.end(); + it++) { + m_specials.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + m.inc_ref(it->m_value.first); + m.inc_ref(it->m_value.second); } } @@ -72,7 +69,13 @@ public: 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); + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + m.dec_ref(it->m_key); + m.dec_ref(it->m_value.first); + m.dec_ref(it->m_value.second); + } } virtual void operator()(model_ref & md, unsigned goal_idx) { @@ -92,7 +95,7 @@ public: virtual model_converter * translate(ast_translation & translator); protected: - fpa2bv_model_converter(ast_manager & m) : m(m) { } + fpa2bv_model_converter(ast_manager & m) : m(m){ } void convert(model * bv_mdl, model * float_mdl); expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) const; @@ -102,10 +105,6 @@ protected: }; -model_converter * mk_fpa2bv_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_hashtable const & decls_to_hide); +model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv); #endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 472f6b30c..eb2aeaa0c 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -43,26 +43,26 @@ class fpa2bv_tactic : public tactic { } void updt_params(params_ref const & p) { - m_rw.cfg().updt_params(p); + m_rw.cfg().updt_params(p); } - + void set_cancel(bool f) { m_rw.set_cancel(f); } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); m_proofs_enabled = g->proofs_enabled(); m_produce_models = g->models_enabled(); m_produce_unsat_cores = g->unsat_core_enabled(); - + mc = 0; pc = 0; core = 0; result.reset(); tactic_report report("fpa2bv", *g); - m_rw.reset(); + m_rw.reset(); TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout);); @@ -70,7 +70,7 @@ class fpa2bv_tactic : public tactic { result.push_back(g.get()); return; } - + m_num_steps = 0; expr_ref new_curr(m); proof_ref new_pr(m); @@ -91,7 +91,7 @@ class fpa2bv_tactic : public tactic { const app * a = to_app(new_curr.get()); if (a->get_family_id() == m_conv.fu().get_family_id() && a->get_decl_kind() == OP_FPA_IS_NAN) { - // Inject auxiliary lemmas that fix e to the one and only NaN value, + // Inject auxiliary lemmas that fix e to the one and only NaN value, // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation // has a value to propagate. expr * sgn, *sig, *exp; @@ -104,8 +104,8 @@ 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(), m_conv.decls_to_hide()); + if (g->models_enabled()) + mc = mk_fpa2bv_model_converter(m, m_conv); g->inc_depth(); result.push_back(g.get()); @@ -114,7 +114,7 @@ class fpa2bv_tactic : public tactic { result.back()->assert_expr(m_conv.m_extra_assertions[i].get()); SASSERT(g->is_well_sorted()); - TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); + TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); if (mc) mc->display(tout); tout << std::endl; ); } }; @@ -141,12 +141,12 @@ public: m_imp->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { + virtual void collect_param_descrs(param_descrs & r) { } - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { try { @@ -156,8 +156,8 @@ public: throw tactic_exception(ex.msg()); } } - - virtual void cleanup() { + + virtual void cleanup() { imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { @@ -173,6 +173,6 @@ protected: } }; -tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) { +tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(fpa2bv_tactic, m, p)); }