diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index d2431174e8..c8a681a369 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2776,13 +2776,12 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * else { SASSERT(!m_arith_util.is_numeral(x)); bv_util & bu = m_bv_util; - arith_util & au = m_arith_util; expr_ref bv0(m), bv1(m), zero(m), two(m); bv0 = bu.mk_numeral(0, 1); bv1 = bu.mk_numeral(1, 1); - zero = au.mk_numeral(rational(0), false); - two = au.mk_numeral(rational(2), false); + zero = m_arith_util.mk_numeral(rational(0), false); + two = m_arith_util.mk_numeral(rational(2), false); expr_ref sgn(m), sig(m), exp(m); sgn = mk_fresh_const("fpa2bv_to_fp_real_sgn", 1); @@ -2792,9 +2791,6 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref rme(bv_rm, m); round(s, rme, sgn, sig, exp, result); - expr * e = m.mk_eq(m_util.mk_to_real(result), x); - m_extra_assertions.push_back(e); - expr_ref r_is_nan(m); mk_is_nan(result, r_is_nan); m_extra_assertions.push_back(m.mk_not(r_is_nan)); @@ -2808,10 +2804,6 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * max_real = max_sig * rational(m_mpf_manager.m_powers2(max_exp)); TRACE(fpa2bv_to_real, tout << "max exp: " << max_exp << " max real: " << max_real << std::endl;); - expr_ref r_is_pinf(m), r_is_ninf(m); - mk_is_pinf(result, r_is_pinf); - mk_is_ninf(result, r_is_ninf); - expr_ref e_max_real(m), e_max_real_neg(m); e_max_real = m_arith_util.mk_numeral(max_real, false); e_max_real_neg = m_arith_util.mk_numeral(-max_real, false); @@ -2823,6 +2815,124 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_tn); mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_tz); + expr_ref r_is_pinf(m), r_is_ninf(m), r_is_zero(m), r_is_neg(m); + mk_is_pinf(result, r_is_pinf); + mk_is_ninf(result, r_is_ninf); + mk_is_zero(result, r_is_zero); + mk_is_neg(result, r_is_neg); + + expr_ref r_sgn(m), r_exp(m), r_sig(m); + split_fp(result, r_sgn, r_exp, r_sig); + + unsigned total_bits = ebits + sbits; + expr_ref sign_mask(m), bv_one(m); + sign_mask = m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, total_bits - 1)); + bv_one = m_bv_util.mk_numeral(1, total_bits); + + expr_ref r_bv(m); + r_bv = m_bv_util.mk_concat({ r_sgn, r_exp, r_sig }); + + // Map IEEE-754 bit patterns to a monotone key for numeric ordering: + // - negative values: bitwise-not + // - non-negative values: flip sign bit + // This makes adjacent keys correspond to adjacent representable values. + auto mk_ordered_key = [&](expr* bv, expr_ref& key) { + expr_ref sign(m), is_neg(m), bv_not(m), bv_flip(m); + sign = m_bv_util.mk_extract(total_bits - 1, total_bits - 1, bv); + is_neg = m.mk_eq(sign, bv1); + bv_not = m_bv_util.mk_bv_not(bv); + bv_flip = m_bv_util.mk_bv_xor(bv, sign_mask); + key = m.mk_ite(is_neg, bv_not, bv_flip); + }; + + // Inverse of mk_ordered_key: recover IEEE-754 bits from the monotone key. + // Keys with top bit 1 decode as non-negative values (flip sign bit back), + // keys with top bit 0 decode as negative values (bitwise-not). + auto mk_from_ordered_key = [&](expr* key, expr_ref& bv) { + expr_ref sign(m), is_pos(m), bv_not(m), bv_flip(m); + sign = m_bv_util.mk_extract(total_bits - 1, total_bits - 1, key); + is_pos = m.mk_eq(sign, bv1); + bv_not = m_bv_util.mk_bv_not(key); + bv_flip = m_bv_util.mk_bv_xor(key, sign_mask); + bv = m.mk_ite(is_pos, bv_flip, bv_not); + }; + + expr_ref r_key(m), prev_key(m), next_key(m), prev_bv(m), next_bv(m); + mk_ordered_key(r_bv, r_key); + prev_key = m_bv_util.mk_bv_sub(r_key, bv_one); + next_key = m_bv_util.mk_bv_add(r_key, bv_one); + mk_from_ordered_key(prev_key, prev_bv); + mk_from_ordered_key(next_key, next_bv); + + // Build an FP value from IEEE-754 layout in 'bv': + // [MSB]=sign, then exponent bits, then significand bits. + auto mk_fp_from_bv = [&](expr* bv, expr_ref& fp) { + fp = m_util.mk_fp(m_bv_util.mk_extract(total_bits - 1, total_bits - 1, bv), + m_bv_util.mk_extract(total_bits - 2, sbits - 1, bv), + m_bv_util.mk_extract(sbits - 2, 0, bv)); + }; + + expr_ref prev_fp(m), next_fp(m); + mk_fp_from_bv(prev_bv, prev_fp); + mk_fp_from_bv(next_bv, next_fp); + + expr_ref prev_is_inf(m), next_is_inf(m); + mk_is_inf(prev_fp, prev_is_inf); + mk_is_inf(next_fp, next_is_inf); + + expr_ref r_real(m), prev_real(m), next_real(m); + r_real = m_util.mk_to_real(result); + prev_real = m_util.mk_to_real(prev_fp); + next_real = m_util.mk_to_real(next_fp); + + expr_ref half(m), lower_mid(m), upper_mid(m); + half = m_arith_util.mk_numeral(rational(1, 2), false); + lower_mid = m_arith_util.mk_mul(half, m_arith_util.mk_add(prev_real, r_real)); + upper_mid = m_arith_util.mk_mul(half, m_arith_util.mk_add(r_real, next_real)); + + expr_ref is_even(m), sig_lsb(m); + sig_lsb = m_bv_util.mk_extract(0, 0, r_sig); + is_even = m.mk_eq(sig_lsb, bv0); + + expr_ref tie_away_lower(m), tie_away_upper(m); + // For RNA ties, pick the value farther from zero: + // lower tie is selected only for positive non-zero results, + // upper tie is selected only for negative non-zero results. + tie_away_lower = m.mk_and(m.mk_not(r_is_neg), m.mk_not(r_is_zero)); + tie_away_upper = m.mk_and(r_is_neg, m.mk_not(r_is_zero)); + + expr_ref prev_lt_x(m), prev_lt_x_or_tie_even(m), prev_lt_x_or_tie_away(m); + prev_lt_x = m_arith_util.mk_lt(prev_real, x); + prev_lt_x_or_tie_even = m.mk_or(m_arith_util.mk_lt(lower_mid, x), m.mk_and(m.mk_eq(x, lower_mid), is_even)); + prev_lt_x_or_tie_away = m.mk_or(m_arith_util.mk_lt(lower_mid, x), m.mk_and(m.mk_eq(x, lower_mid), tie_away_lower)); + prev_lt_x = m.mk_ite(prev_is_inf, m.mk_true(), prev_lt_x); + prev_lt_x_or_tie_even = m.mk_ite(prev_is_inf, m.mk_true(), prev_lt_x_or_tie_even); + prev_lt_x_or_tie_away = m.mk_ite(prev_is_inf, m.mk_true(), prev_lt_x_or_tie_away); + + expr_ref x_lt_next(m), x_lt_next_or_tie_even(m), x_lt_next_or_tie_away(m); + x_lt_next = m_arith_util.mk_lt(x, next_real); + x_lt_next_or_tie_even = m.mk_or(m_arith_util.mk_lt(x, upper_mid), m.mk_and(m.mk_eq(x, upper_mid), is_even)); + x_lt_next_or_tie_away = m.mk_or(m_arith_util.mk_lt(x, upper_mid), m.mk_and(m.mk_eq(x, upper_mid), tie_away_upper)); + x_lt_next = m.mk_ite(next_is_inf, m.mk_true(), x_lt_next); + x_lt_next_or_tie_even = m.mk_ite(next_is_inf, m.mk_true(), x_lt_next_or_tie_even); + x_lt_next_or_tie_away = m.mk_ite(next_is_inf, m.mk_true(), x_lt_next_or_tie_away); + + expr_ref rtp_ok(m), rtn_ok(m), rtz_ok(m), rna_ok(m), rne_ok(m); + rtp_ok = m.mk_and(m_arith_util.mk_le(x, r_real), prev_lt_x); + rtn_ok = m.mk_and(m_arith_util.mk_le(r_real, x), x_lt_next); + rtz_ok = m.mk_ite(r_is_neg, m.mk_and(prev_lt_x, m_arith_util.mk_le(x, r_real)), + m.mk_and(m_arith_util.mk_le(r_real, x), x_lt_next)); + rna_ok = m.mk_and(prev_lt_x_or_tie_away, x_lt_next_or_tie_away); + rne_ok = m.mk_and(prev_lt_x_or_tie_even, x_lt_next_or_tie_even); + + expr_ref finite_result(m), finite_round_ok(m); + finite_result = m.mk_not(m.mk_or(r_is_pinf, r_is_ninf)); + finite_round_ok = m.mk_ite(rm_tp, rtp_ok, + m.mk_ite(rm_tn, rtn_ok, + m.mk_ite(rm_tz, rtz_ok, + m.mk_ite(rm_nta, rna_ok, rne_ok)))); + m_extra_assertions.push_back(m.mk_implies(finite_result, finite_round_ok)); + // IEEE 754: RNE/RNA carry all overflows to infinity with the sign of the result. // RTP carries positive overflow to +inf, RTN carries negative overflow to -inf. expr_ref rm_rounds_to_pinf(m), rm_rounds_to_ninf(m); diff --git a/src/test/fpa.cpp b/src/test/fpa.cpp index 632865cee6..2fc9ce0cde 100644 --- a/src/test/fpa.cpp +++ b/src/test/fpa.cpp @@ -95,8 +95,36 @@ static void test_recfun_defined_function_soundness() { false); } +static void test_to_fp_from_to_real_roundtrip() { + run_fp_test( + "(declare-fun a () Float32)\n" + "(declare-fun t () Float32)\n" + "(assert (fp.eq a ((_ to_fp 8 24) RNE 1.0)))\n" + "(assert (fp.eq t ((_ to_fp 8 24) RNE 0.8)))\n" + "(assert (fp.eq (fp.add RNE a t) ((_ to_fp 8 24) RNE (+ 1.0 (fp.to_real t)))))\n" + "(check-sat)\n", + true); +} + +static void test_to_fp_from_to_real_roundtrip_with_aliases() { + run_fp_test( + "(declare-fun a () Float32)\n" + "(declare-fun t () Float32)\n" + "(declare-fun one () Float32)\n" + "(declare-fun c08 () Float32)\n" + "(assert (= one ((_ to_fp 8 24) RNE 1.0)))\n" + "(assert (= c08 ((_ to_fp 8 24) RNE 0.8)))\n" + "(assert (fp.eq a one))\n" + "(assert (fp.eq t c08))\n" + "(assert (fp.eq (fp.add RNE a t) ((_ to_fp 8 24) RNE (+ 1.0 (fp.to_real t)))))\n" + "(check-sat)\n", + true); +} + void tst_fpa() { test_fp_to_real_denormal(); test_to_fp_from_real_interval(); test_recfun_defined_function_soundness(); + test_to_fp_from_to_real_roundtrip(); + test_to_fp_from_to_real_roundtrip_with_aliases(); }