diff --git a/src/tactic/fpa/fpa2bv_approx_tactic.cpp b/src/tactic/fpa/fpa2bv_approx_tactic.cpp index a348c25e4..77a87ae31 100644 --- a/src/tactic/fpa/fpa2bv_approx_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_approx_tactic.cpp @@ -28,6 +28,8 @@ #include"sat_solver.h" #include"fpa_decl_plugin.h" #include"fpa2bv_converter_prec.h" +#include"fpa2bv_model_converter.h" +#include"fpa2bv_converter.h" #include"fpa2bv_rewriter_prec.h" #include"fpa2bv_approx_tactic.h" #include"const_intro_rewriter.h" @@ -961,7 +963,8 @@ class fpa2bv_approx_tactic: public tactic { TRACE("sat_tactic", model_v2_pp(tout, *md);); model_converter_ref bb_mc = mk_bit_blaster_model_converter(*m_temp_manager, bv2bool.const2bits()); - model_converter_ref bv_mc = mk_fpa2bv_prec_model_converter(*m_temp_manager, fpa2bv.const2bv(), fpa2bv.rm_const2bv()); + + model_converter_ref bv_mc = mk_fpa2bv_model_converter(*m_temp_manager, fpa2bv.const2bv(), fpa2bv.rm_const2bv(), fpa2bv.uf2bvuf(), fpa2bv.uf23bvuf()); bb_mc->operator()(md, 0); bv_mc->operator()(md, 0); diff --git a/src/tactic/fpa/fpa2bv_converter_prec.cpp b/src/tactic/fpa/fpa2bv_converter_prec.cpp index b60a58968..046511199 100644 --- a/src/tactic/fpa/fpa2bv_converter_prec.cpp +++ b/src/tactic/fpa/fpa2bv_converter_prec.cpp @@ -1590,194 +1590,5 @@ void fpa2bv_converter_prec::mk_is_subnormal(func_decl * f, unsigned prec, unsign -void fpa2bv_prec_model_converter::display(std::ostream & out) { - out << "(fpa2bv-model-converter"; - for (obj_map::iterator it = m_const2bv.begin(); - it != m_const2bv.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, m, indent) << ")"; - } - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.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, m, indent) << ")"; - } - out << ")" << std::endl; -} - -model_converter * fpa2bv_prec_model_converter::translate(ast_translation & translator) { - fpa2bv_prec_model_converter * res = alloc(fpa2bv_prec_model_converter, translator.to()); - for (obj_map::iterator it = m_const2bv.begin(); - it != m_const2bv.end(); - it++) - { - func_decl * k = translator(it->m_key); - expr * v = translator(it->m_value); - res->m_const2bv.insert(k, v); - translator.to().inc_ref(k); - translator.to().inc_ref(v); - } - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.end(); - it++) - { - func_decl * k = translator(it->m_key); - expr * v = translator(it->m_value); - res->m_rm_const2bv.insert(k, v); - translator.to().inc_ref(k); - translator.to().inc_ref(v); - } - return res; -} - -void fpa2bv_prec_model_converter::convert(model * bv_mdl, model * float_mdl) { - fpa_util fu(m); - bv_util bu(m); - mpf fp_val,sfp_val; - unsynch_mpz_manager & mpzm = fu.fm().mpz_manager(); - unsynch_mpq_manager & mpqm = fu.fm().mpq_manager(); - - TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl; - for (unsigned i = 0 ; i < bv_mdl->get_num_constants(); i++) - tout << bv_mdl->get_constant(i)->get_name() << " --> " << - mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl; - ); - - obj_hashtable seen; - - for (obj_map::iterator it = m_const2bv.begin(); - it != m_const2bv.end(); - it++) - { - func_decl * var = it->m_key; - app * a = to_app(it->m_value); - SASSERT(fu.is_float(var->get_range())); - SASSERT(var->get_range()->get_num_parameters() == 2); - - unsigned ebits = fu.get_ebits(var->get_range()); - unsigned sbits = fu.get_sbits(var->get_range()); - unsigned sfpa_ebits = fu.get_ebits(a->get_decl()->get_range()); - unsigned sfpa_sbits = fu.get_sbits(a->get_decl()->get_range()); - - expr_ref sgn(m), sig(m), exp(m); - if (a->get_decl_kind() == OP_FPA_TO_FP) - { - bv_mdl->eval(a->get_arg(0), sgn, true); - bv_mdl->eval(a->get_arg(1), sig, true); - bv_mdl->eval(a->get_arg(2), exp, true); - } - else - { - sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl()); - sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); - exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); - } - - seen.insert(to_app(a->get_arg(0))->get_decl()); - seen.insert(to_app(a->get_arg(1))->get_decl()); - seen.insert(to_app(a->get_arg(2))->get_decl()); - - if (!sgn && !sig && !exp) - continue; - - unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0))); - unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1; - unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2))); - - rational sgn_q(0), sig_q(0), exp_q(0); - - if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz); - if (sig) bu.is_numeral(sig, sig_q, sig_sz); - if (exp) bu.is_numeral(exp, exp_q, exp_sz); - - // un-bias exponent - rational exp_unbiased_q; - mpz sig_z; mpf_exp_t exp_z; - - exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(sfpa_ebits-1); - - mpzm.set(sig_z, sig_q.to_mpq().numerator()); - exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); - - TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " << - mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl; ); - - - fu.fm().set(sfp_val, sfpa_ebits, sfpa_sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); - fu.fm().set(fp_val, ebits, sbits,MPF_ROUND_TOWARD_ZERO,sfp_val); - //fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); - /*std::cout<< mk_ismt2_pp(a,m) <<":" << fu.mk_value(fp_val)<register_decl(var, fu.mk_value(fp_val)); - - mpzm.del(sig_z); - fu.fm().del(fp_val); - fu.fm().del(sfp_val); - } - - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.end(); - it++) - { - func_decl * var = it->m_key; - app * a = to_app(it->m_value); - SASSERT(fu.is_rm(var->get_range())); - rational val(0); - unsigned sz = 0; - if (a && bu.is_numeral(a, val, sz)) { - TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; ); - SASSERT(val.is_uint64()); - switch (val.get_uint64()) - { - case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break; - case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break; - case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break; - case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; - case BV_RM_TO_ZERO: - default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); - } - seen.insert(var); - } - } - - fu.fm().del(fp_val); - - // Keep all the non-float constants. - unsigned sz = bv_mdl->get_num_constants(); - for (unsigned i = 0; i < sz; i++) - { - func_decl * c = bv_mdl->get_constant(i); - if (!seen.contains(c)) - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); - } - - // And keep everything else - sz = bv_mdl->get_num_functions(); - for (unsigned i = 0; i < sz; i++) - { - func_decl * c = bv_mdl->get_function(i); - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); - } - - sz = bv_mdl->get_num_uninterpreted_sorts(); - for (unsigned i = 0; i < sz; i++) - { - sort * s = bv_mdl->get_uninterpreted_sort(i); - ptr_vector u = bv_mdl->get_universe(s); - float_mdl->register_usort(s, u.size(), u.c_ptr()); - } -} - -model_converter * mk_fpa2bv_prec_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv) { - return alloc(fpa2bv_prec_model_converter, m, const2bv, rm_const2bv); -} - diff --git a/src/tactic/fpa/fpa2bv_converter_prec.h b/src/tactic/fpa/fpa2bv_converter_prec.h index 330cd271f..24631b1ff 100644 --- a/src/tactic/fpa/fpa2bv_converter_prec.h +++ b/src/tactic/fpa/fpa2bv_converter_prec.h @@ -99,64 +99,5 @@ public: }; -class fpa2bv_prec_model_converter : public model_converter { - ast_manager & m; - obj_map m_const2bv; - obj_map m_rm_const2bv; - -public: - fpa2bv_prec_model_converter(ast_manager & m, obj_map const & const2bv, - obj_map const & rm_const2bv) : - m(m) { - // Just create a copy? - for (obj_map::iterator it = const2bv.begin(); - it != 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(); - it++) - { - m_rm_const2bv.insert(it->m_key, it->m_value); - m.inc_ref(it->m_key); - m.inc_ref(it->m_value); - } - } - - virtual ~fpa2bv_prec_model_converter() { - dec_ref_map_key_values(m, m_const2bv); - dec_ref_map_key_values(m, m_rm_const2bv); - } - - virtual void operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); - model * new_model = alloc(model, m); - obj_hashtable bits; - convert(md.get(), new_model); - md = new_model; - } - - virtual void operator()(model_ref & md) { - operator()(md, 0); - } - - void display(std::ostream & out); - - virtual model_converter * translate(ast_translation & translator); - -protected: - fpa2bv_prec_model_converter(ast_manager & m) : m(m) { } - - void convert(model * bv_mdl, model * float_mdl); -}; - - -model_converter * mk_fpa2bv_prec_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv); #endif