diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index b2b20b8a7..7d2a34ec0 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2783,8 +2783,8 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } -void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++) +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;); SASSERT(f->get_num_parameters() == 1); @@ -2815,25 +2815,34 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg // NaN, Inf, or negative (except -0) -> unspecified expr_ref c1(m), v1(m); - c1 = m.mk_or(x_is_nan, x_is_inf, m.mk_and(x_is_neg, m.mk_not(x_is_nzero))); + 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(bv_sz); + dbg_decouple("fpa2bv_to_bv_c1", c1); // +-Zero -> 0 expr_ref c2(m), v2(m); c2 = x_is_zero; v2 = m_bv_util.mk_numeral(rational(0), bv_srt); - dbg_decouple("fpa2bv_to_ubv_c2", c2); + dbg_decouple("fpa2bv_to_bv_c2", c2); // Otherwise... expr_ref sgn(m), sig(m), exp(m), lz(m); unpack(x, sgn, sig, exp, lz, true); + dbg_decouple("fpa2bv_to_bv_sgn", sgn); + dbg_decouple("fpa2bv_to_bv_sig", sig); + dbg_decouple("fpa2bv_to_bv_exp", exp); + dbg_decouple("fpa2bv_to_bv_lz", lz); + // sig is of the form +- [1].[sig] * 2^(exp-lz) SASSERT(m_bv_util.get_bv_size(sgn) == 1); SASSERT(m_bv_util.get_bv_size(sig) == sbits); SASSERT(m_bv_util.get_bv_size(exp) == ebits); - SASSERT(m_bv_util.get_bv_size(lz) == ebits); - dbg_decouple("fpa2bv_to_ubv_sig", sig); + SASSERT(m_bv_util.get_bv_size(lz) == ebits); + unsigned sig_sz = m_bv_util.get_bv_size(sig); SASSERT(sig_sz == sbits); if (sig_sz < (bv_sz + 3)) @@ -2841,35 +2850,38 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg sig_sz = m_bv_util.get_bv_size(sig); SASSERT(sig_sz >= (bv_sz + 3)); - expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m); + expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m); exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_zero_extend(2, lz)); - shift = m_bv_util.mk_bv_sub(exp_m_lz, - m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); - shift_neg = m_bv_util.mk_bv_neg(shift); + e_m_lz_m_bv_sz = m_bv_util.mk_bv_sub(exp_m_lz, + m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); + shift = m_bv_util.mk_bv_neg(e_m_lz_m_bv_sz); bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); - shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift); + shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), e_m_lz_m_bv_sz, shift); SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2); SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2); - dbg_decouple("fpa2bv_to_ubv_shift", shift); - dbg_decouple("fpa2bv_to_ubv_shift_abs", shift_abs); + dbg_decouple("fpa2bv_to_bv_shift", shift); + dbg_decouple("fpa2bv_to_bv_shift_abs", shift_abs); // x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // [1][ ... sig ... ][r][g][ ... s ...] // [ ... ubv ... ][r][g][ ... s ... ] - expr_ref max_shift(m); - max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); + shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); expr_ref c_in_limits(m); - c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2)); - dbg_decouple("fpa2bv_to_ubv_in_limits", c_in_limits); + if (!is_signed) + c_in_limits = m_bv_util.mk_sle(bv0_e2, shift); + else + c_in_limits = m.mk_or(m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift), + m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift), + m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sbits-1))))); + dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits); expr_ref shifted_sig(m); shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs); - dbg_decouple("fpa2bv_to_ubv_shifted_sig", shifted_sig); + dbg_decouple("fpa2bv_to_bv_shifted_sig", shifted_sig); expr_ref last(m), round(m), sticky(m); last = m_bv_util.mk_extract(sig_sz - bv_sz - 0, sig_sz - bv_sz - 0, shifted_sig); @@ -2878,25 +2890,32 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg m_bv_util.mk_numeral(0, sig_sz - (bv_sz + 3) + 2)), bv0, bv1); - dbg_decouple("fpa2bv_to_ubv_last", last); - dbg_decouple("fpa2bv_to_ubv_round", round); - dbg_decouple("fpa2bv_to_ubv_sticky", sticky); + dbg_decouple("fpa2bv_to_bv_last", last); + dbg_decouple("fpa2bv_to_bv_round", round); + dbg_decouple("fpa2bv_to_bv_sticky", sticky); expr_ref rounding_decision(m); rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky); SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1); - dbg_decouple("fpa2bv_to_ubv_rounding_decision", rounding_decision); + dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision); expr_ref unrounded_sig(m), pre_rounded(m), inc(m); unrounded_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz, shifted_sig)); inc = m_bv_util.mk_zero_extend(1, m_bv_util.mk_zero_extend(bv_sz - 1, rounding_decision)); pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc); + dbg_decouple("fpa2bv_to_bv_inc", inc); + dbg_decouple("fpa2bv_to_bv_pre_rounded", pre_rounded); expr_ref rnd_overflow(m), rnd(m), rnd_has_overflown(m); rnd_overflow = m_bv_util.mk_extract(bv_sz, bv_sz, pre_rounded); rnd = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded); rnd_has_overflown = m.mk_eq(rnd_overflow, bv1); - dbg_decouple("fpa2bv_to_ubv_rnd_has_overflown", rnd_has_overflown); + dbg_decouple("fpa2bv_to_bv_rnd_has_overflown", rnd_has_overflown); + + if (is_signed) + rnd = m.mk_ite(m.mk_eq(sgn, bv1), m_bv_util.mk_bv_neg(rnd), rnd); + + dbg_decouple("fpa2bv_to_bv_rnd", rnd); result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(bv_sz), rnd); result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(bv_sz)); @@ -2906,160 +2925,16 @@ void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * arg SASSERT(is_well_sorted(m, result)); } +void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); + mk_to_bv(f, num, args, false, result); +} + void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { TRACE("fpa2bv_to_sbv", for (unsigned i = 0; i < num; i++) tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); - - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_int()); - SASSERT(num == 2); - SASSERT(m_bv_util.get_bv_size(args[0]) == 3); - SASSERT(m_util.is_float(args[1])); - - expr * rm = args[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(); - - expr_ref bv0(m), bv1(m), bv0_2(m), bv1_2(m), bv3_2(m); - bv0 = m_bv_util.mk_numeral(0, 1); - bv1 = m_bv_util.mk_numeral(1, 1); - bv0_2 = m_bv_util.mk_numeral(0, 2); - bv1_2 = m_bv_util.mk_numeral(1, 2); - bv3_2 = m_bv_util.mk_numeral(3, 2); - - 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 -> unspecified - expr_ref c1(m), v1(m); - c1 = m.mk_or(x_is_nan, x_is_inf); - v1 = mk_to_sbv_unspecified(bv_sz); - dbg_decouple("fpa2bv_to_sbv_c1", c1); - - // +-Zero -> 0 - expr_ref c2(m), v2(m); - c2 = x_is_zero; - v2 = m_bv_util.mk_numeral(rational(0), bv_srt); - dbg_decouple("fpa2bv_to_sbv_c2", c2); - - // Otherwise... - expr_ref sgn(m), sig(m), exp(m), lz(m); - unpack(x, sgn, sig, exp, lz, true); - - dbg_decouple("fpa2bv_to_sbv_sgn", sgn); - dbg_decouple("fpa2bv_to_sbv_sig", sig); - dbg_decouple("fpa2bv_to_sbv_exp", exp); - - // x is of the form +- [1].[sig] * 2^(exp-lz) - SASSERT(m_bv_util.get_bv_size(sgn) == 1); - SASSERT(m_bv_util.get_bv_size(sig) == sbits); - SASSERT(m_bv_util.get_bv_size(exp) == ebits); - SASSERT(m_bv_util.get_bv_size(lz) == ebits); - dbg_decouple("fpa2bv_to_sbv_sig", sig); - unsigned sig_sz = m_bv_util.get_bv_size(sig); - SASSERT(sig_sz == sbits); - if (sig_sz < (bv_sz + 3)) - sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, bv_sz - sig_sz + 3)); - sig_sz = m_bv_util.get_bv_size(sig); - SASSERT(sig_sz >= (bv_sz + 3)); - - expr_ref exp_m_lz(m), shift(m), shift_neg(m), bv0_e2(m), shift_abs(m), shift_neg_dec(m); - exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), - m_bv_util.mk_zero_extend(2, lz)); - shift = m_bv_util.mk_bv_sub(exp_m_lz, - m_bv_util.mk_numeral(bv_sz, ebits + 2)); - shift_neg = m_bv_util.mk_bv_neg(shift); - bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); - shift_neg_dec = m_bv_util.mk_sle(shift, bv0_e2); - shift_abs = m.mk_ite(shift_neg_dec, shift_neg, shift); - SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(shift_neg) == ebits + 2); - SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2); - dbg_decouple("fpa2bv_to_sbv_shift", shift); - - // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long - // [1][ ... sig ... ][r][g][ ... s ...] - // [ ... ubv ... ][r][g][ ... s ... ] - // expr_ref max_shift(m); - // max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); - shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); - SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); - dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); - - expr_ref c_in_limits(m); - c_in_limits = m_bv_util.mk_sle(shift, m_bv_util.mk_numeral(0, ebits + 2)); - dbg_decouple("fpa2bv_to_sbv_in_limits", c_in_limits); - - expr_ref huge_sig(m), huge_shift(m), huge_shifted_sig(m); - huge_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, sig_sz)); - huge_shift = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sig_sz), shift_abs); - huge_shifted_sig = m.mk_ite(shift_neg_dec, - m_bv_util.mk_bv_shl(huge_sig, huge_shift), - m_bv_util.mk_bv_lshr(huge_sig, huge_shift)); - dbg_decouple("fpa2bv_to_sbv_huge_shifted_sig", huge_shifted_sig); - SASSERT(m_bv_util.get_bv_size(huge_shifted_sig) == 2 * sig_sz); - - expr_ref upper_hss(m), lower_hss(m); - upper_hss = m_bv_util.mk_extract(2 * sig_sz - 1, sig_sz + 1, huge_shifted_sig); - lower_hss = m_bv_util.mk_extract(sig_sz, 0, huge_shifted_sig); - SASSERT(m_bv_util.get_bv_size(upper_hss) == sig_sz - 1); - SASSERT(m_bv_util.get_bv_size(lower_hss) == sig_sz + 1); - dbg_decouple("fpa2bv_to_sbv_upper_hss", upper_hss); - dbg_decouple("fpa2bv_to_sbv_lower_hss", lower_hss); - - expr_ref last(m), round(m), sticky(m); - last = m_bv_util.mk_extract(1, 1, upper_hss); - round = m_bv_util.mk_extract(0, 0, upper_hss); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lower_hss.get()); - dbg_decouple("fpa2bv_to_sbv_last", last); - dbg_decouple("fpa2bv_to_sbv_round", round); - dbg_decouple("fpa2bv_to_sbv_sticky", sticky); - - expr_ref upper_hss_w_sticky(m); - upper_hss_w_sticky = m_bv_util.mk_concat(upper_hss, sticky); - dbg_decouple("fpa2bv_to_sbv_upper_hss_w_sticky", upper_hss_w_sticky); - SASSERT(m_bv_util.get_bv_size(upper_hss_w_sticky) == sig_sz); - - expr_ref rounding_decision(m); - rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky); - SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1); - dbg_decouple("fpa2bv_to_sbv_rounding_decision", rounding_decision); - - expr_ref unrounded_sig(m), pre_rounded(m), inc(m); - unrounded_sig = m_bv_util.mk_extract(sig_sz - 1, sig_sz - bv_sz - 1, upper_hss_w_sticky); - inc = m_bv_util.mk_zero_extend(bv_sz, rounding_decision); - pre_rounded = m_bv_util.mk_bv_add(unrounded_sig, inc); - dbg_decouple("fpa2bv_to_sbv_inc", inc); - dbg_decouple("fpa2bv_to_sbv_unrounded_sig", unrounded_sig); - dbg_decouple("fpa2bv_to_sbv_pre_rounded", pre_rounded); - - expr_ref rnd_overflow(m), rnd_abs(m), rnd_signed(m), rnd_has_overflown(m), extra_neg(m); - rnd_overflow = m_bv_util.mk_extract(bv_sz, bv_sz - 1, pre_rounded); - rnd_abs = m_bv_util.mk_extract(bv_sz - 1, 0, pre_rounded); - rnd_signed = m.mk_ite(m.mk_eq(sgn, bv1), m_bv_util.mk_bv_neg(rnd_abs), rnd_abs); - extra_neg = m_bv_util.mk_numeral(fu().fm().m_powers2(bv_sz-1), bv_sz+1); - rnd_has_overflown = m.mk_and(m.mk_not(m.mk_eq(rnd_overflow, bv0_2)), - m.mk_not(m.mk_and(m.mk_eq(sgn, bv1), m.mk_eq(pre_rounded, extra_neg)))); - dbg_decouple("fpa2bv_to_sbv_extra_neg", extra_neg); - dbg_decouple("fpa2bv_to_sbv_rnd_overflow", rnd_overflow); - dbg_decouple("fpa2bv_to_sbv_rnd_abs", rnd_abs); - dbg_decouple("fpa2bv_to_sbv_rnd_has_overflown", rnd_has_overflown); - - result = m.mk_ite(rnd_has_overflown, mk_to_sbv_unspecified(bv_sz), rnd_signed); - result = m.mk_ite(c_in_limits, result, mk_to_sbv_unspecified(bv_sz)); - result = m.mk_ite(c2, v2, result); - result = m.mk_ite(c1, v1, result); - - SASSERT(is_well_sorted(m, result)); + mk_to_bv(f, num, args, true, result); } expr_ref fpa2bv_converter::mk_to_ubv_unspecified(unsigned width) { @@ -3326,7 +3201,7 @@ void fpa2bv_converter::mk_unbias(expr * e, expr_ref & result) { expr_ref e_plus_one(m); e_plus_one = m_bv_util.mk_bv_add(e, m_bv_util.mk_numeral(1, ebits)); - + expr_ref leading(m), n_leading(m), rest(m); leading = m_bv_util.mk_extract(ebits-1, ebits-1, e_plus_one); n_leading = m_bv_util.mk_bv_not(leading); @@ -3350,6 +3225,10 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref SASSERT(m_bv_util.get_bv_size(exp) == ebits); SASSERT(m_bv_util.get_bv_size(sig) == sbits-1); + dbg_decouple("fpa2bv_unpack_sgn", sgn); + dbg_decouple("fpa2bv_unpack_exp", exp); + dbg_decouple("fpa2bv_unpack_sig", sig); + expr_ref is_normal(m); mk_is_normal(e, is_normal); @@ -3359,8 +3238,7 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref dbg_decouple("fpa2bv_unpack_normal_exp", normal_exp); expr_ref denormal_sig(m), denormal_exp(m); - denormal_sig = m_bv_util.mk_zero_extend(1, sig); - // SASSERT(ebits >= 3); // Note: when ebits=2 there is no 1-exponent, so mk_unbias will produce a 0. + denormal_sig = m_bv_util.mk_zero_extend(1, sig); denormal_exp = m_bv_util.mk_numeral(1, ebits); mk_unbias(denormal_exp, denormal_exp); dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 7113319d8..7127c9b69 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -186,7 +186,9 @@ protected: expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp, expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp); - app * mk_fresh_const(char const * prefix, unsigned sz); + app * mk_fresh_const(char const * prefix, unsigned sz); + + void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result); }; #endif