diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 94538861d..d51e34058 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1873,7 +1873,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args m_arith_util.is_numeral(args[1]) && m_arith_util.is_numeral(args[2])) { - // Three arguments, some of them are not numerals. + // rm + real + int -> float SASSERT(m_util.is_float(f->get_range())); unsigned ebits = m_util.get_ebits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range()); @@ -1926,191 +1926,197 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args else if (num == 1 && m_bv_util.is_bv(args[0])) { sort * s = f->get_range(); unsigned to_sbits = m_util.get_sbits(s); - unsigned to_ebits = m_util.get_ebits(s); + unsigned to_ebits = m_util.get_ebits(s); expr * bv = args[0]; int sz = m_bv_util.get_bv_size(bv); SASSERT((unsigned)sz == to_sbits + to_ebits); - + mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv), m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), result); } - else if (num == 2 && + else if (num == 2 && + m_util.is_rm(args[0]) && is_app(args[1]) && - m_util.is_float(m.get_sort(args[1]))) { - // We also support float to float conversion - sort * s = f->get_range(); - expr_ref rm(m), x(m); - rm = args[0]; - x = args[1]; - - unsigned from_sbits = m_util.get_sbits(m.get_sort(x)); - unsigned from_ebits = m_util.get_ebits(m.get_sort(x)); - unsigned to_sbits = m_util.get_sbits(s); - unsigned to_ebits = m_util.get_ebits(s); - - if (from_sbits == to_sbits && from_ebits == to_ebits) - result = x; - else { - expr_ref c1(m), c2(m), c3(m), c4(m), c5(m); - expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m); - expr_ref one1(m); - - one1 = m_bv_util.mk_numeral(1, 1); - expr_ref ninf(m), pinf(m); - mk_pinf(f, pinf); - mk_ninf(f, ninf); - - // NaN -> NaN - mk_is_nan(x, c1); - mk_nan(f, v1); - - // +0 -> +0 - mk_is_pzero(x, c2); - mk_pzero(f, v2); - - // -0 -> -0 - mk_is_nzero(x, c3); - mk_nzero(f, v3); - - // +oo -> +oo - mk_is_pinf(x, c4); - v4 = pinf; - - // -oo -> -oo - mk_is_ninf(x, c5); - v5 = ninf; - - // otherwise: the actual conversion with rounding. - expr_ref sgn(m), sig(m), exp(m), lz(m); - unpack(x, sgn, sig, exp, lz, true); - - dbg_decouple("fpa2bv_to_float_x_sig", sig); - dbg_decouple("fpa2bv_to_float_x_exp", exp); - dbg_decouple("fpa2bv_to_float_lz", lz); - - expr_ref res_sgn(m), res_sig(m), res_exp(m); - - res_sgn = sgn; - - SASSERT(m_bv_util.get_bv_size(sgn) == 1); - SASSERT(m_bv_util.get_bv_size(sig) == from_sbits); - SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); - SASSERT(m_bv_util.get_bv_size(lz) == from_ebits); - - if (from_sbits < (to_sbits + 3)) - { - // make sure that sig has at least to_sbits + 3 - res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits)); - } - else if (from_sbits > (to_sbits + 3)) - { - // collapse the extra bits into a sticky bit. - expr_ref sticky(m), low(m), high(m); - low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); - high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); - sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); - res_sig = m_bv_util.mk_concat(high, sticky); - } - else - res_sig = sig; - - res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder. - unsigned sig_sz = m_bv_util.get_bv_size(res_sig); - SASSERT(sig_sz == to_sbits+4); - - expr_ref exponent_overflow(m); - exponent_overflow = m.mk_false(); - - if (from_ebits < (to_ebits + 2)) - { - res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp); - - // subtract lz for subnormal numbers. - expr_ref lz_ext(m); - lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz); - res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); - } - else if (from_ebits > (to_ebits + 2)) - { - expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); - expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m); - high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp); - low = m_bv_util.mk_extract(to_ebits+1, 0, exp); - lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low); - - high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get()); - high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); - - zero1 = m_bv_util.mk_numeral(0, 1); - m_simp.mk_eq(high_red_and, one1, h_and_eq); - m_simp.mk_eq(high_red_or, zero1, h_or_eq); - m_simp.mk_eq(lows, zero1, s_is_zero); - m_simp.mk_eq(lows, one1, s_is_one); - - expr_ref c2(m); - m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2); - m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow); - - // Note: Upon overflow, we _could_ try to shift the significand around... - - // subtract lz for subnormal numbers. - expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m); - lz_ext = m_bv_util.mk_extract(to_ebits+1, 0, lz); - lz_rest = m_bv_util.mk_extract(from_ebits-1, to_ebits+2, lz); - lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get()); - m_simp.mk_eq(lz_redor, one1, lz_redor_bool); - m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow); - - res_exp = m_bv_util.mk_bv_sub(low, lz_ext); - } - else // from_ebits == (to_ebits + 2) - res_exp = m_bv_util.mk_bv_sub(exp, lz); - - SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); - SASSERT(is_well_sorted(m, res_exp)); - - dbg_decouple("fpa2bv_to_float_res_sig", res_sig); - dbg_decouple("fpa2bv_to_float_res_exp", res_exp); - - expr_ref rounded(m); - round(s, rm, res_sgn, res_sig, res_exp, rounded); - - expr_ref is_neg(m), sig_inf(m); - m_simp.mk_eq(sgn, one1, is_neg); - mk_ite(is_neg, ninf, pinf, sig_inf); - - dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); - mk_ite(exponent_overflow, sig_inf, rounded, v6); - - // And finally, we tie them together. - mk_ite(c5, v5, v6, result); - mk_ite(c4, v4, result, result); - mk_ite(c3, v3, result, result); - mk_ite(c2, v2, result, result); - mk_ite(c1, v1, result, result); - } + m_util.is_float(m.get_sort(args[1]))) { + // float -> float conversion + mk_to_fp_float(f, f->get_range(), args[0], args[1], result); } - else if (num == 2 && + else if (num == 2 && m_util.is_rm(args[0]), m_arith_util.is_real(args[1])) { - // .. other than that, we only support rationals for to_fp - SASSERT(m_util.is_float(f->get_range())); - unsigned ebits = m_util.get_ebits(f->get_range()); - unsigned sbits = m_util.get_sbits(f->get_range()); + // rm + real -> float + mk_to_fp_real(f, f->get_range(), args[0], args[1], result); + } + else + UNREACHABLE(); - SASSERT(m_bv_util.is_numeral(args[0])); + SASSERT(is_well_sorted(m, result)); +} + +void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { + unsigned from_sbits = m_util.get_sbits(m.get_sort(x)); + unsigned from_ebits = m_util.get_ebits(m.get_sort(x)); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + if (from_sbits == to_sbits && from_ebits == to_ebits) + result = x; + else { + expr_ref c1(m), c2(m), c3(m), c4(m), c5(m); + expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m); + expr_ref one1(m); + + one1 = m_bv_util.mk_numeral(1, 1); + expr_ref ninf(m), pinf(m); + mk_pinf(f, pinf); + mk_ninf(f, ninf); + + // NaN -> NaN + mk_is_nan(x, c1); + mk_nan(f, v1); + + // +0 -> +0 + mk_is_pzero(x, c2); + mk_pzero(f, v2); + + // -0 -> -0 + mk_is_nzero(x, c3); + mk_nzero(f, v3); + + // +oo -> +oo + mk_is_pinf(x, c4); + v4 = pinf; + + // -oo -> -oo + mk_is_ninf(x, c5); + v5 = ninf; + + // otherwise: the actual conversion with rounding. + expr_ref sgn(m), sig(m), exp(m), lz(m); + unpack(x, sgn, sig, exp, lz, true); + + dbg_decouple("fpa2bv_to_float_x_sig", sig); + dbg_decouple("fpa2bv_to_float_x_exp", exp); + dbg_decouple("fpa2bv_to_float_lz", lz); + + expr_ref res_sgn(m), res_sig(m), res_exp(m); + + res_sgn = sgn; + + SASSERT(m_bv_util.get_bv_size(sgn) == 1); + SASSERT(m_bv_util.get_bv_size(sig) == from_sbits); + SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); + SASSERT(m_bv_util.get_bv_size(lz) == from_ebits); + + if (from_sbits < (to_sbits + 3)) { + // make sure that sig has at least to_sbits + 3 + res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits + 3 - from_sbits)); + } + else if (from_sbits >(to_sbits + 3)) { + // collapse the extra bits into a sticky bit. + expr_ref sticky(m), low(m), high(m); + low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig); + high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get()); + res_sig = m_bv_util.mk_concat(high, sticky); + } + else + res_sig = sig; + + res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder. + unsigned sig_sz = m_bv_util.get_bv_size(res_sig); + SASSERT(sig_sz == to_sbits + 4); + + expr_ref exponent_overflow(m); + exponent_overflow = m.mk_false(); + + if (from_ebits < (to_ebits + 2)) { + res_exp = m_bv_util.mk_sign_extend(to_ebits - from_ebits + 2, exp); + + // subtract lz for subnormal numbers. + expr_ref lz_ext(m); + lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz); + res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext); + } + else if (from_ebits >(to_ebits + 2)) { + expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m); + expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m); + high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp); + low = m_bv_util.mk_extract(to_ebits + 1, 0, exp); + lows = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low); + + high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get()); + high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get()); + + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(high_red_and, one1, h_and_eq); + m_simp.mk_eq(high_red_or, zero1, h_or_eq); + m_simp.mk_eq(lows, zero1, s_is_zero); + m_simp.mk_eq(lows, one1, s_is_one); + + expr_ref c2(m); + m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2); + m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow); + + // Note: Upon overflow, we _could_ try to shift the significand around... + + // subtract lz for subnormal numbers. + expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m); + lz_ext = m_bv_util.mk_extract(to_ebits + 1, 0, lz); + lz_rest = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, lz); + lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get()); + m_simp.mk_eq(lz_redor, one1, lz_redor_bool); + m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow); + + res_exp = m_bv_util.mk_bv_sub(low, lz_ext); + } + else // from_ebits == (to_ebits + 2) + res_exp = m_bv_util.mk_bv_sub(exp, lz); + + SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits + 2); + SASSERT(is_well_sorted(m, res_exp)); + + dbg_decouple("fpa2bv_to_float_res_sig", res_sig); + dbg_decouple("fpa2bv_to_float_res_exp", res_exp); + + expr_ref rounded(m); + round(s, expr_ref (rm, m), res_sgn, res_sig, res_exp, rounded); + + expr_ref is_neg(m), sig_inf(m); + m_simp.mk_eq(sgn, one1, is_neg); + mk_ite(is_neg, ninf, pinf, sig_inf); + + dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow); + mk_ite(exponent_overflow, sig_inf, rounded, v6); + + // And finally, we tie them together. + mk_ite(c5, v5, v6, result); + mk_ite(c4, v4, result, result); + mk_ite(c3, v3, result, result); + mk_ite(c2, v2, result, result); + mk_ite(c1, v1, result, result); + } + + SASSERT(is_well_sorted(m, result)); +} + +void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) { + SASSERT(m_util.is_float(s)); + unsigned ebits = m_util.get_ebits(s); + unsigned sbits = m_util.get_sbits(s); + + if (m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) { rational tmp_rat; unsigned sz; - m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz); + m_bv_util.is_numeral(to_expr(rm), tmp_rat, sz); SASSERT(tmp_rat.is_int32()); SASSERT(sz == 3); BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned(); mpf_rounding_mode rm; - switch (bv_rm) - { + switch (bv_rm) { case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break; case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break; case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break; @@ -2119,10 +2125,8 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args default: UNREACHABLE(); } - SASSERT(m_util.au().is_numeral(args[1])); - rational q; - m_util.au().is_numeral(args[1], q); + m_util.au().is_numeral(x, q); scoped_mpf v(m_mpf_manager); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); @@ -2135,10 +2139,11 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args mk_triple(sgn, s, e, result); } - else - UNREACHABLE(); + else { + NOT_IMPLEMENTED_YET(); + } - SASSERT(is_well_sorted(m, result)); + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 197c7ce9a..6a7b6e92f 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -129,7 +129,9 @@ public: void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); + void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -186,7 +188,7 @@ 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); }; #endif