mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

FPA: bugfixes, leakfixes, added fp.to_real

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-12-13 19:34:55 +00:00
parent d6ac98a494
commit b30e61e528
7 changed files with 177 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/ast/float_decl_plugin.cpp
View file

@ -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<builtin_name> & 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));

136
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -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 {

2
src/ast/fpa/fpa2bv_converter.h
View file

@ -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);

3
src/ast/fpa/fpa2bv_rewriter.h
View file

@ -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;);

9
src/ast/rewriter/float_rewriter.cpp
View file

@ -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;
}

6
src/smt/theory_fpa.cpp
View file

@ -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())

76
src/util/mpf.cpp
View file

@ -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);