mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 19:27:06 +00:00
fpa2bv slight refactoring
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger
parent
f684675a6e
commit
3266e96e80
|
|
@ -1873,7 +1873,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
m_arith_util.is_numeral(args[1]) &&
|
||||
m_arith_util.is_numeral(args[2]))
|
||||
{
|
||||
// Three arguments, some of them are not numerals.
|
||||
// rm + real + int -> float
|
||||
SASSERT(m_util.is_float(f->get_range()));
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
|
|
@ -1926,191 +1926,197 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
else if (num == 1 && m_bv_util.is_bv(args[0])) {
|
||||
sort * s = f->get_range();
|
||||
unsigned to_sbits = m_util.get_sbits(s);
|
||||
unsigned to_ebits = m_util.get_ebits(s);
|
||||
unsigned to_ebits = m_util.get_ebits(s);
|
||||
|
||||
expr * bv = args[0];
|
||||
int sz = m_bv_util.get_bv_size(bv);
|
||||
SASSERT((unsigned)sz == to_sbits + to_ebits);
|
||||
|
||||
|
||||
mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
|
||||
m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv),
|
||||
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
|
||||
result);
|
||||
}
|
||||
else if (num == 2 &&
|
||||
else if (num == 2 &&
|
||||
m_util.is_rm(args[0]) &&
|
||||
is_app(args[1]) &&
|
||||
m_util.is_float(m.get_sort(args[1]))) {
|
||||
// We also support float to float conversion
|
||||
sort * s = f->get_range();
|
||||
expr_ref rm(m), x(m);
|
||||
rm = args[0];
|
||||
x = args[1];
|
||||
|
||||
unsigned from_sbits = m_util.get_sbits(m.get_sort(x));
|
||||
unsigned from_ebits = m_util.get_ebits(m.get_sort(x));
|
||||
unsigned to_sbits = m_util.get_sbits(s);
|
||||
unsigned to_ebits = m_util.get_ebits(s);
|
||||
|
||||
if (from_sbits == to_sbits && from_ebits == to_ebits)
|
||||
result = x;
|
||||
else {
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
|
||||
expr_ref one1(m);
|
||||
|
||||
one1 = m_bv_util.mk_numeral(1, 1);
|
||||
expr_ref ninf(m), pinf(m);
|
||||
mk_pinf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
|
||||
// NaN -> NaN
|
||||
mk_is_nan(x, c1);
|
||||
mk_nan(f, v1);
|
||||
|
||||
// +0 -> +0
|
||||
mk_is_pzero(x, c2);
|
||||
mk_pzero(f, v2);
|
||||
|
||||
// -0 -> -0
|
||||
mk_is_nzero(x, c3);
|
||||
mk_nzero(f, v3);
|
||||
|
||||
// +oo -> +oo
|
||||
mk_is_pinf(x, c4);
|
||||
v4 = pinf;
|
||||
|
||||
// -oo -> -oo
|
||||
mk_is_ninf(x, c5);
|
||||
v5 = ninf;
|
||||
|
||||
// otherwise: the actual conversion with rounding.
|
||||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_x_sig", sig);
|
||||
dbg_decouple("fpa2bv_to_float_x_exp", exp);
|
||||
dbg_decouple("fpa2bv_to_float_lz", lz);
|
||||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
|
||||
res_sgn = sgn;
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
|
||||
SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
|
||||
|
||||
if (from_sbits < (to_sbits + 3))
|
||||
{
|
||||
// make sure that sig has at least to_sbits + 3
|
||||
res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits+3-from_sbits));
|
||||
}
|
||||
else if (from_sbits > (to_sbits + 3))
|
||||
{
|
||||
// collapse the extra bits into a sticky bit.
|
||||
expr_ref sticky(m), low(m), high(m);
|
||||
low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);
|
||||
high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get());
|
||||
res_sig = m_bv_util.mk_concat(high, sticky);
|
||||
}
|
||||
else
|
||||
res_sig = sig;
|
||||
|
||||
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
|
||||
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
|
||||
SASSERT(sig_sz == to_sbits+4);
|
||||
|
||||
expr_ref exponent_overflow(m);
|
||||
exponent_overflow = m.mk_false();
|
||||
|
||||
if (from_ebits < (to_ebits + 2))
|
||||
{
|
||||
res_exp = m_bv_util.mk_sign_extend(to_ebits-from_ebits+2, exp);
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m);
|
||||
lz_ext = m_bv_util.mk_zero_extend(to_ebits-from_ebits+2, lz);
|
||||
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
|
||||
}
|
||||
else if (from_ebits > (to_ebits + 2))
|
||||
{
|
||||
expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
|
||||
expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m);
|
||||
high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp);
|
||||
low = m_bv_util.mk_extract(to_ebits+1, 0, exp);
|
||||
lows = m_bv_util.mk_extract(to_ebits+1, to_ebits+1, low);
|
||||
|
||||
high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
|
||||
high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
|
||||
|
||||
zero1 = m_bv_util.mk_numeral(0, 1);
|
||||
m_simp.mk_eq(high_red_and, one1, h_and_eq);
|
||||
m_simp.mk_eq(high_red_or, zero1, h_or_eq);
|
||||
m_simp.mk_eq(lows, zero1, s_is_zero);
|
||||
m_simp.mk_eq(lows, one1, s_is_one);
|
||||
|
||||
expr_ref c2(m);
|
||||
m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2);
|
||||
m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow);
|
||||
|
||||
// Note: Upon overflow, we _could_ try to shift the significand around...
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m);
|
||||
lz_ext = m_bv_util.mk_extract(to_ebits+1, 0, lz);
|
||||
lz_rest = m_bv_util.mk_extract(from_ebits-1, to_ebits+2, lz);
|
||||
lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get());
|
||||
m_simp.mk_eq(lz_redor, one1, lz_redor_bool);
|
||||
m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow);
|
||||
|
||||
res_exp = m_bv_util.mk_bv_sub(low, lz_ext);
|
||||
}
|
||||
else // from_ebits == (to_ebits + 2)
|
||||
res_exp = m_bv_util.mk_bv_sub(exp, lz);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits+2);
|
||||
SASSERT(is_well_sorted(m, res_exp));
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
|
||||
|
||||
expr_ref rounded(m);
|
||||
round(s, rm, res_sgn, res_sig, res_exp, rounded);
|
||||
|
||||
expr_ref is_neg(m), sig_inf(m);
|
||||
m_simp.mk_eq(sgn, one1, is_neg);
|
||||
mk_ite(is_neg, ninf, pinf, sig_inf);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
|
||||
mk_ite(exponent_overflow, sig_inf, rounded, v6);
|
||||
|
||||
// And finally, we tie them together.
|
||||
mk_ite(c5, v5, v6, result);
|
||||
mk_ite(c4, v4, result, result);
|
||||
mk_ite(c3, v3, result, result);
|
||||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
}
|
||||
m_util.is_float(m.get_sort(args[1]))) {
|
||||
// float -> float conversion
|
||||
mk_to_fp_float(f, f->get_range(), args[0], args[1], result);
|
||||
}
|
||||
else if (num == 2 &&
|
||||
else if (num == 2 &&
|
||||
m_util.is_rm(args[0]),
|
||||
m_arith_util.is_real(args[1])) {
|
||||
// .. other than that, we only support rationals for to_fp
|
||||
SASSERT(m_util.is_float(f->get_range()));
|
||||
unsigned ebits = m_util.get_ebits(f->get_range());
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
// rm + real -> float
|
||||
mk_to_fp_real(f, f->get_range(), args[0], args[1], result);
|
||||
}
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
||||
SASSERT(m_bv_util.is_numeral(args[0]));
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
|
||||
unsigned from_sbits = m_util.get_sbits(m.get_sort(x));
|
||||
unsigned from_ebits = m_util.get_ebits(m.get_sort(x));
|
||||
unsigned to_sbits = m_util.get_sbits(s);
|
||||
unsigned to_ebits = m_util.get_ebits(s);
|
||||
|
||||
if (from_sbits == to_sbits && from_ebits == to_ebits)
|
||||
result = x;
|
||||
else {
|
||||
expr_ref c1(m), c2(m), c3(m), c4(m), c5(m);
|
||||
expr_ref v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
|
||||
expr_ref one1(m);
|
||||
|
||||
one1 = m_bv_util.mk_numeral(1, 1);
|
||||
expr_ref ninf(m), pinf(m);
|
||||
mk_pinf(f, pinf);
|
||||
mk_ninf(f, ninf);
|
||||
|
||||
// NaN -> NaN
|
||||
mk_is_nan(x, c1);
|
||||
mk_nan(f, v1);
|
||||
|
||||
// +0 -> +0
|
||||
mk_is_pzero(x, c2);
|
||||
mk_pzero(f, v2);
|
||||
|
||||
// -0 -> -0
|
||||
mk_is_nzero(x, c3);
|
||||
mk_nzero(f, v3);
|
||||
|
||||
// +oo -> +oo
|
||||
mk_is_pinf(x, c4);
|
||||
v4 = pinf;
|
||||
|
||||
// -oo -> -oo
|
||||
mk_is_ninf(x, c5);
|
||||
v5 = ninf;
|
||||
|
||||
// otherwise: the actual conversion with rounding.
|
||||
expr_ref sgn(m), sig(m), exp(m), lz(m);
|
||||
unpack(x, sgn, sig, exp, lz, true);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_x_sig", sig);
|
||||
dbg_decouple("fpa2bv_to_float_x_exp", exp);
|
||||
dbg_decouple("fpa2bv_to_float_lz", lz);
|
||||
|
||||
expr_ref res_sgn(m), res_sig(m), res_exp(m);
|
||||
|
||||
res_sgn = sgn;
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(sgn) == 1);
|
||||
SASSERT(m_bv_util.get_bv_size(sig) == from_sbits);
|
||||
SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
|
||||
SASSERT(m_bv_util.get_bv_size(lz) == from_ebits);
|
||||
|
||||
if (from_sbits < (to_sbits + 3)) {
|
||||
// make sure that sig has at least to_sbits + 3
|
||||
res_sig = m_bv_util.mk_concat(sig, m_bv_util.mk_numeral(0, to_sbits + 3 - from_sbits));
|
||||
}
|
||||
else if (from_sbits >(to_sbits + 3)) {
|
||||
// collapse the extra bits into a sticky bit.
|
||||
expr_ref sticky(m), low(m), high(m);
|
||||
low = m_bv_util.mk_extract(from_sbits - to_sbits - 3, 0, sig);
|
||||
high = m_bv_util.mk_extract(from_sbits - 1, from_sbits - to_sbits - 2, sig);
|
||||
sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, low.get());
|
||||
res_sig = m_bv_util.mk_concat(high, sticky);
|
||||
}
|
||||
else
|
||||
res_sig = sig;
|
||||
|
||||
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
|
||||
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
|
||||
SASSERT(sig_sz == to_sbits + 4);
|
||||
|
||||
expr_ref exponent_overflow(m);
|
||||
exponent_overflow = m.mk_false();
|
||||
|
||||
if (from_ebits < (to_ebits + 2)) {
|
||||
res_exp = m_bv_util.mk_sign_extend(to_ebits - from_ebits + 2, exp);
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m);
|
||||
lz_ext = m_bv_util.mk_zero_extend(to_ebits - from_ebits + 2, lz);
|
||||
res_exp = m_bv_util.mk_bv_sub(res_exp, lz_ext);
|
||||
}
|
||||
else if (from_ebits >(to_ebits + 2)) {
|
||||
expr_ref high(m), low(m), lows(m), high_red_or(m), high_red_and(m), h_or_eq(m), h_and_eq(m);
|
||||
expr_ref no_ovf(m), zero1(m), s_is_one(m), s_is_zero(m);
|
||||
high = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, exp);
|
||||
low = m_bv_util.mk_extract(to_ebits + 1, 0, exp);
|
||||
lows = m_bv_util.mk_extract(to_ebits + 1, to_ebits + 1, low);
|
||||
|
||||
high_red_or = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, high.get());
|
||||
high_red_and = m.mk_app(m_bv_util.get_fid(), OP_BREDAND, high.get());
|
||||
|
||||
zero1 = m_bv_util.mk_numeral(0, 1);
|
||||
m_simp.mk_eq(high_red_and, one1, h_and_eq);
|
||||
m_simp.mk_eq(high_red_or, zero1, h_or_eq);
|
||||
m_simp.mk_eq(lows, zero1, s_is_zero);
|
||||
m_simp.mk_eq(lows, one1, s_is_one);
|
||||
|
||||
expr_ref c2(m);
|
||||
m_simp.mk_ite(h_or_eq, s_is_one, m.mk_false(), c2);
|
||||
m_simp.mk_ite(h_and_eq, s_is_zero, c2, exponent_overflow);
|
||||
|
||||
// Note: Upon overflow, we _could_ try to shift the significand around...
|
||||
|
||||
// subtract lz for subnormal numbers.
|
||||
expr_ref lz_ext(m), lz_rest(m), lz_redor(m), lz_redor_bool(m);
|
||||
lz_ext = m_bv_util.mk_extract(to_ebits + 1, 0, lz);
|
||||
lz_rest = m_bv_util.mk_extract(from_ebits - 1, to_ebits + 2, lz);
|
||||
lz_redor = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, lz_rest.get());
|
||||
m_simp.mk_eq(lz_redor, one1, lz_redor_bool);
|
||||
m_simp.mk_or(exponent_overflow, lz_redor_bool, exponent_overflow);
|
||||
|
||||
res_exp = m_bv_util.mk_bv_sub(low, lz_ext);
|
||||
}
|
||||
else // from_ebits == (to_ebits + 2)
|
||||
res_exp = m_bv_util.mk_bv_sub(exp, lz);
|
||||
|
||||
SASSERT(m_bv_util.get_bv_size(res_exp) == to_ebits + 2);
|
||||
SASSERT(is_well_sorted(m, res_exp));
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_res_sig", res_sig);
|
||||
dbg_decouple("fpa2bv_to_float_res_exp", res_exp);
|
||||
|
||||
expr_ref rounded(m);
|
||||
round(s, expr_ref (rm, m), res_sgn, res_sig, res_exp, rounded);
|
||||
|
||||
expr_ref is_neg(m), sig_inf(m);
|
||||
m_simp.mk_eq(sgn, one1, is_neg);
|
||||
mk_ite(is_neg, ninf, pinf, sig_inf);
|
||||
|
||||
dbg_decouple("fpa2bv_to_float_exp_ovf", exponent_overflow);
|
||||
mk_ite(exponent_overflow, sig_inf, rounded, v6);
|
||||
|
||||
// And finally, we tie them together.
|
||||
mk_ite(c5, v5, v6, result);
|
||||
mk_ite(c4, v4, result, result);
|
||||
mk_ite(c3, v3, result, result);
|
||||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
}
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result) {
|
||||
SASSERT(m_util.is_float(s));
|
||||
unsigned ebits = m_util.get_ebits(s);
|
||||
unsigned sbits = m_util.get_sbits(s);
|
||||
|
||||
if (m_bv_util.is_numeral(rm) && m_util.au().is_numeral(x)) {
|
||||
rational tmp_rat; unsigned sz;
|
||||
m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
|
||||
m_bv_util.is_numeral(to_expr(rm), tmp_rat, sz);
|
||||
SASSERT(tmp_rat.is_int32());
|
||||
SASSERT(sz == 3);
|
||||
BV_RM_VAL bv_rm = (BV_RM_VAL)tmp_rat.get_unsigned();
|
||||
|
||||
mpf_rounding_mode rm;
|
||||
switch (bv_rm)
|
||||
{
|
||||
switch (bv_rm) {
|
||||
case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
|
||||
case BV_RM_TIES_TO_EVEN: rm = MPF_ROUND_NEAREST_TEVEN; break;
|
||||
case BV_RM_TO_NEGATIVE: rm = MPF_ROUND_TOWARD_NEGATIVE; break;
|
||||
|
|
@ -2119,10 +2125,8 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
default: UNREACHABLE();
|
||||
}
|
||||
|
||||
SASSERT(m_util.au().is_numeral(args[1]));
|
||||
|
||||
rational q;
|
||||
m_util.au().is_numeral(args[1], q);
|
||||
m_util.au().is_numeral(x, q);
|
||||
|
||||
scoped_mpf v(m_mpf_manager);
|
||||
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
|
||||
|
|
@ -2135,10 +2139,11 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
|
||||
mk_triple(sgn, s, e, result);
|
||||
}
|
||||
else
|
||||
UNREACHABLE();
|
||||
else {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
}
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
||||
void fpa2bv_converter::mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
|
||||
|
|
|
|||
|
|
@ -129,7 +129,9 @@ public:
|
|||
|
||||
void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
|
||||
void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
void mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result);
|
||||
void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
|
||||
void mk_to_fp_unsigned(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);
|
||||
|
|
@ -186,7 +188,7 @@ protected:
|
|||
expr_ref & c_sgn, expr_ref & c_sig, expr_ref & c_exp, expr_ref & d_sgn, expr_ref & d_sig, expr_ref & d_exp,
|
||||
expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp);
|
||||
|
||||
app * mk_fresh_const(char const * prefix, unsigned sz);
|
||||
app * mk_fresh_const(char const * prefix, unsigned sz);
|
||||
};
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Reference in a new issue