mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-03-02 21:03:15 -08:00
commit ed846a9ff3
11 changed files with 712 additions and 347 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/float_decl_plugin.cpp
View file

@ -151,6 +151,10 @@ sort * float_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) { if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) {
m_manager->raise_exception("expecting two integer parameters to floating point sort"); m_manager->raise_exception("expecting two integer parameters to floating point sort");
} }
if (parameters[0].get_int() <= 1 || parameters[1].get_int() <= 1)
m_manager->raise_exception("floating point sorts need parameters > 1");
if (parameters[0].get_int() > parameters[1].get_int())
m_manager->raise_exception("floating point sorts with ebits > sbits are currently not supported");
return mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); return mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
case ROUNDING_MODE_SORT: case ROUNDING_MODE_SORT:
return mk_rm_sort(); return mk_rm_sort();

339
src/tactic/fpa/fpa2bv_converter.cpp
View file

@ -21,8 +21,8 @@ Notes:
#include"fpa2bv_converter.h" #include"fpa2bv_converter.h"
#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); m_simp.mk_and(m_bv_util.mk_ule(X,Y), bvult_not, R); } #define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
#define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); m_simp.mk_and(m_bv_util.mk_sle(X,Y), bvslt_not, R); } #define BVSLT(X,Y,R) { expr_ref bvslt_eq(m), bvslt_not(m); m_simp.mk_eq(X, Y, bvslt_eq); m_simp.mk_not(bvslt_eq, bvslt_not); expr_ref t(m); t = m_bv_util.mk_sle(X,Y); m_simp.mk_and(t, bvslt_not, R); }
fpa2bv_converter::fpa2bv_converter(ast_manager & m) : fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m(m), m(m),
@ -123,17 +123,23 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
unsigned ebits = m_util.get_ebits(srt); unsigned ebits = m_util.get_ebits(srt);
unsigned sbits = m_util.get_sbits(srt); unsigned sbits = m_util.get_sbits(srt);
expr_ref sgn(m), s(m), e(m);
sort_ref s_sgn(m), s_sig(m), s_exp(m);
s_sgn = m_bv_util.mk_sort(1);
s_sig = m_bv_util.mk_sort(sbits-1);
s_exp = m_bv_util.mk_sort(ebits);
#ifdef _DEBUG #ifdef _DEBUG
std::string p("fpa2bv"); std::string p("fpa2bv");
std::string name = f->get_name().str(); std::string name = f->get_name().str();
expr * sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), m_bv_util.mk_sort(1)); sgn = m.mk_fresh_const((p + "_sgn_" + name).c_str(), s_sgn);
expr * s = m.mk_fresh_const((p + "_sig_" + name).c_str(), m_bv_util.mk_sort(sbits-1)); s = m.mk_fresh_const((p + "_sig_" + name).c_str(), s_sig);
expr * e = m.mk_fresh_const((p + "_exp_" + name).c_str(), m_bv_util.mk_sort(ebits)); e = m.mk_fresh_const((p + "_exp_" + name).c_str(), s_exp);
#else #else
expr * sgn = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); sgn = m.mk_fresh_const(0, s_sgn);
expr * s = m.mk_fresh_const(0, m_bv_util.mk_sort(sbits-1)); s = m.mk_fresh_const(0, s_sig);
expr * e = m.mk_fresh_const(0, m_bv_util.mk_sort(ebits)); e = m.mk_fresh_const(0, s_exp);
#endif #endif
mk_triple(sgn, s, e, result); mk_triple(sgn, s, e, result);
@ -245,9 +251,10 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
dbg_decouple("fpa2bv_add_exp_delta", exp_delta); dbg_decouple("fpa2bv_add_exp_delta", exp_delta);
// cap the delta // cap the delta
expr_ref cap(m); expr_ref cap(m), cap_le_delta(m);
cap = m_bv_util.mk_numeral(sbits+2, ebits); cap = m_bv_util.mk_numeral(sbits+2, ebits);
m_simp.mk_ite(m_bv_util.mk_ule(cap, exp_delta), cap, exp_delta, exp_delta); cap_le_delta = m_bv_util.mk_ule(cap, exp_delta);
m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta);
dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta); dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta);
@ -270,21 +277,23 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
SASSERT(is_well_sorted(m, shifted_d_sig)); SASSERT(is_well_sorted(m, shifted_d_sig));
sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big); sticky_raw = m_bv_util.mk_extract(sbits+2, 0, shifted_big);
expr_ref sticky_eq(m); expr_ref sticky_eq(m), nil_sbit3(m), one_sbit3(m);
m_simp.mk_eq(sticky_raw, m_bv_util.mk_numeral(0, sbits+3), sticky_eq); nil_sbit3 = m_bv_util.mk_numeral(0, sbits+3);
m_simp.mk_ite(sticky_eq, one_sbit3 = m_bv_util.mk_numeral(1, sbits+3);
m_bv_util.mk_numeral(0, sbits+3), m_simp.mk_eq(sticky_raw, nil_sbit3, sticky_eq);
m_bv_util.mk_numeral(1, sbits+3), m_simp.mk_ite(sticky_eq, nil_sbit3, one_sbit3, sticky);
sticky);
SASSERT(is_well_sorted(m, sticky)); SASSERT(is_well_sorted(m, sticky));
expr * or_args[2] = { shifted_d_sig.get(), sticky.get() }; expr * or_args[2] = { shifted_d_sig, sticky };
shifted_d_sig = m_bv_util.mk_bv_or(2, or_args); shifted_d_sig = m_bv_util.mk_bv_or(2, or_args);
SASSERT(is_well_sorted(m, shifted_d_sig)); SASSERT(is_well_sorted(m, shifted_d_sig));
expr_ref eq_sgn(m), neq_sgn(m); expr_ref eq_sgn(m);
m_simp.mk_eq(c_sgn, d_sgn, eq_sgn); m_simp.mk_eq(c_sgn, d_sgn, eq_sgn);
// dbg_decouple("fpa2bv_add_eq_sgn", eq_sgn);
TRACE("fpa2bv_add_core", tout << "EQ_SGN = " << mk_ismt2_pp(eq_sgn, m) << std::endl; );
// two extra bits for catching the overflow. // two extra bits for catching the overflow.
c_sig = m_bv_util.mk_zero_extend(2, c_sig); c_sig = m_bv_util.mk_zero_extend(2, c_sig);
shifted_d_sig = m_bv_util.mk_zero_extend(2, shifted_d_sig); shifted_d_sig = m_bv_util.mk_zero_extend(2, shifted_d_sig);
@ -315,14 +324,19 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, expr_ref & rm,
family_id bvfid = m_bv_util.get_fid(); family_id bvfid = m_bv_util.get_fid();
expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m); expr_ref res_sgn_c1(m), res_sgn_c2(m), res_sgn_c3(m);
res_sgn_c1 = m.mk_app(bvfid, OP_BAND, m_bv_util.mk_bv_not(c_sgn), d_sgn, sign_bv); expr_ref not_c_sgn(m), not_d_sgn(m), not_sign_bv(m);
res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, m_bv_util.mk_bv_not(d_sgn), m_bv_util.mk_bv_not(sign_bv)); not_c_sgn = m_bv_util.mk_bv_not(c_sgn);
not_d_sgn = m_bv_util.mk_bv_not(d_sgn);
not_sign_bv = m_bv_util.mk_bv_not(sign_bv);
res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_c_sgn, d_sgn, sign_bv);
res_sgn_c2 = m.mk_app(bvfid, OP_BAND, c_sgn, not_d_sgn, not_sign_bv);
res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, c_sgn, d_sgn);
expr * res_sgn_or_args[3] = { res_sgn_c1.get(), res_sgn_c2.get(), res_sgn_c3.get() }; expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 };
res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args);
expr_ref res_sig_eq(m), sig_abs(m); expr_ref res_sig_eq(m), sig_abs(m), one_1(m);
m_simp.mk_eq(sign_bv, m_bv_util.mk_numeral(1, 1), res_sig_eq); one_1 = m_bv_util.mk_numeral(1, 1);
m_simp.mk_eq(sign_bv, one_1, res_sig_eq);
m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs); m_simp.mk_ite(res_sig_eq, n_sum, sum, sig_abs);
dbg_decouple("fpa2bv_add_sig_abs", sig_abs); dbg_decouple("fpa2bv_add_sig_abs", sig_abs);
@ -388,10 +402,14 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
m_simp.mk_and(x_is_inf, xy_is_neg, v3_and); m_simp.mk_and(x_is_inf, xy_is_neg, v3_and);
mk_ite(v3_and, nan, y, v3); mk_ite(v3_and, nan, y, v3);
expr_ref rm_is_to_neg(m), v4_and(m); expr_ref rm_is_to_neg(m), signs_and(m), signs_xor(m), v4_and(m), rm_and_xor(m), neg_cond(m);
m_simp.mk_and(x_is_zero, y_is_zero, c4); 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(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg);
mk_ite(rm_is_to_neg, nzero, pzero, v4); 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);
m_simp.mk_and(x_is_neg, y_is_neg, v4_and); m_simp.mk_and(x_is_neg, y_is_neg, v4_and);
mk_ite(v4_and, x, v4, v4); mk_ite(v4_and, x, v4, v4);
@ -432,8 +450,9 @@ void fpa2bv_converter::mk_add(func_decl * f, unsigned num, expr * const * args,
c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp, c_sgn, c_sig, c_exp, d_sgn, d_sig, d_exp,
res_sgn, res_sig, res_exp); res_sgn, res_sig, res_exp);
expr_ref is_zero_sig(m); expr_ref is_zero_sig(m), nil_sbit4(m);
m_simp.mk_eq(res_sig, m_bv_util.mk_numeral(0, sbits+4), is_zero_sig); nil_sbit4 = m_bv_util.mk_numeral(0, sbits+4);
m_simp.mk_eq(res_sig, nil_sbit4, is_zero_sig);
SASSERT(is_well_sorted(m, is_zero_sig)); SASSERT(is_well_sorted(m, is_zero_sig));
@ -463,7 +482,7 @@ void fpa2bv_converter::mk_sub(func_decl * f, unsigned num, expr * const * args,
SASSERT(num == 3); SASSERT(num == 3);
expr_ref t(m); expr_ref t(m);
mk_uminus(f, 1, &args[2], t); mk_uminus(f, 1, &args[2], t);
expr * nargs[3] = { args[0], args[1], t.get() }; expr * nargs[3] = { args[0], args[1], t };
mk_add(f, 3, nargs, result); mk_add(f, 3, nargs, result);
} }
@ -589,9 +608,20 @@ void fpa2bv_converter::mk_mul(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(product) == 2*sbits); SASSERT(m_bv_util.get_bv_size(product) == 2*sbits);
expr_ref h_p(m), l_p(m), rbits(m);
h_p = m_bv_util.mk_extract(2*sbits-1, sbits, product);
l_p = m_bv_util.mk_extract(2*sbits-1, sbits, product);
if (sbits >= 4) {
expr_ref sticky(m); expr_ref sticky(m);
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, product)); sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(sbits-4, 0, l_p));
res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(2*sbits-1, sbits-3, product), sticky); rbits = m_bv_util.mk_concat(m_bv_util.mk_extract(sbits-1, sbits-3, l_p), sticky);
}
else
rbits = m_bv_util.mk_concat(l_p, m_bv_util.mk_numeral(0, 4 - m_bv_util.get_bv_size(l_p)));
SASSERT(m_bv_util.get_bv_size(rbits) == 4);
res_sig = m_bv_util.mk_concat(h_p, rbits);
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7);
@ -643,8 +673,8 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos); dbg_decouple("fpa2bv_div_y_is_pos", y_is_pos);
dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf); dbg_decouple("fpa2bv_div_y_is_inf", y_is_inf);
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m); expr_ref c1(m), c2(m), c3(m), c4(m), c5(m), c6(m), c7(m);
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m); expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m), v7(m), v8(m);
// (x is NaN) || (y is NaN) -> NaN // (x is NaN) || (y is NaN) -> NaN
m_simp.mk_or(x_is_nan, y_is_nan, c1); m_simp.mk_or(x_is_nan, y_is_nan, c1);
@ -679,6 +709,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
mk_ite(x_is_pos, pinf, ninf, x_sgn_inf); mk_ite(x_is_pos, pinf, ninf, x_sgn_inf);
mk_ite(x_is_zero, nan, x_sgn_inf, v6); mk_ite(x_is_zero, nan, x_sgn_inf, v6);
// (x is 0) -> result is zero with sgn = x.sgn^y.sgn
// This is a special case to avoid problems with the unpacking of zero.
c7 = x_is_zero;
mk_ite(signs_xor, nzero, pzero, v7);
// else comes the actual division. // else comes the actual division.
unsigned ebits = m_util.get_ebits(f->get_range()); unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range()); unsigned sbits = m_util.get_sbits(f->get_range());
@ -716,10 +751,11 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args,
SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4));
round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8);
// And finally, we tie them together. // And finally, we tie them together.
mk_ite(c6, v6, v7, result); mk_ite(c7, v7, v8, result);
mk_ite(c6, v6, result, result);
mk_ite(c5, v5, result, result); mk_ite(c5, v5, result, result);
mk_ite(c4, v4, result, result); mk_ite(c4, v4, result, result);
mk_ite(c3, v3, result, result); mk_ite(c3, v3, result, result);
@ -783,7 +819,7 @@ void fpa2bv_converter::mk_remainder(func_decl * f, unsigned num, expr * const *
// (x is 0) -> x // (x is 0) -> x
c4 = x_is_zero; c4 = x_is_zero;
v4 = x; v4 = pzero;
// (y is 0) -> NaN. // (y is 0) -> NaN.
c5 = y_is_zero; c5 = y_is_zero;
@ -1108,8 +1144,9 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar
sig_size = m_bv_util.get_bv_size(res_sig); sig_size = m_bv_util.get_bv_size(res_sig);
SASSERT(sig_size == sbits+4); SASSERT(sig_size == sbits+4);
expr_ref is_zero_sig(m); expr_ref is_zero_sig(m), nil_sbits4(m);
m_simp.mk_eq(res_sig, m_bv_util.mk_numeral(0, sbits+4), is_zero_sig); nil_sbits4 = m_bv_util.mk_numeral(0, sbits+4);
m_simp.mk_eq(res_sig, nil_sbits4, is_zero_sig);
SASSERT(is_well_sorted(m, is_zero_sig)); SASSERT(is_well_sorted(m, is_zero_sig));
@ -1175,10 +1212,10 @@ void fpa2bv_converter::mk_round_to_integral(func_decl * f, unsigned num, expr *
expr_ref a_sgn(m), a_sig(m), a_exp(m); expr_ref a_sgn(m), a_sig(m), a_exp(m);
unpack(x, a_sgn, a_sig, a_exp, true); unpack(x, a_sgn, a_sig, a_exp, true);
expr_ref exp_is_small(m); expr_ref exp_is_small(m), exp_h(m), one_1(m);
m_simp.mk_eq(m_bv_util.mk_extract(ebits-1, ebits-1, a_exp), exp_h = m_bv_util.mk_extract(ebits-1, ebits-1, a_exp);
m_bv_util.mk_numeral(1, 1), one_1 = m_bv_util.mk_numeral(1, 1);
exp_is_small); m_simp.mk_eq(exp_h, one_1, exp_is_small);
dbg_decouple("fpa2bv_r2i_exp_is_small", exp_is_small); dbg_decouple("fpa2bv_r2i_exp_is_small", exp_is_small);
c3 = exp_is_small; c3 = exp_is_small;
mk_ite(x_is_pos, pzero, nzero, v3); mk_ite(x_is_pos, pzero, nzero, v3);
@ -1273,12 +1310,13 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a
split(x, x_sgn, x_sig, x_exp); split(x, x_sgn, x_sig, x_exp);
split(y, y_sgn, y_sig, y_exp); split(y, y_sgn, y_sig, y_exp);
expr_ref c3(m), t3(m), t4(m); expr_ref c3(m), t3(m), t4(m), one_1(m), nil_1(m);
one_1 = m_bv_util.mk_numeral(1, 1);
m_simp.mk_eq(x_sgn, m_bv_util.mk_numeral(1, 1), c3); nil_1 = m_bv_util.mk_numeral(0, 1);
m_simp.mk_eq(x_sgn, one_1, c3);
expr_ref y_sgn_eq_0(m), y_lt_x_exp(m), y_lt_x_sig(m), y_eq_x_exp(m), y_le_x_sig_exp(m), t3_or(m); expr_ref y_sgn_eq_0(m), y_lt_x_exp(m), y_lt_x_sig(m), y_eq_x_exp(m), y_le_x_sig_exp(m), t3_or(m);
m_simp.mk_eq(y_sgn, m_bv_util.mk_numeral(0, 1), y_sgn_eq_0); m_simp.mk_eq(y_sgn, nil_1, y_sgn_eq_0);
BVULT(y_exp, x_exp, y_lt_x_exp); BVULT(y_exp, x_exp, y_lt_x_exp);
BVULT(y_sig, x_sig, y_lt_x_sig); BVULT(y_sig, x_sig, y_lt_x_sig);
m_simp.mk_eq(y_exp, x_exp, y_eq_x_exp); m_simp.mk_eq(y_exp, x_exp, y_eq_x_exp);
@ -1287,7 +1325,7 @@ void fpa2bv_converter::mk_float_lt(func_decl * f, unsigned num, expr * const * a
m_simp.mk_ite(y_sgn_eq_0, m.mk_true(), t3_or, t3); m_simp.mk_ite(y_sgn_eq_0, m.mk_true(), t3_or, t3);
expr_ref y_sgn_eq_1(m), x_lt_y_exp(m), x_eq_y_exp(m), x_lt_y_sig(m), x_le_y_sig_exp(m), t4_or(m); expr_ref y_sgn_eq_1(m), x_lt_y_exp(m), x_eq_y_exp(m), x_lt_y_sig(m), x_le_y_sig_exp(m), t4_or(m);
m_simp.mk_eq(y_sgn, m_bv_util.mk_numeral(1, 1), y_sgn_eq_1); m_simp.mk_eq(y_sgn, one_1, y_sgn_eq_1);
BVULT(x_exp, y_exp, x_lt_y_exp); BVULT(x_exp, y_exp, x_lt_y_exp);
m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp); m_simp.mk_eq(x_exp, y_exp, x_eq_y_exp);
BVULT(x_sig, y_sig, x_lt_y_sig); BVULT(x_sig, y_sig, x_lt_y_sig);
@ -1418,10 +1456,11 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
// exp == 1^n , sig != 0 // exp == 1^n , sig != 0
expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m); expr_ref sig_is_zero(m), sig_is_not_zero(m), exp_is_top(m), top_exp(m), zero(m);
mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), sig_is_zero); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
m_simp.mk_eq(sig, zero, sig_is_zero);
m_simp.mk_not(sig_is_zero, sig_is_not_zero); m_simp.mk_not(sig_is_zero, sig_is_not_zero);
m_simp.mk_eq(exp, top_exp, exp_is_top); m_simp.mk_eq(exp, top_exp, exp_is_top);
m_simp.mk_and(exp_is_top, sig_is_not_zero, result); m_simp.mk_and(exp_is_top, sig_is_not_zero, result);
@ -1430,9 +1469,10 @@ void fpa2bv_converter::mk_is_nan(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_inf(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
expr_ref eq1(m), eq2(m), top_exp(m); expr_ref eq1(m), eq2(m), top_exp(m), zero(m);
mk_top_exp(m_bv_util.get_bv_size(exp), top_exp); mk_top_exp(m_bv_util.get_bv_size(exp), top_exp);
m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), eq1); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
m_simp.mk_eq(sig, zero, eq1);
m_simp.mk_eq(exp, top_exp, eq2); m_simp.mk_eq(exp, top_exp, eq2);
m_simp.mk_and(eq1, eq2, result); m_simp.mk_and(eq1, eq2, result);
} }
@ -1455,22 +1495,27 @@ void fpa2bv_converter::mk_is_pos(expr * e, expr_ref & result) {
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
SASSERT(to_app(e)->get_num_args() == 3); SASSERT(to_app(e)->get_num_args() == 3);
expr * a0 = to_app(e)->get_arg(0); expr * a0 = to_app(e)->get_arg(0);
m_simp.mk_eq(a0, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0)), result); expr_ref zero(m);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(a0));
m_simp.mk_eq(a0, zero, result);
} }
void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_neg(expr * e, expr_ref & result) {
SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT));
SASSERT(to_app(e)->get_num_args() == 3); SASSERT(to_app(e)->get_num_args() == 3);
expr * a0 = to_app(e)->get_arg(0); expr * a0 = to_app(e)->get_arg(0);
m_simp.mk_eq(a0, m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0)), result); expr_ref one(m);
one = m_bv_util.mk_numeral(1, m_bv_util.get_bv_size(a0));
m_simp.mk_eq(a0, one, result);
} }
void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
expr_ref eq1(m), eq2(m), bot_exp(m); expr_ref eq1(m), eq2(m), bot_exp(m), zero(m);
mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp); mk_bot_exp(m_bv_util.get_bv_size(exp), bot_exp);
m_simp.mk_eq(sig, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig)), eq1); zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(sig));
m_simp.mk_eq(sig, zero, eq1);
m_simp.mk_eq(exp, bot_exp, eq2); m_simp.mk_eq(exp, bot_exp, eq2);
m_simp.mk_and(eq1, eq2, result); m_simp.mk_and(eq1, eq2, result);
} }
@ -1478,35 +1523,40 @@ void fpa2bv_converter::mk_is_zero(expr * e, expr_ref & result) {
void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_nzero(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
expr_ref e_is_zero(m), eq(m); expr_ref e_is_zero(m), eq(m), one_1(m);
mk_is_zero(e, e_is_zero); mk_is_zero(e, e_is_zero);
m_simp.mk_eq(sgn, m_bv_util.mk_numeral(1, 1), eq); one_1 = m_bv_util.mk_numeral(1, 1);
m_simp.mk_eq(sgn, one_1, eq);
m_simp.mk_and(eq, e_is_zero, result); m_simp.mk_and(eq, e_is_zero, result);
} }
void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_pzero(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
expr_ref e_is_zero(m), eq(m); expr_ref e_is_zero(m), eq(m), nil_1(m);
mk_is_zero(e, e_is_zero); mk_is_zero(e, e_is_zero);
m_simp.mk_eq(sgn, m_bv_util.mk_numeral(0, 1), eq); nil_1 = m_bv_util.mk_numeral(0, 1);
m_simp.mk_eq(sgn, nil_1, eq);
m_simp.mk_and(eq, e_is_zero, result); m_simp.mk_and(eq, e_is_zero, result);
} }
void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_denormal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
m_simp.mk_eq(exp, m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp)), result); expr_ref zero(m);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
m_simp.mk_eq(exp, zero, result);
} }
void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) { void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {
expr * sgn, * sig, * exp; expr * sgn, * sig, * exp;
split(e, sgn, sig, exp); split(e, sgn, sig, exp);
expr_ref is_special(m), is_denormal(m); expr_ref is_special(m), is_denormal(m), p(m);
mk_is_denormal(e, is_denormal); mk_is_denormal(e, is_denormal);
unsigned ebits = m_bv_util.get_bv_size(exp); unsigned ebits = m_bv_util.get_bv_size(exp);
m_simp.mk_eq(exp, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits), is_special); p = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits), ebits);
m_simp.mk_eq(exp, p, is_special);
expr_ref or_ex(m); expr_ref or_ex(m);
m_simp.mk_or(is_special, is_denormal, or_ex); m_simp.mk_or(is_special, is_denormal, or_ex);
@ -1557,9 +1607,12 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref &
if (bv_sz == 0) if (bv_sz == 0)
result = m_bv_util.mk_numeral(0, max_bits); result = m_bv_util.mk_numeral(0, max_bits);
else if (bv_sz == 1) { else if (bv_sz == 1) {
expr_ref eq(m); expr_ref eq(m), nil_1(m), one_m(m), nil_m(m);
m_simp.mk_eq(e, m_bv_util.mk_numeral(0, 1), eq); nil_1 = m_bv_util.mk_numeral(0, 1);
m_simp.mk_ite(eq, m_bv_util.mk_numeral(1, max_bits), m_bv_util.mk_numeral(0, max_bits), result); one_m = m_bv_util.mk_numeral(1, max_bits);
nil_m = m_bv_util.mk_numeral(0, max_bits);
m_simp.mk_eq(e, nil_1, eq);
m_simp.mk_ite(eq, one_m, nil_m, result);
} }
else { else {
expr_ref H(m), L(m); expr_ref H(m), L(m);
@ -1573,11 +1626,13 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref &
mk_leading_zeros(H, max_bits, lzH); /* recursive! */ mk_leading_zeros(H, max_bits, lzH); /* recursive! */
mk_leading_zeros(L, max_bits, lzL); mk_leading_zeros(L, max_bits, lzL);
expr_ref H_is_zero(m); expr_ref H_is_zero(m), nil_h(m);
m_simp.mk_eq(H, m_bv_util.mk_numeral(0, H_size), H_is_zero); nil_h = m_bv_util.mk_numeral(0, H_size);
m_simp.mk_eq(H, nil_h, H_is_zero);
expr_ref sum(m); expr_ref sum(m), h_m(m);
sum = m_bv_util.mk_bv_add(m_bv_util.mk_numeral(H_size, max_bits), lzL); h_m = m_bv_util.mk_numeral(H_size, max_bits);
sum = m_bv_util.mk_bv_add(h_m, lzL);
m_simp.mk_ite(H_is_zero, sum, lzH, result); m_simp.mk_ite(H_is_zero, sum, lzH, result);
} }
@ -1633,26 +1688,46 @@ void fpa2bv_converter::unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref
denormal_exp = m_bv_util.mk_numeral(1, ebits); denormal_exp = m_bv_util.mk_numeral(1, ebits);
mk_unbias(denormal_exp, denormal_exp); mk_unbias(denormal_exp, denormal_exp);
dbg_decouple("fpa2bv_unpack_denormal_exp", denormal_exp);
if (normalize) { if (normalize) {
expr_ref is_sig_zero(m), shift(m), lz(m); expr_ref is_sig_zero(m), shift(m), lz(m), zero_s(m), zero_e(m);
m_simp.mk_eq(m_bv_util.mk_numeral(0, sbits-1), sig, is_sig_zero); zero_s = m_bv_util.mk_numeral(0, sbits-1);
zero_e = m_bv_util.mk_numeral(0, ebits);
m_simp.mk_eq(zero_s, sig, is_sig_zero);
mk_leading_zeros(sig, ebits, lz); mk_leading_zeros(sig, ebits, lz);
m_simp.mk_ite(is_sig_zero, m_bv_util.mk_numeral(0, ebits), lz, shift); m_simp.mk_ite(is_sig_zero, zero_e, lz, shift);
SASSERT(is_well_sorted(m, is_sig_zero)); SASSERT(is_well_sorted(m, is_sig_zero));
SASSERT(is_well_sorted(m, lz)); SASSERT(is_well_sorted(m, lz));
SASSERT(is_well_sorted(m, shift)); SASSERT(is_well_sorted(m, shift));
if (ebits < sbits) { SASSERT(m_bv_util.get_bv_size(shift) == ebits);
if (ebits <= sbits) {
expr_ref q(m); expr_ref q(m);
q = m_bv_util.mk_zero_extend(sbits-ebits, shift); q = m_bv_util.mk_zero_extend(sbits-ebits, shift);
denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q); denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, q);
} }
else { else {
denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, shift); // the maximum shift is `sbits', because after that the mantissa
// would be zero anyways. So we can safely cut the shift variable down,
// as long as we check the higher bits.
expr_ref sh(m), is_sh_zero(m), sl(m), zero_s(m), sbits_s(m), short_shift(m);
zero_s = m_bv_util.mk_numeral(0, sbits-1);
sbits_s = m_bv_util.mk_numeral(sbits, sbits);
sh = m_bv_util.mk_extract(ebits-1, sbits, shift);
m_simp.mk_eq(zero_s, sh, is_sh_zero);
short_shift = m_bv_util.mk_extract(sbits-1, 0, shift);
m_simp.mk_ite(is_sh_zero, short_shift, sbits_s, sl);
denormal_sig = m_bv_util.mk_bv_shl(denormal_sig, sl);
} }
denormal_exp = m_bv_util.mk_bv_sub(denormal_exp, shift);
} }
SASSERT(is_well_sorted(m, normal_sig)); SASSERT(is_well_sorted(m, normal_sig));
SASSERT(is_well_sorted(m, denormal_sig)); SASSERT(is_well_sorted(m, denormal_sig));
SASSERT(is_well_sorted(m, normal_exp));
SASSERT(is_well_sorted(m, denormal_exp));
dbg_decouple("fpa2bv_unpack_is_normal", is_normal);
m_simp.mk_ite(is_normal, normal_sig, denormal_sig, sig); m_simp.mk_ite(is_normal, normal_sig, denormal_sig, sig);
m_simp.mk_ite(is_normal, normal_exp, denormal_exp, exp); m_simp.mk_ite(is_normal, normal_exp, denormal_exp, exp);
@ -1685,6 +1760,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) { void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef _DEBUG #ifdef _DEBUG
// return;
expr_ref new_e(m); expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e)); new_e = m.mk_fresh_const(prefix, m.get_sort(e));
extra_assertions.push_back(m.mk_eq(new_e, e)); extra_assertions.push_back(m.mk_eq(new_e, e));
@ -1737,15 +1813,23 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
"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 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); expr_ref e3(m), ne3(m), e2(m), e1(m), e21(m), one_1(m), h_exp(m), sh_exp(m), th_exp(m);
m_simp.mk_eq(m_bv_util.mk_extract(ebits+1, ebits+1, exp), m_bv_util.mk_numeral(1, 1), e3); one_1 = m_bv_util.mk_numeral(1, 1);
m_simp.mk_eq(m_bv_util.mk_extract(ebits, ebits, exp), m_bv_util.mk_numeral(1, 1), e2); h_exp = m_bv_util.mk_extract(ebits+1, ebits+1, exp);
m_simp.mk_eq(m_bv_util.mk_extract(ebits-1, ebits-1, exp), m_bv_util.mk_numeral(1, 1), e1); sh_exp = m_bv_util.mk_extract(ebits, ebits, exp);
th_exp = m_bv_util.mk_extract(ebits-1, ebits-1, exp);
m_simp.mk_eq(h_exp, one_1, e3);
m_simp.mk_eq(sh_exp, one_1, e2);
m_simp.mk_eq(th_exp, one_1, e1);
m_simp.mk_or(e2, e1, e21); m_simp.mk_or(e2, e1, e21);
m_simp.mk_not(e3, ne3); m_simp.mk_not(e3, ne3);
m_simp.mk_and(ne3, e21, e_top_three); m_simp.mk_and(ne3, e21, e_top_three);
m_simp.mk_eq(m_bv_util.mk_zero_extend(2, e_max), exp, e_eq_emax);
m_simp.mk_eq(m_bv_util.mk_extract(sbits+3, sbits+3, sig), m_bv_util.mk_numeral(1, 1), sigm1); expr_ref ext_emax(m), t_sig(m);
ext_emax = m_bv_util.mk_zero_extend(2, e_max);
t_sig = m_bv_util.mk_extract(sbits+3, sbits+3, sig);
m_simp.mk_eq(ext_emax, exp, e_eq_emax);
m_simp.mk_eq(t_sig, one_1, sigm1);
m_simp.mk_and(e_eq_emax, sigm1, e_eq_emax_and_sigm1); m_simp.mk_and(e_eq_emax, sigm1, e_eq_emax_and_sigm1);
m_simp.mk_or(e_top_three, e_eq_emax_and_sigm1, OVF1); m_simp.mk_or(e_top_three, e_eq_emax_and_sigm1, OVF1);
@ -1797,10 +1881,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
SASSERT(sig_size == sbits+4); SASSERT(sig_size == sbits+4);
unsigned sigma_size = m_bv_util.get_bv_size(sigma); unsigned sigma_size = m_bv_util.get_bv_size(sigma);
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); 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);
sigma_neg = m_bv_util.mk_bv_neg(sigma); sigma_neg = m_bv_util.mk_bv_neg(sigma);
sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size); sigma_cap = m_bv_util.mk_numeral(sbits+2, sigma_size);
m_simp.mk_ite(m_bv_util.mk_sle(sigma_neg, sigma_cap), sigma_neg, sigma_cap, sigma_neg_capped); sigma_le_cap = m_bv_util.mk_sle(sigma_neg, sigma_cap);
m_simp.mk_ite(sigma_le_cap, sigma_neg, sigma_cap, sigma_neg_capped);
dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg); dbg_decouple("fpa2bv_rnd_sigma_neg", sigma_neg);
dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped); dbg_decouple("fpa2bv_rnd_sigma_neg_capped", sigma_neg_capped);
sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size)); sigma_lt_zero = m_bv_util.mk_sle(sigma, m_bv_util.mk_numeral(-1, sigma_size));
@ -1826,13 +1912,17 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
SASSERT(is_well_sorted(m, sig)); SASSERT(is_well_sorted(m, sig));
// put the sticky bit into the significand. // put the sticky bit into the significand.
expr * tmp[] = { sig, m_bv_util.mk_zero_extend(sbits+1, sticky) }; expr_ref ext_sticky(m);
ext_sticky = m_bv_util.mk_zero_extend(sbits+1, sticky);
expr * tmp[] = { sig, ext_sticky };
sig = m_bv_util.mk_bv_or(2, tmp); sig = m_bv_util.mk_bv_or(2, tmp);
SASSERT(is_well_sorted(m, sig)); SASSERT(is_well_sorted(m, sig));
SASSERT(m_bv_util.get_bv_size(sig) == sbits+2); SASSERT(m_bv_util.get_bv_size(sig) == sbits+2);
// CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken. // CMW: The (OVF1 && OVFen) and (TINY && UNFen) cases are never taken.
m_simp.mk_ite(TINY, m_bv_util.mk_zero_extend(2, e_min), beta, exp); expr_ref ext_emin(m);
ext_emin = m_bv_util.mk_zero_extend(2, e_min);
m_simp.mk_ite(TINY, ext_emin, beta, exp);
SASSERT(is_well_sorted(m, exp)); SASSERT(is_well_sorted(m, exp));
// Significand rounding // Significand rounding
@ -1849,13 +1939,18 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
sig = m_bv_util.mk_extract(sbits+1, 2, sig); sig = m_bv_util.mk_extract(sbits+1, 2, sig);
expr_ref last_or_sticky(m), round_or_sticky(m), not_round(m), not_lors(m), not_rors(m), not_sgn(m);
expr * last_sticky[2] = { last, sticky }; expr * last_sticky[2] = { last, sticky };
expr * round_sticky[2] = { round, sticky }; expr * round_sticky[2] = { round, sticky };
expr * last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky); last_or_sticky = m_bv_util.mk_bv_or(2, last_sticky);
expr * round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky); round_or_sticky = m_bv_util.mk_bv_or(2, round_sticky);
expr * round_lors[2] = { m_bv_util.mk_bv_not(round), m_bv_util.mk_bv_not(last_or_sticky) }; not_round = m_bv_util.mk_bv_not(round);
expr * pos_args[2] = { sgn, m_bv_util.mk_bv_not(round_or_sticky) }; not_lors = m_bv_util.mk_bv_not(last_or_sticky);
expr * neg_args[2] = { m_bv_util.mk_bv_not(sgn), m_bv_util.mk_bv_not(round_or_sticky) }; not_rors = m_bv_util.mk_bv_not(round_or_sticky);
not_sgn = m_bv_util.mk_bv_not(sgn);
expr * round_lors[2] = { not_round, not_lors };
expr * pos_args[2] = { sgn, not_rors };
expr * neg_args[2] = { not_sgn, not_rors };
expr_ref inc_teven(m), inc_taway(m), inc_pos(m), inc_neg(m); 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, round_lors)); inc_teven = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, round_lors));
@ -1864,12 +1959,13 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args)); inc_neg = m_bv_util.mk_bv_not(m_bv_util.mk_bv_or(2, neg_args));
expr_ref inc(m), inc_c2(m), inc_c3(m), inc_c4(m); expr_ref inc(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); 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(rm, BV_RM_TO_NEGATIVE, rm_is_to_neg); 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_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_AWAY, rm_is_away);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even); mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_is_even);
m_simp.mk_ite(rm_is_to_neg, inc_neg, m_bv_util.mk_numeral(0, 1), inc_c4); 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_to_pos, inc_pos, inc_c4, inc_c3);
m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2); m_simp.mk_ite(rm_is_away, inc_taway, inc_c3, inc_c2);
m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, inc); m_simp.mk_ite(rm_is_even, inc_teven, inc_c2, inc);
@ -1885,21 +1981,21 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
// Post normalization // Post normalization
SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1); SASSERT(m_bv_util.get_bv_size(sig) == sbits + 1);
expr_ref SIGovf(m); expr_ref SIGovf(m);
m_simp.mk_eq(m_bv_util.mk_extract(sbits, sbits, sig), m_bv_util.mk_numeral(1, 1), SIGovf); t_sig = m_bv_util.mk_extract(sbits, sbits, sig);
m_simp.mk_eq(t_sig, one_1, SIGovf);
SASSERT(is_well_sorted(m, SIGovf)); SASSERT(is_well_sorted(m, SIGovf));
dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf); dbg_decouple("fpa2bv_rnd_SIGovf", SIGovf);
m_simp.mk_ite(SIGovf, expr_ref hallbut1_sig(m), lallbut1_sig(m);
m_bv_util.mk_extract(sbits, 1, sig), hallbut1_sig = m_bv_util.mk_extract(sbits, 1, sig);
m_bv_util.mk_extract(sbits-1, 0, sig), lallbut1_sig = m_bv_util.mk_extract(sbits-1, 0, sig);
sig); m_simp.mk_ite(SIGovf, hallbut1_sig, lallbut1_sig, sig);
SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2); SASSERT(m_bv_util.get_bv_size(exp) == ebits + 2);
m_simp.mk_ite(SIGovf, expr_ref exp_p1(m);
m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2)), exp_p1 = m_bv_util.mk_bv_add(exp, m_bv_util.mk_numeral(1, ebits+2));
exp, m_simp.mk_ite(SIGovf, exp_p1, exp, exp);
exp);
SASSERT(is_well_sorted(m, sig)); SASSERT(is_well_sorted(m, sig));
SASSERT(is_well_sorted(m, exp)); SASSERT(is_well_sorted(m, exp));
@ -1920,12 +2016,12 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
SASSERT(is_well_sorted(m, OVF1)); SASSERT(is_well_sorted(m, OVF1));
SASSERT(m.is_bool(OVF1)); SASSERT(m.is_bool(OVF1));
expr_ref preOVF2(m), OVF2(m), OVF(m); expr_ref preOVF2(m), OVF2(m), OVF(m), exp_redand(m), pem2m1(m);
m_simp.mk_eq(m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get()), m_bv_util.mk_numeral(1, 1), preOVF2); exp_redand = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, biased_exp.get());
m_simp.mk_eq(exp_redand, one_1, preOVF2);
m_simp.mk_and(SIGovf, preOVF2, OVF2); m_simp.mk_and(SIGovf, preOVF2, OVF2);
m_simp.mk_ite(OVF2, m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits), pem2m1 = m_bv_util.mk_numeral(fu().fm().m_powers2.m1(ebits-2), ebits);
biased_exp, m_simp.mk_ite(OVF2, pem2m1, biased_exp, biased_exp);
biased_exp);
m_simp.mk_or(OVF1, OVF2, OVF); m_simp.mk_or(OVF1, OVF2, OVF);
SASSERT(is_well_sorted(m, OVF2)); SASSERT(is_well_sorted(m, OVF2));
@ -1962,15 +2058,17 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
m_simp.mk_ite(rm_zero_or_neg, max_exp, inf_exp, max_inf_exp_neg); m_simp.mk_ite(rm_zero_or_neg, max_exp, inf_exp, max_inf_exp_neg);
m_simp.mk_ite(rm_zero_or_pos, max_exp, inf_exp, max_inf_exp_pos); m_simp.mk_ite(rm_zero_or_pos, max_exp, inf_exp, max_inf_exp_pos);
m_simp.mk_ite(sgn_is_zero, max_inf_exp_neg, max_inf_exp_pos, ovfl_exp); m_simp.mk_ite(sgn_is_zero, max_inf_exp_neg, max_inf_exp_pos, ovfl_exp);
m_simp.mk_eq(m_bv_util.mk_extract(sbits-1, sbits-1, sig), m_bv_util.mk_numeral(0, 1), n_d_check); t_sig = m_bv_util.mk_extract(sbits-1, sbits-1, sig);
m_simp.mk_eq(t_sig, nil_1, n_d_check);
m_simp.mk_ite(n_d_check, bot_exp /* denormal */, biased_exp, n_d_exp); m_simp.mk_ite(n_d_check, bot_exp /* denormal */, biased_exp, n_d_exp);
m_simp.mk_ite(OVF, ovfl_exp, n_d_exp, exp); m_simp.mk_ite(OVF, ovfl_exp, n_d_exp, exp);
expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m); expr_ref max_inf_sig_neg(m), max_inf_sig_pos(m), ovfl_sig(m), rest_sig(m);
m_simp.mk_ite(rm_zero_or_neg, max_sig, inf_sig, max_inf_sig_neg); m_simp.mk_ite(rm_zero_or_neg, max_sig, inf_sig, max_inf_sig_neg);
m_simp.mk_ite(rm_zero_or_pos, max_sig, inf_sig, max_inf_sig_pos); m_simp.mk_ite(rm_zero_or_pos, max_sig, inf_sig, max_inf_sig_pos);
m_simp.mk_ite(sgn_is_zero, max_inf_sig_neg, max_inf_sig_pos, ovfl_sig); m_simp.mk_ite(sgn_is_zero, max_inf_sig_neg, max_inf_sig_pos, ovfl_sig);
m_simp.mk_ite(OVF, ovfl_sig, m_bv_util.mk_extract(sbits-2, 0, sig), sig); rest_sig = m_bv_util.mk_extract(sbits-2, 0, sig);
m_simp.mk_ite(OVF, ovfl_sig, rest_sig, sig);
dbg_decouple("fpa2bv_rnd_sgn_final", sgn); dbg_decouple("fpa2bv_rnd_sgn_final", sgn);
dbg_decouple("fpa2bv_rnd_sig_final", sig); dbg_decouple("fpa2bv_rnd_sig_final", sig);
@ -1993,11 +2091,6 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; ); TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
} }
fpa2bv_model_converter * fpa2bv_converter::mk_model_converter() {
return alloc(fpa2bv_model_converter, m, m_const2bv, m_rm_const2bv);
}
void fpa2bv_model_converter::display(std::ostream & out) { void fpa2bv_model_converter::display(std::ostream & out) {
out << "(fpa2bv-model-converter"; out << "(fpa2bv-model-converter";
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin(); for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
@ -2024,11 +2117,23 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator
for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin(); for (obj_map<func_decl, expr*>::iterator it = m_const2bv.begin();
it != m_const2bv.end(); it != m_const2bv.end();
it++) it++)
res->m_const2bv.insert(translator(it->m_key), translator(it->m_value)); {
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin(); for (obj_map<func_decl, expr*>::iterator it = m_rm_const2bv.begin();
it != m_rm_const2bv.end(); it != m_rm_const2bv.end();
it++) it++)
res->m_rm_const2bv.insert(translator(it->m_key), translator(it->m_value)); {
func_decl * k = translator(it->m_key);
expr * v = translator(it->m_value);
res->m_rm_const2bv.insert(k, v);
translator.to().inc_ref(k);
translator.to().inc_ref(v);
}
return res; return res;
} }
@ -2151,3 +2256,9 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
float_mdl->register_usort(s, u.size(), u.c_ptr()); float_mdl->register_usort(s, u.size(), u.c_ptr());
} }
} }
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv) {
return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv);
}

12
src/tactic/fpa/fpa2bv_converter.h
View file

@ -102,7 +102,8 @@ public:
void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
fpa2bv_model_converter * mk_model_converter(); obj_map<func_decl, expr*> const & const2bv() const { return m_const2bv; }
obj_map<func_decl, expr*> const & rm_const2bv() const { return m_rm_const2bv; }
void dbg_decouple(const char * prefix, expr_ref & e); void dbg_decouple(const char * prefix, expr_ref & e);
expr_ref_vector extra_assertions; expr_ref_vector extra_assertions;
@ -149,8 +150,8 @@ class fpa2bv_model_converter : public model_converter {
obj_map<func_decl, expr*> m_rm_const2bv; obj_map<func_decl, expr*> m_rm_const2bv;
public: public:
fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> & const2bv, fpa2bv_model_converter(ast_manager & m, obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> & rm_const2bv) : obj_map<func_decl, expr*> const & rm_const2bv) :
m(m) { m(m) {
// Just create a copy? // Just create a copy?
for (obj_map<func_decl, expr*>::iterator it = const2bv.begin(); for (obj_map<func_decl, expr*>::iterator it = const2bv.begin();
@ -198,4 +199,9 @@ protected:
void convert(model * bv_mdl, model * float_mdl); void convert(model * bv_mdl, model * float_mdl);
}; };
model_converter * mk_fpa2bv_model_converter(ast_manager & m,
obj_map<func_decl, expr*> const & const2bv,
obj_map<func_decl, expr*> const & rm_const2bv);
#endif #endif

2
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -90,7 +90,7 @@ class fpa2bv_tactic : public tactic {
} }
if (g->models_enabled()) if (g->models_enabled())
mc = m_conv.mk_model_converter(); mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv());
g->inc_depth(); g->inc_depth();
result.push_back(g.get()); result.push_back(g.get());

1
src/test/heap_trie.cpp
View file

@ -25,6 +25,7 @@ static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) {
} }
void tst_heap_trie() { void tst_heap_trie() {
heap_trie_t ht; heap_trie_t ht;

5
src/test/hilbert_basis.cpp
View file

@ -253,7 +253,7 @@ static void saturate_basis(hilbert_basis& hb) {
case l_true: case l_true:
std::cout << "sat\n"; std::cout << "sat\n";
hb.display(std::cout); hb.display(std::cout);
validate_sat(hb); //validate_sat(hb);
break; break;
case l_false: case l_false:
std::cout << "unsat\n"; std::cout << "unsat\n";
@ -522,6 +522,9 @@ void tst_hilbert_basis() {
tst3(); tst3();
tst4(); tst4();
tst4(); tst4();
tst4();
tst4();
tst4();
tst4(); tst4();
tst5(); tst5();
tst6(); tst6();

213
src/test/karr.cpp Normal file
View file

@ -0,0 +1,213 @@
#include "hilbert_basis.h"
/*
Test generation of linear congruences a la Karr.
*/
namespace karr {
struct matrix {
vector<vector<rational> > A;
vector<rational> b;
unsigned size() const { return A.size(); }
void reset() {
A.reset();
b.reset();
}
matrix& operator=(matrix const& other) {
reset();
append(other);
return *this;
}
void append(matrix const& other) {
A.append(other.A);
b.append(other.b);
}
void display(std::ostream& out) {
for (unsigned i = 0; i < A.size(); ++i) {
for (unsigned j = 0; j < A[i].size(); ++j) {
out << A[i][j] << " ";
}
out << " = " << -b[i] << "\n";
}
}
};
// treat src as a homogeneous matrix.
void dualizeH(matrix& dst, matrix const& src) {
hilbert_basis hb;
for (unsigned i = 0; i < src.size(); ++i) {
vector<rational> v(src.A[i]);
v.append(src.b[i]);
hb.add_eq(v, rational(0));
}
for (unsigned i = 0; i < 1 + src.A[0].size(); ++i) {
hb.set_is_int(i);
}
lbool is_sat = hb.saturate();
hb.display(std::cout);
SASSERT(is_sat == l_true);
dst.reset();
unsigned basis_size = hb.get_basis_size();
bool first_initial = true;
for (unsigned i = 0; i < basis_size; ++i) {
bool is_initial;
vector<rational> soln;
hb.get_basis_solution(i, soln, is_initial);
if (!is_initial) {
dst.b.push_back(soln.back());
soln.pop_back();
dst.A.push_back(soln);
}
}
}
// treat src as an inhomegeneous matrix.
void dualizeI(matrix& dst, matrix const& src) {
hilbert_basis hb;
for (unsigned i = 0; i < src.size(); ++i) {
hb.add_eq(src.A[i], -src.b[i]);
}
for (unsigned i = 0; i < src.A[0].size(); ++i) {
hb.set_is_int(i);
}
lbool is_sat = hb.saturate();
hb.display(std::cout);
SASSERT(is_sat == l_true);
dst.reset();
unsigned basis_size = hb.get_basis_size();
bool first_initial = true;
for (unsigned i = 0; i < basis_size; ++i) {
bool is_initial;
vector<rational> soln;
hb.get_basis_solution(i, soln, is_initial);
if (is_initial && first_initial) {
dst.A.push_back(soln);
dst.b.push_back(rational(1));
first_initial = false;
}
else if (!is_initial) {
dst.A.push_back(soln);
dst.b.push_back(rational(0));
}
}
}
void juxtapose(matrix& dst, matrix const& M, matrix const& N) {
dst = M;
dst.append(N);
}
void join(matrix& dst, matrix const& M, matrix const& N) {
matrix MD, ND, dstD;
dualizeI(MD, M);
dualizeI(ND, N);
juxtapose(dstD, MD, ND);
dualizeH(dst, dstD);
}
void joinD(matrix& dst, matrix const& MD, matrix const& ND) {
matrix dstD;
juxtapose(dstD, MD, ND);
dualizeH(dst, dstD);
}
void transition(
matrix& dst,
matrix const& src,
matrix const& Ab) {
matrix T;
// length of rows in Ab are twice as long as
// length of rows in src.
SASSERT(2*src.A[0].size() == Ab.A[0].size());
vector<rational> zeros;
for (unsigned i = 0; i < src.A[0].size(); ++i) {
zeros.push_back(rational(0));
}
for (unsigned i = 0; i < src.size(); ++i) {
T.A.push_back(src.A[i]);
T.A.back().append(zeros);
}
T.b.append(src.b);
T.append(Ab);
T.display(std::cout << "T:\n");
matrix TD;
dualizeI(TD, T);
TD.display(std::cout << "TD:\n");
for (unsigned i = 0; i < TD.size(); ++i) {
vector<rational> v;
v.append(src.size(), TD.A[i].c_ptr() + src.size());
dst.A.push_back(v);
dst.b.push_back(TD.b[i]);
}
dst.display(std::cout << "dst\n");
}
static vector<rational> V(int i, int j) {
vector<rational> v;
v.push_back(rational(i));
v.push_back(rational(j));
return v;
}
static vector<rational> V(int i, int j, int k, int l) {
vector<rational> v;
v.push_back(rational(i));
v.push_back(rational(j));
v.push_back(rational(k));
v.push_back(rational(l));
return v;
}
#define R(_x_) rational(_x_)
static void tst1() {
matrix Theta;
matrix Ab;
//
Theta.A.push_back(V(1, 0));
Theta.b.push_back(R(0));
Theta.A.push_back(V(0, 1));
Theta.b.push_back(R(-2));
Theta.display(std::cout << "Theta\n");
Ab.A.push_back(V(-1, 0, 1, 0));
Ab.b.push_back(R(1));
Ab.A.push_back(V(-1, -2, 0, 1));
Ab.b.push_back(R(1));
Ab.display(std::cout << "Ab\n");
matrix ThetaD;
dualizeI(ThetaD, Theta);
ThetaD.display(std::cout);
matrix t1D, e1;
transition(t1D, Theta, Ab);
joinD(e1, t1D, ThetaD);
t1D.display(std::cout << "t1D\n");
e1.display(std::cout << "e1\n");
matrix t2D, e2;
transition(t2D, e1, Ab);
joinD(e2, t2D, ThetaD);
t2D.display(std::cout << "t2D\n");
e2.display(std::cout << "e2\n");
}
};
void tst_karr() {
karr::tst1();
}

1
src/test/main.cpp
View file

@ -209,6 +209,7 @@ int main(int argc, char ** argv) {
TST(rcf); TST(rcf);
TST(hilbert_basis); TST(hilbert_basis);
TST(heap_trie); TST(heap_trie);
TST(karr);
} }
void initialize_mam() {} void initialize_mam() {}

20
src/util/hwf.cpp
View file

@ -609,6 +609,25 @@ unsigned hwf_manager::prev_power_of_two(hwf const & a) {
void hwf_manager::set_rounding_mode(mpf_rounding_mode rm) void hwf_manager::set_rounding_mode(mpf_rounding_mode rm)
{ {
#ifdef _WINDOWS #ifdef _WINDOWS
#ifdef USE_INTRINSICS
switch (rm) {
case MPF_ROUND_NEAREST_TEVEN:
SETRM(_MM_ROUND_NEAREST);
break;
case MPF_ROUND_TOWARD_POSITIVE:
SETRM(_MM_ROUND_UP);
break;
case MPF_ROUND_TOWARD_NEGATIVE:
SETRM(_MM_ROUND_DOWN);
break;
case MPF_ROUND_TOWARD_ZERO:
SETRM(_MM_ROUND_TOWARD_ZERO);
break;
case MPF_ROUND_NEAREST_TAWAY:
default:
UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware!
}
#else
switch (rm) { switch (rm) {
case MPF_ROUND_NEAREST_TEVEN: case MPF_ROUND_NEAREST_TEVEN:
SETRM(_RC_NEAR); SETRM(_RC_NEAR);
@ -626,6 +645,7 @@ void hwf_manager::set_rounding_mode(mpf_rounding_mode rm)
default: default:
UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware!
} }
#endif
#else // OSX/Linux #else // OSX/Linux
switch (rm) { switch (rm) {
case MPF_ROUND_NEAREST_TEVEN: case MPF_ROUND_NEAREST_TEVEN:

44
src/util/mpf.cpp
View file

@ -520,9 +520,8 @@ void mpf_manager::add_sub(mpf_rounding_mode rm, mpf const & x, mpf const & y, mp
} }
} }
else if (is_zero(x) && is_zero(y)) { else if (is_zero(x) && is_zero(y)) {
if (sgn(x) && sgn_y) if ((x.sign && sgn_y) ||
set(o, x); ((rm == MPF_ROUND_TOWARD_NEGATIVE) && (x.sign != sgn_y)))
else if (rm == MPF_ROUND_TOWARD_NEGATIVE)
mk_nzero(x.ebits, x.sbits, o); mk_nzero(x.ebits, x.sbits, o);
else else
mk_pzero(x.ebits, x.sbits, o); mk_pzero(x.ebits, x.sbits, o);
@ -627,29 +626,28 @@ void mpf_manager::mul(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf &
if (is_zero(y)) if (is_zero(y))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, sgn(y), o); mk_inf(x.ebits, x.sbits, y.sign, o);
} }
else if (is_pinf(y)) { else if (is_pinf(y)) {
if (is_zero(x)) if (is_zero(x))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, sgn(x), o); mk_inf(x.ebits, x.sbits, x.sign, o);
} }
else if (is_ninf(x)) { else if (is_ninf(x)) {
if (is_zero(y)) if (is_zero(y))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, !sgn(y), o); mk_inf(x.ebits, x.sbits, !y.sign, o);
} }
else if (is_ninf(y)) { else if (is_ninf(y)) {
if (is_zero(x)) if (is_zero(x))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, !sgn(x), o); mk_inf(x.ebits, x.sbits, !x.sign, o);
} }
else if (is_zero(x) || is_zero(y)) { else if (is_zero(x) || is_zero(y)) {
set(o, x); mk_zero(x.ebits, x.sbits, x.sign != y.sign, o);
o.sign = x.sign ^ y.sign;
} }
else { else {
o.ebits = x.ebits; o.ebits = x.ebits;
@ -699,31 +697,35 @@ void mpf_manager::div(mpf_rounding_mode rm, mpf const & x, mpf const & y, mpf &
if (is_inf(y)) if (is_inf(y))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, sgn(y), o); mk_inf(x.ebits, x.sbits, y.sign, o);
} }
else if (is_pinf(y)) { else if (is_pinf(y)) {
if (is_inf(x)) if (is_inf(x))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_zero(x.ebits, x.sbits, (x.sign ^ y.sign) == 1, o); mk_zero(x.ebits, x.sbits, x.sign != y.sign, o);
} }
else if (is_ninf(x)) { else if (is_ninf(x)) {
if (is_inf(y)) if (is_inf(y))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, !sgn(y), o); mk_inf(x.ebits, x.sbits, !y.sign, o);
} }
else if (is_ninf(y)) { else if (is_ninf(y)) {
if (is_inf(x)) if (is_inf(x))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_zero(x.ebits, x.sbits, (x.sign ^ y.sign) == 1, o); mk_zero(x.ebits, x.sbits, x.sign != y.sign, o);
} }
else if (is_zero(y)) { else if (is_zero(y)) {
if (is_zero(x)) if (is_zero(x))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else else
mk_inf(x.ebits, x.sbits, sgn(x), o); mk_inf(x.ebits, x.sbits, x.sign != y.sign, o);
}
else if (is_zero(x)) {
// Special case to avoid problems with unpacking of zeros.
mk_zero(x.ebits, x.sbits, x.sign != y.sign, o);
} }
else { else {
o.ebits = x.ebits; o.ebits = x.ebits;
@ -837,6 +839,10 @@ void mpf_manager::sqrt(mpf_rounding_mode rm, mpf const & x, mpf & o) {
else else
mk_nzero(x.ebits, x.sbits, o); mk_nzero(x.ebits, x.sbits, o);
} }
else if (is_pzero(x))
mk_pzero(x.ebits, x.sbits, o);
else if (is_nzero(x))
mk_nzero(x.ebits, x.sbits, o);
else { else {
o.ebits = x.ebits; o.ebits = x.ebits;
o.sbits = x.sbits; o.sbits = x.sbits;
@ -933,7 +939,7 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
else if (is_inf(y)) else if (is_inf(y))
set(o, x); set(o, x);
else if (is_zero(x)) else if (is_zero(x))
set(o, x); mk_pzero(x.ebits, x.sbits, o);
else if (is_zero(y)) else if (is_zero(y))
mk_nan(x.ebits, x.sbits, o); mk_nan(x.ebits, x.sbits, o);
else { else {
@ -982,9 +988,9 @@ void mpf_manager::rem(mpf const & x, mpf const & y, mpf & o) {
void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) { void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x)) if (is_nan(x))
set(o, y); set(o, y);
else if (is_nan(y) || (sgn(y) && is_zero(x) && is_zero(y))) else if (is_nan(y))
set(o, x); set(o, x);
else if (gt(x, y)) else if (gt(x, y) || (is_zero(x) && is_nzero(y)))
set(o, x); set(o, x);
else else
set(o, y); set(o, y);
@ -993,9 +999,9 @@ void mpf_manager::maximum(mpf const & x, mpf const & y, mpf & o) {
void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) { void mpf_manager::minimum(mpf const & x, mpf const & y, mpf & o) {
if (is_nan(x)) if (is_nan(x))
set(o, y); set(o, y);
else if (is_nan(y) || (sgn(x) && is_zero(x) && is_zero(y))) else if (is_nan(y))
set(o, x); set(o, x);
else if (lt(x, y)) else if (lt(x, y) || (is_nzero(x) && is_zero(y)))
set(o, x); set(o, x);
else else
set(o, y); set(o, y);