diff --git a/src/api/z3_api.h b/src/api/z3_api.h index bfc0b93a2..154b8eb3c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -993,18 +993,6 @@ typedef enum 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE, 4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO. - - Z3_OP_FPA_MIN_I: The same as Z3_OP_FPA_MIN, but the arguments are - expected not to be zeroes with different signs. - - - Z3_OP_FPA_MAX_I: The same as Z3_OP_FPA_MAX, but the arguments are - expected not to be zeroes with different signs. - - - Z3_OP_FPA_MIN_UNSPECIFIED: The same as Z3_OP_FPA_MIN, but the - arguments are expected to be zeroes with different signs. - - - 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_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. @@ -1291,13 +1279,8 @@ typedef enum { Z3_OP_FPA_TO_IEEE_BV, - Z3_OP_FPA_MIN_I, - Z3_OP_FPA_MAX_I, - Z3_OP_FPA_BVWRAP, Z3_OP_FPA_BV2RM, - Z3_OP_FPA_MIN_UNSPECIFIED, - Z3_OP_FPA_MAX_UNSPECIFIED, Z3_OP_INTERNAL, diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 30d41bc53..93bd79571 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -62,8 +62,8 @@ bv2fpa_converter::bv2fpa_converter(ast_manager & m, fpa2bv_converter & conv) : 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(); + for (obj_map >::iterator it = conv.m_min_max_ufs.begin(); + it != conv.m_min_max_ufs.end(); it++) { m_specials.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index bc0364994..f09ddcd42 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -230,39 +230,7 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result) result = m_util.mk_fp(sgn, e, s); } -void fpa2bv_converter::mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result) { - if (m_util.is_float(rng)) { - unsigned ebits = m_util.get_ebits(rng); - unsigned sbits = m_util.get_sbits(rng); - unsigned bv_sz = ebits + sbits; - - app_ref na(m); - na = m.mk_app(fbv, fbv->get_arity(), new_args); - result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na), - m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na), - m_bv_util.mk_extract(sbits - 2, 0, na)); - } - else if (m_util.is_rm(rng)) { - app_ref na(m); - na = m.mk_app(fbv, fbv->get_arity(), new_args); - result = m_util.mk_bv2rm(na); - } - else - result = m.mk_app(fbv, fbv->get_arity(), new_args); -} - -func_decl * fpa2bv_converter::get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity) { - func_decl * res; - if (!m_uf2bvuf.find(f, res)) { - res = m.mk_fresh_func_decl(f->get_name(), symbol("bv"), arity, f->get_domain(), bv_rng); - m_uf2bvuf.insert(f, res); - m.inc_ref(f); - m.inc_ref(res); - TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;); - } - return res; -} -void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result) +void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv", tout << "UF: " << mk_ismt2_pp(f, m) << std::endl; ); @@ -278,7 +246,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a unsigned sbits = m_util.get_sbits(rng); unsigned bv_sz = ebits+sbits; bv_rng = m_bv_util.mk_sort(bv_sz); - func_decl * bv_f = get_bv_uf(f, bv_rng, num); + func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng); bv_app = m.mk_app(bv_f, num, args); flt_app = m_util.mk_fp(m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app), m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app), @@ -291,7 +259,7 @@ void fpa2bv_converter::mk_function(func_decl * f, unsigned num, expr * const * a sort_ref bv_rng(m); expr_ref new_eq(m); bv_rng = m_bv_util.mk_sort(3); - func_decl * bv_f = get_bv_uf(f, bv_rng, num); + func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng); bv_app = m.mk_app(bv_f, num, args); flt_app = m_util.mk_bv2rm(bv_app); new_eq = m.mk_eq(fapp, flt_app); @@ -1211,61 +1179,89 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) { } void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - expr_ref x(m), y(m); - x = args[0]; - y = args[1]; - - expr_ref x_is_zero(m), y_is_zero(m), both_are_zero(m); - x_is_zero = m_util.mk_is_zero(x); - y_is_zero = m_util.mk_is_zero(y); - both_are_zero = m.mk_and(x_is_zero, y_is_zero); - - expr_ref x_is_positive(m), x_is_negative(m), y_is_positive(m), y_is_negative(m), pn(m), np(m), pn_or_np(m); - x_is_positive = m_util.mk_is_positive(x); - x_is_negative = m_util.mk_is_negative(x); - y_is_positive = m_util.mk_is_positive(y); - y_is_negative = m_util.mk_is_negative(y); - pn = m.mk_and(x_is_positive, y_is_negative); - np = m.mk_and(x_is_negative, y_is_positive); - pn_or_np = m.mk_or(pn, np); - - expr_ref c(m), v(m); - c = m.mk_and(both_are_zero, pn_or_np); - v = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_UNSPECIFIED, x, y); - - // Note: This requires BR_REWRITE_FULL afterwards. - expr_ref min_i(m); - min_i = m.mk_app(m_util.get_family_id(), OP_FPA_MIN_I, x, y); - m_simp.mk_ite(c, v, min_i, result); -} - -void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); expr * x = args[0], * y = args[1]; - expr * x_sgn, * x_sig, * x_exp; - expr * y_sgn, * y_sig, * y_exp; + expr * x_sgn, *x_sig, *x_exp; + expr * y_sgn, *y_sig, *y_exp; split_fp(x, x_sgn, x_exp, x_sig); split_fp(y, y_sgn, y_exp, y_sig); - expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); - mk_is_zero(x, x_is_zero); - mk_is_zero(y, y_is_zero); - m_simp.mk_and(x_is_zero, y_is_zero, both_zero); + expr_ref bv0(m), bv1(m); + bv0 = m_bv_util.mk_numeral(0, 1); + bv1 = m_bv_util.mk_numeral(1, 1); + + expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), xy_are_zero(m); mk_is_nan(x, x_is_nan); mk_is_nan(y, y_is_nan); - mk_pzero(f, pzero); + mk_is_zero(x, x_is_zero); + mk_is_zero(y, y_is_zero); + xy_are_zero = m.mk_and(x_is_zero, y_is_zero); - expr_ref sgn_eq(m), sgn_diff(m); - sgn_eq = m.mk_eq(x_sgn, y_sgn); - sgn_diff = m.mk_not(sgn_eq); + expr_ref x_is_pos(m), x_is_neg(m); + expr_ref y_is_pos(m), y_is_neg(m); + expr_ref pn(m), np(m), pn_or_np_zeros(m); + mk_is_pos(x, x_is_pos); + mk_is_pos(y, y_is_pos); + mk_is_neg(x, x_is_neg); + mk_is_neg(y, y_is_neg); + pn_or_np_zeros = m.mk_and(xy_are_zero, m.mk_not(m.mk_eq(x_sgn, y_sgn))); - expr_ref lt(m); - mk_float_lt(f, num, args, lt); + expr_ref unspec(m); + unspec = mk_min_max_unspecified(f, x, y); - mk_ite(lt, x, y, result); - mk_ite(both_zero, y, result, result); + expr_ref x_lt_y(m); + mk_float_lt(f, num, args, x_lt_y); + + mk_ite(x_lt_y, x, y, result); + mk_ite(xy_are_zero, y, result, result); + mk_ite(pn_or_np_zeros, unspec, result, result); + mk_ite(y_is_nan, x, result, result); + mk_ite(x_is_nan, y, result, result); + + SASSERT(is_well_sorted(m, result)); +} + +void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 2); + unsigned ebits = m_util.get_ebits(f->get_range()); + unsigned sbits = m_util.get_sbits(f->get_range()); + + expr * x = args[0], *y = args[1]; + + expr * x_sgn, *x_sig, *x_exp; + expr * y_sgn, *y_sig, *y_exp; + split_fp(x, x_sgn, x_exp, x_sig); + split_fp(y, y_sgn, y_exp, y_sig); + + expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), xy_are_zero(m); + mk_is_nan(x, x_is_nan); + mk_is_nan(y, y_is_nan); + mk_is_zero(x, x_is_zero); + mk_is_zero(y, y_is_zero); + xy_are_zero = m.mk_and(x_is_zero, y_is_zero); + + expr_ref x_is_pos(m), x_is_neg(m); + expr_ref y_is_pos(m), y_is_neg(m); + expr_ref pn(m), np(m), pn_or_np_zeros(m); + mk_is_pos(x, x_is_pos); + mk_is_pos(y, y_is_pos); + mk_is_neg(x, x_is_neg); + mk_is_neg(y, y_is_neg); + pn_or_np_zeros = m.mk_and(xy_are_zero, m.mk_not(m.mk_eq(x_sgn, y_sgn))); + + expr_ref unspec(m); + unspec = mk_min_max_unspecified(f, x, y); + + expr_ref x_gt_y(m); + mk_float_gt(f, num, args, x_gt_y); + + mk_ite(x_gt_y, x, y, result); + mk_ite(xy_are_zero, y, result, result); + mk_ite(pn_or_np_zeros, unspec, result, result); mk_ite(y_is_nan, x, result, result); mk_ite(x_is_nan, y, result, result); @@ -1281,10 +1277,10 @@ expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr // There is no "hardware interpretation" for fp.min/fp.max. std::pair decls(0, 0); - if (!m_min_max_specials.find(f, decls)) { + if (!m_min_max_ufs.find(f, decls)) { decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_min_max_specials.insert(f, decls); + m_min_max_ufs.insert(f, decls); m.inc_ref(f); m.inc_ref(decls.first); m.inc_ref(decls.second); @@ -1303,68 +1299,6 @@ expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr return res; } -void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - expr_ref x(m), y(m); - x = args[0]; - y = args[1]; - - expr_ref x_is_zero(m), y_is_zero(m), both_are_zero(m); - x_is_zero = m_util.mk_is_zero(x); - y_is_zero = m_util.mk_is_zero(y); - both_are_zero = m.mk_and(x_is_zero, y_is_zero); - - expr_ref x_is_positive(m), x_is_negative(m), y_is_positive(m), y_is_negative(m), pn(m), np(m), pn_or_np(m); - x_is_positive = m_util.mk_is_positive(x); - x_is_negative = m_util.mk_is_negative(x); - y_is_positive = m_util.mk_is_positive(y); - y_is_negative = m_util.mk_is_negative(y); - pn = m.mk_and(x_is_positive, y_is_negative); - np = m.mk_and(x_is_negative, y_is_positive); - pn_or_np = m.mk_or(pn, np); - - expr_ref c(m), v(m); - c = m.mk_and(both_are_zero, pn_or_np); - v = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_UNSPECIFIED, x, y); - - // Note: This requires BR_REWRITE_FULL afterwards. - expr_ref max_i(m); - max_i = m.mk_app(m_util.get_family_id(), OP_FPA_MAX_I, x, y); - m_simp.mk_ite(c, v, max_i, 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]; - - expr * x_sgn, *x_sig, *x_exp; - expr * y_sgn, *y_sig, *y_exp; - split_fp(x, x_sgn, x_exp, x_sig); - split_fp(y, y_sgn, y_exp, y_sig); - - expr_ref x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m), both_zero(m), pzero(m); - mk_is_zero(x, x_is_zero); - mk_is_zero(y, y_is_zero); - m_simp.mk_and(x_is_zero, y_is_zero, both_zero); - mk_is_nan(x, x_is_nan); - mk_is_nan(y, y_is_nan); - mk_pzero(f, pzero); - - expr_ref sgn_diff(m), sgn_eq(m); - sgn_eq = m.mk_eq(x_sgn, y_sgn); - sgn_diff = m.mk_not(sgn_eq); - - expr_ref gt(m); - mk_float_gt(f, num, args, gt); - - mk_ite(gt, x, y, result); - mk_ite(both_zero, y, result, result); - mk_ite(y_is_nan, x, result, result); - mk_ite(x_is_nan, y, result, result); - - SASSERT(is_well_sorted(m, result)); -} - void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 4); SASSERT(m_util.is_bv2rm(args[0])); @@ -3150,19 +3084,12 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * unsigned ebits = m_util.get_ebits(fp_srt); unsigned sbits = m_util.get_sbits(fp_srt); - expr_ref nanv(m); - if (m_hi_fp_unspecified) - // The "hardware interpretation" is 01...10...01. - nanv = 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)))); - else - mk_to_ieee_bv_unspecified(f, num, args, nanv); + expr_ref unspec(m); + mk_to_ieee_bv_unspecified(f, num, args, unspec); expr_ref sgn_e_s(m); join_fp(x, sgn_e_s); - m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result); + m_simp.mk_ite(x_is_nan, unspec, sgn_e_s, result); TRACE("fpa2bv_to_ieee_bv", tout << "result=" << mk_ismt2_pp(result, m) << std::endl;); SASSERT(is_well_sorted(m, result)); @@ -3174,26 +3101,15 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex unsigned ebits = f->get_domain()[0]->get_parameter(0).get_int(); unsigned sbits = f->get_domain()[0]->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)); - } + if (m_hi_fp_unspecified) + mk_nan(f->get_range(), result); else { 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(f_bv); - } - + sort * domain[1] = { m.get_sort(n_bv) }; + func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); result = m.mk_app(f_bv, n_bv); expr_ref exp_bv(m), exp_all_ones(m); @@ -3382,14 +3298,8 @@ void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr * 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(f_bv); - } + sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(n_bv) }; + func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); result = m.mk_app(f_bv, rm_bv, n_bv); } @@ -3407,14 +3317,8 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr 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(f_bv); - } + sort * domain[1] = { m.get_sort(n_bv) }; + func_decl * f_bv = mk_bv_uf(f, domain, f->get_range()); result = m.mk_app(f_bv, n_bv); } } @@ -4190,13 +4094,25 @@ void fpa2bv_converter::reset(void) { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); - for (obj_map >::iterator it = m_min_max_specials.begin(); - it != m_min_max_specials.end(); + for (obj_map >::iterator it = m_min_max_ufs.begin(); + it != m_min_max_ufs.end(); it++) { m.dec_ref(it->m_key); m.dec_ref(it->m_value.first); m.dec_ref(it->m_value.second); } - m_min_max_specials.reset(); + m_min_max_ufs.reset(); m_extra_assertions.reset(); } + +func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) { + func_decl * res; + if (!m_uf2bvuf.find(f, res)) { + res = m.mk_fresh_func_decl(0, f->get_arity(), domain, range); + m_uf2bvuf.insert(f, res); + m.inc_ref(f); + m.inc_ref(res); + TRACE("fpa2bv", tout << "New UF func_decl: " << std::endl << mk_ismt2_pp(res, m) << std::endl;); + } + return res; +} diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index d54adac78..f0e50ba2d 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -53,7 +53,7 @@ protected: const2bv_t m_const2bv; const2bv_t m_rm_const2bv; uf2bvuf_t m_uf2bvuf; - special_t m_min_max_specials; + special_t m_min_max_ufs; friend class fpa2bv_model_converter; friend class bv2fpa_converter; @@ -87,7 +87,7 @@ public: void mk_numeral(sort * s, mpf const & v, expr_ref & result); virtual void mk_const(func_decl * f, expr_ref & result); virtual void mk_rm_const(func_decl * f, expr_ref & result); - virtual void mk_function(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + virtual void mk_uf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_var(unsigned base_inx, sort * srt, expr_ref & result); void mk_pinf(func_decl * f, expr_ref & result); @@ -147,18 +147,15 @@ public: void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } void mk_min(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); - virtual expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y); - void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y); 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; }; + special_t const & get_min_max_specials() const { return m_min_max_ufs; }; const2bv_t const & get_const2bv() const { return m_const2bv; }; const2bv_t const & get_rm_const2bv() const { return m_rm_const2bv; }; uf2bvuf_t const & get_uf2bvuf() const { return m_uf2bvuf; }; @@ -202,12 +199,6 @@ protected: void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result); - sort_ref replace_float_sorts(sort * s); - func_decl_ref replace_function(func_decl * f); - expr_ref replace_float_arg(expr * a); - void mk_function_output(sort * rng, func_decl * fbv, expr * const * new_args, expr_ref & result); - func_decl * get_bv_uf(func_decl * f, sort * bv_rng, unsigned arity); - private: void mk_nan(sort * s, expr_ref & result); void mk_nzero(sort * s, expr_ref & result); @@ -226,6 +217,8 @@ 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); + + func_decl * mk_bv_uf(func_decl * f, sort * const * domain, sort * range); }; #endif diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 07623ec48..6c96d92c1 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -124,6 +124,8 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co 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_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; @@ -147,14 +149,6 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co 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: 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; - - case OP_FPA_MIN_UNSPECIFIED: - case OP_FPA_MAX_UNSPECIFIED: result = m_conv.mk_min_max_unspecified(f, args[0], args[1]); return BR_DONE; - case OP_FPA_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; - case OP_FPA_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; - case OP_FPA_BVWRAP: case OP_FPA_BV2RM: return BR_FAILED; @@ -169,7 +163,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co { SASSERT(!m_conv.is_float_family(f)); if (m_conv.fu().contains_floats(f)) { - m_conv.mk_function(f, num, args, result); + m_conv.mk_uf(f, num, args, result); return BR_DONE; } } diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 9bee51af7..9d298b413 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -361,10 +361,6 @@ 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_MIN_I: name = "fp.min_i"; break; - case OP_FPA_MAX_I: name = "fp.max_i"; break; - case OP_FPA_MIN_UNSPECIFIED: name = "fp.min_unspecified"; break; - case OP_FPA_MAX_UNSPECIFIED: name = "fp.max_unspecified"; break; default: UNREACHABLE(); break; @@ -781,12 +777,6 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, case OP_FPA_BV2RM: return mk_bv2rm(k, num_parameters, parameters, arity, domain, range); - case OP_FPA_MIN_I: - case OP_FPA_MAX_I: - case OP_FPA_MIN_UNSPECIFIED: - case OP_FPA_MAX_UNSPECIFIED: - return mk_binary_decl(k, num_parameters, parameters, arity, domain, range); - default: m_manager->raise_exception("unsupported floating point operator"); return 0; diff --git a/src/ast/fpa_decl_plugin.h b/src/ast/fpa_decl_plugin.h index f59c8f92f..4e86c9d3f 100644 --- a/src/ast/fpa_decl_plugin.h +++ b/src/ast/fpa_decl_plugin.h @@ -89,11 +89,6 @@ enum fpa_op_kind { OP_FPA_BVWRAP, OP_FPA_BV2RM, - OP_FPA_MIN_I, - OP_FPA_MAX_I, - OP_FPA_MIN_UNSPECIFIED, - OP_FPA_MAX_UNSPECIFIED, - LAST_FLOAT_OP }; @@ -351,21 +346,12 @@ public: } 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; } bool is_bv2rm(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BV2RM); } - bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; } - - bool is_min_interpreted(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_MIN_I); } - 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(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_bvwrap(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BVWRAP; } + bool is_bv2rm(func_decl const * f) const { return f->get_family_id() == get_family_id() && f->get_decl_kind() == OP_FPA_BV2RM; } 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; } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 6420dd968..818336c75 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -94,12 +94,6 @@ 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_MIN_I:SASSERT(num_args == 2); st = mk_min_i(f, args[0], args[1], result); break; - case OP_FPA_MAX_I: SASSERT(num_args == 2); st = mk_max_i(f, args[0], args[1], result); break; - case OP_FPA_MIN_UNSPECIFIED: - case OP_FPA_MAX_UNSPECIFIED: - SASSERT(num_args == 2); st = BR_FAILED; break; - 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; @@ -385,38 +379,13 @@ 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 = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); - return BR_REWRITE1; - } - else { - 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_MIN_UNSPECIFIED, arg1, arg2); - - result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MIN_I, arg1, arg2)); - return BR_REWRITE_FULL; - } -} - -br_status fpa_rewriter::mk_min_i(func_decl * f, 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 = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); - else - result = m_util.mk_min(arg1, arg2); + return BR_FAILED; + + scoped_mpf r(m_fm); + m_fm.minimum(v1, v2, r); + result = m_util.mk_value(r); return BR_DONE; } @@ -434,38 +403,13 @@ 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 = m().mk_app(get_fid(), OP_FPA_MAX_UNSPECIFIED, arg1, arg2); - return BR_REWRITE1; - } - else { - 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_MAX_UNSPECIFIED, arg1, arg2); - - result = m().mk_ite(c, v, m().mk_app(get_fid(), OP_FPA_MAX_I, arg1, arg2)); - return BR_REWRITE_FULL; - } -} - -br_status fpa_rewriter::mk_max_i(func_decl * f, 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 = m().mk_app(get_fid(), OP_FPA_MIN_UNSPECIFIED, arg1, arg2); - else - result = m_util.mk_max(arg1, arg2); + return BR_FAILED; + + scoped_mpf r(m_fm); + m_fm.maximum(v1, v2, r); + result = m_util.mk_value(r); return BR_DONE; } diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index d337cc65d..cc9b0017d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -884,22 +884,4 @@ namespace smt { out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl; } } - - bool theory_fpa::include_func_interp(func_decl * f) { - 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) || - 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); - return true; - } - return false; - } - else - return true; - } }; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h index 7be82816e..9e9801ee0 100644 --- a/src/smt/theory_fpa.h +++ b/src/smt/theory_fpa.h @@ -158,7 +158,6 @@ namespace smt { virtual char const * get_name() const { return "fpa"; } virtual model_value_proc * mk_value(enode * n, model_generator & mg); - virtual bool include_func_interp(func_decl * f); void assign_eh(bool_var v, bool is_true); virtual void relevant_eh(app * n); @@ -180,8 +179,6 @@ namespace smt { expr_ref convert_term(expr * e); expr_ref convert_conversion_term(expr * e); - void add_trail(ast * a); - void attach_new_th_var(enode * n); void assert_cnstr(expr * e);