mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2016-04-24 09:21:10 -07:00
parent d97bddc3b5 be424d9cbb
commit 271b56aa1b
4 changed files with 321 additions and 300 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -335,10 +335,13 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
}
void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) {
sort * srt = f->get_range();
SASSERT(is_float(srt));
unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt);
mk_pinf(f->get_range(), result);
}
void fpa2bv_converter::mk_pinf(sort * s, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
expr_ref top_exp(m);
mk_top_exp(ebits, top_exp);
mk_fp(m_bv_util.mk_numeral(0, 1),
@ -348,10 +351,13 @@ void fpa2bv_converter::mk_pinf(func_decl * f, expr_ref & result) {
}
void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
sort * srt = f->get_range();
SASSERT(is_float(srt));
unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt);
mk_ninf(f->get_range(), result);
}
void fpa2bv_converter::mk_ninf(sort * s, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
expr_ref top_exp(m);
mk_top_exp(ebits, top_exp);
mk_fp(m_bv_util.mk_numeral(1, 1),
@ -361,23 +367,29 @@ void fpa2bv_converter::mk_ninf(func_decl * f, expr_ref & result) {
}
void fpa2bv_converter::mk_nan(func_decl * f, expr_ref & result) {
sort * srt = f->get_range();
SASSERT(is_float(srt));
unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt);
mk_nan(f->get_range(), result);
}
void fpa2bv_converter::mk_nan(sort * s, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
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),
m_bv_util.mk_numeral(1, sbits - 1),
result);
}
void fpa2bv_converter::mk_nzero(func_decl *f, expr_ref & result) {
sort * srt = f->get_range();
SASSERT(is_float(srt));
unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt);
void fpa2bv_converter::mk_nzero(func_decl * f, expr_ref & result) {
mk_nzero(f->get_range(), result);
}
void fpa2bv_converter::mk_nzero(sort * s, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
expr_ref bot_exp(m);
mk_bot_exp(ebits, bot_exp);
mk_fp(m_bv_util.mk_numeral(1, 1),
@ -386,11 +398,14 @@ void fpa2bv_converter::mk_nzero(func_decl *f, expr_ref & result) {
result);
}
void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) {
sort * srt = f->get_range();
SASSERT(is_float(srt));
unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt);
void fpa2bv_converter::mk_pzero(func_decl * f, expr_ref & result) {
mk_pzero(f->get_range(), result);
}
void fpa2bv_converter::mk_pzero(sort * s, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
expr_ref bot_exp(m);
mk_bot_exp(ebits, bot_exp);
mk_fp(m_bv_util.mk_numeral(0, 1),
@ -399,11 +414,22 @@ void fpa2bv_converter::mk_pzero(func_decl *f, expr_ref & result) {
result);
}
void fpa2bv_converter::mk_one(func_decl *f, expr_ref sign, expr_ref & result) {
sort * srt = f->get_range();
SASSERT(is_float(srt));
unsigned sbits = m_util.get_sbits(srt);
unsigned ebits = m_util.get_ebits(srt);
void fpa2bv_converter::mk_zero(sort * s, expr_ref & sgn, expr_ref & result) {
expr_ref is_pos(m), pzero(m), nzero(m);
is_pos = m.mk_eq(sgn, m_bv_util.mk_numeral(0, 1));
mk_pzero(s, pzero);
mk_nzero(s, nzero);
mk_ite(is_pos, pzero, nzero, result);
}
void fpa2bv_converter::mk_one(func_decl * f, expr_ref & sign, expr_ref & result) {
mk_one(f->get_range(), sign, result);
}
void fpa2bv_converter::mk_one(sort * s, expr_ref & sign, expr_ref & result) {
SASSERT(is_float(s));
unsigned sbits = m_util.get_sbits(s);
unsigned ebits = m_util.get_ebits(s);
mk_fp(sign,
m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-1), ebits),
m_bv_util.mk_numeral(0, sbits-1),
@ -524,15 +550,18 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
SASSERT(num == 3);
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m), x(m), y(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m), y(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
y = args[2];
mk_add(f->get_range(), rm, x, y, result);
}
void fpa2bv_converter::mk_add(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
expr_ref nan(m), nzero(m), pzero(m);
mk_nan(f, nan);
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_nan(s, nan);
mk_nzero(s, nzero);
mk_pzero(s, pzero);
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_neg(m), x_is_inf(m);
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_neg(m), y_is_inf(m);
@ -582,7 +611,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
m_simp.mk_and(x_is_zero, y_is_zero, c4);
m_simp.mk_and(x_is_neg, y_is_neg, signs_and);
m_simp.mk_xor(x_is_neg, y_is_neg, signs_xor);
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
m_simp.mk_and(rm_is_to_neg, signs_xor, rm_and_xor);
m_simp.mk_or(signs_and, rm_and_xor, neg_cond);
mk_ite(neg_cond, nzero, pzero, v4);
@ -595,9 +624,9 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
c6 = y_is_zero;
v6 = x;
//// Actual addition.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
// Actual addition.
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, false);
@ -638,7 +667,7 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
mk_ite(rm_is_to_neg, nzero, pzero, zero_case);
expr_ref rounded(m);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, rounded);
round(s, rm, res_sgn, res_sig, res_exp, rounded);
mk_ite(is_zero_sig, zero_case, rounded, v7);
@ -656,39 +685,55 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
expr_ref rm(m), x(m), y(m);
rm = args[0];
x = args[1];
y = args[2];
mk_sub(f->get_range(), rm, x, y, result);
}
void fpa2bv_converter::mk_sub(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
expr_ref t(m);
mk_neg(f, 1, &args[2], t);
expr * nargs[3] = { args[0], args[1], t };
mk_add(f, 3, nargs, result);
mk_neg(s, y, t);
mk_add(s, rm, x, t, result);
}
void fpa2bv_converter::mk_neg(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
expr * sgn, * s, * e;
split_fp(args[0], sgn, e, s);
expr_ref x(m);
x = args[0];
mk_neg(f->get_range(), x, result);
}
void fpa2bv_converter::mk_neg(sort * srt, expr_ref & x, expr_ref & result) {
expr * sgn, *sig, *e;
split_fp(x, sgn, e, sig);
expr_ref c(m), nsgn(m);
mk_is_nan(args[0], c);
mk_is_nan(x, c);
nsgn = m_bv_util.mk_bv_not(sgn);
expr_ref r_sgn(m);
m_simp.mk_ite(c, sgn, nsgn, r_sgn);
mk_fp(r_sgn, e, s, result);
mk_fp(r_sgn, e, sig, result);
}
void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m), x(m), y(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m), y(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
y = args[2];
mk_mul(f->get_range(), rm, x, y, result);
}
void fpa2bv_converter::mk_mul(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
mk_nan(f, nan);
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_ninf(f, ninf);
mk_pinf(f, pinf);
mk_nan(s, nan);
mk_nzero(s, nzero);
mk_pzero(s, pzero);
mk_ninf(s, ninf);
mk_pinf(s, pinf);
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
@ -748,7 +793,7 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
mk_ite(sign_xor, nzero, pzero, v6);
// else comes the actual multiplication.
unsigned sbits = m_util.get_sbits(f->get_range());
unsigned sbits = m_util.get_sbits(s);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
@ -806,7 +851,7 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(rbits) == 4);
res_sig = m_bv_util.mk_concat(h_p, rbits);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v7);
round(s, rm, res_sgn, res_sig, res_exp, v7);
// And finally, we tie them together.
mk_ite(c6, v6, v7, result);
@ -824,18 +869,20 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 3);
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m), x(m), y(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m), y(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
y = args[2];
mk_div(f->get_range(), rm, x, y, result);
}
void fpa2bv_converter::mk_div(sort * s, expr_ref & rm, expr_ref & x, expr_ref & y, expr_ref & result) {
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
mk_nan(f, nan);
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_ninf(f, ninf);
mk_pinf(f, pinf);
mk_nan(s, nan);
mk_nzero(s, nzero);
mk_pzero(s, pzero);
mk_ninf(s, ninf);
mk_pinf(s, pinf);
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
@ -899,8 +946,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
mk_ite(signs_xor, nzero, pzero, v7);
// else comes the actual division.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
SASSERT(ebits <= sbits);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m), b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
@ -956,7 +1003,7 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
m_simp.mk_ite(shift_cond, res_sig, res_sig_shifted, res_sig);
m_simp.mk_ite(shift_cond, res_exp, res_exp_shifted, res_exp);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v8);
round(s, rm, res_sgn, res_sig, res_exp, v8);
// And finally, we tie them together.
mk_ite(c7, v7, v8, result);
@ -974,21 +1021,22 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
// Remainder is always exact, so there is no rounding mode.
expr_ref x(m), y(m);
x = args[0];
y = args[1];
mk_rem(f->get_range(), x, y, result);
}
void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result) {
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);
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_ninf(f, ninf);
mk_pinf(f, pinf);
mk_nan(s, nan);
mk_nzero(s, nzero);
mk_pzero(s, pzero);
mk_ninf(s, ninf);
mk_pinf(s, pinf);
expr_ref x_is_nan(m), x_is_zero(m), x_is_pos(m), x_is_inf(m);
expr_ref y_is_nan(m), y_is_zero(m), y_is_pos(m), y_is_inf(m);
@ -1033,71 +1081,32 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
c5 = x_is_zero;
v5 = pzero;
// else the actual remainder.
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
expr_ref b_sgn(m), b_sig(m), b_exp(m), b_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
unpack(y, b_sgn, b_sig, b_exp, b_lz, true);
dbg_decouple("fpa2bv_rem_a_sgn", a_sgn);
dbg_decouple("fpa2bv_rem_a_sig", a_sig);
dbg_decouple("fpa2bv_rem_a_exp", a_exp);
dbg_decouple("fpa2bv_rem_a_lz", a_lz);
dbg_decouple("fpa2bv_rem_b_sgn", b_sgn);
dbg_decouple("fpa2bv_rem_b_sig", b_sig);
dbg_decouple("fpa2bv_rem_b_exp", b_exp);
dbg_decouple("fpa2bv_rem_b_lz", b_lz);
BVSLT(a_exp, b_exp, c6);
// exp(x) < exp(y) -> x
expr * x_sgn, *x_sig, *x_exp;
expr * y_sgn, *y_sig, *y_exp;
split_fp(x, x_sgn, x_exp, x_sig);
split_fp(y, y_sgn, y_exp, y_sig);
BVSLT(x_exp, y_exp, c6);
v6 = x;
// max. exponent difference is (2^ebits) - 3
const mpz & two_to_ebits = fu().fm().m_powers2(ebits);
mpz max_exp_diff;
m_mpz_manager.sub(two_to_ebits, 3, max_exp_diff);
SASSERT(m_mpz_manager.is_int64(max_exp_diff));
SASSERT(m_mpz_manager.get_uint64(max_exp_diff) <= UINT_MAX);
// else the actual remainder, r = x - y * n
expr_ref rne(m), nr(m), n(m), yn(m), r(m);
rne = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
mk_div(s, rne, x, y, nr);
mk_round_to_integral(s, rne, nr, n);
mk_mul(s, rne, y, n, yn);
mk_sub(s, rne, x, yn, r);
unsigned int max_exp_diff_ui = (unsigned int)m_mpz_manager.get_uint64(max_exp_diff);
m_mpz_manager.del(max_exp_diff);
expr_ref r_is_zero(m), x_sgn_ref(x_sgn, m), x_sgn_zero(m);
mk_is_zero(r, r_is_zero);
mk_zero(s, x_sgn_ref, x_sgn_zero);
mk_ite(r_is_zero, x_sgn_zero, r, v7);
expr_ref a_exp_ext(m), b_exp_ext(m);
a_exp_ext = m_bv_util.mk_sign_extend(2, a_exp);
b_exp_ext = m_bv_util.mk_sign_extend(2, b_exp);
expr_ref a_lz_ext(m), b_lz_ext(m);
a_lz_ext = m_bv_util.mk_zero_extend(2, a_lz);
b_lz_ext = m_bv_util.mk_zero_extend(2, b_lz);
expr_ref exp_diff(m);
exp_diff = 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));
dbg_decouple("fpa2bv_rem_exp_diff", exp_diff);
// CMW: This creates _huge_ bit-vectors, which is potentially sub-optimal,
// but calculating this via rem = x - y * nearest(x/y) creates huge circuits.
expr_ref huge_sig(m), shifted_sig(m), huge_rem(m);
huge_sig = m_bv_util.mk_zero_extend(max_exp_diff_ui, a_sig);
shifted_sig = m_bv_util.mk_bv_shl(huge_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui + sbits - ebits - 2, exp_diff));
huge_rem = m_bv_util.mk_bv_urem(shifted_sig, m_bv_util.mk_zero_extend(max_exp_diff_ui, b_sig));
dbg_decouple("fpa2bv_rem_huge_rem", huge_rem);
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));
res_exp = m_bv_util.mk_bv_sub(b_exp_ext, b_lz_ext);
// CMW: Actual rounding is not necessary here, this is
// just convenience to get rid of the extra bits.
expr_ref bv_rm(m);
bv_rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v7);
dbg_decouple("fpa2bv_rem_nr", nr);
dbg_decouple("fpa2bv_rem_n", n);
dbg_decouple("fpa2bv_rem_yn", yn);
dbg_decouple("fpa2bv_rem_r", r);
dbg_decouple("fpa2bv_rem_v7", v7);
// And finally, we tie them together.
mk_ite(c6, v6, v7, result);
@ -1302,8 +1311,8 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
// fusedma means (x * y) + z
expr_ref bv_rm(m), x(m), y(m), z(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m), y(m), z(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
y = args[2];
z = args[3];
@ -1335,7 +1344,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
mk_is_inf(z, z_is_inf);
expr_ref rm_is_to_neg(m);
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
dbg_decouple("fpa2bv_fma_x_is_nan", x_is_nan);
dbg_decouple("fpa2bv_fma_x_is_zero", x_is_zero);
@ -1597,7 +1606,7 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args,
mk_ite(rm_is_to_neg, nzero, pzero, zero_case);
expr_ref rounded(m);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, rounded);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);
mk_ite(is_zero_sig, zero_case, rounded, v8);
@ -1619,8 +1628,8 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
SASSERT(num == 2);
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m), x(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
@ -1752,7 +1761,7 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(res_sig) == sbits + 4);
expr_ref rounded(m);
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, rounded);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, rounded);
v5 = rounded;
// And finally, we tie them together.
@ -1768,21 +1777,24 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
SASSERT(num == 2);
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
expr_ref bv_rm(m), x(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
mk_round_to_integral(f->get_range(), rm, x, result);
}
void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result) {
expr_ref rm_is_rta(m), rm_is_rte(m), rm_is_rtp(m), rm_is_rtn(m), rm_is_rtz(m);
mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_is_rta);
mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_is_rte);
mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_is_rtp);
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_rtn);
mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_is_rtz);
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_rta);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_rte);
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_rtp);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_rtn);
mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_rtz);
expr_ref nan(m), nzero(m), pzero(m), ninf(m), pinf(m);
mk_nan(f, nan);
mk_nzero(f, nzero);
mk_pzero(f, pzero);
mk_nan(s, nan);
mk_nzero(s, nzero);
mk_pzero(s, pzero);
expr_ref x_is_zero(m), x_is_pos(m), x_is_neg(m);
mk_is_zero(x, x_is_zero);
@ -1812,14 +1824,16 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
one_1 = m_bv_util.mk_numeral(1, 1);
zero_1 = m_bv_util.mk_numeral(0, 1);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
expr_ref a_sgn(m), a_sig(m), a_exp(m), a_lz(m);
unpack(x, a_sgn, a_sig, a_exp, a_lz, true);
dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig);
dbg_decouple("fpa2bv_r2i_unpacked_sgn", a_sgn);
dbg_decouple("fpa2bv_r2i_unpacked_exp", a_exp);
dbg_decouple("fpa2bv_r2i_unpacked_sig", a_sig);
dbg_decouple("fpa2bv_r2i_unpacked_lz", a_lz);
expr_ref xzero(m), sgn_eq_1(m);
sgn_eq_1 = m.mk_eq(a_sgn, one_1);
@ -1833,8 +1847,8 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
c4 = exp_lt_zero;
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_one(s, zero_1, pone);
mk_one(s, one_1, none);
mk_ite(sgn_eq_1, none, pone, xone);
expr_ref pow_2_sbitsm1(m), m1(m);
@ -1882,49 +1896,53 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
res_sgn = a_sgn;
res_exp = a_exp;
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));
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);
SASSERT(m_bv_util.get_bv_size(a_sig) == sbits);
SASSERT(m_bv_util.get_bv_size(a_exp) == ebits);
expr_ref zero_s(m);
zero_s = m_bv_util.mk_numeral(0, sbits);
expr_ref shift(m), shifted_sig(m), div(m), rem(m);
shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits - 1, sbits),
m_bv_util.mk_zero_extend(sbits-ebits, a_exp));
shifted_sig = m_bv_util.mk_bv_lshr(m_bv_util.mk_concat(a_sig, zero_s),
m_bv_util.mk_concat(zero_s, shift));
div = m_bv_util.mk_extract(2*sbits-1, sbits, shifted_sig);
rem = m_bv_util.mk_extract(sbits-1, 0, shifted_sig);
SASSERT(is_well_sorted(m, div));
SASSERT(is_well_sorted(m, rem));
SASSERT(m_bv_util.get_bv_size(div) == sbits + 1);
SASSERT(m_bv_util.get_bv_size(rem) == sbits + 1);
SASSERT(m_bv_util.get_bv_size(shift) == sbits);
SASSERT(m_bv_util.get_bv_size(div) == sbits);
SASSERT(m_bv_util.get_bv_size(rem) == sbits);
dbg_decouple("fpa2bv_r2i_shifted_sig", shifted_sig);
dbg_decouple("fpa2bv_r2i_shift", shift);
dbg_decouple("fpa2bv_r2i_rshift", rshift);
dbg_decouple("fpa2bv_r2i_div", div);
dbg_decouple("fpa2bv_r2i_rem", rem);
expr_ref div_p1(m);
div_p1 = m_bv_util.mk_bv_add(div, m_bv_util.mk_numeral(1, sbits+1));
div_p1 = m_bv_util.mk_bv_add(div, m_bv_util.mk_numeral(1, sbits));
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);
expr_ref tie_pttrn(m), tie2(m), tie2_c(m), div_last(m), v51(m);
tie_pttrn = m_bv_util.mk_concat(one_1, m_bv_util.mk_numeral(0, sbits-1));
m_simp.mk_eq(rem, tie_pttrn, 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)));
tie2_c = m.mk_ite(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_bv_util.mk_ule(tie_pttrn, rem));
m_simp.mk_ite(tie2_c, div_p1, div, v51);
dbg_decouple("fpa2bv_r2i_v51", v51);
dbg_decouple("fpa2bv_r2i_tie2", tie2);
dbg_decouple("fpa2bv_r2i_tie2_c", tie2_c);
SASSERT(is_well_sorted(m, tie2));
SASSERT(is_well_sorted(m, tie2_c));
SASSERT(is_well_sorted(m, v51));
expr_ref c521(m), v52(m), rem_eq_0(m), sgn_eq_zero(m);
rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits + 1));
rem_eq_0 = m.mk_eq(rem, m_bv_util.mk_numeral(0, sbits));
sgn_eq_zero = m.mk_eq(res_sgn, zero_1);
m_simp.mk_not(rem_eq_0, c521);
m_simp.mk_and(c521, sgn_eq_zero, c521);
@ -1945,14 +1963,14 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
m_simp.mk_ite(c53, v53, res_sig, res_sig);
m_simp.mk_ite(c52, v52, res_sig, res_sig);
m_simp.mk_ite(c51, v51, res_sig, res_sig);
res_sig = m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3)); // rounding bits are all 0.
res_sig = m_bv_util.mk_zero_extend(1, m_bv_util.mk_concat(res_sig, m_bv_util.mk_numeral(0, 3))); // rounding bits are all 0.
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits);
SASSERT(m_bv_util.get_bv_size(shift) == sbits + 1);
SASSERT(m_bv_util.get_bv_size(shift) == sbits);
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), 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);
@ -1961,7 +1979,7 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
SASSERT(m_bv_util.get_bv_size(res_exp) == ebits + 2);
// CMW: We use the rounder for normalization.
round(f->get_range(), bv_rm, res_sgn, res_sig, res_exp, v6);
round(s, rm, res_sgn, res_sig, res_exp, v6);
// And finally, we tie them together.
mk_ite(c5, v5, v6, result);
@ -2683,8 +2701,8 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
SASSERT(m_bv_util.is_bv(args[1]));
expr_ref bv_rm(m), x(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
dbg_decouple("fpa2bv_to_fp_signed_x", x);
@ -2692,7 +2710,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
unsigned bv_sz = m_bv_util.get_bv_size(x);
SASSERT(m_bv_util.get_bv_size(bv_rm) == 3);
SASSERT(m_bv_util.get_bv_size(rm) == 3);
expr_ref bv0_1(m), bv1_1(m), bv0_sz(m), bv1_sz(m);
bv0_1 = m_bv_util.mk_numeral(0, 1);
@ -2802,7 +2820,7 @@ void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const
SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
expr_ref v2(m);
round(f->get_range(), bv_rm, sgn, sig, exp, v2);
round(f->get_range(), rm, sgn, sig, exp, v2);
mk_ite(c1, v1, v2, result);
}
@ -2825,8 +2843,8 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
SASSERT(m_bv_util.is_bv(args[1]));
expr_ref bv_rm(m), x(m);
bv_rm = to_app(args[0])->get_arg(0);
expr_ref rm(m), x(m);
rm = to_app(args[0])->get_arg(0);
x = args[1];
dbg_decouple("fpa2bv_to_fp_unsigned_x", x);
@ -2834,7 +2852,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
unsigned bv_sz = m_bv_util.get_bv_size(x);
SASSERT(m_bv_util.get_bv_size(bv_rm) == 3);
SASSERT(m_bv_util.get_bv_size(rm) == 3);
expr_ref bv0_1(m), bv1_1(m), bv0_sz(m), bv1_sz(m);
bv0_1 = m_bv_util.mk_numeral(0, 1);
@ -2935,7 +2953,7 @@ void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * con
SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
expr_ref v2(m);
round(f->get_range(), bv_rm, sgn, sig, exp, v2);
round(f->get_range(), rm, sgn, sig, exp, v2);
mk_ite(c1, v1, v2, result);
}
@ -2977,7 +2995,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
SASSERT(is_app_of(args[0], m_util.get_family_id(), OP_FPA_INTERNAL_RM));
SASSERT(m_util.is_float(args[1]));
expr * bv_rm = to_app(args[0])->get_arg(0);
expr * rm = to_app(args[0])->get_arg(0);
expr * x = args[1];
sort * xs = m.get_sort(x);
sort * bv_srt = f->get_range();
@ -3080,7 +3098,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args
dbg_decouple("fpa2bv_to_bv_sticky", sticky);
expr_ref rounding_decision(m);
rounding_decision = mk_rounding_decision(bv_rm, sgn, last, round, sticky);
rounding_decision = mk_rounding_decision(rm, sgn, last, round, sticky);
SASSERT(m_bv_util.get_bv_size(rounding_decision) == 1);
dbg_decouple("fpa2bv_to_bv_rounding_decision", rounding_decision);
@ -3382,7 +3400,7 @@ void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
m_simp.mk_not(or_ex, result);
}
void fpa2bv_converter::mk_is_rm(expr * bv_rm, BV_RM_VAL rm, expr_ref & result) {
void fpa2bv_converter::mk_is_rm(expr * rme, BV_RM_VAL rm, expr_ref & result) {
expr_ref rm_num(m);
rm_num = m_bv_util.mk_numeral(rm, 3);
@ -3393,7 +3411,7 @@ void fpa2bv_converter::mk_is_rm(expr * bv_rm, BV_RM_VAL rm, expr_ref & result) {
case BV_RM_TO_NEGATIVE:
case BV_RM_TO_POSITIVE:
case BV_RM_TO_ZERO:
return m_simp.mk_eq(bv_rm, rm_num, result);
return m_simp.mk_eq(rme, rm_num, result);
default:
UNREACHABLE();
}
@ -3598,15 +3616,34 @@ void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#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;
if (is_app_of(e, m_plugin->get_family_id(), OP_FPA_FP)) {
expr_ref new_bv(m);
expr *e_sgn, *e_sig, *e_exp;
split_fp(e, e_sgn, e_exp, e_sig);
unsigned ebits = m_bv_util.get_bv_size(e_exp);
unsigned sbits = m_bv_util.get_bv_size(e_sig) + 1;
unsigned bv_sz = ebits + sbits;
new_bv = m.mk_fresh_const(prefix, m_bv_util.mk_sort(bv_sz));
expr_ref bv_sgn(m), bv_exp(m), bv_sig(m);
bv_sgn = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, new_bv);
bv_exp = m_bv_util.mk_extract(bv_sz-2, bv_sz-ebits-1, new_bv);
bv_sig = m_bv_util.mk_extract(sbits-2, 0, new_bv);
m_extra_assertions.push_back(m.mk_eq(e_sgn, bv_sgn));
m_extra_assertions.push_back(m.mk_eq(e_exp, bv_exp));
m_extra_assertions.push_back(m.mk_eq(e_sig, bv_sig));
e = m_util.mk_fp(bv_sgn, bv_exp, bv_sig);
}
else {
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
}
expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr * last, expr * round, expr * sticky) {
expr_ref rmr(bv_rm, m);
expr_ref fpa2bv_converter::mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky) {
expr_ref rmr(rm, m);
expr_ref sgnr(sgn, m);
expr_ref lastr(last, m);
expr_ref roundr(round, m);
@ -3645,10 +3682,10 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr *
expr_ref res(m), inc_c2(m), inc_c3(m), inc_c4(m);
expr_ref rm_is_to_neg(m), rm_is_to_pos(m), rm_is_away(m), rm_is_even(m), nil_1(m);
nil_1 = m_bv_util.mk_numeral(0, 1);
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
mk_is_rm(bv_rm, BV_RM_TIES_TO_AWAY, rm_is_away);
mk_is_rm(bv_rm, BV_RM_TIES_TO_EVEN, rm_is_even);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_is_away);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even);
m_simp.mk_ite(rm_is_to_neg, inc_neg, nil_1, inc_c4);
m_simp.mk_ite(rm_is_to_pos, inc_pos, inc_c4, inc_c3);
m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
@ -3658,16 +3695,16 @@ expr_ref fpa2bv_converter::mk_rounding_decision(expr * bv_rm, expr * sgn, expr *
return res;
}
void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result) {
void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result) {
unsigned ebits = m_util.get_ebits(s);
unsigned sbits = m_util.get_sbits(s);
dbg_decouple("fpa2bv_rnd_rm", bv_rm);
dbg_decouple("fpa2bv_rnd_rm", rm);
dbg_decouple("fpa2bv_rnd_sgn", sgn);
dbg_decouple("fpa2bv_rnd_sig", sig);
dbg_decouple("fpa2bv_rnd_exp", exp);
SASSERT(is_well_sorted(m, bv_rm));
SASSERT(is_well_sorted(m, rm));
SASSERT(is_well_sorted(m, sgn));
SASSERT(is_well_sorted(m, sig));
SASSERT(is_well_sorted(m, exp));
@ -3683,7 +3720,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
// i.e., it has 2 + (sbits-1) + 3 = sbits + 4 bits, where the first one is in sgn.
// Furthermore, note that sig is an unsigned bit-vector, while exp is signed.
SASSERT(m_bv_util.is_bv(bv_rm) && m_bv_util.get_bv_size(bv_rm) == 3);
SASSERT(m_bv_util.is_bv(rm) && m_bv_util.get_bv_size(rm) == 3);
SASSERT(m_bv_util.is_bv(sgn) && m_bv_util.get_bv_size(sgn) == 1);
SASSERT(m_bv_util.is_bv(sig) && m_bv_util.get_bv_size(sig) >= 5);
SASSERT(m_bv_util.is_bv(exp) && m_bv_util.get_bv_size(exp) >= 4);
@ -3833,7 +3870,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
sig = m_bv_util.mk_extract(sbits+1, 2, sig);
expr_ref inc(m);
inc = mk_rounding_decision(bv_rm, sgn, last, round, sticky);
inc = mk_rounding_decision(rm, sgn, last, round, sticky);
SASSERT(m_bv_util.get_bv_size(inc) == 1 && is_well_sorted(m, inc));
dbg_decouple("fpa2bv_rnd_inc", inc);
@ -3906,9 +3943,9 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re
nil_1 = m_bv_util.mk_numeral(0, 1);
expr_ref rm_is_to_zero(m), rm_is_to_neg(m), rm_is_to_pos(m), rm_zero_or_neg(m), rm_zero_or_pos(m);
mk_is_rm(bv_rm, BV_RM_TO_ZERO, rm_is_to_zero);
mk_is_rm(bv_rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_is_rm(bv_rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
mk_is_rm(rm, BV_RM_TO_ZERO, rm_is_to_zero);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_is_to_pos);
m_simp.mk_or(rm_is_to_zero, rm_is_to_neg, rm_zero_or_neg);
m_simp.mk_or(rm_is_to_zero, rm_is_to_pos, rm_zero_or_pos);
dbg_decouple("fpa2bv_rnd_rm_is_to_zero", rm_is_to_zero);

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

@ -145,7 +145,7 @@ public:
expr_ref_vector m_extra_assertions;
protected:
void mk_one(func_decl *f, expr_ref sign, expr_ref & result);
void mk_one(func_decl *f, expr_ref & sign, expr_ref & result);
void mk_is_nan(expr * e, expr_ref & result);
void mk_is_inf(expr * e, expr_ref & result);
@ -184,6 +184,23 @@ protected:
void mk_to_bv(func_decl * f, unsigned num, expr * const * args, bool is_signed, expr_ref & result);
void mk_uninterpreted_output(sort * rng, func_decl * fbv, expr_ref_buffer & new_args, expr_ref & result);
private:
void mk_nan(sort * s, expr_ref & result);
void mk_nzero(sort * s, expr_ref & result);
void mk_pzero(sort * s, expr_ref & result);
void mk_zero(sort * s, expr_ref & sgn, expr_ref & result);
void mk_ninf(sort * s, expr_ref & result);
void mk_pinf(sort * s, expr_ref & result);
void mk_one(sort * s, expr_ref & sign, expr_ref & result);
void mk_neg(sort * s, expr_ref & x, expr_ref & result);
void mk_add(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
void mk_sub(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
void mk_mul(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
void mk_div(sort * s, expr_ref & bv_rm, expr_ref & x, expr_ref & y, expr_ref & result);
void mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & result);
void mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & x, expr_ref & result);
};
#endif

85
src/util/hwf.cpp
View file

@ -38,13 +38,13 @@ Revision History:
// Note:
// Which FPU will be used is determined by compiler settings. On x64 it's always SSE2,
// on x86 we have to chose SSE2 by enabling /arch:SSE2 (otherwise the x87 FPU will be used).
// on x86 we have to chose SSE2 by enabling /arch:SSE2 (otherwise the x87 FPU will be used).
// Christoph has decided that we don't want to use the x87; this makes everything a lot easier.
// For SSE2, it is best to use compiler intrinsics because this makes it completely
// clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects
// the x87 FPU, even when /arch:SSE2 is on.
// the x87 FPU, even when /arch:SSE2 is on.
// Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
#ifdef __clang__
#undef USE_INTRINSICS
@ -56,19 +56,19 @@ Revision History:
hwf_manager::hwf_manager() :
m_mpz_manager(m_mpq_manager)
{
{
#ifdef _WINDOWS
#if defined(_AMD64_) || defined(_M_IA64)
// Precision control is not supported on x64.
// Precision control is not supported on x64.
// See: http://msdn.microsoft.com/en-us/library/e9b52ceh(VS.110).aspx
// CMW: I think this is okay though, the compiler will chose the right instructions
// CMW: I think this is okay though, the compiler will chose the right instructions
// (the x64/SSE2 FPU has separate instructions for different precisions).
#else
// Setting the precision should only be required on the x87, but it won't hurt to do it anyways.
// _PC_53 means double precision (53 significand bits). For extended precision use _PC_64.
#ifndef USE_INTRINSICS
__control87_2(_PC_53, _MCW_PC, &x86_state, &sse2_state);
__control87_2(_PC_53, _MCW_PC, &x86_state, &sse2_state);
#endif
#endif
#else
@ -78,7 +78,7 @@ hwf_manager::hwf_manager() :
// We only set the precision of the FPU here in the constructor. At the moment, there are no
// other parts of the code that could overwrite this, and Windows takes care of context switches.
// CMW: I'm not sure what happens on CPUs with hyper-threading (since the FPU is shared).
// CMW: I'm not sure what happens on CPUs with hyper-threading (since the FPU is shared).
// I have yet to discover whether Linux and OSX save the FPU state when switching context.
// As long as we stick to using the SSE2 FPU though, there shouldn't be any problems with respect
// to the precision (not sure about the rounding modes though).
@ -104,7 +104,7 @@ void hwf_manager::set(hwf & o, double value) {
o.value = value;
}
void hwf_manager::set(hwf & o, float value) {
void hwf_manager::set(hwf & o, float value) {
o.value = (double)value;
}
@ -113,7 +113,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & value) {
o.value = m_mpq_manager.get_double(value);
}
void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) {
void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) {
// We expect [i].[f]P[e], where P means that the exponent is interpreted as 2^e instead of 10^e.
std::string v(value);
@ -123,17 +123,17 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, char const * value) {
std::string f, e;
f = (e_pos != std::string::npos) ? v.substr(0, e_pos) : v;
e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0";
e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0";
TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;);
TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;);
mpq q;
mpq q;
m_mpq_manager.set(q, f.c_str());
mpz ex;
m_mpz_manager.set(ex, e.c_str());
set(o, rm, q, ex);
set(o, rm, q, ex);
TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;);
}
@ -142,7 +142,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp
// Assumption: this represents significand * 2^exponent.
set_rounding_mode(rm);
mpq sig;
mpq sig;
m_mpq_manager.set(sig, significand);
int64 exp = m_mpz_manager.get_int64(exponent);
@ -150,7 +150,7 @@ void hwf_manager::set(hwf & o, mpf_rounding_mode rm, mpq const & significand, mp
o.value = 0.0;
else
{
while (m_mpq_manager.lt(sig, 1))
while (m_mpq_manager.lt(sig, 1))
{
m_mpq_manager.mul(sig, 2, sig);
exp--;
@ -176,7 +176,7 @@ void hwf_manager::set(hwf & o, hwf const & x) {
o.value = x.value;
}
void hwf_manager::abs(hwf & o) {
void hwf_manager::abs(hwf & o) {
o.value = fabs(o.value);
}
@ -244,14 +244,14 @@ void hwf_manager::mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
// On the x86 FPU (x87), we use custom assembly routines because
// the code generated for x*y and x/y suffers from the double
// rounding on underflow problem. The scaling trick is described
// in Roger Golliver: `Efficiently producing default orthogonal IEEE
// in Roger Golliver: `Efficiently producing default orthogonal IEEE
// double results using extended IEEE hardware', see
// http://www.open-std.org/JTC1/SC22/JSG/docs/m3/docs/jsgn326.pdf
// CMW: Tthis is not really needed if we use only the SSE2 FPU,
// it shouldn't hurt the performance too much though.
static const int const1 = -DBL_SCALE;
static const int const2 = +DBL_SCALE;
static const int const2 = +DBL_SCALE;
double xv = x.value;
double yv = y.value;
double & ov = o.value;
@ -266,14 +266,14 @@ void hwf_manager::mul(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
fxch st(1);
fscale;
fstp ov;
}
}
#endif
}
void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf & o) {
set_rounding_mode(rm);
#ifdef USE_INTRINSICS
_mm_store_sd(&o.value, _mm_div_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
_mm_store_sd(&o.value, _mm_div_sd(_mm_set_sd(x.value), _mm_set_sd(y.value)));
#else
o.value = x.value / y.value;
#endif
@ -306,18 +306,18 @@ void hwf_manager::div(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf &
#endif
void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf const &z, hwf & o) {
// CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium,
// CMW: fused_mul_add is not available on most CPUs. As of 2012, only Itanium,
// Intel Sandybridge and AMD Bulldozers support that (via AVX).
set_rounding_mode(rm);
#ifdef _M_IA64
// IA64 (Itanium) will do it, if contractions are on.
// IA64 (Itanium) will do it, if contractions are on.
o.value = x.value * y.value + z.value;
#else
#if defined(_WINDOWS)
#if defined(_WINDOWS)
#if _MSC_VER >= 1800
o.value = ::fma(x.value, y.value, z.value);
o.value = ::fma(x.value, y.value, z.value);
#else // Windows, older than VS 2013
#ifdef USE_INTRINSICS
_mm_store_sd(&o.value, _mm_fmadd_sd(_mm_set_sd(x.value), _mm_set_sd(y.value), _mm_set_sd(z.value)));
@ -351,7 +351,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
// CMW: modf is not the right function here.
// modf(x.value, &o.value);
// According to the Intel Architecture manual, the x87-instrunction FRNDINT is the
// According to the Intel Architecture manual, the x87-instrunction FRNDINT is the
// same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
#ifdef _WINDOWS
#ifdef USE_INTRINSICS
@ -383,17 +383,10 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
}
void hwf_manager::rem(hwf const & x, hwf const & y, hwf & o) {
// The built-in fmod() works, except for the special numbers.
o.value = remainder(x.value, y.value);
if (is_inf(x) && is_inf(y))
o.value = x.value/y.value; // NaN
else if (is_inf(y))
o.value = x.value;
else
o.value = fmod(x.value, y.value);
// Here is an x87 alternative if the above makes problems; this may also be faster.
#if 0
// Here is an x87 alternative if the above makes problems; this may also be faster.
double xv = x.value;
double yv = y.value;
double & ov = o.value;
@ -423,7 +416,7 @@ void hwf_manager::maximum(hwf const & x, hwf const & y, hwf & o) {
o.value = x.value;
else if (lt(x, y))
o.value = y.value;
else
else
o.value = x.value;
#endif
}
@ -439,12 +432,12 @@ void hwf_manager::minimum(hwf const & x, hwf const & y, hwf & o) {
o.value = x.value;
else if (lt(x, y))
o.value = x.value;
else
else
o.value = y.value;
#endif
}
std::string hwf_manager::to_string(hwf const & x) {
std::string hwf_manager::to_string(hwf const & x) {
std::stringstream ss("");
ss << std::scientific << x.value;
return ss.str();
@ -488,9 +481,9 @@ void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o)
int e = exp(x);
if (e >= 0)
qm.mul2k(n, (unsigned)e);
else
else
qm.mul2k(d, (unsigned)-e);
qm.set(o, n, d);
qm.set(o, n, d);
}
bool hwf_manager::is_zero(hwf const & x) {
@ -559,13 +552,13 @@ bool hwf_manager::is_denormal(hwf const & x) {
(t & 0x000FFFFFFFFFFFFFull) != 0x0);
}
bool hwf_manager::is_regular(hwf const & x) {
bool hwf_manager::is_regular(hwf const & x) {
// Everything that doesn't have the top-exponent is considered regular.
// Note that +-0.0 and denormal numbers have exponent==0; these are regular.
// All normal numbers are also regular. What remains is +-Inf and NaN, they are
// All normal numbers are also regular. What remains is +-Inf and NaN, they are
// not regular and they are the only numbers that have exponent 7FF.
uint64 e = RAW(x.value) & 0x7FF0000000000000ull; // the exponent
return (e != 0x7FF0000000000000ull);
return (e != 0x7FF0000000000000ull);
}
bool hwf_manager::is_int(hwf const & x) {
@ -596,8 +589,8 @@ void hwf_manager::mk_pzero(hwf & o) {
}
void hwf_manager::mk_zero(bool sign, hwf & o) {
if (sign)
mk_nzero(o);
if (sign)
mk_nzero(o);
else
mk_pzero(o);
}
@ -627,7 +620,7 @@ void hwf_manager::mk_ninf(hwf & o) {
#ifdef USE_INTRINSICS
#define SETRM(RM) _MM_SET_ROUNDING_MODE(RM)
#else
#define SETRM(RM) _controlfp_s(&sse2_state, RM, _MCW_RC);
#define SETRM(RM) _controlfp_s(&sse2_state, RM, _MCW_RC);
#endif
#else
#ifdef USE_INTRINSICS
@ -691,7 +684,7 @@ void hwf_manager::set_rounding_mode(mpf_rounding_mode rm)
#endif
#else // OSX/Linux
switch (rm) {
case MPF_ROUND_NEAREST_TEVEN:
case MPF_ROUND_NEAREST_TEVEN:
SETRM(FE_TONEAREST);
break;
case MPF_ROUND_TOWARD_POSITIVE:

56
src/util/mpf.cpp
View file

@ -1077,21 +1077,20 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
unsigned shift = (o.sbits - 1) - ((unsigned)o.exponent);
const mpz & shift_p = m_powers2(shift);
const mpz & shiftm1_p = m_powers2(shift-1);
TRACE("mpf_dbg", tout << "shift=" << shift << std::endl;);
TRACE("mpf_dbg", tout << "shiftm1_p=" << m_mpz_manager.to_string(shiftm1_p) << std::endl;);
scoped_mpz div(m_mpz_manager), rem(m_mpz_manager);
m_mpz_manager.machine_div_rem(o.significand, shift_p, div, rem);
TRACE("mpf_dbg", tout << "div=" << m_mpz_manager.to_string(div) << " rem=" << m_mpz_manager.to_string(rem) << std::endl;);
const mpz & shift_p1 = m_powers2(shift-1);
TRACE("mpf_dbg", tout << "shift_p1=" << m_mpz_manager.to_string(shift_p1) << std::endl;);
switch (rm) {
case MPF_ROUND_NEAREST_TEVEN:
case MPF_ROUND_NEAREST_TAWAY: {
bool tie = m_mpz_manager.eq(rem, shift_p1);
bool less_than_tie = m_mpz_manager.lt(rem, shift_p1);
bool more_than_tie = m_mpz_manager.gt(rem, shift_p1);
bool tie = m_mpz_manager.eq(rem, shiftm1_p);
bool less_than_tie = m_mpz_manager.lt(rem, shiftm1_p);
bool more_than_tie = m_mpz_manager.gt(rem, shiftm1_p);
TRACE("mpf_dbg", tout << "tie= " << tie << "; <tie = " << less_than_tie << "; >tie = " << more_than_tie << std::endl;);
if (tie) {
if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
@ -1231,43 +1230,18 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
else if (is_zero(x))
set(o, x);
else {
o.ebits = x.ebits;
o.sbits = x.sbits;
o.sign = x.sign;
// r = x - y * n
scoped_mpf nr(*this), n(*this), yn(*this);
div(MPF_ROUND_NEAREST_TEVEN, x, y, nr);
round_to_integral(MPF_ROUND_NEAREST_TEVEN, nr, n);
mul(MPF_ROUND_NEAREST_TEVEN, y, n, yn);
sub(MPF_ROUND_NEAREST_TEVEN, x, yn, o);
scoped_mpf a(*this), b(*this);
set(a, x);
set(b, y);
unpack(a, true);
unpack(b, true);
if (is_zero(o))
o.sign = x.sign;
TRACE("mpf_dbg", tout << "A = " << to_string(a) << std::endl;);
TRACE("mpf_dbg", tout << "B = " << to_string(b) << std::endl;);
if (a.exponent() < b.exponent())
set(o, x);
else {
mpf_exp_t exp_diff = a.exponent() - b.exponent();
SASSERT(exp_diff >= 0);
TRACE("mpf_dbg", tout << "exp_diff = " << exp_diff << std::endl;);
SASSERT(exp_diff < INT_MAX);
// CMW: This requires rather a lot of memory. There are algorithms that trade space for time by
// computing only a small chunk of the remainder bits at a time.
unsigned extra_bits = (unsigned) exp_diff;
m_mpz_manager.mul2k(a.significand(), extra_bits);
m_mpz_manager.rem(a.significand(), b.significand(), o.significand);
TRACE("mpf_dbg", tout << "REM' = " << to_string(o) << std::endl;);
if (m_mpz_manager.is_zero(o.significand))
mk_zero(o.ebits, o.sbits, o.sign, o);
else {
o.exponent = b.exponent();
m_mpz_manager.mul2k(o.significand, 3); // rounding bits
round(MPF_ROUND_NEAREST_TEVEN, o);
}
}
TRACE("mpf_dbg", tout << "N = " << to_string(n) << std::endl;);
TRACE("mpf_dbg", tout << "YN = " << to_string(yn) << std::endl;);
}
TRACE("mpf_dbg", tout << "REMAINDER = " << to_string(o) << std::endl;);