diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 00b5cdef5..c03d76b5f 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -45,7 +45,7 @@ def init_project_def(): # Simplifier module will be deleted in the future. # It has been replaced with rewriter module. add_lib('simplifier', ['rewriter'], 'ast/simplifier') - add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa') + add_lib('fpa', ['ast', 'util', 'simplifier', 'model'], 'ast/fpa') add_lib('macros', ['simplifier'], 'ast/macros') add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern') add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster') diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp new file mode 100644 index 000000000..fb3af396c --- /dev/null +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -0,0 +1,543 @@ +/*++ + Copyright (c) 2012 Microsoft Corporation + +Module Name: + + bv2fpa_converter.cpp + +Abstract: + + Model conversion for fpa2bv_converter + +Author: + + Christoph (cwinter) 2016-10-15 + +Notes: + +--*/ +#include + +#include"ast_smt2_pp.h" +#include"well_sorted.h" +#include"th_rewriter.h" +#include"fpa_rewriter.h" + +#include"bv2fpa_converter.h" + + +bv2fpa_converter::bv2fpa_converter(ast_manager & m) : + m(m), + m_fpa_util(m), + m_bv_util(m), + m_th_rw(m) { +} + +bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) : + m(m), + m_fpa_util(m), + m_bv_util(m), + m_th_rw(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 = 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 = 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_map >::iterator it = conv.m_min_max_specials.begin(); + it != conv.m_min_max_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); + } +} + +bv2fpa_converter::~bv2fpa_converter() { + 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); + 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); + } +} + +expr_ref bv2fpa_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) { + unsynch_mpz_manager & mpzm = m_fpa_util.fm().mpz_manager(); + unsynch_mpq_manager & mpqm = m_fpa_util.fm().mpq_manager(); + + expr_ref res(m); + mpf fp_val; + + unsigned ebits = m_fpa_util.get_ebits(s); + unsigned sbits = m_fpa_util.get_sbits(s); + + unsigned sgn_sz = 1; + unsigned exp_sz = ebits; + unsigned sig_sz = sbits - 1; + + rational sgn_q(0), sig_q(0), exp_q(0); + + if (sgn) m_bv_util.is_numeral(sgn, sgn_q, sgn_sz); + if (exp) m_bv_util.is_numeral(exp, exp_q, exp_sz); + if (sig) m_bv_util.is_numeral(sig, sig_q, sig_sz); + + // un-bias exponent + rational exp_unbiased_q; + exp_unbiased_q = exp_q - m_fpa_util.fm().m_powers2.m1(ebits - 1); + + mpz sig_z; mpf_exp_t exp_z; + mpzm.set(sig_z, sig_q.to_mpq().numerator()); + exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); + + m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z); + + mpzm.del(sig_z); + + res = m_fpa_util.mk_value(fp_val); + + TRACE("bv2fpa", tout << "[" << mk_ismt2_pp(sgn, m) << + " " << mk_ismt2_pp(exp, m) << + " " << mk_ismt2_pp(sig, m) << "] == " << + mk_ismt2_pp(res, m) << std::endl;); + m_fpa_util.fm().del(fp_val); + + return res; +} + +expr_ref bv2fpa_converter::convert_bv2fp(model_core * mc, sort * s, app * bv) { + SASSERT(m_bv_util.is_bv(bv)); + + unsigned ebits = m_fpa_util.get_ebits(s); + unsigned sbits = m_fpa_util.get_sbits(s); + unsigned bv_sz = sbits + ebits; + + expr_ref bv_num(m); + if (m_bv_util.is_numeral(bv)) + bv_num = bv; + else if (!mc->eval(bv->get_decl(), bv_num)) + bv_num = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(bv)); + + expr_ref sgn(m), exp(m), sig(m); + sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv_num); + exp = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv_num); + sig = m_bv_util.mk_extract(sbits - 2, 0, bv_num); + + expr_ref v_sgn(m), v_exp(m), v_sig(m); + m_th_rw(sgn, v_sgn); + m_th_rw(exp, v_exp); + m_th_rw(sig, v_sig); + + return convert_bv2fp(s, v_sgn, v_exp, v_sig); +} + +expr_ref bv2fpa_converter::convert_bv2rm(expr * bv_rm) { + expr_ref res(m); + rational bv_val(0); + unsigned sz = 0; + + if (m_bv_util.is_numeral(bv_rm, bv_val, sz)) { + SASSERT(bv_val.is_uint64()); + switch (bv_val.get_uint64()) { + case BV_RM_TIES_TO_AWAY: res = m_fpa_util.mk_round_nearest_ties_to_away(); break; + case BV_RM_TIES_TO_EVEN: res = m_fpa_util.mk_round_nearest_ties_to_even(); break; + case BV_RM_TO_NEGATIVE: res = m_fpa_util.mk_round_toward_negative(); break; + case BV_RM_TO_POSITIVE: res = m_fpa_util.mk_round_toward_positive(); break; + case BV_RM_TO_ZERO: + default: res = m_fpa_util.mk_round_toward_zero(); + } + } + + return res; +} + +expr_ref bv2fpa_converter::convert_bv2rm(model_core * mc, app * val) { + expr_ref res(m); + + if (val) { + expr_ref eval_v(m); + if (m_bv_util.is_numeral(val)) + res = convert_bv2rm(val); + else if (mc->eval(val->get_decl(), eval_v)) + res = convert_bv2rm(eval_v); + else + res = m_fpa_util.mk_round_toward_zero(); + } + + return res; +} + +expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * e) { + expr_ref result(m); + TRACE("bv2fpa", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for "; + if (e) tout << mk_ismt2_pp(e, m); + else tout << "nil"; + tout << std::endl; ); + + if (m_fpa_util.is_float(s)) { + if (e == 0) + result = m_fpa_util.mk_pzero(s); + else if (m_fpa_util.is_numeral(e)) + result = e; + else { + SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == (m_fpa_util.get_ebits(s) + m_fpa_util.get_sbits(s))); + result = convert_bv2fp(mc, s, e); + } + } + else if (m_fpa_util.is_rm(s)) { + if (e == 0) + result = m_fpa_util.mk_round_toward_zero(); + else if (m_fpa_util.is_rm_numeral(e)) + result = e; + else { + SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3); + result = convert_bv2rm(mc, e); + } + } + else if (is_app(e)) { + app * a = to_app(e); + expr_ref_vector new_args(m); + for (unsigned i = 0; i < a->get_num_args(); i++) + new_args.push_back(rebuild_floats(mc, a->get_decl()->get_domain()[i], to_app(a->get_arg(i)))); + result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr()); + } + + return result; +} + +bv2fpa_converter::array_model bv2fpa_converter::convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f) { + SASSERT(f->get_arity() == 0); + array_util arr_util(m); + + array_model am(m); + sort_ref_vector array_domain(m); + unsigned arity = f->get_range()->get_num_parameters()-1; + + expr_ref as_arr_mdl(m); + as_arr_mdl = mc->get_const_interp(bv_f); + if (as_arr_mdl == 0) return am; + TRACE("bv2fpa", tout << "arity=0 func_interp for " << mk_ismt2_pp(f, m) << " := " << mk_ismt2_pp(as_arr_mdl, m) << std::endl;); + SASSERT(arr_util.is_as_array(as_arr_mdl)); + for (unsigned i = 0; i < arity; i++) + array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast())); + sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast()); + + bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl)); + + am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng); + am.new_float_fi = convert_func_interp(mc, am.new_float_fd, bv_f); + am.bv_fd = bv_f; + am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd); + return am; +} + +func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f) { + SASSERT(f->get_arity() > 0); + func_interp * result = 0; + sort * rng = f->get_range(); + sort * const * dmn = f->get_domain(); + + unsigned arity = bv_f->get_arity(); + func_interp * bv_fi = mc->get_func_interp(bv_f); + + if (bv_fi != 0) { + fpa_rewriter rw(m); + expr_ref ai(m); + result = alloc(func_interp, m, 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); + + for (unsigned j = 0; j < arity; j++) { + sort * ft_dj = dmn[j]; + expr * bv_aj = bv_args[j]; + ai = rebuild_floats(mc, ft_dj, to_app(bv_aj)); + m_th_rw(ai); + new_args.push_back(ai); + } + + expr_ref bv_fres(m), ft_fres(m); + bv_fres = bv_fe->get_result(); + ft_fres = rebuild_floats(mc, rng, to_app(bv_fres)); + m_th_rw(ft_fres); + result->insert_new_entry(new_args.c_ptr(), ft_fres); + } + + app_ref bv_els(m); + expr_ref ft_els(m); + bv_els = (app*)bv_fi->get_else(); + ft_els = rebuild_floats(mc, rng, bv_els); + m_th_rw(ft_els); + result->set_else(ft_els); + } + + return result; +} + +void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model, obj_hashtable & seen) { + for (obj_map::iterator it = m_const2bv.begin(); + it != m_const2bv.end(); + it++) + { + func_decl * var = it->m_key; + app * val = to_app(it->m_value); + SASSERT(m_fpa_util.is_float(var->get_range())); + SASSERT(var->get_range()->get_num_parameters() == 2); + unsigned ebits = m_fpa_util.get_ebits(var->get_range()); + unsigned sbits = m_fpa_util.get_sbits(var->get_range()); + + app * a0 = to_app(val->get_arg(0)); + app * a1 = to_app(val->get_arg(1)); + app * a2 = to_app(val->get_arg(2)); + + expr_ref v0(m), v1(m), v2(m); + v0 = mc->get_const_interp(a0->get_decl()); + v1 = mc->get_const_interp(a1->get_decl()); + v2 = mc->get_const_interp(a2->get_decl()); + + if (!v0) v0 = m_bv_util.mk_numeral(0, 1); + if (!v1) v1 = m_bv_util.mk_numeral(0, ebits); + if (!v2) v2 = m_bv_util.mk_numeral(0, sbits-1); + + expr_ref sgn(m), exp(m), sig(m); + m_th_rw(v0, sgn); + m_th_rw(v1, exp); + m_th_rw(v2, sig); + + SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP)); + +#ifdef Z3DEBUG + SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0); + SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0); + SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0); + seen.insert(to_app(val->get_arg(0))->get_decl()); + seen.insert(to_app(val->get_arg(1))->get_decl()); + seen.insert(to_app(val->get_arg(2))->get_decl()); +#else + SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT); + SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT); + seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl()); +#endif + + if (!sgn && !sig && !exp) + continue; + + expr_ref cv(m); + cv = convert_bv2fp(var->get_range(), sgn, exp, sig); + target_model->register_decl(var, cv); + + TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;); + } +} + +void bv2fpa_converter::convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable & seen) { + for (obj_map::iterator it = m_rm_const2bv.begin(); + it != m_rm_const2bv.end(); + it++) + { + func_decl * var = it->m_key; + SASSERT(m_fpa_util.is_rm(var->get_range())); + expr * val = it->m_value; + SASSERT(m_fpa_util.is_bv2rm(val)); + expr * bvval = to_app(val)->get_arg(0); + expr_ref fv(m); + fv = convert_bv2rm(mc, to_app(bvval)); + TRACE("bv2fpa", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;); + target_model->register_decl(var, fv); + seen.insert(to_app(bvval)->get_decl()); + } +} + +void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable & seen) { + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + func_decl * f = it->m_key; + app * pn_cnst = it->m_value.first; + app * np_cnst = it->m_value.second; + + expr_ref pzero(m), nzero(m); + pzero = m_fpa_util.mk_pzero(f->get_range()); + nzero = m_fpa_util.mk_nzero(f->get_range()); + + expr_ref pn(m), np(m); + if (!mc->eval(pn_cnst->get_decl(), pn)) pn = pzero; + if (!mc->eval(np_cnst->get_decl(), np)) np = pzero; + seen.insert(pn_cnst->get_decl()); + seen.insert(np_cnst->get_decl()); + + rational pn_num, np_num; + unsigned bv_sz; + m_bv_util.is_numeral(pn, pn_num, bv_sz); + m_bv_util.is_numeral(np, np_num, bv_sz); + + 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, (pn_num.is_one() ? nzero : pzero)); + flt_fi->set_else(np_num.is_one() ? nzero : pzero); + + target_model->register_decl(f, flt_fi); + TRACE("bv2fpa", tout << "fp.min/fp.max special: " << std::endl << + mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;); + } +} + +void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable & seen) { + for (obj_map::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.end(); + it++) { + seen.insert(it->m_value); + + func_decl * f = it->m_key; + if (f->get_arity() == 0) + { + array_util au(m); + if (au.is_array(f->get_range())) { + array_model am = convert_array_func_interp(mc, f, it->m_value); + if (am.new_float_fd) target_model->register_decl(am.new_float_fd, am.new_float_fi); + if (am.result) target_model->register_decl(f, am.result); + if (am.bv_fd) seen.insert(am.bv_fd); + } + else { + // Just keep. + SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range())); + expr_ref var(m), val(m); + if (mc->eval(it->m_value, val)) + target_model->register_decl(f, val); + } + } + else { + func_interp * fmv = convert_func_interp(mc, f, it->m_value); + if (fmv) target_model->register_decl(f, fmv); + } + } +} + +void bv2fpa_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) << ")"; + } + for (obj_map::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.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_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 << ")"; +} + +bv2fpa_converter * bv2fpa_converter::translate(ast_translation & translator) { + bv2fpa_converter * res = alloc(bv2fpa_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); + } + for (obj_map::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.end(); + it++) { + func_decl * k = translator(it->m_key); + func_decl * v = translator(it->m_value); + res->m_uf2bvuf.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + 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; +} + +void bv2fpa_converter::convert(model_core * mc, model_core * float_mdl) { + TRACE("bv2fpa", tout << "BV Model: " << std::endl; + for (unsigned i = 0; i < mc->get_num_constants(); i++) + tout << mc->get_constant(i)->get_name() << " --> " << + mk_ismt2_pp(mc->get_const_interp(mc->get_constant(i)), m) << std::endl; + for (unsigned i = 0; i < mc->get_num_functions(); i++) { + func_decl * f = mc->get_function(i); + tout << f->get_name() << "(...) := " << std::endl; + func_interp * fi = mc->get_func_interp(f); + for (unsigned j = 0; j < fi->num_entries(); j++) { + func_entry const * fe = fi->get_entry(j); + for (unsigned k = 0; k < f->get_arity(); k++) { + tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; + } + tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; + } + tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; + }); + +} \ No newline at end of file diff --git a/src/ast/fpa/bv2fpa_converter.h b/src/ast/fpa/bv2fpa_converter.h new file mode 100644 index 000000000..c441ea6ff --- /dev/null +++ b/src/ast/fpa/bv2fpa_converter.h @@ -0,0 +1,74 @@ +/*++ + Copyright (c) 2016 Microsoft Corporation + +Module Name: + + bv2fpa_converter.h + +Abstract: + + Model conversion for fpa2bv_converter + +Author: + + Christoph (cwinter) 2016-10-15 + +Notes: + +--*/ +#ifndef BV2FPA_CONVERTER_H_ +#define BV2FPA_CONVERTER_H_ + +#include"fpa_decl_plugin.h" +#include"bv_decl_plugin.h" +#include"th_rewriter.h" +#include"model_core.h" +#include"fpa2bv_converter.h" + + +class bv2fpa_converter { + ast_manager & m; + fpa_util m_fpa_util; + bv_util m_bv_util; + th_rewriter m_th_rw; + + obj_map m_const2bv; + obj_map m_rm_const2bv; + obj_map m_uf2bvuf; + obj_map > m_specials; + +public: + bv2fpa_converter(ast_manager & m); + bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv); + virtual ~bv2fpa_converter(); + + void display(std::ostream & out); + bv2fpa_converter * translate(ast_translation & translator); + + expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig); + expr_ref convert_bv2fp(model_core * mc, sort * s, app * bv); + expr_ref convert_bv2rm(expr * eval_v); + expr_ref convert_bv2rm(model_core * mc, app * val); + + void convert(model_core * mc, model_core * float_mdl); + void convert_consts(model_core * mc, model_core * target_model, obj_hashtable & seen); + void convert_rm_consts(model_core * mc, model_core * target_model, obj_hashtable & seen); + void convert_min_max_specials(model_core * mc, model_core * target_model, obj_hashtable & seen); + void convert_uf2bvuf(model_core * mc, model_core * target_model, obj_hashtable & seen); + + func_interp * convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f); + expr_ref rebuild_floats(model_core * mc, sort * s, app * e); + + class array_model { + public: + func_decl * new_float_fd; + func_interp * new_float_fi; + func_decl * bv_fd; + expr_ref result; + array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {} + }; + + array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f); +}; + +#endif \ No newline at end of file diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6bba4663d..05c45c925 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -23,6 +23,7 @@ Notes: #include"th_rewriter.h" #include"fpa2bv_converter.h" +#include"fpa_rewriter.h" #define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); } @@ -32,7 +33,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m_util(m), m_bv_util(m), m_arith_util(m), - m_array_util(m), m_dt_util(m), m_seq_util(m), m_mpf_manager(m_util.fm()), @@ -165,7 +165,6 @@ void fpa2bv_converter::mk_numeral(sort * s, mpf const & v, expr_ref & result) { result = m_util.mk_fp(bv_sgn, biased_exp, bv_sig); TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is " << mk_ismt2_pp(result, m) << std::endl;); - } } @@ -2772,6 +2771,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar expr_ref unspec(m); unspec = mk_to_real_unspecified(ebits, sbits); + result = m.mk_ite(x_is_zero, zero, res); result = m.mk_ite(x_is_inf, unspec, result); result = m.mk_ite(x_is_nan, unspec, result); @@ -3073,50 +3073,95 @@ 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 - nanv = mk_to_ieee_bv_unspecified(ebits, sbits); + else { + app_ref unspec(m); + unspec = m_util.mk_internal_to_ieee_bv_unspecified(ebits, sbits); + mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv); + } expr_ref sgn_e_s(m); sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result); + TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); + SASSERT(is_well_sorted(m, result)); +} + +void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 0); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + + if (m_hi_fp_unspecified) { + result = m_bv_util.mk_concat(m_bv_util.mk_concat( + m_bv_util.mk_numeral(0, 1), + m_bv_util.mk_numeral(-1, ebits)), + m_bv_util.mk_numeral(1, sbits-1)); + } + else { + func_decl * fd; + if (m_uf2bvuf.find(f, fd)) + result = m.mk_const(fd); + else { + fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); + m_uf2bvuf.insert(f, fd); + m.inc_ref(f); + m.inc_ref(fd); + result = m.mk_const(fd); + + expr_ref exp_bv(m), exp_all_ones(m); + exp_bv = m_bv_util.mk_extract(ebits+sbits-2, sbits-1, result); + exp_all_ones = m.mk_eq(exp_bv, m_bv_util.mk_numeral(-1, ebits)); + m_extra_assertions.push_back(exp_all_ones); + + expr_ref sig_bv(m), sig_is_non_zero(m); + sig_bv = m_bv_util.mk_extract(sbits-2, 0, result); + sig_is_non_zero = m.mk_not(m.mk_eq(sig_bv, m_bv_util.mk_numeral(0, sbits-1))); + m_extra_assertions.push_back(sig_is_non_zero); + } + } + + TRACE("fpa2bv_to_ieee_bv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); SASSERT(is_well_sorted(m, 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;); + TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); - SASSERT(num == 2); - SASSERT(m_util.is_bv2rm(args[0])); - SASSERT(m_util.is_float(args[1])); + SASSERT(num == 2); + SASSERT(m_util.is_bv2rm(args[0])); + SASSERT(m_util.is_float(args[1])); - expr * rm = to_app(args[0])->get_arg(0); - expr * x = args[1]; - sort * xs = m.get_sort(x); - sort * bv_srt = f->get_range(); + expr * rm = to_app(args[0])->get_arg(0); + expr * x = args[1]; + sort * xs = m.get_sort(x); + sort * bv_srt = f->get_range(); - unsigned ebits = m_util.get_ebits(xs); - unsigned sbits = m_util.get_sbits(xs); - unsigned bv_sz = (unsigned)f->get_parameter(0).get_int(); + unsigned ebits = m_util.get_ebits(xs); + unsigned sbits = m_util.get_sbits(xs); + unsigned bv_sz = (unsigned)f->get_parameter(0).get_int(); - expr_ref bv0(m), bv1(m); - bv1 = m_bv_util.mk_numeral(1, 1); + expr_ref bv0(m), bv1(m); + bv1 = m_bv_util.mk_numeral(1, 1); - expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m); - mk_is_nan(x, x_is_nan); - mk_is_inf(x, x_is_inf); - mk_is_zero(x, x_is_zero); - mk_is_neg(x, x_is_neg); - mk_is_nzero(x, x_is_nzero); + expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m), x_is_neg(m), x_is_nzero(m); + mk_is_nan(x, x_is_nan); + mk_is_inf(x, x_is_inf); + mk_is_zero(x, x_is_zero); + mk_is_neg(x, x_is_neg); + mk_is_nzero(x, x_is_nzero); - // NaN, Inf, or negative (except -0) -> unspecified - expr_ref c1(m), v1(m); - if (!is_signed) - c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); - else - c1 = m.mk_or(x_is_nan, x_is_inf); - v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz); + // NaN, Inf, or negative (except -0) -> unspecified + expr_ref c1(m), v1(m); + if (!is_signed) { + c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); + v1 = mk_to_ubv_unspecified(ebits, sbits, bv_sz); + } + else { + c1 = m.mk_or(x_is_nan, x_is_inf); + v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz); + } dbg_decouple("fpa2bv_to_bv_c1", c1); // +-Zero -> 0 @@ -3226,7 +3271,8 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_rnd", rnd); expr_ref unspec(m); - unspec = mk_to_ubv_unspecified(ebits, sbits, bv_sz); + unspec = is_signed ? mk_to_sbv_unspecified(ebits, sbits, bv_sz) : + mk_to_ubv_unspecified(ebits, sbits, bv_sz); result = m.mk_ite(rnd_has_overflown, unspec, rnd); result = m.mk_ite(c_in_limits, result, unspec); result = m.mk_ite(c2, v2, result); @@ -3247,101 +3293,89 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg mk_to_bv(f, num, args, true, result); } +void fpa2bv_converter::mk_to_ubv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 0); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + unsigned width = m_bv_util.get_bv_size(f->get_range()); + + if (m_hi_fp_unspecified) + result = m_bv_util.mk_numeral(0, width); + else { + func_decl * fd; + if (!m_uf2bvuf.find(f, fd)) { + fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); + m_uf2bvuf.insert(f, fd); + m.inc_ref(f); + m.inc_ref(fd); + } + result = m.mk_const(fd); + } + + TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); + SASSERT(is_well_sorted(m, result)); +} + expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { - expr_ref result(m); - if (m_hi_fp_unspecified) - result = m_bv_util.mk_numeral(0, width); - else { - app_ref unspec(m); - unspec = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); - 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; + expr_ref res(m); + app_ref u(m); + u = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); + mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); + return res; +} + +void fpa2bv_converter::mk_to_sbv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 0); + unsigned ebits = f->get_parameter(0).get_int(); + unsigned sbits = f->get_parameter(1).get_int(); + unsigned width = m_bv_util.get_bv_size(f->get_range()); + + if (m_hi_fp_unspecified) + result = m_bv_util.mk_numeral(0, width); + else { + func_decl * fd; + if (!m_uf2bvuf.find(f, fd)) { + fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); + m_uf2bvuf.insert(f, fd); + m.inc_ref(f); + m.inc_ref(fd); + } + result = m.mk_const(fd); + } + + TRACE("fpa2bv_to_sbv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); + SASSERT(is_well_sorted(m, result)); } expr_ref fpa2bv_converter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { - expr_ref result(m); - if (m_hi_fp_unspecified) - result = m_bv_util.mk_numeral(0, width); - else { - app_ref unspec(m); - unspec = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); - 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; + expr_ref res(m); + app_ref u(m); + u = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); + mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); + return res; } -expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { - expr_ref result(m); +void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { if (m_hi_fp_unspecified) result = m_arith_util.mk_numeral(rational(0), false); else { - app_ref unspec(m); - unspec = m_util.mk_internal_to_real_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); + if (!m_uf2bvuf.find(f, fd)) { + fd = m.mk_fresh_func_decl(0, 0, 0, f->get_range()); + m_uf2bvuf.insert(f, fd); + m.inc_ref(f); 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), result_and_mask(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 }; - result_and_mask = m.mk_app(m_bv_util.get_fid(), OP_BAND, 2, args); - extra = m.mk_eq(result_and_mask, mask); - m_extra_assertions.push_back(extra); - - return result; +expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { + expr_ref res(m); + app_ref u(m); + u = m_util.mk_internal_to_real_unspecified(ebits, sbits); + mk_to_real_unspecified(u->get_decl(), 0, 0, res); + return res; } void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 3f5e76c66..247cfcacb 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -43,7 +43,6 @@ protected: fpa_util m_util; bv_util m_bv_util; arith_util m_arith_util; - array_util m_array_util; datatype_util m_dt_util; seq_util m_seq_util; mpf_manager & m_mpf_manager; @@ -57,6 +56,7 @@ protected: special_t m_min_max_specials; friend class fpa2bv_model_converter; + friend class bv2fpa_converter; public: fpa2bv_converter(ast_manager & m); @@ -71,9 +71,9 @@ public: bool is_rm(expr * e) { return is_app(e) && m_util.is_rm(e); } bool is_rm(sort * s) { return m_util.is_rm(s); } bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); } - + void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - + 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; @@ -133,12 +133,16 @@ public: 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); + void mk_to_ieee_bv_unspecified(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); void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv_unspecified(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_sbv_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_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } @@ -149,16 +153,11 @@ public: 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); - 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); void dbg_decouple(const char * prefix, expr_ref & e); expr_ref_vector m_extra_assertions; - + special_t const & get_min_max_specials() const { return m_min_max_specials; }; const2bv_t const & get_const2bv() const { return m_const2bv; }; const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; }; @@ -227,6 +226,10 @@ private: void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result); void mk_to_fp_float(sort * s, expr * rm, expr * x, expr_ref & result); + + 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); }; #endif diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 5f89e12db..725c0b043 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -143,9 +143,13 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(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_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(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_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE; case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; @@ -157,12 +161,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BV2RM: - - case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: return BR_FAILED; + default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 6c8b7ac6f..d8bf70e80 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -665,14 +665,14 @@ func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, pa func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (arity != 1) - m_manager->raise_exception("invalid number of arguments to to_ieee_bv"); + m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv"); if (!is_float_sort(domain[0])) m_manager->raise_exception("sort mismatch, expected argument of FloatingPoint sort"); unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int(); parameter ps[] = { parameter(float_sz) }; sort * bv_srt = m_bv_plugin->mk_sort(BV_SORT, 1, ps); - symbol name("to_ieee_bv"); + symbol name("fp.to_ieee_bv"); return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k)); } @@ -758,15 +758,15 @@ func_decl * fpa_decl_plugin::mk_internal_to_ieee_bv_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 to_ieee_bv_unspecified; expecting none"); + m_manager->raise_exception("invalid number of arguments to fp.to_ieee_bv_unspecified; expecting none"); if (num_parameters != 2) - m_manager->raise_exception("invalid number of parameters to to_ieee_bv_unspecified; expecting 2"); + m_manager->raise_exception("invalid number of parameters to fp.to_ieee_bv_unspecified; expecting 2"); if (!parameters[0].is_int() || !parameters[1].is_int()) - m_manager->raise_exception("invalid parameters type provided to to_ieee_bv_unspecified; expecting 2 integers"); + m_manager->raise_exception("invalid parameters type provided to fp.to_ieee_bv_unspecified; expecting 2 integers"); parameter width_p[1] = { parameter(parameters[0].get_int() + parameters[1].get_int()) }; sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, width_p); - return m_manager->mk_func_decl(symbol("to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); + return m_manager->mk_func_decl(symbol("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } @@ -915,7 +915,8 @@ void fpa_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("to_fp_unsigned", OP_FPA_TO_FP_UNSIGNED)); /* Extensions */ - op_names.push_back(builtin_name("to_ieee_bv", OP_FPA_TO_IEEE_BV)); + 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)); } void fpa_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index ee7325014..c00bed7ae 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -259,7 +259,7 @@ public: bool is_rm(sort * s) const { return is_sort_of(s, m_fid, ROUNDING_MODE_SORT); } bool is_float(expr * e) const { return is_float(m_manager.get_sort(e)); } bool is_rm(expr * e) const { return is_rm(m_manager.get_sort(e)); } - bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); } + bool is_fp(expr * e) const { return is_app_of(e, m_fid, OP_FPA_FP); } unsigned get_ebits(sort * s) const; unsigned get_sbits(sort * s) const; @@ -294,13 +294,13 @@ public: bool is_pzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_pzero(v); } bool is_nzero(expr * n) { scoped_mpf v(fm()); return is_numeral(n, v) && fm().is_nzero(v); } - app * mk_fp(expr * sgn, expr * exp, expr * sig) { + app * mk_fp(expr * sgn, expr * exp, expr * sig) { SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.is_bv(exp)); - SASSERT(m_bv_util.is_bv(sig)); - return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); + SASSERT(m_bv_util.is_bv(sig)); + return m().mk_app(m_fid, OP_FPA_FP, sgn, exp, sig); } - + app * mk_to_fp(sort * s, expr * bv_t) { SASSERT(is_float(s) && s->get_num_parameters() == 2); return m().mk_app(m_fid, OP_FPA_TO_FP, 2, s->get_parameters(), 1, &bv_t); @@ -377,28 +377,28 @@ public: app * mk_internal_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); app * mk_internal_to_real_unspecified(unsigned ebits, unsigned sbits); - bool is_bvwrap(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } - bool is_bvwrap(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; } - bool is_bv2rm(expr * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); } - bool is_bv2rm(func_decl * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; } + bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BVWRAP); } + bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BVWRAP; } + bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_BV2RM); } + bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_BV2RM; } - bool is_min_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); } - bool is_min_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); } - bool is_max_interpreted(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); } - bool is_max_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); } - bool is_to_ubv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); } - bool is_to_sbv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); } - bool is_to_ieee_bv_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); } - bool is_to_real_unspecified(expr * e) { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); } + bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_I); } + bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED); } + bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_I); } + bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED); } + bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED); } + bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED); } + bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED); } + bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED); } - bool is_min_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; } - bool is_min_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; } - bool is_max_interpreted(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; } - bool is_max_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; } - bool is_to_ubv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; } - bool is_to_sbv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; } - bool is_to_ieee_bv_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; } - bool is_to_real_unspecified(func_decl * f) { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; } + bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_I; } + bool is_min_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MIN_UNSPECIFIED; } + bool is_max_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_I; } + bool is_max_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_MAX_UNSPECIFIED; } + bool is_to_ubv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED; } + bool is_to_sbv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED; } + bool is_to_ieee_bv_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED; } + bool is_to_real_unspecified(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED; } bool contains_floats(ast * a); }; diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index b8d9c232f..26487c5a4 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -18,11 +18,12 @@ Notes: --*/ #include"fpa_rewriter.h" #include"fpa_rewriter_params.hpp" +#include"ast_smt2_pp.h" fpa_rewriter::fpa_rewriter(ast_manager & m, params_ref const & p) : m_util(m), m_fm(m_util.fm()), - m_hi_fp_unspecified(true) { + m_hi_fp_unspecified(false) { updt_params(p); } @@ -98,7 +99,7 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_INTERNAL_MIN_UNSPECIFIED: case OP_FPA_INTERNAL_MAX_UNSPECIFIED: SASSERT(num_args == 2); st = BR_FAILED; break; - + case OP_FPA_INTERNAL_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; case OP_FPA_INTERNAL_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break; @@ -117,34 +118,40 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con br_status fpa_rewriter::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { bv_util bu(m()); - if (m_hi_fp_unspecified) + if (m_hi_fp_unspecified) { // The "hardware interpretation" is 0. result = bu.mk_numeral(0, width); - else + return BR_DONE; + } + else { result = m_util.mk_internal_to_ubv_unspecified(ebits, sbits, width); - - return BR_DONE; + return BR_REWRITE1; + } } br_status fpa_rewriter::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width, expr_ref & result) { bv_util bu(m()); - if (m_hi_fp_unspecified) + if (m_hi_fp_unspecified) { // The "hardware interpretation" is 0. result = bu.mk_numeral(0, width); - else + return BR_DONE; + } + else { result = m_util.mk_internal_to_sbv_unspecified(ebits, sbits, width); - - return BR_DONE; + return BR_REWRITE1; + } } br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) { - if (m_hi_fp_unspecified) + if (m_hi_fp_unspecified) { // The "hardware interpretation" is 0. result = m_util.au().mk_numeral(rational(0), false); - else + return BR_DONE; + } + else { result = m_util.mk_internal_to_real_unspecified(ebits, sbits); - - return BR_DONE; + return BR_REWRITE1; + } } br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { @@ -776,10 +783,8 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ m_util.is_numeral(arg2, v)) { const mpf & x = v.get(); - if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) { - mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); - return BR_REWRITE_FULL; - } + if (m_fm.is_nan(v) || m_fm.is_inf(v) || m_fm.is_neg(v)) + return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -789,11 +794,13 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ rational ul, ll; ul = m_fm.m_powers2.m1(bv_sz); ll = rational(0); - if (r >= ll && r <= ul) + if (r >= ll && r <= ul) { result = bu.mk_numeral(r, bv_sz); + return BR_DONE; + } else - mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); - return BR_DONE; + return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); + } return BR_FAILED; @@ -810,10 +817,8 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ m_util.is_numeral(arg2, v)) { const mpf & x = v.get(); - if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); - return BR_REWRITE_FULL; - } + if (m_fm.is_nan(v) || m_fm.is_inf(v)) + return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -823,46 +828,42 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ rational ul, ll; ul = m_fm.m_powers2.m1(bv_sz - 1); ll = - m_fm.m_powers2(bv_sz - 1); - if (r >= ll && r <= ul) + if (r >= ll && r <= ul) { result = bu.mk_numeral(r, bv_sz); + return BR_DONE; + } else - mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); - return BR_DONE; + return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); } return BR_FAILED; } br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & result) { + TRACE("fp_rewriter", tout << "to_ieee_bv of " << mk_ismt2_pp(arg, m()) << std::endl;); scoped_mpf v(m_fm); if (m_util.is_numeral(arg, v)) { + TRACE("fp_rewriter", tout << "to_ieee_bv numeral: " << m_fm.to_string(v) << std::endl;); bv_util bu(m()); const mpf & x = v.get(); if (m_fm.is_nan(v)) { 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)))); + expr * args[4] = { bu.mk_numeral(0, 1), + bu.mk_numeral(-1, x.get_ebits()), + bu.mk_numeral(0, x.get_sbits() - 2), + bu.mk_numeral(1, 1) }; + result = bu.mk_concat(4, args); } - else { - app_ref unspec(m()), mask(m()), extra(m()); - unspec = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); - mask = 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)))); - expr * args[2] = { unspec, mask }; - result = m().mk_app(bu.get_fid(), OP_BOR, 2, args); - } - return BR_REWRITE_FULL; + else + result = m_util.mk_internal_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + + return BR_REWRITE1; } else { scoped_mpz rz(m_fm.mpq_manager()); m_fm.to_ieee_bv_mpz(v, rz); - result = bu.mk_numeral(rational(rz), x.get_ebits() + x.get_sbits()); return BR_DONE; } diff --git a/src/ast/rewriter/fpa_rewriter_params.pyg b/src/ast/rewriter/fpa_rewriter_params.pyg index 85973e744..f0cfbdf55 100644 --- a/src/ast/rewriter/fpa_rewriter_params.pyg +++ b/src/ast/rewriter/fpa_rewriter_params.pyg @@ -1,5 +1,5 @@ def_module_params(module_name='rewriter', class_name='fpa_rewriter_params', export=True, - params=(("hi_fp_unspecified", BOOL, True, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, and fp.to_real"), + params=(("hi_fp_unspecified", BOOL, False, "use the 'hardware interpretation' for unspecified values in fp.to_ubv, fp.to_sbv, fp.to_real, and fp.to_ieee_bv"), )) diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 3c10f8704..bef2e6494 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -87,3 +87,19 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { } } +void model_core::unregister_decl(func_decl * d) { + decl2expr::obj_map_entry * ec = m_interp.find_core(d); + if (ec && ec->get_data().m_value != 0) { + m_manager.dec_ref(ec->get_data().m_key); + m_manager.dec_ref(ec->get_data().m_value); + m_interp.remove(d); + return; + } + + decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); + if (ef && ef->get_data().m_value != 0) { + m_manager.dec_ref(ef->get_data().m_key); + dealloc(ef->get_data().m_value); + m_finterp.remove(d); + } +} \ No newline at end of file diff --git a/src/model/model_core.h b/src/model/model_core.h index 8527a0bca..371106b05 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -60,6 +60,7 @@ public: void register_decl(func_decl * d, expr * v); void register_decl(func_decl * f, func_interp * fi); + void unregister_decl(func_decl * d); virtual expr * get_some_value(sort * s) = 0; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index ee7559500..248d5b84d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -21,6 +21,7 @@ Revision History: #include"theory_fpa.h" #include"theory_bv.h" #include"smt_model_generator.h" +#include"bv2fpa_converter.h" namespace smt { @@ -83,15 +84,15 @@ namespace smt { } } - theory_fpa::theory_fpa(ast_manager & m) : - theory(m.mk_family_id("fpa")), - m_converter(m, this), - m_rw(m, m_converter, params_ref()), - m_th_rw(m), - m_trail_stack(*this), - m_fpa_util(m_converter.fu()), - m_bv_util(m_converter.bu()), - m_arith_util(m_converter.au()), + theory_fpa::theory_fpa(ast_manager & m) : + theory(m.mk_family_id("fpa")), + m_converter(m, this), + m_rw(m, m_converter, params_ref()), + m_th_rw(m), + m_trail_stack(*this), + m_fpa_util(m_converter.fu()), + m_bv_util(m_converter.bu()), + m_arith_util(m_converter.au()), m_is_initialized(false) { params_ref p; @@ -116,15 +117,15 @@ namespace smt { SASSERT(m_trail_stack.get_num_scopes() == 0); SASSERT(m_conversions.empty()); - SASSERT(m_is_added_to_model.empty()); - } + SASSERT(m_is_added_to_model.empty()); + } void theory_fpa::init(context * ctx) { smt::theory::init(ctx); m_is_initialized = true; } app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector & values) { - TRACE("t_fpa_detail", + TRACE("t_fpa_detail", ast_manager & m = m_th.get_manager(); for (unsigned i = 0; i < values.size(); i++) tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); @@ -201,7 +202,7 @@ namespace smt { app * theory_fpa::fpa_rm_value_proc::mk_value(model_generator & mg, ptr_vector & values) { SASSERT(values.size() == 1); - TRACE("t_fpa_detail", + TRACE("t_fpa_detail", ast_manager & m = m_th.get_manager(); for (unsigned i = 0; i < values.size(); i++) tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;); @@ -235,12 +236,12 @@ namespace smt { app_ref res(m); if (m_fpa_util.is_fp(e)) { - expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; + expr * cargs[3] = { to_app(e)->get_arg(0), to_app(e)->get_arg(1), to_app(e)->get_arg(2) }; res = m_bv_util.mk_concat(3, cargs); m_th_rw((expr_ref&)res); } else { - sort * es = m.get_sort(e); + sort * es = m.get_sort(e); sort_ref bv_srt(m); if (m_converter.is_rm(es)) @@ -264,7 +265,7 @@ namespace smt { SASSERT(!m_fpa_util.is_fp(e)); SASSERT(m_bv_util.is_bv(e)); SASSERT(m_fpa_util.is_float(s) || m_fpa_util.is_rm(s)); - ast_manager & m = get_manager(); + ast_manager & m = get_manager(); app_ref res(m); unsigned bv_sz = m_bv_util.get_bv_size(e); @@ -285,7 +286,7 @@ namespace smt { m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e), m_bv_util.mk_extract(sbits - 2, 0, e)); } - + return res; } @@ -312,7 +313,7 @@ namespace smt { TRACE("t_fpa_detail", tout << "term: " << mk_ismt2_pp(e, get_manager()) << std::endl; tout << "converted term: " << mk_ismt2_pp(e_conv, get_manager()) << std::endl;); - if (m_fpa_util.is_rm(e)) { + if (m_fpa_util.is_rm(e)) { SASSERT(m_fpa_util.is_bv2rm(e_conv)); expr_ref bv_rm(m); m_th_rw(to_app(e_conv)->get_arg(0), bv_rm); @@ -329,7 +330,7 @@ namespace smt { } else UNREACHABLE(); - + return res; } @@ -362,7 +363,7 @@ namespace smt { res = convert_atom(e); else if (m_fpa_util.is_float(e) || m_fpa_util.is_rm(e)) res = convert_term(e); - else + else res = convert_conversion_term(e); TRACE("t_fpa_detail", tout << "converted; caching:" << std::endl; @@ -448,7 +449,7 @@ namespace smt { TRACE("t_fpa_internalize", tout << "internalizing term: " << mk_ismt2_pp(term, get_manager()) << "\n";); SASSERT(term->get_family_id() == get_family_id()); SASSERT(!get_context().e_internalized(term)); - + ast_manager & m = get_manager(); context & ctx = get_context(); @@ -494,7 +495,7 @@ namespace smt { SASSERT(n->get_owner()->get_decl()->get_range() == s); ast_manager & m = get_manager(); - context & ctx = get_context(); + context & ctx = get_context(); app_ref owner(n->get_owner(), m); if (!is_attached_to_var(n)) { @@ -510,7 +511,7 @@ namespace smt { assert_cnstr(valid); } } - + if (!ctx.relevancy()) relevant_eh(owner); } @@ -600,7 +601,7 @@ namespace smt { xe_eq_ye = m.mk_eq(xe, ye); not_xe_eq_ye = m.mk_not(xe_eq_ye); c_eq_iff = m.mk_iff(not_xe_eq_ye, c); - assert_cnstr(c_eq_iff); + assert_cnstr(c_eq_iff); assert_cnstr(mk_side_conditions()); return; @@ -689,10 +690,10 @@ namespace smt { pop_scope_eh(m_trail_stack.get_num_scopes()); m_converter.reset(); m_rw.reset(); - m_th_rw.reset(); - m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); + m_th_rw.reset(); + m_trail_stack.pop_scope(m_trail_stack.get_num_scopes()); if (m_factory) { - dealloc(m_factory); + dealloc(m_factory); m_factory = 0; } ast_manager & m = get_manager(); @@ -712,20 +713,6 @@ namespace smt { ast_manager & m = get_manager(); m_factory = alloc(fpa_value_factory, m, get_family_id()); mg.register_factory(m_factory); - - fpa2bv_converter::uf2bvuf_t const & uf2bvuf = m_converter.get_uf2bvuf(); - for (fpa2bv_converter::uf2bvuf_t::iterator it = uf2bvuf.begin(); - it != uf2bvuf.end(); - it++) { - mg.hide(it->m_value); - } - fpa2bv_converter::special_t const & specials = m_converter.get_min_max_specials(); - for (fpa2bv_converter::special_t::iterator it = specials.begin(); - it != specials.end(); - it++) { - mg.hide(it->m_value.first->get_decl()); - mg.hide(it->m_value.second->get_decl()); - } } model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { @@ -811,7 +798,33 @@ namespace smt { return res; } - void theory_fpa::finalize_model(model_generator & mg) {} + void theory_fpa::finalize_model(model_generator & mg) { + ast_manager & m = get_manager(); + proto_model & mdl = mg.get_model(); + proto_model new_model(m); + + bv2fpa_converter bv2fp(m, m_converter); + + obj_hashtable seen; + bv2fp.convert_min_max_specials(&mdl, &new_model, seen); + bv2fp.convert_uf2bvuf(&mdl, &new_model, seen); + + for (obj_hashtable::iterator it = seen.begin(); + it != seen.end(); + it++) + mdl.unregister_decl(*it); + + for (unsigned i = 0; i < new_model.get_num_constants(); i++) { + func_decl * f = new_model.get_constant(i); + mdl.register_decl(f, new_model.get_const_interp(f)); + } + + for (unsigned i = 0; i < new_model.get_num_functions(); i++) { + func_decl * f = new_model.get_function(i); + func_interp * fi = new_model.get_func_interp(f)->copy(); + mdl.register_decl(f, fi); + } + } void theory_fpa::display(std::ostream & out) const { @@ -862,8 +875,8 @@ namespace smt { } bool theory_fpa::include_func_interp(func_decl * f) { - TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;); - + TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;); + if (f->get_family_id() == get_family_id()) { bool include = m_fpa_util.is_min_unspecified(f) || diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 20d8bbbcc..9b95cf921 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -22,448 +22,54 @@ Notes: void fpa2bv_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) << ")"; - } - for (obj_map::iterator it = m_uf2bvuf.begin(); - it != m_uf2bvuf.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_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) << ")"; - } + m_bv2fp->display(out); out << ")"; } model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { - fpa2bv_model_converter * res = alloc(fpa2bv_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); - } - for (obj_map::iterator it = m_uf2bvuf.begin(); - it != m_uf2bvuf.end(); - it++) { - func_decl * k = translator(it->m_key); - func_decl * v = translator(it->m_value); - res->m_uf2bvuf.insert(k, v); - translator.to().inc_ref(k); - translator.to().inc_ref(v); - } - for (obj_map >::iterator it = m_specials.begin(); - it != m_specials.end(); - it++) { - 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); - } + fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to()); + res->m_bv2fp = m_bv2fp->translate(translator); return res; } -expr_ref fpa2bv_model_converter::convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) { - unsynch_mpz_manager & mpzm = m_fpa_util.fm().mpz_manager(); - unsynch_mpq_manager & mpqm = m_fpa_util.fm().mpq_manager(); +void fpa2bv_model_converter::convert(model_core * mc, model * float_mdl) { + obj_hashtable seen; + m_bv2fp->convert_consts(mc, float_mdl, seen); + m_bv2fp->convert_rm_consts(mc, float_mdl, seen); + m_bv2fp->convert_min_max_specials(mc, float_mdl, seen); + m_bv2fp->convert_uf2bvuf(mc, float_mdl, seen); - expr_ref res(m); - mpf fp_val; + // Keep all the non-float constants. + unsigned sz = mc->get_num_constants(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * c = mc->get_constant(i); + if (!seen.contains(c)) + float_mdl->register_decl(c, mc->get_const_interp(c)); + } - unsigned ebits = m_fpa_util.get_ebits(s); - unsigned sbits = m_fpa_util.get_sbits(s); + // And keep everything else + sz = mc->get_num_functions(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * f = mc->get_function(i); + if (!seen.contains(f)) + { + TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;); + func_interp * val = mc->get_func_interp(f)->copy(); + float_mdl->register_decl(f, val); + } + } - unsigned sgn_sz = 1; - unsigned exp_sz = ebits; - unsigned sig_sz = sbits - 1; - - rational sgn_q(0), sig_q(0), exp_q(0); - - if (sgn) m_bv_util.is_numeral(sgn, sgn_q, sgn_sz); - if (exp) m_bv_util.is_numeral(exp, exp_q, exp_sz); - if (sig) m_bv_util.is_numeral(sig, sig_q, sig_sz); - - // un-bias exponent - rational exp_unbiased_q; - exp_unbiased_q = exp_q - m_fpa_util.fm().m_powers2.m1(ebits - 1); - - mpz sig_z; mpf_exp_t exp_z; - mpzm.set(sig_z, sig_q.to_mpq().numerator()); - exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); - - m_fpa_util.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), exp_z, sig_z); - - mpzm.del(sig_z); - - res = m_fpa_util.mk_value(fp_val); - - TRACE("fpa2bv_mc", tout << "[" << mk_ismt2_pp(sgn, m) << - " " << mk_ismt2_pp(exp, m) << - " " << mk_ismt2_pp(sig, m) << "] == " << - mk_ismt2_pp(res, m) << std::endl;); - m_fpa_util.fm().del(fp_val); - - return res; + sz = mc->get_num_uninterpreted_sorts(); + for (unsigned i = 0; i < sz; i++) + { + sort * s = mc->get_uninterpreted_sort(i); + ptr_vector u = mc->get_universe(s); + float_mdl->register_usort(s, u.size(), u.c_ptr()); + } } -expr_ref fpa2bv_model_converter::convert_bv2fp(model * bv_mdl, sort * s, expr * bv) { - SASSERT(m_bv_util.is_bv(bv)); - - unsigned ebits = m_fpa_util.get_ebits(s); - unsigned sbits = m_fpa_util.get_sbits(s); - unsigned bv_sz = sbits + ebits; - - expr_ref sgn(m), exp(m), sig(m); - sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv); - exp = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv); - sig = m_bv_util.mk_extract(sbits - 2, 0, bv); - - expr_ref v_sgn(m), v_exp(m), v_sig(m); - bv_mdl->eval(sgn, v_sgn); - bv_mdl->eval(exp, v_exp); - bv_mdl->eval(sig, v_sig); - - return convert_bv2fp(s, v_sgn, v_exp, v_sig); -} - -expr_ref fpa2bv_model_converter::convert_bv2rm(expr * bv_rm) { - expr_ref res(m); - rational bv_val(0); - unsigned sz = 0; - - if (m_bv_util.is_numeral(bv_rm, bv_val, sz)) { - SASSERT(bv_val.is_uint64()); - switch (bv_val.get_uint64()) { - case BV_RM_TIES_TO_AWAY: res = m_fpa_util.mk_round_nearest_ties_to_away(); break; - case BV_RM_TIES_TO_EVEN: res = m_fpa_util.mk_round_nearest_ties_to_even(); break; - case BV_RM_TO_NEGATIVE: res = m_fpa_util.mk_round_toward_negative(); break; - case BV_RM_TO_POSITIVE: res = m_fpa_util.mk_round_toward_positive(); break; - case BV_RM_TO_ZERO: - default: res = m_fpa_util.mk_round_toward_zero(); - } - } - - return res; -} - -expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, expr * val) { - expr_ref res(m); - expr_ref eval_v(m); - - if (val && bv_mdl->eval(val, eval_v, true)) - res = convert_bv2rm(eval_v); - - return res; -} - -expr_ref fpa2bv_model_converter::rebuild_floats(model * bv_mdl, sort * s, expr * e) { - expr_ref result(m); - TRACE("fpa2bv_mc", tout << "rebuild floats in " << mk_ismt2_pp(s, m) << " for " << mk_ismt2_pp(e, m) << std::endl;); - - if (m_fpa_util.is_float(s)) { - if (m_fpa_util.is_numeral(e)) { - result = e; - } - else { - SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == (m_fpa_util.get_ebits(s) + m_fpa_util.get_sbits(s))); - result = convert_bv2fp(bv_mdl, s, e); - } - } - else if (m_fpa_util.is_rm(s)) { - if (m_fpa_util.is_rm_numeral(e)) { - result = e; - } - else { - SASSERT(m_bv_util.is_bv(e) && m_bv_util.get_bv_size(e) == 3); - result = convert_bv2rm(bv_mdl, e); - } - } - else if (is_app(e)) { - app * a = to_app(e); - expr_ref_vector new_args(m); - for (unsigned i = 0; i < a->get_num_args(); i++) - new_args.push_back(rebuild_floats(bv_mdl, a->get_decl()->get_domain()[i], a->get_arg(i))); - result = m.mk_app(a->get_decl(), new_args.size(), new_args.c_ptr()); - } - - return result; -} - -fpa2bv_model_converter::array_model fpa2bv_model_converter::convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) { - SASSERT(f->get_arity() == 0); - array_util arr_util(m); - - array_model am(m); - sort_ref_vector array_domain(m); - unsigned arity = f->get_range()->get_num_parameters()-1; - - expr_ref as_arr_mdl(m); - as_arr_mdl = bv_mdl->get_const_interp(bv_f); - if (as_arr_mdl == 0) return am; - TRACE("fpa2bv_mc", tout << "arity=0 func_interp for " << mk_ismt2_pp(f, m) << " := " << mk_ismt2_pp(as_arr_mdl, m) << std::endl;); - SASSERT(arr_util.is_as_array(as_arr_mdl)); - for (unsigned i = 0; i < arity; i++) - array_domain.push_back(to_sort(f->get_range()->get_parameter(i).get_ast())); - sort * rng = to_sort(f->get_range()->get_parameter(arity).get_ast()); - - bv_f = arr_util.get_as_array_func_decl(to_app(as_arr_mdl)); - - am.new_float_fd = m.mk_fresh_func_decl(arity, array_domain.c_ptr(), rng); - am.new_float_fi = convert_func_interp(am.new_float_fd, bv_f, bv_mdl); - am.bv_fd = bv_f; - am.result = arr_util.mk_as_array(f->get_range(), am.new_float_fd); - return am; -} - -func_interp * fpa2bv_model_converter::convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl) { - SASSERT(f->get_arity() > 0); - func_interp * result = 0; - sort * rng = f->get_range(); - sort * const * dmn = f->get_domain(); - - unsigned arity = bv_f->get_arity(); - func_interp * bv_fi = bv_mdl->get_func_interp(bv_f); - - if (bv_fi != 0) { - fpa_rewriter rw(m); - expr_ref ai(m); - result = alloc(func_interp, m, 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); - - for (unsigned j = 0; j < arity; j++) { - sort * ft_dj = dmn[j]; - expr * bv_aj = bv_args[j]; - ai = rebuild_floats(bv_mdl, ft_dj, bv_aj); - m_th_rw(ai); - new_args.push_back(ai); - } - - expr_ref bv_fres(m), ft_fres(m); - bv_fres = bv_fe->get_result(); - ft_fres = rebuild_floats(bv_mdl, rng, bv_fres); - m_th_rw(ft_fres); - result->insert_new_entry(new_args.c_ptr(), ft_fres); - } - - expr_ref bv_els(m), ft_els(m); - bv_els = bv_fi->get_else(); - ft_els = rebuild_floats(bv_mdl, rng, bv_els); - m_th_rw(ft_els); - result->set_else(ft_els); - } - - return result; -} - -void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { - 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; - for (unsigned i = 0; i < bv_mdl->get_num_functions(); i++) { - func_decl * f = bv_mdl->get_function(i); - tout << f->get_name() << "(...) := " << std::endl; - func_interp * fi = bv_mdl->get_func_interp(f); - for (unsigned j = 0; j < fi->num_entries(); j++) { - func_entry const * fe = fi->get_entry(j); - for (unsigned k = 0; k < f->get_arity(); k++) { - tout << mk_ismt2_pp(fe->get_arg(k), m) << " "; - } - tout << "--> " << mk_ismt2_pp(fe->get_result(), m) << std::endl; - } - tout << "else " << mk_ismt2_pp(fi->get_else(), m) << std::endl; - }); - - obj_hashtable seen; - - 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 = m_fpa_util.mk_pzero(f->get_range()); - nzero = m_fpa_util.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()); - - rational pn_num, np_num; - unsigned bv_sz; - m_bv_util.is_numeral(pn, pn_num, bv_sz); - m_bv_util.is_numeral(np, np_num, bv_sz); - - 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, (pn_num.is_one() ? nzero : pzero)); - flt_fi->set_else(np_num.is_one() ? 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(); - it++) - { - func_decl * var = it->m_key; - app * val = to_app(it->m_value); - SASSERT(m_fpa_util.is_float(var->get_range())); - SASSERT(var->get_range()->get_num_parameters() == 2); - - expr_ref sgn(m), sig(m), exp(m); - bv_mdl->eval(val->get_arg(0), sgn, true); - bv_mdl->eval(val->get_arg(1), exp, true); - bv_mdl->eval(val->get_arg(2), sig, true); - - SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP)); - -#ifdef Z3DEBUG - SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0); - SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0); - SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0); - seen.insert(to_app(val->get_arg(0))->get_decl()); - seen.insert(to_app(val->get_arg(1))->get_decl()); - seen.insert(to_app(val->get_arg(2))->get_decl()); -#else - SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT); - SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT); - seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl()); -#endif - - if (!sgn && !sig && !exp) - continue; - - expr_ref cv(m); - cv = convert_bv2fp(var->get_range(), sgn, exp, sig); - float_mdl->register_decl(var, cv); - - TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(cv, m) << std::endl;); - } - - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.end(); - it++) - { - func_decl * var = it->m_key; - SASSERT(m_fpa_util.is_rm(var->get_range())); - expr * val = it->m_value; - SASSERT(m_fpa_util.is_bv2rm(val)); - expr * bvval = to_app(val)->get_arg(0); - expr_ref fv(m); - fv = convert_bv2rm(bv_mdl, bvval); - TRACE("fpa2bv_mc", tout << var->get_name() << " == " << mk_ismt2_pp(fv, m) << ")" << std::endl;); - float_mdl->register_decl(var, fv); - seen.insert(to_app(bvval)->get_decl()); - } - - for (obj_map::iterator it = m_uf2bvuf.begin(); - it != m_uf2bvuf.end(); - it++) { - seen.insert(it->m_value); - - func_decl * f = it->m_key; - if (f->get_arity() == 0) - { - array_util au(m); - if (au.is_array(f->get_range())) { - array_model am = convert_array_func_interp(f, it->m_value, bv_mdl); - if (am.new_float_fd) float_mdl->register_decl(am.new_float_fd, am.new_float_fi); - if (am.result) float_mdl->register_decl(f, am.result); - if (am.bv_fd) seen.insert(am.bv_fd); - } - else { - // Just keep. - SASSERT(!m_fpa_util.is_float(f->get_range()) && !m_fpa_util.is_rm(f->get_range())); - expr_ref val(m); - bv_mdl->eval(it->m_value, val); - if (val) float_mdl->register_decl(f, val); - } - } - else { - func_interp * fmv = convert_func_interp(f, it->m_value, bv_mdl); - if (fmv) float_mdl->register_decl(f, fmv); - } - } - - // 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 * f = bv_mdl->get_function(i); - if (!seen.contains(f)) - { - TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;); - func_interp * val = bv_mdl->get_func_interp(f)->copy(); - float_mdl->register_decl(f, val); - } - } - - 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_model_converter(ast_manager & m, fpa2bv_converter const & conv) { +model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & 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 909a7cb78..7a39c0fba 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -19,79 +19,29 @@ Notes: #ifndef FPA2BV_MODEL_CONVERTER_H_ #define FPA2BV_MODEL_CONVERTER_H_ -#include"th_rewriter.h" #include"fpa2bv_converter.h" #include"model_converter.h" +#include"bv2fpa_converter.h" class fpa2bv_model_converter : public model_converter { ast_manager & m; - fpa_util m_fpa_util; - bv_util m_bv_util; - th_rewriter m_th_rw; + bv2fpa_converter * m_bv2fp; - obj_map m_const2bv; - obj_map m_rm_const2bv; - obj_map m_uf2bvuf; - obj_map > m_specials; - public: - fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : - m(m), - m_fpa_util(m), - m_bv_util(m), - m_th_rw(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 = 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 = 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_map >::iterator it = conv.m_min_max_specials.begin(); - it != conv.m_min_max_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); - } + fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv) : + m(m) { + m_bv2fp = alloc(bv2fpa_converter, m, conv); } virtual ~fpa2bv_model_converter() { - 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); - 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); - } + if (m_bv2fp) dealloc(m_bv2fp); + m_bv2fp = 0; } 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); + convert(md.get(), new_model); md = new_model; } @@ -106,32 +56,12 @@ public: protected: fpa2bv_model_converter(ast_manager & m) : m(m), - m_fpa_util(m), - m_bv_util(m), - m_th_rw(m) {} + m_bv2fp(0) {} - void convert(model * bv_mdl, model * float_mdl); - expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig); - expr_ref convert_bv2fp(model * bv_mdl, sort * s, expr * bv); - expr_ref convert_bv2rm(expr * eval_v); - expr_ref convert_bv2rm(model * bv_mdl, expr * val); - - func_interp * convert_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl); - expr_ref rebuild_floats(model * bv_mdl, sort * s, expr * e); - - class array_model { - public: - func_decl * new_float_fd; - func_interp * new_float_fi; - func_decl * bv_fd; - expr_ref result; - array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {} - }; - - array_model convert_array_func_interp(func_decl * f, func_decl * bv_f, model * bv_mdl); + void convert(model_core * mc, model * float_mdl); }; -model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv); +model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter & conv); #endif