diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index 231d826b2..9b6af92ff 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -413,9 +413,13 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa m_manager->raise_exception("invalid number of parameters to to_fp"); if (!parameters[0].is_int() || !parameters[1].is_int()) m_manager->raise_exception("invalid parameter type to to_fp"); + int ebits = parameters[0].get_int(); int sbits = parameters[1].get_int(); + if (domain[0]->get_parameter(0).get_int() != (ebits + sbits)) + m_manager->raise_exception("sort mismtach; invalid bit-vector size, expected bitvector of size (ebits+sbits)"); + sort * fp = mk_float_sort(ebits, sbits); symbol name("to_fp"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); @@ -461,7 +465,7 @@ func_decl * float_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, pa if (arity != 2 && arity != 3) m_manager->raise_exception("invalid number of arguments to to_fp operator"); if (arity == 3 && domain[2] != m_int_sort) - m_manager->raise_exception("sort mismatch, expected second argument of Int sort"); + m_manager->raise_exception("sort mismatch, expected third argument of Int sort"); if (domain[1] != m_real_sort) m_manager->raise_exception("sort mismatch, expected second argument of Real sort"); @@ -701,6 +705,7 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("fp", OP_FLOAT_FP)); op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV)); op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV)); + op_names.push_back(builtin_name("fp.to_real", OP_FLOAT_TO_REAL)); op_names.push_back(builtin_name("to_fp", OP_FLOAT_TO_FP)); op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED)); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 3fbb7ccf8..5fd96eace 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1858,9 +1858,9 @@ void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const result = m.mk_and(m.mk_not(t1), t2); } -void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { - TRACE("fpa2bv_to_float", for (unsigned i=0; i < num; i++) - tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; ); +void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + TRACE("fpa2bv_to_fp", 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]) && @@ -1884,16 +1884,16 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a rational q; if (!m_arith_util.is_numeral(args[1], q)) - NOT_IMPLEMENTED_YET(); + UNREACHABLE(); rational e; if (!m_arith_util.is_numeral(args[2], e)) - NOT_IMPLEMENTED_YET(); + UNREACHABLE(); SASSERT(e.is_int64()); SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1)); - mpf nte, nta, tp, tn, tz; + scoped_mpf nte(m_mpf_manager), nta(m_mpf_manager), tp(m_mpf_manager), tn(m_mpf_manager), tz(m_mpf_manager); m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator()); m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator()); @@ -1914,21 +1914,26 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a mk_value(a_tn->get_decl(), 0, 0, bv_tn); mk_value(a_tz->get_decl(), 0, 0, bv_tz); - mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tn, bv_tz, result); - mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tp, result, result); - mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), bv_nta, result, result); - mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), bv_nte, result, result); + expr_ref c1(m), c2(m), c3(m), c4(m); + c1 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); + c2 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)); + c3 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)); + c4 = m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)); + + mk_ite(c1, bv_tn, bv_tz, result); + mk_ite(c2, bv_tp, result, result); + mk_ite(c3, bv_nta, result, result); + mk_ite(c4, bv_nte, result, result); } 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); - - m_bv_util.mk_extract(sz - 1, sz - 1, bv); + 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), @@ -2093,8 +2098,8 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a 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 asFloat - SASSERT(m_util.is_float(f->get_range())); + // .. 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()); @@ -2121,16 +2126,16 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a rational q; m_util.au().is_numeral(args[1], q); - mpf v; + scoped_mpf v(m_mpf_manager); m_util.fm().set(v, ebits, sbits, rm, q.to_mpq()); - expr * sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1); - expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); - expr * e = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); + expr_ref sgn(m), s(m), e(m), unbiased_exp(m); + sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1); + s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1); + unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits); + mk_bias(unbiased_exp, e); mk_triple(sgn, s, e, result); - - m_util.fm().del(v); } else UNREACHABLE(); @@ -2187,19 +2192,92 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg } void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + TRACE("fpa2bv_to_real", for (unsigned i = 0; i < num; i++) + tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;); SASSERT(num == 1); + SASSERT(f->get_num_parameters() == 0); + SASSERT(is_app_of(args[0], m_plugin->get_family_id(), OP_FLOAT_TO_FP)); + + expr * x = args[0]; + sort * s = m.get_sort(x); + unsigned ebits = m_util.get_ebits(s); + unsigned sbits = m_util.get_sbits(s); - //unsigned ebits = m_util.get_ebits(f->get_range()); - //unsigned sbits = m_util.get_sbits(f->get_range()); - //int width = f->get_parameter(0).get_int(); + sort * rs = m_arith_util.mk_real(); + expr_ref x_is_nan(m), x_is_inf(m), x_is_zero(m); + mk_is_nan(x, x_is_nan); + mk_is_inf(x, x_is_inf); + mk_is_zero(x, x_is_zero); - //expr * rm = args[0]; - //expr * x = args[1]; + expr_ref sgn(m), sig(m), exp(m), lz(m); + unpack(x, sgn, sig, exp, lz, true); + // sig is of the form [1].[sigbits] - //expr * sgn, *s, *e; - //split(x, sgn, s, e); + 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); - NOT_IMPLEMENTED_YET(); + expr_ref rsig(m), bit(m), zero(m), one(m), two(m), bv0(m), bv1(m); + zero = m_arith_util.mk_numeral(rational(0), rs); + one = m_arith_util.mk_numeral(rational(1), rs); + two = m_arith_util.mk_numeral(rational(2), rs); + bv0 = m_bv_util.mk_numeral(0, 1); + bv1 = m_bv_util.mk_numeral(1, 1); + rsig = one; + for (unsigned i = sbits-2; i != (unsigned)-1; i--) + { + bit = m_bv_util.mk_extract(i, i, sig); + rsig = m_arith_util.mk_mul(rsig, two); + rsig = m_arith_util.mk_add(rsig, m.mk_ite(m.mk_eq(bit, bv1), one, zero)); + } + + const mpz & p2 = fu().fm().m_powers2(sbits-1); + expr_ref ep2(m); + ep2 = m_arith_util.mk_numeral(rational(p2), false); + rsig = m_arith_util.mk_div(rsig, ep2); + dbg_decouple("fpa2bv_to_real_ep2", ep2); + dbg_decouple("fpa2bv_to_real_rsig", rsig); + + expr_ref exp_n(m), exp_p(m), exp_is_neg(m), exp_abs(m); + exp_is_neg = m.mk_eq(m_bv_util.mk_extract(ebits - 1, ebits - 1, exp), bv1); + dbg_decouple("fpa2bv_to_real_exp_is_neg", exp_is_neg); + exp_p = m_bv_util.mk_sign_extend(1, exp); + exp_n = m_bv_util.mk_bv_not(m_bv_util.mk_sign_extend(1, exp)); + exp_abs = m.mk_ite(exp_is_neg, exp_n, exp_p); + dbg_decouple("fpa2bv_to_real_exp_abs", exp); + SASSERT(m_bv_util.get_bv_size(exp_abs) == ebits + 1); + + expr_ref exp2(m), prev_bit(m); + exp2 = zero; + prev_bit = bv0; + for (unsigned i = ebits; i != (unsigned)-1; i--) + { + bit = m_bv_util.mk_extract(i, i, exp_abs); + exp2 = m_arith_util.mk_mul(exp2, two); + exp2 = m_arith_util.mk_add(exp2, m.mk_ite(m.mk_eq(bit, prev_bit), zero, one)); + prev_bit = bit; + } + + exp2 = m.mk_ite(exp_is_neg, m_arith_util.mk_div(one, exp2), exp2); + dbg_decouple("fpa2bv_to_real_exp2", exp2); + + expr_ref res(m), two_exp2(m); + two_exp2 = m_arith_util.mk_power(two, exp2); + res = m_arith_util.mk_mul(rsig, two_exp2); + res = m.mk_ite(m.mk_eq(sgn, bv1), m_arith_util.mk_uminus(res), res); + dbg_decouple("fpa2bv_to_real_sig_times_exp2", res); + + TRACE("fpa2bv_to_real", tout << "rsig = " << mk_ismt2_pp(rsig, m) << std::endl; + tout << "exp2 = " << mk_ismt2_pp(exp2, m) << std::endl;); + + expr_ref undef(m); + undef = m.mk_fresh_const(0, rs); + + result = m.mk_ite(x_is_zero, zero, res); + result = m.mk_ite(x_is_inf, undef, result); + result = m.mk_ite(x_is_nan, undef, result); + + SASSERT(is_well_sorted(m, result)); } void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 08542cd40..caad0875c 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -121,7 +121,7 @@ public: void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_float(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_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index 62554e06e..a5ff8f5ca 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -144,11 +144,12 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_SUBNORMAL: m_conv.mk_is_subnormal(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_POSITIVE: m_conv.mk_is_positive(f, num, args, result); return BR_DONE; case OP_FLOAT_IS_NEGATIVE: m_conv.mk_is_negative(f, num, args, result); return BR_DONE; - case OP_FLOAT_TO_FP: m_conv.mk_to_float(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_FP: m_conv.mk_to_fp(f, num, args, result); return BR_DONE; case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index d1e1ab00e..42a4e5660 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -552,5 +552,14 @@ br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) } br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) { + scoped_mpf fv(m_util.fm()); + + if (m_util.is_value(arg1, fv)) { + scoped_mpq r(m_fm.mpq_manager()); + m_fm.to_rational(fv, r); + result = m_util.au().mk_numeral(r.get(), false); + return BR_DONE; + } + return BR_FAILED; } \ No newline at end of file diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 5efac6596..ba53dc20f 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -136,7 +136,8 @@ namespace smt { m_converter.mk_triple(sgn, sig, exp, bv_term); } - else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV) { + else if (term->get_decl_kind() == OP_FLOAT_TO_IEEE_BV || + term->get_decl_kind() == OP_FLOAT_TO_REAL) { SASSERT(is_app(t)); expr_ref bv_e(m); proof_ref bv_pr(m); @@ -420,7 +421,8 @@ namespace smt { ctx.mark_as_relevant(bv_sig); ctx.mark_as_relevant(bv_exp); } - else if (n->get_decl()->get_decl_kind() == OP_FLOAT_TO_IEEE_BV) { + else if (n->get_decl()->get_decl_kind() == OP_FLOAT_TO_IEEE_BV || + n->get_decl()->get_decl_kind() == OP_FLOAT_TO_REAL) { expr_ref eq(m); app * ex_a = to_app(ex); if (n->get_id() > ex_a->get_id()) diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index f5785c072..c4fa17d9a 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -199,35 +199,59 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode o.sign = m_mpq_manager.is_neg(value); m_mpz_manager.set(o.significand, 0); - const mpz & p = m_powers2(sbits+2); - signed lz = 0; - - o.exponent = sbits+2; + const mpz & p = m_powers2(sbits+3); + + scoped_mpq v(m_mpq_manager); + m_mpq_manager.set(v, value); + o.exponent = 0; - // CMW: This could be optimized considerably. - scoped_mpz t(m_mpz_manager); - retry: - m_mpz_manager.mul2k(value.numerator(), lz, t); - m_mpz_manager.machine_div(t, value.denominator(), o.significand); - m_mpz_manager.abs(o.significand); - if (m_mpz_manager.lt(o.significand, p)) { - lz++; - goto retry; - } - o.exponent -= lz; - - bool sticky = false; - while (m_mpz_manager.ge(o.significand, m_powers2(sbits+3))) { - sticky = sticky || !m_mpz_manager.is_even(o.significand); - m_mpz_manager.machine_div2k(o.significand, 1); + // Normalize + while (m_mpq_manager.ge(v, mpq(2))) + { + m_mpq_manager.div(v, mpq(2), v); o.exponent++; } - if (sticky && m_mpz_manager.is_even(o.significand)) - m_mpz_manager.inc(o.significand); - TRACE("mpf_dbg", tout << "QUOTIENT = " << m_mpz_manager.to_string(o.significand) << " shift=" << lz << std::endl;); + while (m_mpq_manager.lt(v, mpq(1))) + { + m_mpq_manager.mul(v, mpq(2), v); + o.exponent--; + } - SASSERT(m_mpz_manager.ge(o.significand, m_powers2(sbits+2))); + m_mpz_manager.set(o.significand, 0); + // o.exponent += sbits ; + + SASSERT(m_mpq_manager.lt(v, mpq(2))); + SASSERT(m_mpq_manager.ge(v, mpq(1))); + + // 1.0 <= v < 2.0 (* 2^o.exponent) + // (and v != 0.0) + for (unsigned i = 0; i < sbits + 3 ; i++) + { + m_mpz_manager.mul(o.significand, mpz(2), o.significand); + if (m_mpq_manager.ge(v, mpq(1))) + m_mpz_manager.add(o.significand, mpz(1), o.significand); + m_mpq_manager.sub(v, mpq(1), v); // v := v - 1.0 + m_mpq_manager.mul(mpq(2), v, v); // v := 2.0 * v + } + + // Sticky + // m_mpz_manager.mul(o.significand, mpz(2), o.significand); + /*if (!m_mpq_manager.is_zero(v)) + m_mpz_manager.add(o.significand, mpz(1), o.significand);*/ + + // bias? + // o.exponent += m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false)); + + // mpq pow; + // m_mpq_manager.power(mpq(2), sbits + 3, pow); + // m_mpq_manager.div(o.significand, pow, o.significand); + // SASSERT(m_mpz_manager.ge(o.significand, mpq(1.0))); + // SASSERT(m_mpz_manager.lt(o.significand, mpq(2.0))); + + TRACE("mpf_dbg", tout << "sig=" << m_mpz_manager.to_string(o.significand) << " exp=" << o.exponent << + " sticky=" << (!m_mpq_manager.is_zero(v)) << std::endl;); + round(rm, o); } @@ -253,7 +277,6 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;); - // [Leo]: potential memory leak. moving q and ex to scoped versions scoped_mpq q(m_mpq_manager); m_mpq_manager.set(q, f.c_str()); @@ -276,9 +299,6 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode if (m_mpq_manager.is_zero(significand)) mk_zero(ebits, sbits, o.sign, o); else { - // [Leo]: The following two lines may produce a memory leak. Moving to scoped version - // mpq sig; - // mpz exp; scoped_mpq sig(m_mpq_manager); scoped_mpz exp(m_mpq_manager);