From e5f03f999abb3af7743163975301bbfc9f9b6d34 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 4 Mar 2013 20:21:14 +0000 Subject: [PATCH] FPA: Added conversion operator float -> float. Signed-off-by: Christoph M. Wintersteiger --- src/ast/float_decl_plugin.cpp | 23 ++-- src/ast/rewriter/float_rewriter.cpp | 23 ++-- src/tactic/fpa/fpa2bv_converter.cpp | 169 ++++++++++++++++++++++++++-- src/util/mpf.cpp | 2 +- 4 files changed, 188 insertions(+), 29 deletions(-) diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index f2d6591dc..62ec3a4cf 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -353,27 +353,22 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) m_manager->raise_exception("expecting two integer parameters to asFloat"); if (arity != 2 && arity != 3) m_manager->raise_exception("invalid number of arguments to asFloat operator"); - if (!is_rm_sort(domain[0]) || domain[1] != m_real_sort) + if (arity == 3 && domain[2] != m_int_sort) + m_manager->raise_exception("sort mismatch"); + if (!is_rm_sort(domain[0]) || + !(domain[1] == m_real_sort || is_sort_of(domain[1], m_family_id, FLOAT_SORT))) m_manager->raise_exception("sort mismatch"); - if (arity == 2) { - sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("asFloat"); - return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } - else { - if (domain[2] != m_int_sort) - m_manager->raise_exception("sort mismatch"); - sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); - symbol name("asFloat"); - return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("asFloat"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); } } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 482e280e3..18fea6c47 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -77,14 +77,23 @@ br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * c return BR_FAILED; rational q; - if (!m_util.au().is_numeral(args[1], q)) + mpf q_mpf; + if (m_util.au().is_numeral(args[1], q)) { + mpf v; + m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); + result = m_util.mk_value(v); + m_util.fm().del(v); + return BR_DONE; + } + else if (m_util.is_value(args[1], q_mpf)) { + mpf v; + m_util.fm().set(v, ebits, sbits, rm, q_mpf); + result = m_util.mk_value(v); + m_util.fm().del(v); + return BR_DONE; + } + else return BR_FAILED; - - mpf v; - m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); - result = m_util.mk_value(v); - m_util.fm().del(v); - return BR_DONE; } else if (num_args == 3 && m_util.is_rm(m().get_sort(args[0])) && diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 2600cb3ec..37eaa365a 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1403,23 +1403,176 @@ void fpa2bv_converter::mk_is_sign_minus(func_decl * f, unsigned num, expr * cons } void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - if (num == 3 && m_bv_util.is_bv(args[0]) && - m_bv_util.is_bv(args[1]) && m_bv_util.is_bv(args[2])) { + TRACE("fpa2bv_to_float", for (unsigned i=0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; ); + + if (num == 3 && + m_bv_util.is_bv(args[0]) && + m_bv_util.is_bv(args[1]) && + m_bv_util.is_bv(args[2])) { // Theoretically, the user could have thrown in it's own triple of bit-vectors. // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { + // We also support float to float conversion + expr_ref rm(m), x(m); + rm = args[0]; + x = args[1]; + + 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_plus_inf(f, pinf); + mk_minus_inf(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. + sort * s = f->get_range(); + expr_ref sgn(m), sig(m), exp(m); + unpack(x, sgn, sig, exp, true); + + expr_ref res_sgn(m), res_sig(m), res_exp(m); + + res_sgn = sgn; + + unsigned from_sbits = m_util.get_sbits(m.get_sort(args[1])); + unsigned from_ebits = m_util.get_ebits(m.get_sort(args[1])); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + 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); + + 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); + unsigned high_sz = m_bv_util.get_bv_size(high); + sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low); + 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+2-from_ebits, exp); + else if (from_ebits > (to_ebits + 2)) + { + expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), or_eq(m), not_or_eq(m), 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); + high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high); + + zero1 = m_bv_util.mk_numeral(0, 1); + m_simp.mk_eq(high_red_and, one1, and_eq); + m_simp.mk_eq(high_red_or, zero1, 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(or_eq, s_is_one, m.mk_false(), c2); + m_simp.mk_ite(and_eq, s_is_zero, c2, exponent_overflow); + + // Note: Upon overflow, we _could_ try to shift the significand around... + + res_exp = low; + } + else + res_exp = exp; + + SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2); + + 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); + } else { + // .. other than that, we only support rationals for asFloat SASSERT(num == 2); 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()); - - SASSERT(m_util.is_rm(to_app(args[0])->get_decl()->get_range())); + unsigned sbits = m_util.get_sbits(f->get_range()); + + //SASSERT(m_bv_util.is_numeral(args[0])); + //rational tmp_rat; unsigned sz; + //m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz); + //SASSERT(tmp_rat.is_int32()); + //SASSERT(sz == 3); + //BV_RM_VAL rm = (BV_RM_VAL) tmp_rat.get_unsigned(); + + /*mpf_rounding_mode 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; + case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break; + case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break; + default: UNREACHABLE(); + }*/ + + SASSERT(m_util.au().is_numeral(args[1])); + + sort * rm_rng = to_app(args[0])->get_decl()->get_range(); + SASSERT(m_util.is_rm(rm_rng)); mpf_rounding_mode rm = static_cast(to_app(args[1])->get_decl_kind()); - + rational q; - SASSERT(m_util.au().is_numeral(args[1])); + SASSERT(m_util.au().is_numeral(args[1])); m_util.au().is_numeral(args[1], q); mpf v; @@ -1433,6 +1586,8 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a m_util.fm().del(v); } + + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 9618ffbce..dfac97626 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -367,7 +367,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode o.ebits = ebits; o.sbits = sbits; - signed ds = sbits - x.sbits; + signed ds = sbits - x.sbits + 4; // plus rounding bits if (ds > 0) { m_mpz_manager.mul2k(o.significand, ds);