mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
FPA fixed omissions reported by user xor88 (codeplex discussion 554193)
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
1944283253
commit
b423418810
|
@ -28,9 +28,10 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
|
|||
m(m),
|
||||
m_simp(m),
|
||||
m_util(m),
|
||||
m_mpf_manager(m_util.fm()),
|
||||
m_mpz_manager(m_mpf_manager.mpz_manager()),
|
||||
m_bv_util(m),
|
||||
m_arith_util(m),
|
||||
m_mpf_manager(m_util.fm()),
|
||||
m_mpz_manager(m_mpf_manager.mpz_manager()),
|
||||
extra_assertions(m) {
|
||||
m_plugin = static_cast<float_decl_plugin*>(m.get_plugin(m.mk_family_id("float")));
|
||||
}
|
||||
|
@ -268,7 +269,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
|
|||
result = r;
|
||||
}
|
||||
else {
|
||||
SASSERT(is_rm_sort(f->get_range()));
|
||||
SASSERT(is_rm(f->get_range()));
|
||||
|
||||
result = m.mk_fresh_const(
|
||||
#ifdef Z3DEBUG
|
||||
|
@ -281,6 +282,10 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
|
|||
m_rm_const2bv.insert(f, result);
|
||||
m.inc_ref(f);
|
||||
m.inc_ref(result);
|
||||
|
||||
expr_ref rcc(m);
|
||||
rcc = bu().mk_ule(result, bu().mk_numeral(4, 3));
|
||||
extra_assertions.push_back(rcc);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -1847,6 +1852,55 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
// Just keep it here, as there will be something else that uses it.
|
||||
mk_triple(args[0], args[1], args[2], result);
|
||||
}
|
||||
else if (num == 3 &&
|
||||
m_bv_util.is_bv(args[0]) &&
|
||||
m_arith_util.is_numeral(args[1]) &&
|
||||
m_arith_util.is_numeral(args[2]))
|
||||
{
|
||||
// Three arguments, some of them are not numerals.
|
||||
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());
|
||||
|
||||
expr * rm = args[0];
|
||||
|
||||
rational q;
|
||||
if (!m_arith_util.is_numeral(args[1], q))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
rational e;
|
||||
if (!m_arith_util.is_numeral(args[2], e))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
SASSERT(e.is_int64());
|
||||
SASSERT(m_mpz_manager.eq(e.to_mpq().denominator(), 1));
|
||||
|
||||
mpf nte, nta, tp, tn, tz;
|
||||
m_mpf_manager.set(nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq(), e.to_mpq().numerator());
|
||||
m_mpf_manager.set(nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq(), e.to_mpq().numerator());
|
||||
m_mpf_manager.set(tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq(), e.to_mpq().numerator());
|
||||
m_mpf_manager.set(tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq(), e.to_mpq().numerator());
|
||||
m_mpf_manager.set(tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq(), e.to_mpq().numerator());
|
||||
|
||||
app_ref a_nte(m), a_nta(m), a_tp(m), a_tn(m), a_tz(m);
|
||||
a_nte = m_plugin->mk_value(nte);
|
||||
a_nta = m_plugin->mk_value(nta);
|
||||
a_tp = m_plugin->mk_value(tp);
|
||||
a_tn = m_plugin->mk_value(tn);
|
||||
a_tz = m_plugin->mk_value(tz);
|
||||
|
||||
expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
|
||||
mk_value(a_nte->get_decl(), 0, 0, bv_nte);
|
||||
mk_value(a_nta->get_decl(), 0, 0, bv_nta);
|
||||
mk_value(a_tp->get_decl(), 0, 0, bv_tp);
|
||||
mk_value(a_tn->get_decl(), 0, 0, bv_tn);
|
||||
mk_value(a_tz->get_decl(), 0, 0, bv_tz);
|
||||
|
||||
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tn, bv_tz, result);
|
||||
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), bv_tp, result, result);
|
||||
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), bv_nta, result, result);
|
||||
mk_ite(m.mk_eq(rm, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), bv_nte, result, result);
|
||||
}
|
||||
else if (num == 1 && m_bv_util.is_bv(args[0])) {
|
||||
sort * s = f->get_range();
|
||||
unsigned to_sbits = m_util.get_sbits(s);
|
||||
|
@ -1862,7 +1916,9 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv),
|
||||
result);
|
||||
}
|
||||
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
|
||||
sort * s = f->get_range();
|
||||
expr_ref rm(m), x(m);
|
||||
|
@ -2015,23 +2071,24 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
mk_ite(c2, v2, result, result);
|
||||
mk_ite(c1, v1, result, result);
|
||||
}
|
||||
}
|
||||
else {
|
||||
}
|
||||
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 asFloat
|
||||
SASSERT(num == 2);
|
||||
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());
|
||||
|
||||
SASSERT(m_bv_util.is_numeral(args[0]));
|
||||
rational tmp_rat; unsigned sz;
|
||||
m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
|
||||
unsigned sbits = m_util.get_sbits(f->get_range());
|
||||
|
||||
SASSERT(m_bv_util.is_numeral(args[0]));
|
||||
rational tmp_rat; unsigned sz;
|
||||
m_bv_util.is_numeral(to_expr(args[0]), tmp_rat, sz);
|
||||
SASSERT(tmp_rat.is_int32());
|
||||
SASSERT(sz == 3);
|
||||
BV_RM_VAL bv_rm = (BV_RM_VAL) tmp_rat.get_unsigned();
|
||||
|
||||
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;
|
||||
|
@ -2042,22 +2099,23 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
|
|||
}
|
||||
|
||||
SASSERT(m_util.au().is_numeral(args[1]));
|
||||
|
||||
|
||||
rational q;
|
||||
SASSERT(m_util.au().is_numeral(args[1]));
|
||||
m_util.au().is_numeral(args[1], q);
|
||||
|
||||
mpf v;
|
||||
m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
|
||||
|
||||
|
||||
expr * sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v)) ? 1 : 0, 1);
|
||||
expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits-1);
|
||||
expr * s = m_bv_util.mk_numeral(m_util.fm().sig(v), sbits - 1);
|
||||
expr * e = m_bv_util.mk_numeral(m_util.fm().exp(v), ebits);
|
||||
|
||||
mk_triple(sgn, s, e, result);
|
||||
|
||||
m_util.fm().del(v);
|
||||
}
|
||||
else
|
||||
UNREACHABLE();
|
||||
|
||||
SASSERT(is_well_sorted(m, result));
|
||||
}
|
||||
|
|
|
@ -45,9 +45,10 @@ class fpa2bv_converter {
|
|||
ast_manager & m;
|
||||
basic_simplifier_plugin m_simp;
|
||||
float_util m_util;
|
||||
bv_util m_bv_util;
|
||||
arith_util m_arith_util;
|
||||
mpf_manager & m_mpf_manager;
|
||||
unsynch_mpz_manager & m_mpz_manager;
|
||||
bv_util m_bv_util;
|
||||
unsynch_mpz_manager & m_mpz_manager;
|
||||
float_decl_plugin * m_plugin;
|
||||
|
||||
obj_map<func_decl, expr*> m_const2bv;
|
||||
|
@ -64,8 +65,9 @@ public:
|
|||
|
||||
bool is_float(sort * s) { return m_util.is_float(s); }
|
||||
bool is_float(expr * e) { return is_app(e) && m_util.is_float(to_app(e)->get_decl()->get_range()); }
|
||||
bool is_rm(expr * e) { return m_util.is_rm(e); }
|
||||
bool is_rm(sort * s) { return m_util.is_rm(s); }
|
||||
bool is_float_family(func_decl * f) { return f->get_family_id() == m_util.get_family_id(); }
|
||||
bool is_rm_sort(sort * s) { return m_util.is_rm(s); }
|
||||
|
||||
void mk_triple(expr * sign, expr * significand, expr * exponent, expr_ref & result) {
|
||||
SASSERT(m_bv_util.is_bv(sign) && m_bv_util.get_bv_size(sign) == 1);
|
||||
|
|
|
@ -78,17 +78,23 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg {
|
|||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm_sort(f->get_range())) {
|
||||
if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) {
|
||||
m_conv.mk_rm_const(f, result);
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
if (m().is_eq(f)) {
|
||||
SASSERT(num == 2);
|
||||
if (m_conv.is_float(args[0])) {
|
||||
SASSERT(m().get_sort(args[0]) == m().get_sort(args[1]));
|
||||
sort * ds = f->get_domain()[0];
|
||||
if (m_conv.is_float(ds)) {
|
||||
m_conv.mk_eq(args[0], args[1], result);
|
||||
return BR_DONE;
|
||||
}
|
||||
else if (m_conv.is_rm(ds)) {
|
||||
result = m().mk_eq(args[0], args[1]);
|
||||
return BR_DONE;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue