mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
Fixed potential memory leakage issues in fpa2bv_converfter
This commit is contained in:
Christoph M. Wintersteiger
parent
3ffcea0fe4
commit
6db0a15d29
1 changed files with 200 additions and 176 deletions
|
|
@ -3,15 +3,15 @@ Copyright (c) 2012 Microsoft Corporation
|
|||
|
||||
Module Name:
|
||||
|
||||
fpa2bv_converter.cpp
|
||||
fpa2bv_converter.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Conversion routines for Floating Point -> Bit-Vector
|
||||
Conversion routines for Floating Point -> Bit-Vector
|
||||
|
||||
Author:
|
||||
|
||||
Christoph (cwinter) 2012-02-09
|
||||
Christoph (cwinter) 2012-02-09
|
||||
|
||||
Notes:
|
||||
|
||||
|
|
@ -50,7 +50,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
|
|||
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
|
||||
|
||||
TRACE("fpa2bv", tout << "mk_eq a=" << mk_ismt2_pp(a, m) << std::endl;
|
||||
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
|
||||
tout << "mk_eq b=" << mk_ismt2_pp(b, m) << std::endl;);
|
||||
|
||||
expr_ref eq_sgn(m), eq_exp(m), eq_sig(m);
|
||||
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), eq_sgn);
|
||||
|
|
@ -81,7 +81,7 @@ void fpa2bv_converter::mk_eq(expr * a, expr * b, expr_ref & result) {
|
|||
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_INTERNAL_RM));
|
||||
|
||||
TRACE("fpa2bv", tout << "mk_eq_rm a=" << mk_ismt2_pp(a, m) << std::endl;
|
||||
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
|
||||
tout << "mk_eq_rm b=" << mk_ismt2_pp(b, m) << std::endl;);
|
||||
|
||||
m_simp.mk_eq(to_app(a)->get_arg(0), to_app(b)->get_arg(0), result);
|
||||
}
|
||||
|
|
@ -146,7 +146,7 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar
|
|||
}
|
||||
else {
|
||||
expr_ref bv_sgn(m), bv_sig(m), e(m), biased_exp(m);
|
||||
bv_sgn = m_bv_util.mk_numeral( (sign) ? 1 : 0, 1);
|
||||
bv_sgn = m_bv_util.mk_numeral((sign) ? 1 : 0, 1);
|
||||
bv_sig = m_bv_util.mk_numeral(rational(sig), sbits-1);
|
||||
e = m_bv_util.mk_numeral(exp, ebits);
|
||||
|
||||
|
|
@ -154,7 +154,7 @@ void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * ar
|
|||
|
||||
mk_fp(bv_sgn, biased_exp, bv_sig, result);
|
||||
TRACE("fpa2bv_dbg", tout << "value of [" << sign << " " << m_mpz_manager.to_string(sig) << " " << exp << "] is "
|
||||
<< mk_ismt2_pp(result, m) << std::endl;);
|
||||
<< mk_ismt2_pp(result, m) << std::endl;);
|
||||
|
||||
}
|
||||
}
|
||||
|
|
@ -183,8 +183,8 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
|
|||
std::string name = f->get_name().str();
|
||||
|
||||
sgn = mk_fresh_const((p + "_sgn_" + name).c_str(), 1);
|
||||
s = mk_fresh_const((p + "_sig_" + name).c_str(), sbits - 1);
|
||||
e = mk_fresh_const((p + "_exp_" + name).c_str(), ebits);
|
||||
s = mk_fresh_const((p + "_sig_" + name).c_str(), sbits-1);
|
||||
#else
|
||||
app_ref bv(m);
|
||||
unsigned bv_sz = 1 + ebits + (sbits - 1);
|
||||
|
|
@ -215,8 +215,8 @@ void fpa2bv_converter::mk_var(unsigned base_inx, sort * srt, expr_ref & result)
|
|||
expr_ref sgn(m), s(m), e(m);
|
||||
|
||||
sgn = m.mk_var(base_inx, m_bv_util.mk_sort(1));
|
||||
s = m.mk_var(base_inx + 1, m_bv_util.mk_sort(sbits-1));
|
||||
e = m.mk_var(base_inx + 2, m_bv_util.mk_sort(ebits));
|
||||
s = m.mk_var(base_inx+1, m_bv_util.mk_sort(sbits-1));
|
||||
e = m.mk_var(base_inx+2, m_bv_util.mk_sort(ebits));
|
||||
|
||||
mk_fp(sgn, e, s, result);
|
||||
}
|
||||
|
|
@ -230,9 +230,9 @@ void fpa2bv_converter::mk_uninterpreted_output(sort * rng, func_decl * fbv, expr
|
|||
app_ref na(m);
|
||||
na = m.mk_app(fbv, new_args.size(), new_args.c_ptr());
|
||||
mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, na),
|
||||
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
|
||||
m_bv_util.mk_extract(sbits - 2, 0, na),
|
||||
result);
|
||||
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, na),
|
||||
m_bv_util.mk_extract(sbits - 2, 0, na),
|
||||
result);
|
||||
}
|
||||
else if (m_util.is_rm(rng)) {
|
||||
app_ref na(m);
|
||||
|
|
@ -316,11 +316,11 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
|
|||
|
||||
expr_ref bv3(m);
|
||||
bv3 = m.mk_fresh_const(
|
||||
#ifdef Z3DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
"fpa2bv_rm"
|
||||
#else
|
||||
#else
|
||||
0
|
||||
#endif
|
||||
#endif
|
||||
, m_bv_util.mk_sort(3));
|
||||
|
||||
mk_rm(bv3, result);
|
||||
|
|
@ -342,9 +342,9 @@ void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) {
|
|||
expr_ref top_exp(m);
|
||||
mk_top_exp(ebits, top_exp);
|
||||
mk_fp(m_bv_util.mk_numeral(0, 1),
|
||||
top_exp,
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
top_exp,
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
|
||||
|
|
@ -355,9 +355,9 @@ void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
|
|||
expr_ref top_exp(m);
|
||||
mk_top_exp(ebits, top_exp);
|
||||
mk_fp(m_bv_util.mk_numeral(1, 1),
|
||||
top_exp,
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
top_exp,
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) {
|
||||
|
|
@ -368,9 +368,9 @@ void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) {
|
|||
expr_ref top_exp(m);
|
||||
mk_top_exp(ebits, top_exp);
|
||||
mk_fp(m_bv_util.mk_numeral(0, 1),
|
||||
top_exp,
|
||||
m_bv_util.mk_numeral(1, sbits-1),
|
||||
result);
|
||||
top_exp,
|
||||
m_bv_util.mk_numeral(1, sbits-1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_nzero(func_decl *f, expr_ref & result) {
|
||||
|
|
@ -381,9 +381,9 @@ void fpa2bv_converter::mk_nzero(func_decl *f, expr_ref & result) {
|
|||
expr_ref bot_exp(m);
|
||||
mk_bot_exp(ebits, bot_exp);
|
||||
mk_fp(m_bv_util.mk_numeral(1, 1),
|
||||
bot_exp,
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
result);
|
||||
bot_exp,
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) {
|
||||
|
|
@ -394,9 +394,9 @@ void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) {
|
|||
expr_ref bot_exp(m);
|
||||
mk_bot_exp(ebits, bot_exp);
|
||||
mk_fp(m_bv_util.mk_numeral(0, 1),
|
||||
bot_exp,
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
bot_exp,
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_one(func_decl *f, expr_ref sign, expr_ref & result) {
|
||||
|
|
@ -405,9 +405,9 @@ void fpa2bv_converter::mk_one(func_decl *f, expr_ref sign, expr_ref & result) {
|
|||
unsigned sbits = m_util.get_sbits(srt);
|
||||
unsigned ebits = m_util.get_ebits(srt);
|
||||
mk_fp(sign,
|
||||
m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits),
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits),
|
||||
m_bv_util.mk_numeral(0, sbits-1),
|
||||
result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits,
|
||||
|
|
@ -623,8 +623,8 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
add_core(sbits, ebits,
|
||||
c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp,
|
||||
res_sgn, res_sig, res_exp);
|
||||
c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp,
|
||||
res_sgn, res_sig, res_exp);
|
||||
|
||||
expr_ref is_zero_sig(m), nil_sbit4(m);
|
||||
nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
|
||||
|
|
@ -781,8 +781,8 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
|
|||
dbg_decouple("fpa2bv_mul_res_sgn", res_sgn);
|
||||
|
||||
res_exp = m_bv_util.mk_bv_add(
|
||||
m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
|
||||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
|
||||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
|
||||
expr_ref product(m);
|
||||
product = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
|
||||
|
|
@ -925,8 +925,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
|
|||
b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
|
||||
|
||||
res_exp = m_bv_util.mk_bv_sub(
|
||||
m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
|
||||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
|
||||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
|
||||
expr_ref quotient(m);
|
||||
// b_sig_ext can't be 0 here, so it's safe to use OP_BUDIV_I
|
||||
|
|
@ -981,7 +981,7 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
|
|||
y = args[1];
|
||||
|
||||
TRACE("fpa2bv_rem", tout << "X = " << mk_ismt2_pp(x, m) << std::endl;
|
||||
tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
|
||||
tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
|
||||
|
||||
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
|
||||
mk_nan(f, nan);
|
||||
|
|
@ -1089,7 +1089,7 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
|
|||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
res_sgn = a_sgn;
|
||||
res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits, 0, huge_rem),
|
||||
m_bv_util.mk_numeral(0, 3));
|
||||
m_bv_util.mk_numeral(0, 3));
|
||||
|
||||
res_exp = m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext);
|
||||
|
||||
|
|
@ -1136,7 +1136,9 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
|
|||
v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, x, y);
|
||||
|
||||
// Note: This requires BR_REWRITE_FULL afterwards.
|
||||
result = m.mk_ite(c, v, m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_I, x, y));
|
||||
expr_ref min_i(m);
|
||||
min_i = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MIN_I, x, y);
|
||||
m_simp.mk_ite(c, v, min_i, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
|
|
@ -1163,8 +1165,7 @@ void fpa2bv_converter::mk_min_i(func_decl * f, unsigned num, expr * const * args
|
|||
expr_ref lt(m);
|
||||
mk_float_lt(f, num, args, lt);
|
||||
|
||||
result = y;
|
||||
mk_ite(lt, x, result, result);
|
||||
mk_ite(lt, x, y, result);
|
||||
mk_ite(both_zero, y, result, result);
|
||||
mk_ite(y_is_nan, x, result, result);
|
||||
mk_ite(x_is_nan, y, result, result);
|
||||
|
|
@ -1192,13 +1193,13 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y)
|
|||
|
||||
expr_ref pn(m), np(m);
|
||||
mk_fp(decls.first,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
pn);
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
pn);
|
||||
mk_fp(decls.second,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
np);
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
np);
|
||||
|
||||
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
|
||||
mk_is_pzero(x, x_is_pzero);
|
||||
|
|
@ -1221,7 +1222,9 @@ void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args,
|
|||
v = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, x, y);
|
||||
|
||||
// Note: This requires BR_REWRITE_FULL afterwards.
|
||||
result = m.mk_ite(c, v, m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_I, x, y));
|
||||
expr_ref max_i(m);
|
||||
max_i = m.mk_app(m_util.get_family_id(), OP_FPA_INTERNAL_MAX_I, x, y);
|
||||
m_simp.mk_ite(c, v, max_i, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
|
|
@ -1242,14 +1245,14 @@ void fpa2bv_converter::mk_max_i(func_decl * f, unsigned num, expr * const * args
|
|||
mk_is_nan(y, y_is_nan);
|
||||
mk_pzero(f, pzero);
|
||||
|
||||
expr_ref sgn_diff(m);
|
||||
sgn_diff = m.mk_not(m.mk_eq(x_sgn, y_sgn));
|
||||
expr_ref sgn_diff(m), sgn_eq(m);
|
||||
sgn_eq = m.mk_eq(x_sgn, y_sgn);
|
||||
sgn_diff = m.mk_not(sgn_eq);
|
||||
|
||||
expr_ref gt(m);
|
||||
mk_float_gt(f, num, args, gt);
|
||||
|
||||
result = y;
|
||||
mk_ite(gt, x, result, result);
|
||||
mk_ite(gt, x, y, result);
|
||||
mk_ite(both_zero, y, result, result);
|
||||
mk_ite(y_is_nan, x, result, result);
|
||||
mk_ite(x_is_nan, y, result, result);
|
||||
|
|
@ -1277,13 +1280,13 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y)
|
|||
|
||||
expr_ref pn(m), np(m);
|
||||
mk_fp(decls.first,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
pn);
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
pn);
|
||||
mk_fp(decls.second,
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
np);
|
||||
m_bv_util.mk_numeral(0, ebits),
|
||||
m_bv_util.mk_numeral(0, sbits - 1),
|
||||
np);
|
||||
|
||||
expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m);
|
||||
mk_is_pzero(x, x_is_pzero);
|
||||
|
|
@ -1440,7 +1443,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
dbg_decouple("fpa2bv_fma_mul_sgn", mul_sgn);
|
||||
|
||||
mul_exp = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(a_exp_ext, a_lz_ext),
|
||||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext));
|
||||
dbg_decouple("fpa2bv_fma_mul_exp", mul_exp);
|
||||
|
||||
mul_sig = m_bv_util.mk_bv_mul(a_sig_ext, b_sig_ext);
|
||||
|
|
@ -1501,8 +1504,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
// Alignment shift with sticky bit computation.
|
||||
expr_ref shifted_big(m), shifted_f_sig(m), sticky_raw(m);
|
||||
shifted_big = m_bv_util.mk_bv_lshr(
|
||||
m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)),
|
||||
m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta));
|
||||
m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)),
|
||||
m_bv_util.mk_zero_extend((3*sbits)-(ebits+2), exp_delta));
|
||||
shifted_f_sig = m_bv_util.mk_extract(3*sbits-1, sbits, shifted_big);
|
||||
sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big);
|
||||
SASSERT(m_bv_util.get_bv_size(shifted_f_sig) == 2 * sbits);
|
||||
|
|
@ -1535,7 +1538,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
|
|||
expr_ref sum(m), e_plus_f(m), e_minus_f(m);
|
||||
e_plus_f = m_bv_util.mk_bv_add(e_sig, shifted_f_sig);
|
||||
e_minus_f = m_bv_util.mk_bv_sub(e_sig, shifted_f_sig),
|
||||
m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
|
||||
m_simp.mk_ite(eq_sgn, e_plus_f, e_minus_f, sum);
|
||||
|
||||
SASSERT(is_well_sorted(m, sum));
|
||||
|
||||
|
|
@ -1721,7 +1724,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
|
|||
|
||||
expr * or_args[2] = { Q, S };
|
||||
expr_ref Q_or_S(m), R_shftd(m), T_lsds4(m);
|
||||
Q_or_S = m_bv_util.mk_bv_or(2, or_args);
|
||||
Q_or_S = m_bv_util.mk_bv_or(2, or_args);
|
||||
m_simp.mk_ite(t_lt_0, Q, Q_or_S, Q);
|
||||
R_shftd = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits + 3, 0, R), zero1);
|
||||
T_lsds4 = m_bv_util.mk_extract(sbits + 4, 0, T);
|
||||
|
|
@ -1818,8 +1821,9 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig);
|
||||
dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp);
|
||||
|
||||
expr_ref xzero(m);
|
||||
mk_ite(m.mk_eq(a_sgn, one_1), nzero, pzero, xzero);
|
||||
expr_ref xzero(m), sgn_eq_1(m);
|
||||
sgn_eq_1 = m.mk_eq(a_sgn, one_1);
|
||||
mk_ite(sgn_eq_1, nzero, pzero, xzero);
|
||||
|
||||
// exponent < 0 -> 0/1
|
||||
expr_ref exp_lt_zero(m), exp_h(m);
|
||||
|
|
@ -1831,7 +1835,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
expr_ref pone(m), none(m), xone(m), c421(m), c422(m), c423(m), t1(m), t2(m), tie(m), v42(m), exp_lt_m1(m);
|
||||
mk_one(f, zero_1, pone);
|
||||
mk_one(f, one_1, none);
|
||||
mk_ite(m.mk_eq(a_sgn, one_1), none, pone, xone);
|
||||
mk_ite(sgn_eq_1, none, pone, xone);
|
||||
|
||||
expr_ref pow_2_sbitsm1(m), m1(m);
|
||||
pow_2_sbitsm1 = m_bv_util.mk_numeral(fu().fm().m_powers2(sbits - 1), sbits);
|
||||
|
|
@ -1880,7 +1884,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
|
||||
expr_ref shift(m), rshift(m), div(m), rem(m);
|
||||
shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits - 1, sbits + 1),
|
||||
m_bv_util.mk_sign_extend(sbits - ebits + 1, a_exp));
|
||||
m_bv_util.mk_sign_extend(sbits - ebits + 1, a_exp));
|
||||
rshift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits, sbits + 1), shift);
|
||||
div = m_bv_util.mk_bv_lshr(m_bv_util.mk_zero_extend(1, a_sig), shift);
|
||||
rem = m_bv_util.mk_bv_lshr(m_bv_util.mk_bv_shl(m_bv_util.mk_zero_extend(1, a_sig), rshift), rshift);
|
||||
|
|
@ -1901,15 +1905,15 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
expr_ref tie2(m), tie2_c(m), div_last(m), v51(m), rem_shl(m);
|
||||
rem_shl = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits - 1, 0, rem), zero_1);
|
||||
m_simp.mk_eq(rem_shl,
|
||||
m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits+1), shift),
|
||||
tie2);
|
||||
m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits+1), shift),
|
||||
tie2);
|
||||
div_last = m_bv_util.mk_extract(0, 0, div);
|
||||
tie2_c = m.mk_or(m.mk_and(tie2,
|
||||
m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)),
|
||||
m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1)))),
|
||||
m.mk_xor(m.mk_eq(a_sgn, one_1),
|
||||
m_bv_util.mk_sle(m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits + 1), shift),
|
||||
rem_shl)));
|
||||
m.mk_or(m.mk_and(rm_is_rte, m.mk_eq(div_last, one_1)),
|
||||
m.mk_and(rm_is_rta, m.mk_eq(div_last, zero_1)))),
|
||||
m.mk_xor(m.mk_eq(a_sgn, one_1),
|
||||
m_bv_util.mk_sle(m_bv_util.mk_bv_shl(m_bv_util.mk_numeral(1, sbits + 1), shift),
|
||||
rem_shl)));
|
||||
m_simp.mk_ite(tie2_c, div_p1, div, v51);
|
||||
|
||||
dbg_decouple("fpa2bv_r2i_v51", v51);
|
||||
|
|
@ -1948,7 +1952,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
|
|||
|
||||
expr_ref e_shift(m);
|
||||
e_shift = (ebits + 2 <= sbits + 1) ? m_bv_util.mk_extract(ebits + 1, 0, shift) :
|
||||
m_bv_util.mk_sign_extend((ebits + 2) - (sbits + 1), shift);
|
||||
m_bv_util.mk_sign_extend((ebits + 2) - (sbits + 1), shift);
|
||||
SASSERT(m_bv_util.get_bv_size(e_shift) == ebits + 2);
|
||||
res_exp = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(2, res_exp), e_shift);
|
||||
|
||||
|
|
@ -1977,7 +1981,7 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
|
|||
expr * x = args[0], * y = args[1];
|
||||
|
||||
TRACE("fpa2bv_float_eq", tout << "X = " << mk_ismt2_pp(x, m) << std::endl;
|
||||
tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
|
||||
tout << "Y = " << mk_ismt2_pp(y, m) << std::endl;);
|
||||
|
||||
expr_ref c1(m), c2(m), x_is_nan(m), y_is_nan(m), x_is_zero(m), y_is_zero(m);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
|
|
@ -2004,7 +2008,6 @@ void fpa2bv_converter::mk_float_eq(func_decl * f, unsigned num, expr * const * a
|
|||
expr_ref c3t4(m), c2else(m);
|
||||
m_simp.mk_ite(c3, m.mk_false(), t4, c3t4);
|
||||
m_simp.mk_ite(c2, m.mk_true(), c3t4, c2else);
|
||||
|
||||
m_simp.mk_ite(c1, m.mk_false(), c2else, result);
|
||||
|
||||
TRACE("fpa2bv_float_eq", tout << "FLOAT_EQ = " << mk_ismt2_pp(result, m) << std::endl; );
|
||||
|
|
@ -2154,7 +2157,7 @@ void fpa2bv_converter::mk_is_positive(func_decl * f, unsigned num, expr * const
|
|||
|
||||
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; );
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl; );
|
||||
|
||||
if (num == 1 &&
|
||||
m_bv_util.is_bv(args[0])) {
|
||||
|
|
@ -2167,33 +2170,33 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
SASSERT((unsigned)sz == to_sbits + to_ebits);
|
||||
|
||||
mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
|
||||
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
|
||||
m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
|
||||
result);
|
||||
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
|
||||
m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
|
||||
result);
|
||||
}
|
||||
else if (num == 2 &&
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_util.is_float(m.get_sort(args[1]))) {
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_util.is_float(m.get_sort(args[1]))) {
|
||||
// rm + float -> float
|
||||
mk_to_fp_float(f, f->get_range(), args[0], args[1], result);
|
||||
}
|
||||
else if (num == 2 &&
|
||||
m_util.is_rm(args[0]) &&
|
||||
(m_arith_util.is_int(args[1]) ||
|
||||
m_arith_util.is_real(args[1]))) {
|
||||
m_util.is_rm(args[0]) &&
|
||||
(m_arith_util.is_int(args[1]) ||
|
||||
m_arith_util.is_real(args[1]))) {
|
||||
// rm + real -> float
|
||||
mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
|
||||
}
|
||||
else if (num == 2 &&
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_bv_util.is_bv(args[1])) {
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_bv_util.is_bv(args[1])) {
|
||||
// rm + signed bv -> float
|
||||
mk_to_fp_signed(f, num, args, result);
|
||||
}
|
||||
else if (num == 3 &&
|
||||
m_bv_util.is_bv(args[0]) &&
|
||||
m_bv_util.is_bv(args[1]) &&
|
||||
m_bv_util.is_bv(args[2])) {
|
||||
m_bv_util.is_bv(args[0]) &&
|
||||
m_bv_util.is_bv(args[1]) &&
|
||||
m_bv_util.is_bv(args[2])) {
|
||||
// 3 BV -> float
|
||||
SASSERT(m_bv_util.get_bv_size(args[0]) == 1);
|
||||
SASSERT(m_util.get_ebits(f->get_range()) == m_bv_util.get_bv_size(args[1]));
|
||||
|
|
@ -2201,9 +2204,9 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
mk_fp(args[0], args[1], args[2], result);
|
||||
}
|
||||
else if (num == 3 &&
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_arith_util.is_numeral(args[1]) &&
|
||||
m_arith_util.is_numeral(args[2]))
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_arith_util.is_numeral(args[1]) &&
|
||||
m_arith_util.is_numeral(args[2]))
|
||||
{
|
||||
// rm + real + int -> float
|
||||
mk_to_fp_real_int(f, num, args, result);
|
||||
|
|
@ -2309,15 +2312,15 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
|
|||
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
|
||||
}
|
||||
else if (from_ebits > (to_ebits + 2)) {
|
||||
unsigned ebits_diff = from_ebits - (to_ebits + 2);
|
||||
unsigned ebits_diff = from_ebits - (to_ebits + 2);
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref exp_sub_lz(m);
|
||||
exp_sub_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_sign_extend(2, lz));
|
||||
dbg_decouple("fpa2bv_to_float_exp_sub_lz", exp_sub_lz);
|
||||
|
||||
// check whether exponent is within roundable (to_ebits+2) range.
|
||||
expr_ref max_exp(m), min_exp(m), exp_in_range(m);
|
||||
// check whether exponent is within roundable (to_ebits+2) range.
|
||||
expr_ref max_exp(m), min_exp(m), exp_in_range(m);
|
||||
const mpz & z = m_mpf_manager.m_powers2(to_ebits + 1, true);
|
||||
max_exp = m_bv_util.mk_concat(
|
||||
m_bv_util.mk_numeral(m_mpf_manager.m_powers2.m1(to_ebits, false), to_ebits + 1),
|
||||
|
|
@ -2330,23 +2333,23 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
|
|||
const mpz & ovft = m_mpf_manager.m_powers2.m1(to_ebits+1, false);
|
||||
first_ovf_exp = m_bv_util.mk_numeral(ovft, from_ebits+2);
|
||||
first_udf_exp = m_bv_util.mk_concat(
|
||||
m_bv_util.mk_numeral(-1, ebits_diff + 3),
|
||||
m_bv_util.mk_numeral(1, to_ebits + 1));
|
||||
m_bv_util.mk_numeral(-1, ebits_diff + 3),
|
||||
m_bv_util.mk_numeral(1, to_ebits + 1));
|
||||
dbg_decouple("fpa2bv_to_float_first_ovf_exp", first_ovf_exp);
|
||||
dbg_decouple("fpa2bv_to_float_first_udf_exp", first_udf_exp);
|
||||
|
||||
exp_in_range = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz);
|
||||
SASSERT(m_bv_util.get_bv_size(exp_in_range) == to_ebits + 2);
|
||||
exp_in_range = m_bv_util.mk_extract(to_ebits + 1, 0, exp_sub_lz);
|
||||
SASSERT(m_bv_util.get_bv_size(exp_in_range) == to_ebits + 2);
|
||||
|
||||
expr_ref ovf_cond(m), udf_cond(m);
|
||||
ovf_cond = m_bv_util.mk_sle(first_ovf_exp, exp_sub_lz);
|
||||
udf_cond = m_bv_util.mk_sle(exp_sub_lz, first_udf_exp);
|
||||
expr_ref ovf_cond(m), udf_cond(m);
|
||||
ovf_cond = m_bv_util.mk_sle(first_ovf_exp, exp_sub_lz);
|
||||
udf_cond = m_bv_util.mk_sle(exp_sub_lz, first_udf_exp);
|
||||
dbg_decouple("fpa2bv_to_float_exp_ovf", ovf_cond);
|
||||
dbg_decouple("fpa2bv_to_float_exp_udf", udf_cond);
|
||||
|
||||
res_exp = exp_in_range;
|
||||
res_exp = m.mk_ite(ovf_cond, max_exp, res_exp);
|
||||
res_exp = m.mk_ite(udf_cond, min_exp, res_exp);
|
||||
res_exp = exp_in_range;
|
||||
res_exp = m.mk_ite(ovf_cond, max_exp, res_exp);
|
||||
res_exp = m.mk_ite(udf_cond, min_exp, res_exp);
|
||||
}
|
||||
else { // from_ebits == (to_ebits + 2)
|
||||
res_exp = m_bv_util.mk_bv_sub(exp, lz);
|
||||
|
|
@ -2381,7 +2384,7 @@ void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr *
|
|||
|
||||
void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
|
||||
TRACE("fpa2bv_to_fp_real", tout << "rm: " << mk_ismt2_pp(rm, m) << std::endl <<
|
||||
"x: " << mk_ismt2_pp(x, m) << std::endl;);
|
||||
"x: " << mk_ismt2_pp(x, m) << std::endl;);
|
||||
SASSERT(m_util.is_float(s));
|
||||
SASSERT(au().is_real(x) || au().is_int(x));
|
||||
SASSERT(is_app_of(rm, m_util.get_family_id(), OP_FPA_INTERNAL_RM));
|
||||
|
|
@ -2572,7 +2575,7 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
|
|||
|
||||
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;);
|
||||
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_FPA_FP));
|
||||
|
|
@ -2596,7 +2599,7 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
SASSERT(m_bv_util.get_bv_size(sig) == sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == ebits);
|
||||
|
||||
expr_ref rsig(m), bit(m), zero(m), one(m), two(m), bv0(m), bv1(m);
|
||||
expr_ref rsig(m), bit(m), bit_eq_1(m), rsig_mul_2(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);
|
||||
|
|
@ -2605,8 +2608,10 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
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_add(m_arith_util.mk_mul(rsig, two),
|
||||
m.mk_ite(m.mk_eq(bit, bv1), one, zero));
|
||||
bit_eq_1 = m.mk_eq(bit, bv1);
|
||||
rsig_mul_2 = m_arith_util.mk_mul(rsig, two);
|
||||
rsig = m_arith_util.mk_add(rsig_mul_2,
|
||||
m.mk_ite(bit_eq_1, one, zero));
|
||||
}
|
||||
|
||||
const mpz & p2 = fu().fm().m_powers2(sbits - 1);
|
||||
|
|
@ -2625,37 +2630,44 @@ void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * ar
|
|||
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);
|
||||
expr_ref exp2(m), exp2_mul_2(m), prev_bit(m);
|
||||
exp2 = zero;
|
||||
for (unsigned i = ebits; i != (unsigned)-1; i--) {
|
||||
bit = m_bv_util.mk_extract(i, i, exp_abs);
|
||||
exp2 = m_arith_util.mk_add(m_arith_util.mk_mul(exp2, two),
|
||||
m.mk_ite(m.mk_eq(bit, bv1), one, zero));
|
||||
bit_eq_1 = m.mk_eq(bit, bv1);
|
||||
exp2_mul_2 = m_arith_util.mk_mul(exp2, two);
|
||||
exp2 = m_arith_util.mk_add(exp2_mul_2,
|
||||
m.mk_ite(bit_eq_1, one, zero));
|
||||
prev_bit = bit;
|
||||
}
|
||||
|
||||
exp2 = m.mk_ite(exp_is_neg, m_arith_util.mk_div(one, exp2), exp2);
|
||||
expr_ref one_div_exp2(m);
|
||||
one_div_exp2 = m_arith_util.mk_div(one, exp2);
|
||||
exp2 = m.mk_ite(exp_is_neg, one_div_exp2, exp2);
|
||||
dbg_decouple("fpa2bv_to_real_exp2", exp2);
|
||||
|
||||
expr_ref res(m), two_exp2(m);
|
||||
expr_ref res(m), two_exp2(m), minus_res(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);
|
||||
minus_res = m_arith_util.mk_uminus(res);
|
||||
res = m.mk_ite(m.mk_eq(sgn, bv1), minus_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 unspec(m);
|
||||
unspec = mk_to_real_unspecified(ebits, sbits);
|
||||
result = m.mk_ite(x_is_zero, zero, res);
|
||||
result = m.mk_ite(x_is_inf, mk_to_real_unspecified(ebits, sbits), result);
|
||||
result = m.mk_ite(x_is_nan, mk_to_real_unspecified(ebits, sbits), result);
|
||||
result = m.mk_ite(x_is_inf, unspec, result);
|
||||
result = m.mk_ite(x_is_nan, unspec, 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) {
|
||||
TRACE("fpa2bv_to_fp_signed", for (unsigned i = 0; i < num; i++)
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
|
||||
// This is a conversion from signed bitvector to float:
|
||||
// ; from signed machine integer, represented as a 2's complement bit vector
|
||||
|
|
@ -2702,10 +2714,11 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
|
||||
// Special case: x != 0
|
||||
expr_ref is_neg_bit(m), exp_too_large(m), sig_4(m), exp_2(m);
|
||||
expr_ref is_neg(m), x_abs(m);
|
||||
expr_ref is_neg(m), x_abs(m), neg_x(m);
|
||||
is_neg_bit = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, x);
|
||||
is_neg = m.mk_eq(is_neg_bit, bv1_1);
|
||||
x_abs = m.mk_ite(is_neg, m_bv_util.mk_bv_neg(x), x);
|
||||
neg_x = m_bv_util.mk_bv_neg(x);
|
||||
x_abs = m.mk_ite(is_neg, neg_x, x);
|
||||
dbg_decouple("fpa2bv_to_fp_signed_is_neg", is_neg);
|
||||
// x_abs has an extra bit in the front.
|
||||
// x_abs is [bv_sz-1, bv_sz-2] . [bv_sz-3 ... 0] * 2^(bv_sz-2)
|
||||
|
|
@ -2736,7 +2749,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
extra_zeros = m_bv_util.mk_numeral(0, extra_bits);
|
||||
sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros);
|
||||
lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz),
|
||||
m_bv_util.mk_numeral(extra_bits, sig_sz));
|
||||
m_bv_util.mk_numeral(extra_bits, sig_sz));
|
||||
bv_sz = bv_sz + extra_bits;
|
||||
SASSERT(is_well_sorted(m, lz));
|
||||
}
|
||||
|
|
@ -2762,15 +2775,16 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
// exp_sz < exp_worst_case_sz and exp >= 0.
|
||||
// Take the maximum legal exponent; this
|
||||
// allows us to keep the most precision.
|
||||
expr_ref max_exp(m), max_exp_bvsz(m);
|
||||
expr_ref max_exp(m), max_exp_bvsz(m), zero_sig_sz(m);
|
||||
mk_max_exp(exp_sz, max_exp);
|
||||
max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp);
|
||||
|
||||
exp_too_large = m_bv_util.mk_ule(m_bv_util.mk_bv_add(
|
||||
max_exp_bvsz,
|
||||
m_bv_util.mk_numeral(1, bv_sz)),
|
||||
s_exp);
|
||||
sig_4 = m.mk_ite(exp_too_large, m_bv_util.mk_numeral(0, sig_sz), sig_4);
|
||||
max_exp_bvsz,
|
||||
m_bv_util.mk_numeral(1, bv_sz)),
|
||||
s_exp);
|
||||
zero_sig_sz = m_bv_util.mk_numeral(0, sig_sz);
|
||||
sig_4 = m.mk_ite(exp_too_large, zero_sig_sz, sig_4);
|
||||
exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2);
|
||||
}
|
||||
dbg_decouple("fpa2bv_to_fp_signed_exp_too_large", exp_too_large);
|
||||
|
|
@ -2795,7 +2809,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
|
|||
|
||||
void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
TRACE("fpa2bv_to_fp_unsigned", for (unsigned i = 0; i < num; i++)
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
|
||||
// This is a conversion from unsigned bitvector to float:
|
||||
// ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
|
||||
|
|
@ -2870,7 +2884,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
extra_zeros = m_bv_util.mk_numeral(0, extra_bits);
|
||||
sig_4 = m_bv_util.mk_concat(shifted_sig, extra_zeros);
|
||||
lz = m_bv_util.mk_bv_add(m_bv_util.mk_concat(extra_zeros, lz),
|
||||
m_bv_util.mk_numeral(extra_bits, sig_sz));
|
||||
m_bv_util.mk_numeral(extra_bits, sig_sz));
|
||||
bv_sz = bv_sz + extra_bits;
|
||||
SASSERT(is_well_sorted(m, lz));
|
||||
}
|
||||
|
|
@ -2886,15 +2900,15 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
// the remaining bits are 0 if ebits is large enough.
|
||||
exp_too_large = m.mk_false(); // This is always in range.
|
||||
|
||||
// The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
|
||||
// exp < bv_sz (+sign bit which is [0])
|
||||
// The exponent is at most bv_sz, i.e., we need ld(bv_sz)+1 ebits.
|
||||
// exp < bv_sz (+sign bit which is [0])
|
||||
unsigned exp_worst_case_sz = (unsigned)((log((double)bv_sz) / log((double)2)) + 1.0);
|
||||
|
||||
if (exp_sz < exp_worst_case_sz) {
|
||||
// exp_sz < exp_worst_case_sz and exp >= 0.
|
||||
// Take the maximum legal exponent; this
|
||||
// allows us to keep the most precision.
|
||||
expr_ref max_exp(m), max_exp_bvsz(m);
|
||||
expr_ref max_exp(m), max_exp_bvsz(m), zero_sig_sz(m);
|
||||
mk_max_exp(exp_sz, max_exp);
|
||||
max_exp_bvsz = m_bv_util.mk_zero_extend(bv_sz - exp_sz, max_exp);
|
||||
|
||||
|
|
@ -2902,7 +2916,8 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
|
|||
max_exp_bvsz,
|
||||
m_bv_util.mk_numeral(1, bv_sz)),
|
||||
s_exp);
|
||||
sig_4 = m.mk_ite(exp_too_large, m_bv_util.mk_numeral(0, sig_sz), sig_4);
|
||||
zero_sig_sz = m_bv_util.mk_numeral(0, sig_sz);
|
||||
sig_4 = m.mk_ite(exp_too_large, zero_sig_sz, sig_4);
|
||||
exp_2 = m.mk_ite(exp_too_large, max_exp, exp_2);
|
||||
}
|
||||
dbg_decouple("fpa2bv_to_fp_unsigned_exp_too_large", exp_too_large);
|
||||
|
|
@ -2941,20 +2956,22 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
|
|||
if (m_hi_fp_unspecified)
|
||||
// The "hardware interpretation" is 01...10...01.
|
||||
nanv = m_bv_util.mk_concat(m_bv_util.mk_numeral(0, 1),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
|
||||
m_bv_util.mk_numeral(1, 1))));
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(-1, ebits),
|
||||
m_bv_util.mk_concat(m_bv_util.mk_numeral(0, sbits - 2),
|
||||
m_bv_util.mk_numeral(1, 1))));
|
||||
else
|
||||
nanv = mk_to_ieee_bv_unspecified(ebits, sbits);
|
||||
|
||||
result = m.mk_ite(x_is_nan, nanv, m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s));
|
||||
expr_ref sgn_e_s(m);
|
||||
sgn_e_s = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s);
|
||||
m_simp.mk_ite(x_is_nan, nanv, sgn_e_s, result);
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result) {
|
||||
TRACE("fpa2bv_to_bv", for (unsigned i = 0; i < num; i++)
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
|
||||
SASSERT(num == 2);
|
||||
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
|
||||
|
|
@ -3016,14 +3033,15 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
sig_sz = m_bv_util.get_bv_size(sig);
|
||||
SASSERT(sig_sz >= (bv_sz + 3));
|
||||
|
||||
expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m);
|
||||
expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), bv0_e2(m), shift_abs(m), shift_le_0(m);
|
||||
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
|
||||
m_bv_util.mk_zero_extend(2, lz));
|
||||
m_bv_util.mk_zero_extend(2, lz));
|
||||
e_m_lz_m_bv_sz = m_bv_util.mk_bv_sub(exp_m_lz,
|
||||
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
|
||||
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
|
||||
shift = m_bv_util.mk_bv_neg(e_m_lz_m_bv_sz);
|
||||
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
|
||||
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), e_m_lz_m_bv_sz, shift);
|
||||
shift_le_0 = m_bv_util.mk_sle(shift, bv0_e2);
|
||||
shift_abs = m.mk_ite(shift_le_0, e_m_lz_m_bv_sz, shift);
|
||||
SASSERT(m_bv_util.get_bv_size(shift) == ebits + 2);
|
||||
SASSERT(m_bv_util.get_bv_size(shift_abs) == ebits + 2);
|
||||
dbg_decouple("fpa2bv_to_bv_shift", shift);
|
||||
|
|
@ -3041,15 +3059,15 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
c_in_limits = m_bv_util.mk_sle(bv0_e2, shift);
|
||||
else
|
||||
c_in_limits = m.mk_or(m_bv_util.mk_sle(m_bv_util.mk_numeral(1, ebits + 2), shift),
|
||||
m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift),
|
||||
m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sig_sz-1)))));
|
||||
m.mk_and(m.mk_eq(m_bv_util.mk_numeral(0, ebits + 2), shift),
|
||||
m.mk_eq(sig, m_bv_util.mk_concat(bv1, m_bv_util.mk_numeral(0, sig_sz-1)))));
|
||||
dbg_decouple("fpa2bv_to_bv_in_limits", c_in_limits);
|
||||
|
||||
expr_ref r_shifted_sig(m), l_shifted_sig(m);
|
||||
r_shifted_sig = m_bv_util.mk_bv_lshr(sig, shift_abs);
|
||||
l_shifted_sig = m_bv_util.mk_bv_shl(sig, m_bv_util.mk_bv_sub(
|
||||
m_bv_util.mk_numeral(m_bv_util.get_bv_size(sig), m_bv_util.get_bv_size(sig)),
|
||||
shift_abs));
|
||||
m_bv_util.mk_numeral(m_bv_util.get_bv_size(sig), m_bv_util.get_bv_size(sig)),
|
||||
shift_abs));
|
||||
dbg_decouple("fpa2bv_to_bv_r_shifted_sig", r_shifted_sig);
|
||||
dbg_decouple("fpa2bv_to_bv_l_shifted_sig", l_shifted_sig);
|
||||
|
||||
|
|
@ -3079,13 +3097,19 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
rnd_has_overflown = m.mk_eq(rnd_overflow, bv1);
|
||||
dbg_decouple("fpa2bv_to_bv_rnd_has_overflown", rnd_has_overflown);
|
||||
|
||||
if (is_signed)
|
||||
rnd = m.mk_ite(m.mk_eq(sgn, bv1), m_bv_util.mk_bv_neg(rnd), rnd);
|
||||
if (is_signed) {
|
||||
expr_ref sgn_eq_1(m), neg_rnd(m);
|
||||
sgn_eq_1 = m.mk_eq(sgn, bv1);
|
||||
neg_rnd = m_bv_util.mk_bv_neg(rnd);
|
||||
m_simp.mk_ite(sgn_eq_1, neg_rnd, rnd, rnd);
|
||||
}
|
||||
|
||||
dbg_decouple("fpa2bv_to_bv_rnd", rnd);
|
||||
|
||||
result = m.mk_ite(rnd_has_overflown, mk_to_ubv_unspecified(ebits, sbits, bv_sz), rnd);
|
||||
result = m.mk_ite(c_in_limits, result, mk_to_ubv_unspecified(ebits, sbits, bv_sz));
|
||||
expr_ref unspec(m);
|
||||
unspec = mk_to_ubv_unspecified(ebits, sbits, bv_sz);
|
||||
result = m.mk_ite(rnd_has_overflown, unspec, rnd);
|
||||
result = m.mk_ite(c_in_limits, result, unspec);
|
||||
result = m.mk_ite(c2, v2, result);
|
||||
result = m.mk_ite(c1, v1, result);
|
||||
|
||||
|
|
@ -3094,13 +3118,13 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
|
|||
|
||||
void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
TRACE("fpa2bv_to_ubv", for (unsigned i = 0; i < num; i++)
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
mk_to_bv(f, num, args, false, result);
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
TRACE("fpa2bv_to_sbv", for (unsigned i = 0; i < num; i++)
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
tout << "arg" << i << " = " << mk_ismt2_pp(args[i], m) << std::endl;);
|
||||
mk_to_bv(f, num, args, true, result);
|
||||
}
|
||||
|
||||
|
|
@ -3571,14 +3595,14 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
|
|||
}
|
||||
|
||||
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
||||
#ifdef Z3DEBUG
|
||||
#ifdef Z3DEBUG
|
||||
return;
|
||||
// CMW: This works only for quantifier-free formulas.
|
||||
expr_ref new_e(m);
|
||||
new_e = m.mk_fresh_const(prefix, m.get_sort(e));
|
||||
m_extra_assertions.push_back(m.mk_eq(new_e, e));
|
||||
e = new_e;
|
||||
#endif
|
||||
#endif
|
||||
}
|
||||
|
||||
expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr * last, expr * round, expr * sticky) {
|
||||
|
|
@ -3598,7 +3622,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr *
|
|||
expr * round_sticky[2] = { round, sticky };
|
||||
last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky);
|
||||
round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky);
|
||||
not_last= m_bv_util.mk_bv_not(last);
|
||||
not_last = m_bv_util.mk_bv_not(last);
|
||||
not_round = m_bv_util.mk_bv_not(round);
|
||||
not_sticky = m_bv_util.mk_bv_not(sticky);
|
||||
not_lors = m_bv_util.mk_bv_not(last_or_sticky);
|
||||
|
|
@ -3613,7 +3637,7 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr *
|
|||
expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m);
|
||||
inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nround_lors));
|
||||
expr *taway_args[2] = { m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, nl_r)),
|
||||
m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(3, nl_nr_sn)) };
|
||||
m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(3, nl_nr_sn)) };
|
||||
inc_taway = m_bv_util.mk_bv_or(2, taway_args);
|
||||
inc_pos = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, pos_args));
|
||||
inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args));
|
||||
|
|
@ -3649,11 +3673,11 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
SASSERT(is_well_sorted(m, exp));
|
||||
|
||||
TRACE("fpa2bv_dbg", tout << "RND: " << std::endl <<
|
||||
"ebits = " << ebits << std::endl <<
|
||||
"sbits = " << sbits << std::endl <<
|
||||
"sgn = " << mk_ismt2_pp(sgn, m) << std::endl <<
|
||||
"sig = " << mk_ismt2_pp(sig, m) << std::endl <<
|
||||
"exp = " << mk_ismt2_pp(exp, m) << std::endl; );
|
||||
"ebits = " << ebits << std::endl <<
|
||||
"sbits = " << sbits << std::endl <<
|
||||
"sgn = " << mk_ismt2_pp(sgn, m) << std::endl <<
|
||||
"sig = " << mk_ismt2_pp(sig, m) << std::endl <<
|
||||
"exp = " << mk_ismt2_pp(exp, m) << std::endl; );
|
||||
|
||||
// Assumptions: sig is of the form f[-1:0] . f[1:sbits-1] [guard,round,sticky],
|
||||
// i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn.
|
||||
|
|
@ -3675,7 +3699,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
mk_max_exp(ebits, e_max);
|
||||
|
||||
TRACE("fpa2bv_dbg", tout << "e_min = " << mk_ismt2_pp(e_min, m) << std::endl <<
|
||||
"e_max = " << mk_ismt2_pp(e_max, m) << std::endl;);
|
||||
"e_max = " << mk_ismt2_pp(e_max, m) << std::endl;);
|
||||
|
||||
expr_ref OVF1(m), e_top_three(m), sigm1(m), e_eq_emax_and_sigm1(m), e_eq_emax(m);
|
||||
expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m), one_1(m), h_exp(m), sh_exp(m), th_exp(m);
|
||||
|
|
@ -3724,7 +3748,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
expr_ref beta(m);
|
||||
beta = m_bv_util.mk_bv_add(m_bv_util.mk_bv_sub(exp, lz), m_bv_util.mk_numeral(1, ebits+2));
|
||||
|
||||
TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m)<< std::endl; );
|
||||
TRACE("fpa2bv_dbg", tout << "beta = " << mk_ismt2_pp(beta, m) << std::endl; );
|
||||
SASSERT(is_well_sorted(m, beta));
|
||||
|
||||
dbg_decouple("fpa2bv_rnd_beta", beta);
|
||||
|
|
@ -3745,12 +3769,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
dbg_decouple("fpa2bv_rnd_sig_before_shift", sig);
|
||||
|
||||
unsigned sig_size = m_bv_util.get_bv_size(sig);
|
||||
SASSERT(sig_size == sbits+4);
|
||||
SASSERT(sig_size == sbits + 4);
|
||||
SASSERT(m_bv_util.get_bv_size(sigma) == ebits+2);
|
||||
unsigned sigma_size = ebits+2;
|
||||
unsigned sigma_size = ebits + 2;
|
||||
|
||||
expr_ref sigma_neg(m), sigma_cap(m), sigma_neg_capped(m), sigma_lt_zero(m), sig_ext(m),
|
||||
rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m);
|
||||
rs_sig(m), ls_sig(m), big_sh_sig(m), sigma_le_cap(m);
|
||||
sigma_neg = m_bv_util.mk_bv_neg(sigma);
|
||||
sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size);
|
||||
sigma_le_cap = m_bv_util.mk_ule(sigma_neg, sigma_cap);
|
||||
|
|
@ -3815,7 +3839,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
dbg_decouple("fpa2bv_rnd_inc", inc);
|
||||
|
||||
sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig),
|
||||
m_bv_util.mk_zero_extend(sbits, inc));
|
||||
m_bv_util.mk_zero_extend(sbits, inc));
|
||||
SASSERT(is_well_sorted(m, sig));
|
||||
dbg_decouple("fpa2bv_rnd_sig_plus_inc", sig);
|
||||
|
||||
|
|
@ -3900,7 +3924,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
|
|||
expr_ref max_sig(m), max_exp(m), inf_sig(m), inf_exp(m);
|
||||
max_sig = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(sbits-1, false), sbits-1);
|
||||
max_exp = m_bv_util.mk_concat(m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1, false), ebits-1),
|
||||
m_bv_util.mk_numeral(0, 1));
|
||||
m_bv_util.mk_numeral(0, 1));
|
||||
inf_sig = m_bv_util.mk_numeral(0, sbits-1);
|
||||
inf_exp = top_exp;
|
||||
|
||||
|
|
@ -3956,8 +3980,8 @@ void fpa2bv_converter::reset(void) {
|
|||
dec_ref_map_key_values(m, m_rm_const2bv);
|
||||
dec_ref_map_key_values(m, m_uf2bvuf);
|
||||
for (obj_map<func_decl, std::pair<app*, app*> >::iterator it = m_specials.begin();
|
||||
it != m_specials.end();
|
||||
it++) {
|
||||
it != m_specials.end();
|
||||
it++) {
|
||||
m.dec_ref(it->m_key);
|
||||
m.dec_ref(it->m_value.first);
|
||||
m.dec_ref(it->m_value.second);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue