diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 2d6419d69..f5f5b10c0 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -35,7 +35,11 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m_arith_util(m), m_mpf_manager(m_util.fm()), m_mpz_manager(m_mpf_manager.mpz_manager()), - m_hi_fp_unspecified(true), + 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"))); } @@ -1064,7 +1068,7 @@ void fpa2bv_converter::mk_abs(func_decl * f, unsigned num, expr * const * args, mk_fp(m_bv_util.mk_numeral(0, 1), e, s, result); } -void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); expr * x = args[0], * y = args[1]; @@ -1086,16 +1090,11 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn)); expr_ref lt(m); - mk_float_lt(f, num, args, lt); - - expr_ref zz(m); - zz = mk_min_unspecified(f, x, y); - TRACE("fpa2bv", tout << "min = " << mk_ismt2_pp(zz, m) << std::endl;); + mk_float_lt(f, num, args, lt); result = y; mk_ite(lt, x, result, result); mk_ite(both_zero, y, result, result); - mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1111,33 +1110,40 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) if (m_hi_fp_unspecified) // The hardware interpretation is -0.0. - mk_nzero(f, res); + mk_nzero(f, res); else { - app_ref pn_nondet(m), np_nondet(m); - pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert(pn_nondet->get_decl()); - m_decls_to_hide.insert(np_nondet->get_decl()); + if (m_min_pn_zeros.get() == 0) m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + if (m_min_np_zeros.get() == 0) m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); expr_ref pn(m), np(m); - mk_fp(pn_nondet, + mk_fp(m_min_pn_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(np_nondet, + mk_fp(m_min_np_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); - expr_ref x_is_pzero(m), x_is_nzero(m); + + expr_ref x_is_pzero(m), x_is_nzero(m), ite(m); mk_is_pzero(x, x_is_pzero); mk_is_nzero(y, x_is_nzero); - mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, res); + mk_ite(m.mk_and(x_is_pzero, x_is_nzero), pn, np, ite); + + expr * args[] = { x, y }; + mk_uninterpreted_function(f, 2, args, res); + + expr_ref pzero(m), nzero(m), extra(m); + mk_pzero(f, pzero); + mk_nzero(f, nzero); + extra = m.mk_or(m.mk_eq(ite, pzero), m.mk_eq(ite, nzero)); + m_extra_assertions.push_back(extra); } return res; } -void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { +void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); expr * x = args[0], *y = args[1]; @@ -1160,14 +1166,10 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref gt(m); mk_float_gt(f, num, args, gt); - - expr_ref zz(m); - zz = mk_max_unspecified(f, x, y); - + result = y; mk_ite(gt, x, result, result); - mk_ite(both_zero, y, result, result); - mk_ite(m.mk_and(both_zero, sgn_diff), zz, result, result); + mk_ite(both_zero, y, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1185,21 +1187,19 @@ 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 { - app_ref pn_nondet(m), np_nondet(m); - pn_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - np_nondet = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert(pn_nondet->get_decl()); - m_decls_to_hide.insert(np_nondet->get_decl()); + if (m_max_pn_zeros.get() == 0) m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + if (m_max_np_zeros.get() == 0) m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); expr_ref pn(m), np(m); - mk_fp(pn_nondet, + mk_fp(m_max_pn_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(np_nondet, + mk_fp(m_max_np_zeros, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); + expr_ref x_is_pzero(m), x_is_nzero(m); mk_is_pzero(x, x_is_pzero); mk_is_nzero(y, x_is_nzero); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index d17a6f770..6fb905708 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -57,6 +57,11 @@ protected: 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; public: fpa2bv_converter(ast_manager & m); @@ -102,8 +107,8 @@ public: 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_min(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_min_i(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); 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); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 1b7d55173..054133cc8 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -141,9 +141,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; - case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_DONE; - case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_DONE; + case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; @@ -166,8 +164,16 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + + case OP_FPA_MIN: + case OP_FPA_MAX: + throw rewriter_exception("operator is not supported, you must simplify the goal before applying fpa2bv"); + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE; case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE; + case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; + case OP_FPA_INTERNAL_BVWRAP: case OP_FPA_INTERNAL_BVUNWRAP: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index ec410fd18..5a8063c37 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -359,6 +359,10 @@ func_decl * fpa_decl_plugin::mk_binary_decl(decl_kind k, unsigned num_parameters case OP_FPA_REM: name = "fp.rem"; break; case OP_FPA_MIN: name = "fp.min"; break; case OP_FPA_MAX: name = "fp.max"; break; + case OP_FPA_INTERNAL_MIN_I: name = "fp.min_i"; break; + case OP_FPA_INTERNAL_MAX_I: name = "fp.max_i"; break; + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break; + case OP_FPA_INTERNAL_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break; default: UNREACHABLE(); break; @@ -689,32 +693,6 @@ func_decl * fpa_decl_plugin::mk_internal_bv_unwrap(decl_kind k, unsigned num_par return m_manager->mk_func_decl(symbol("bv_unwrap"), 1, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); } -func_decl * fpa_decl_plugin::mk_internal_min_unspecified( - decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - if (arity != 2) - m_manager->raise_exception("invalid number of arguments to fp.min_unspecified"); - if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); - if (!is_float_sort(range)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); - - return m_manager->mk_func_decl(symbol("fp.min_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - -func_decl * fpa_decl_plugin::mk_internal_max_unspecified( - decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - if (arity != 2) - m_manager->raise_exception("invalid number of arguments to fp.max_unspecified"); - if (domain[0] != domain[1] || !is_float_sort(domain[0])) - m_manager->raise_exception("sort mismatch, expected arguments of equal FloatingPoint sorts"); - if (!is_float_sort(range)) - m_manager->raise_exception("sort mismatch, expected range of FloatingPoint sort"); - - return m_manager->mk_func_decl(symbol("fp.max_unspecified"), 2, domain, range, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - func_decl * fpa_decl_plugin::mk_internal_to_ubv_unspecified( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -822,10 +800,13 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, return mk_internal_bv_wrap(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_BVUNWRAP: return mk_internal_bv_unwrap(k, num_parameters, parameters, arity, domain, range); + + case OP_FPA_INTERNAL_MIN_I: + case OP_FPA_INTERNAL_MAX_I: case OP_FPA_INTERNAL_MIN_UNSPECIFIED: - return mk_internal_min_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_MAX_UNSPECIFIED: - return mk_internal_max_unspecified(k, num_parameters, parameters, arity, domain, range); + return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: return mk_internal_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: @@ -1031,18 +1012,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_internal_min_unspecified(expr * x, expr * y) { - SASSERT(m().get_sort(x) == m().get_sort(y)); - expr * args[] = { x, y }; - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x)); -} - -app * fpa_util::mk_internal_max_unspecified(expr * x, expr * y) { - SASSERT(m().get_sort(x) == m().get_sort(y)); - expr * args[] = { x, y }; - return m().mk_app(get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, 0, 0, 2, args, m().get_sort(x)); -} - app * fpa_util::mk_internal_to_ubv_unspecified(unsigned width) { parameter ps[] = { parameter(width) }; sort * range = m_bv_util.mk_sort(width); diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index 50b388047..34a9daa59 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -86,7 +86,10 @@ enum fpa_op_kind { /* Internal use only */ OP_FPA_INTERNAL_BVWRAP, - OP_FPA_INTERNAL_BVUNWRAP, + OP_FPA_INTERNAL_BVUNWRAP, + + OP_FPA_INTERNAL_MIN_I, + OP_FPA_INTERNAL_MAX_I, OP_FPA_INTERNAL_MIN_UNSPECIFIED, OP_FPA_INTERNAL_MAX_UNSPECIFIED, OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED, @@ -162,10 +165,6 @@ class fpa_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_bv_unwrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_min_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_internal_max_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); func_decl * mk_internal_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, @@ -338,8 +337,6 @@ public: app * mk_to_ieee_bv(expr * arg1) { return m().mk_app(m_fid, OP_FPA_TO_IEEE_BV, arg1); } - app * mk_internal_min_unspecified(expr * x, expr * y); - app * mk_internal_max_unspecified(expr * x, expr * y); app * mk_internal_to_ubv_unspecified(unsigned width); app * mk_internal_to_sbv_unspecified(unsigned width); app * mk_internal_to_ieee_bv_unspecified(unsigned width); diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index d336c3a56..2a800f004 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -93,6 +93,8 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(f, args[0], result); break; case OP_FPA_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; + case OP_FPA_INTERNAL_MIN_I: + case OP_FPA_INTERNAL_MAX_I: case OP_FPA_INTERNAL_MIN_UNSPECIFIED: case OP_FPA_INTERNAL_MAX_UNSPECIFIED: SASSERT(num_args == 2); st = BR_FAILED; break; @@ -432,21 +434,23 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { } scoped_mpf v1(m_fm), v2(m_fm); - 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 could be +zero or -zero. - result = m_util.mk_internal_min_unspecified(arg1, arg2); - return BR_DONE; - } - else { - scoped_mpf r(m_fm); - m_fm.minimum(v1, v2, r); - result = m_util.mk_value(r); - return BR_DONE; - } + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2) && + !(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))) { + scoped_mpf r(m_fm); + m_fm.minimum(v1, v2, r); + result = m_util.mk_value(r); + return BR_DONE; } + else { + expr_ref c(m()), v(m()); + c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), + m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)), + m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2)))); + v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); - return BR_FAILED; + result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_I, arg1, arg2)); + return BR_REWRITE_FULL; + } } br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { @@ -460,21 +464,23 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { } scoped_mpf v1(m_fm), v2(m_fm); - 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 could be +zero or -zero. - result = m_util.mk_internal_max_unspecified(arg1, arg2); - return BR_REWRITE_FULL; - } - else { - scoped_mpf r(m_fm); - m_fm.maximum(v1, v2, r); - result = m_util.mk_value(r); - return BR_DONE; - } + if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2) && + !(m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2))) { + scoped_mpf r(m_fm); + m_fm.maximum(v1, v2, r); + result = m_util.mk_value(r); + return BR_DONE; } + else { + expr_ref c(m()), v(m()); + c = m().mk_and(m().mk_and(m_util.mk_is_zero(arg1), m_util.mk_is_zero(arg2)), + m().mk_or(m().mk_and(m_util.mk_is_positive(arg1), m_util.mk_is_negative(arg2)), + m().mk_and(m_util.mk_is_negative(arg1), m_util.mk_is_positive(arg2)))); + v = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); - return BR_FAILED; + result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_I, arg1, arg2)); + return BR_REWRITE_FULL; + } } br_status fpa_rewriter::mk_fma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) { diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index f9d2eeed4..af0d5e5fc 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -45,11 +45,6 @@ void fpa2bv_model_converter::display(std::ostream & out) { unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; } - for (obj_hashtable::iterator it = m_decls_to_hide.begin(); - it != m_decls_to_hide.end(); - it++) { - out << "\n to hide: " << mk_ismt2_pp(*it, m); - } out << ")" << std::endl; } @@ -84,13 +79,6 @@ 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(); - it++) { - func_decl * k = translator(*it); - res->m_decls_to_hide.insert(k); - translator.to().inc_ref(k); - } return res; } @@ -204,16 +192,23 @@ 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; - ); + 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_hashtable::iterator it = m_decls_to_hide.begin(); - it != m_decls_to_hide.end(); - it++) - seen.insert(*it); - for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); it++) @@ -317,8 +312,8 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { els = convert_bv2rm(els); flt_fi->set_else(els); - - float_mdl->register_decl(f, flt_fi); + + float_mdl->register_decl(f, flt_fi); } // Keep all the non-float constants. @@ -355,7 +350,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); + obj_map const & uf2bvuf) { + return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf); } diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index a6ae73eb8..021538ac1 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -27,13 +27,11 @@ 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; 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) : + obj_map const & uf2bvuf) : m(m) { // Just create a copy? for (obj_map::iterator it = const2bv.begin(); @@ -60,19 +58,12 @@ public: 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); - } } 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); - dec_ref_collection_values(m, m_decls_to_hide); } virtual void operator()(model_ref & md, unsigned goal_idx) { @@ -105,7 +96,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 & m_decls_to_hide); + obj_map const & uf2bvuf); -#endif +#endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 158bb935e..07669f513 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -107,7 +107,7 @@ 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()); + mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf()); g->inc_depth(); result.push_back(g.get());