From 31cfca0444d2df3f231e0a8b92e80a8fa531f7c1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 12 Sep 2017 19:43:45 +0100 Subject: [PATCH] Eliminated unspecified operators for fp.to_*bv, fp.to_real. Also fixes #1191. --- src/api/api_ast.cpp | 4 - src/api/z3_api.h | 16 --- src/ast/fpa/bv2fpa_converter.cpp | 26 ++++- src/ast/fpa/fpa2bv_converter.cpp | 183 +++++++++++++----------------- src/ast/fpa/fpa2bv_converter.h | 8 +- src/ast/fpa/fpa2bv_rewriter.cpp | 4 - src/ast/fpa_decl_plugin.cpp | 91 --------------- src/ast/fpa_decl_plugin.h | 44 +------ src/ast/rewriter/fpa_rewriter.cpp | 64 +---------- src/ast/rewriter/fpa_rewriter.h | 4 +- src/smt/theory_fpa.cpp | 11 +- 11 files changed, 118 insertions(+), 337 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index cfea4098f..491e08cf4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1210,10 +1210,6 @@ extern "C" { case OP_FPA_BV2RM: return Z3_OP_FPA_BV2RM; case OP_FPA_MIN_UNSPECIFIED: return Z3_OP_FPA_MIN_UNSPECIFIED; case OP_FPA_MAX_UNSPECIFIED: return Z3_OP_FPA_MAX_UNSPECIFIED; - case OP_FPA_TO_UBV_UNSPECIFIED: return Z3_OP_FPA_TO_UBV_UNSPECIFIED; - case OP_FPA_TO_SBV_UNSPECIFIED: return Z3_OP_FPA_TO_SBV_UNSPECIFIED; - case OP_FPA_TO_REAL_UNSPECIFIED: return Z3_OP_FPA_TO_REAL_UNSPECIFIED; - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: return Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED; return Z3_OP_UNINTERPRETED; default: return Z3_OP_INTERNAL; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 663a59fd9..bfc0b93a2 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1005,18 +1005,6 @@ typedef enum - Z3_OP_FPA_MAX_UNSPECIFIED: The same as Z3_OP_FPA_MAX, but the arguments are expected to be zeroes with different signs. - - Z3_OP_FPA_TO_UBV_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_UBV. - - - Z3_OP_FPA_TO_SBV_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_SBV. - - - Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_IEEE_BV. - - - Z3_OP_FPA_TO_REAL_UNSPECIFIED: A term representing the unspecified - results of Z3_OP_FPA_TO_IEEE_BV. - - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information. @@ -1310,10 +1298,6 @@ typedef enum { Z3_OP_FPA_BV2RM, Z3_OP_FPA_MIN_UNSPECIFIED, Z3_OP_FPA_MAX_UNSPECIFIED, - Z3_OP_FPA_TO_UBV_UNSPECIFIED, - Z3_OP_FPA_TO_SBV_UNSPECIFIED, - Z3_OP_FPA_TO_REAL_UNSPECIFIED, - Z3_OP_FPA_TO_IEEE_BV_UNSPECIFIED, Z3_OP_INTERNAL, diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 7e4f2f133..59f24779e 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -291,9 +291,11 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * 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); + if (bv_els != 0) { + ft_els = rebuild_floats(mc, rng, bv_els); + m_th_rw(ft_els); + result->set_else(ft_els); + } } return result; @@ -447,8 +449,22 @@ void bv2fpa_converter::convert_uf2bvuf(model_core * mc, model_core * target_mode } } else { - func_interp * fmv = convert_func_interp(mc, f, it->m_value); - if (fmv) target_model->register_decl(f, fmv); + if (it->get_key().get_family_id() == m_fpa_util.get_fid()) { + // it->m_value contains the model for the unspecified cases of it->m_key. + continue; + + // Upon request, add this 'recursive' definition? + func_interp * fmv = convert_func_interp(mc, f, it->m_value); + unsigned n = fmv->get_arity(); + expr_ref_vector args(m); + for (unsigned i = 0; i < n; i++) + args.push_back(m.mk_var(i, f->get_domain()[i])); + fmv->set_else(m.mk_app(it->m_key, n, args.c_ptr())); + } + else { + func_interp * fmv = convert_func_interp(mc, f, it->m_value); + if (fmv) target_model->register_decl(f, fmv); + } } } } diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6f0c83df9..da4052108 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2855,8 +2855,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); expr_ref unspec(m); - unspec = mk_to_real_unspecified(ebits, sbits); - + mk_to_real_unspecified(f, num, args, unspec); 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); @@ -3141,11 +3140,12 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 1); - expr_ref x(m), x_is_nan(m); + expr_ref x(m), x_is_nan(m), x_flat(m); expr * sgn, * s, * e; x = args[0]; split_fp(x, sgn, e, s); mk_is_nan(x, x_is_nan); + join_fp(x, x_flat); sort * fp_srt = m.get_sort(x); unsigned ebits = m_util.get_ebits(fp_srt); @@ -3159,13 +3159,12 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2), m_bv_util.mk_numeral(1, 1)))); else { - app_ref unspec(m); - unspec = m_util.mk_to_ieee_bv_unspecified(ebits, sbits); - mk_to_ieee_bv_unspecified(unspec->get_decl(), 0, 0, nanv); + expr * x_flatp = x_flat.get(); + mk_to_ieee_bv_unspecified(f, 1, &x_flatp, nanv); } expr_ref sgn_e_s(m); - sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); + join_fp(x, 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;); @@ -3173,7 +3172,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * } void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - SASSERT(num == 0); + SASSERT(num == 1); + SASSERT(m_util.is_float(args[0])); unsigned ebits = f->get_parameter(0).get_int(); unsigned sbits = f->get_parameter(1).get_int(); @@ -3184,26 +3184,30 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex 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); + expr * n = args[0]; + expr_ref n_bv(m); + join_fp(n, n_bv); + + func_decl * f_bv; + if (!m_uf2bvuf.find(f, f_bv)) { + sort * domain[2] = { m.get_sort(n_bv) }; + f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range()); + m_uf2bvuf.insert(f, f_bv); 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); + m.inc_ref(f_bv); } + + result = m.mk_app(f_bv, n_bv); + + 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;); @@ -3238,15 +3242,13 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args mk_is_nzero(x, x_is_nzero); // NaN, Inf, or negative (except -0) -> unspecified - expr_ref c1(m), v1(m); - if (!is_signed) { + expr_ref c1(m), v1(m), unspec_v(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 { + else c1 = m.mk_or(x_is_nan, x_is_inf); - v1 = mk_to_sbv_unspecified(ebits, sbits, bv_sz); - } + mk_to_bv_unspecified(f, num, args, unspec_v); + v1 = unspec_v; dbg_decouple("fpa2bv_to_bv_c1", c1); // +-Zero -> 0 @@ -3355,11 +3357,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 = 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(rnd_has_overflown, unspec_v, rnd); + result = m.mk_ite(c_in_limits, result, unspec_v); result = m.mk_ite(c2, v2, result); result = m.mk_ite(c1, v1, result); @@ -3378,85 +3377,54 @@ 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 width = m_bv_util.get_bv_size(f->get_range()); +void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + SASSERT(m_util.is_bv2rm(args[0])); + SASSERT(m_util.is_float(args[1])); if (m_hi_fp_unspecified) - result = m_bv_util.mk_numeral(0, width); + result = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(f->get_range())); 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); + expr * rm_bv = to_app(args[0])->get_arg(0); + expr * n = args[1]; + expr_ref n_bv(m); + join_fp(n, n_bv); + + func_decl * f_bv; + if (!m_uf2bvuf.find(f, f_bv)) { + sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) }; + f_bv = m.mk_fresh_func_decl(0, 2, domain, f->get_range()); + m_uf2bvuf.insert(f, f_bv); m.inc_ref(f); - m.inc_ref(fd); + m.inc_ref(f_bv); } - result = m.mk_const(fd); + result = m.mk_app(f_bv, rm_bv, n_bv); } - TRACE("fpa2bv_to_ubv_unspecified", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); + TRACE("fpa2bv_to_bv_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 res(m); - app_ref u(m); - u = m_util.mk_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 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 res(m); - app_ref u(m); - u = m_util.mk_to_sbv_unspecified(ebits, sbits, width); - mk_to_sbv_unspecified(u->get_decl(), 0, 0, res); - return res; -} - void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 1); + if (m_hi_fp_unspecified) result = m_arith_util.mk_numeral(rational(0), false); 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); - } -} + expr * n = args[0]; + expr_ref n_bv(m); + join_fp(n, n_bv); -expr_ref fpa2bv_converter::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { - expr_ref res(m); - app_ref u(m); - u = m_util.mk_to_real_unspecified(ebits, sbits); - mk_to_real_unspecified(u->get_decl(), 0, 0, res); - return res; + func_decl * f_bv; + if (!m_uf2bvuf.find(f, f_bv)) { + sort * domain[2] = { m.get_sort(n_bv) }; + f_bv = m.mk_fresh_func_decl(0, 1, domain, f->get_range()); + m_uf2bvuf.insert(f, f_bv); + m.inc_ref(f); + m.inc_ref(f_bv); + } + result = m.mk_app(f_bv, n_bv); + } } void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { @@ -3467,6 +3435,7 @@ void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, e result = m_util.mk_fp(args[0], args[1], args[2]); TRACE("fpa2bv_mk_fp", tout << "mk_fp result = " << mk_ismt2_pp(result, m) << std::endl;); } + void fpa2bv_converter::split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const { SASSERT(m_util.is_fp(e)); SASSERT(to_app(e)->get_num_args() == 3); @@ -3485,6 +3454,14 @@ void fpa2bv_converter::split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_r sig = e_sig; } +void fpa2bv_converter::join_fp(expr * e, expr_ref & res) { + SASSERT(m_util.is_fp(e)); + SASSERT(to_app(e)->get_num_args() == 3); + expr *sgn, *exp, *sig; + split_fp(e, sgn, exp, sig); + res = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, exp), sig); +} + void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) { expr * sgn, * sig, * exp; split_fp(e, sgn, exp, sig); @@ -4051,7 +4028,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & // put the sticky bit into the significand. expr_ref ext_sticky(m); ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky); - expr * tmp[] = { sig, ext_sticky }; + expr * tmp[2] = { sig, ext_sticky }; sig = m_bv_util.mk_bv_or(2, tmp); SASSERT(is_well_sorted(m, sig)); SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 1e3e5d9b3..d54adac78 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -76,6 +76,7 @@ public: void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const; void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const; + void join_fp(expr * e, expr_ref & res); void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); @@ -138,9 +139,8 @@ public: 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_bv_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); @@ -226,10 +226,6 @@ 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 28ec35536..07623ec48 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -143,13 +143,9 @@ 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_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_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_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_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; diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index c50d6b985..9bee51af7 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -711,65 +711,6 @@ func_decl * fpa_decl_plugin::mk_bv_wrap(decl_kind k, unsigned num_parameters, pa } } -func_decl * fpa_decl_plugin::mk_to_ubv_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 fp.to_ubv_unspecified"); - if (num_parameters != 3) - m_manager->raise_exception("invalid number of parameters to fp.to_ubv_unspecified; expecting 3"); - if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_ubv_unspecified; expecting 3 integers"); - - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ¶meters[2]); - return m_manager->mk_func_decl(symbol("fp.to_ubv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - -func_decl * fpa_decl_plugin::mk_to_sbv_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 fp.to_sbv_unspecified"); - if (num_parameters != 3) - m_manager->raise_exception("invalid number of parameters to fp.to_sbv_unspecified; expecting 3"); - if (!parameters[0].is_int() || !parameters[1].is_int() || !parameters[2].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_sbv_unspecified; expecting 3 integers"); - - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ¶meters[2]); - return m_manager->mk_func_decl(symbol("fp.to_sbv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - -func_decl * fpa_decl_plugin::mk_to_real_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 fp.to_real_unspecified"); - if (num_parameters != 2) - m_manager->raise_exception("invalid number of parameters to fp.to_real_unspecified; expecting 2"); - if (!parameters[0].is_int() || !parameters[1].is_int()) - m_manager->raise_exception("invalid parameters type provided to fp.to_real_unspecified; expecting 2 integers"); - if (!is_sort_of(range, m_arith_fid, REAL_SORT)) - m_manager->raise_exception("sort mismatch, expected range of Real sort"); - - return m_manager->mk_func_decl(symbol("fp.to_real_unspecified"), 0, domain, m_real_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - -func_decl * fpa_decl_plugin::mk_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 fp.to_ieee_bv_unspecified; expecting none"); - if (num_parameters != 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 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("fp.to_ieee_bv_unspecified"), 0, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); -} - - func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -846,14 +787,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_MAX_UNSPECIFIED: return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_UBV_UNSPECIFIED: - return mk_to_ubv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_SBV_UNSPECIFIED: - return mk_to_sbv_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_REAL_UNSPECIFIED: - return mk_to_real_unspecified(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: - return mk_to_ieee_bv_unspecified(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -1054,30 +987,6 @@ app * fpa_util::mk_nzero(unsigned ebits, unsigned sbits) { return mk_value(v); } -app * fpa_util::mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { - parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) }; - sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED, 3, ps, 0, 0, range); -} - -app * fpa_util::mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width) { - parameter ps[] = { parameter(ebits), parameter(sbits), parameter(width) }; - sort * range = m_bv_util.mk_sort(width); - return m().mk_app(get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED, 3, ps, 0, 0, range); -} - -app * fpa_util::mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits) { - parameter ps[] = { parameter(ebits), parameter(sbits) }; - sort * range = m_bv_util.mk_sort(ebits+sbits); - return m().mk_app(get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED, 2, ps, 0, 0, range); -} - -app * fpa_util::mk_to_real_unspecified(unsigned ebits, unsigned sbits) { - parameter ps[] = { parameter(ebits), parameter(sbits) }; - sort * range = m_a_util.mk_real(); - return m().mk_app(get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED, 2, ps, 0, 0, range); -} - bool fpa_util::contains_floats(ast * a) { switch (a->get_kind()) { case AST_APP: { diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index c78194b63..79f44a13d 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -93,10 +93,6 @@ enum fpa_op_kind { OP_FPA_MAX_I, OP_FPA_MIN_UNSPECIFIED, OP_FPA_MAX_UNSPECIFIED, - OP_FPA_TO_UBV_UNSPECIFIED, - OP_FPA_TO_SBV_UNSPECIFIED, - OP_FPA_TO_IEEE_BV_UNSPECIFIED, - OP_FPA_TO_REAL_UNSPECIFIED, LAST_FLOAT_OP }; @@ -167,34 +163,12 @@ class fpa_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_ubv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_sbv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_real_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - func_decl * mk_to_ieee_bv_unspecified(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); - virtual bool is_considered_uninterpreted(func_decl * f) { - if (f->get_family_id() != get_family_id()) - return false; - switch (f->get_decl_kind()) - { - case OP_FPA_TO_UBV_UNSPECIFIED: - case OP_FPA_TO_SBV_UNSPECIFIED: - case OP_FPA_TO_REAL_UNSPECIFIED: - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: - return true; - default: - return false; - } - return false; - } + virtual bool is_considered_uninterpreted(func_decl * f) { return false; } public: fpa_decl_plugin(); @@ -374,10 +348,6 @@ public: SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3); return m().mk_app(m_fid, OP_FPA_BV2RM, 0, 0, 1, &bv3, mk_rm_sort()); } - app * mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned width); - app * mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned width); - app * mk_to_ieee_bv_unspecified(unsigned ebits, unsigned sbits); - app * mk_to_real_unspecified(unsigned ebits, unsigned sbits); bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); } bool is_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; } @@ -388,19 +358,15 @@ public: bool is_min_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_UNSPECIFIED); } bool is_max_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_I); } bool is_max_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MAX_UNSPECIFIED); } - bool is_to_ubv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV_UNSPECIFIED); } - bool is_to_sbv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV_UNSPECIFIED); } - bool is_to_ieee_bv_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_IEEE_BV_UNSPECIFIED); } - bool is_to_real_unspecified(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_REAL_UNSPECIFIED); } + bool is_to_ubv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_UBV); } + bool is_to_sbv(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_TO_SBV); } bool is_min_interpreted(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_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_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_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_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_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_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_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_TO_REAL_UNSPECIFIED; } + bool is_to_ubv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_UBV; } + bool is_to_sbv(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_TO_SBV; } bool contains_floats(ast * a); }; diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index b31270ce8..644aff630 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -103,57 +103,12 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con case OP_FPA_BVWRAP: SASSERT(num_args == 1); st = mk_bvwrap(args[0], result); break; case OP_FPA_BV2RM: SASSERT(num_args == 1); st = mk_bv2rm(args[0], result); break; - case OP_FPA_TO_UBV_UNSPECIFIED: - case OP_FPA_TO_SBV_UNSPECIFIED: - case OP_FPA_TO_REAL_UNSPECIFIED: - case OP_FPA_TO_IEEE_BV_UNSPECIFIED: - st = BR_FAILED; - break; - default: NOT_IMPLEMENTED_YET(); } return st; } -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) { - // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, width); - return BR_DONE; - } - else { - result = m_util.mk_to_ubv_unspecified(ebits, sbits, width); - 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) { - // The "hardware interpretation" is 0. - result = bu.mk_numeral(0, width); - return BR_DONE; - } - else { - result = m_util.mk_to_sbv_unspecified(ebits, sbits, width); - return BR_REWRITE1; - } -} - -br_status fpa_rewriter::mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result) { - if (m_hi_fp_unspecified) { - // The "hardware interpretation" is 0. - result = m_util.au().mk_numeral(rational(0), false); - return BR_DONE; - } - else { - result = m_util.mk_to_real_unspecified(ebits, sbits); - return BR_REWRITE1; - } -} - br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { SASSERT(f->get_num_parameters() == 2); SASSERT(f->get_parameter(0).is_int()); @@ -808,7 +763,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ const mpf & x = v.get(); 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); + return BR_FAILED; bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -822,9 +777,6 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_ result = bu.mk_numeral(r, bv_sz); return BR_DONE; } - else - return mk_to_ubv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); - } return BR_FAILED; @@ -842,7 +794,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ const mpf & x = v.get(); 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); + return BR_FAILED; bv_util bu(m()); scoped_mpq q(m_fm.mpq_manager()); @@ -856,8 +808,6 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_ result = bu.mk_numeral(r, bv_sz); return BR_DONE; } - else - return mk_to_sbv_unspecified(x.get_ebits(), x.get_sbits(), bv_sz, result); } return BR_FAILED; @@ -881,7 +831,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu result = bu.mk_concat(4, args); } else - result = m_util.mk_to_ieee_bv_unspecified(x.get_ebits(), x.get_sbits()); + return BR_FAILED; return BR_REWRITE1; } @@ -900,16 +850,12 @@ br_status fpa_rewriter::mk_to_real(expr * arg, expr_ref & result) { scoped_mpf v(m_fm); if (m_util.is_numeral(arg, v)) { - if (m_fm.is_nan(v) || m_fm.is_inf(v)) { - const mpf & x = v.get(); - result = m_util.mk_to_real_unspecified(x.get_ebits(), x.get_sbits()); - } - else { + if (!m_fm.is_nan(v) && !m_fm.is_inf(v)) { scoped_mpq r(m_fm.mpq_manager()); m_fm.to_rational(v, r); result = m_util.au().mk_numeral(r.get(), false); + return BR_DONE; } - return BR_DONE; } return BR_FAILED; diff --git a/src/ast/rewriter/fpa_rewriter.h b/src/ast/rewriter/fpa_rewriter.h index 282cec4df..5d5b7e57d 100644 --- a/src/ast/rewriter/fpa_rewriter.h +++ b/src/ast/rewriter/fpa_rewriter.h @@ -88,9 +88,7 @@ public: br_status mk_min_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); br_status mk_max_i(func_decl * f, expr * arg1, expr * arg2, expr_ref & result); - br_status mk_to_ubv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); - br_status mk_to_sbv_unspecified(unsigned ebits, unsigned sbits, unsigned with, expr_ref & result); - br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr_ref & result); + br_status mk_to_real_unspecified(unsigned ebits, unsigned sbits, expr * n, expr_ref & result); br_status mk_bvwrap(expr * arg, expr_ref & result); }; diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 12c5fb0b1..d337cc65d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -119,6 +119,7 @@ namespace smt { SASSERT(m_conversions.empty()); SASSERT(m_is_added_to_model.empty()); } + void theory_fpa::init(context * ctx) { smt::theory::init(ctx); m_is_initialized = true; @@ -890,14 +891,10 @@ namespace smt { if (f->get_family_id() == get_family_id()) { bool include = m_fpa_util.is_min_unspecified(f) || - m_fpa_util.is_max_unspecified(f) || - m_fpa_util.is_to_ubv_unspecified(f) || - m_fpa_util.is_to_sbv_unspecified(f) || - m_fpa_util.is_to_ieee_bv_unspecified(f) || - m_fpa_util.is_to_real_unspecified(f); + m_fpa_util.is_max_unspecified(f) ; if (include && !m_is_added_to_model.contains(f)) { - m_is_added_to_model.insert(f); - get_manager().inc_ref(f); + //m_is_added_to_model.insert(f); + //get_manager().inc_ref(f); return true; } return false;