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

optimizations for float to float conversions

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-11-14 16:56:13 +00:00
parent 4b0c00969c
commit 6a2f987fb7
2 changed files with 120 additions and 114 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1826,10 +1826,19 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
} }
else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) {
// We also support float to float conversion // We also support float to float conversion
sort * s = f->get_range();
expr_ref rm(m), x(m); expr_ref rm(m), x(m);
rm = args[0]; rm = args[0];
x = args[1]; x = args[1];
unsigned from_sbits = m_util.get_sbits(m.get_sort(args[1]));
unsigned from_ebits = m_util.get_ebits(m.get_sort(args[1]));
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 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 v1(m), v2(m), v3(m), v4(m), v5(m), v6(m);
expr_ref one1(m); expr_ref one1(m);
@ -1860,7 +1869,6 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
v5 = ninf; v5 = ninf;
// otherwise: the actual conversion with rounding. // otherwise: the actual conversion with rounding.
sort * s = f->get_range();
expr_ref sgn(m), sig(m), exp(m), lz(m); expr_ref sgn(m), sig(m), exp(m), lz(m);
unpack(x, sgn, sig, exp, lz, true); unpack(x, sgn, sig, exp, lz, true);
@ -1872,11 +1880,6 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
res_sgn = sgn; res_sgn = sgn;
unsigned from_sbits = m_util.get_sbits(m.get_sort(args[1]));
unsigned from_ebits = m_util.get_ebits(m.get_sort(args[1]));
unsigned to_sbits = m_util.get_sbits(s);
unsigned to_ebits = m_util.get_ebits(s);
SASSERT(m_bv_util.get_bv_size(sgn) == 1); 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(sig) == from_sbits);
SASSERT(m_bv_util.get_bv_size(exp) == from_ebits); SASSERT(m_bv_util.get_bv_size(exp) == from_ebits);
@ -1966,6 +1969,7 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
mk_ite(c2, v2, result, result); mk_ite(c2, v2, result, result);
mk_ite(c1, v1, result, result); mk_ite(c1, v1, result, result);
} }
}
else { else {
// .. other than that, we only support rationals for asFloat // .. other than that, we only support rationals for asFloat
SASSERT(num == 2); SASSERT(num == 2);

2
src/util/mpf.cpp
View file

@ -360,6 +360,8 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
mk_inf(ebits, sbits, x.sign, o); mk_inf(ebits, sbits, x.sign, o);
else if (is_zero(x)) else if (is_zero(x))
mk_zero(ebits, sbits, x.sign, o); mk_zero(ebits, sbits, x.sign, o);
else if (x.ebits == ebits && x.sbits == sbits)
set(o, x);
else { else {
set(o, x); set(o, x);
unpack(o, true); unpack(o, true);