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 pull request #15 from wintersteiger/unstable

Browse source 
Integrating fixes for #10, #13, #14
This commit is contained in:
Christoph M. Wintersteiger 2015-03-29 14:44:21 +01:00
parent 4bfe20647b 5911f788c3
commit 4a0eb93f87
2 changed files with 70 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1837,7 +1837,10 @@ void fpa2bv_converter::mk_is_subnormal(func_decl * f, unsigned num, expr * const
void fpa2bv_converter::mk_is_negative(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 1);
mk_is_neg(args[0], result);
expr_ref t1(m), t2(m);
mk_is_nan(args[0], t1);
mk_is_neg(args[0], t2);
result = m.mk_and(m.mk_not(t1), t2);
TRACE("fpa2bv_is_negative", tout << "result = " << mk_ismt2_pp(result, m) << std::endl;);
}
@ -2104,6 +2107,64 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr *
mk_fp(sgn, e, s, result);
}
else if (m_util.au().is_numeral(x)) {
rational q;
bool is_int;
m_util.au().is_numeral(x, q, is_int);
expr_ref rm_nta(m), rm_nte(m), rm_tp(m), rm_tn(m), rm_tz(m);
mk_is_rm(rm, BV_RM_TIES_TO_AWAY, rm_nta);
mk_is_rm(rm, BV_RM_TIES_TO_EVEN, rm_nte);
mk_is_rm(rm, BV_RM_TO_POSITIVE, rm_tp);
mk_is_rm(rm, BV_RM_TO_NEGATIVE, rm_tn);
mk_is_rm(rm, BV_RM_TO_ZERO, rm_tz);
scoped_mpf v_nta(m_mpf_manager), v_nte(m_mpf_manager), v_tp(m_mpf_manager);
scoped_mpf v_tn(m_mpf_manager), v_tz(m_mpf_manager);
m_util.fm().set(v_nta, ebits, sbits, MPF_ROUND_NEAREST_TAWAY, q.to_mpq());
m_util.fm().set(v_nte, ebits, sbits, MPF_ROUND_NEAREST_TEVEN, q.to_mpq());
m_util.fm().set(v_tp, ebits, sbits, MPF_ROUND_TOWARD_POSITIVE, q.to_mpq());
m_util.fm().set(v_tn, ebits, sbits, MPF_ROUND_TOWARD_NEGATIVE, q.to_mpq());
m_util.fm().set(v_tz, ebits, sbits, MPF_ROUND_TOWARD_ZERO, q.to_mpq());
expr_ref v1(m), v2(m), v3(m), v4(m);
expr_ref sgn(m), s(m), e(m), unbiased_exp(m);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nta)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nta), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nta), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v1);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_nte)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_nte), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_nte), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v2);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v3);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tn)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tn), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tn), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, v4);
sgn = m_bv_util.mk_numeral((m_util.fm().sgn(v_tp)) ? 1 : 0, 1);
s = m_bv_util.mk_numeral(m_util.fm().sig(v_tp), sbits - 1);
unbiased_exp = m_bv_util.mk_numeral(m_util.fm().exp(v_tp), ebits);
mk_bias(unbiased_exp, e);
mk_fp(sgn, e, s, result);
mk_ite(rm_tn, v4, result, result);
mk_ite(rm_tp, v3, result, result);
mk_ite(rm_nte, v2, result, result);
mk_ite(rm_nta, v1, result, result);
}
else {
bv_util & bu = m_bv_util;
arith_util & au = m_arith_util;
@ -2952,11 +3013,16 @@ void fpa2bv_converter::mk_is_pzero(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_fp(e, sgn, exp, sig);
expr_ref zero(m);
expr_ref zero(m), zexp(m), is_zero(m), n_is_zero(m);
zero = m_bv_util.mk_numeral(0, m_bv_util.get_bv_size(exp));
m_simp.mk_eq(exp, zero, result);
m_simp.mk_eq(exp, zero, zexp);
mk_is_zero(e, is_zero);
m_simp.mk_not(is_zero, n_is_zero);
m_simp.mk_and(n_is_zero, zexp, result);
}
void fpa2bv_converter::mk_is_normal(expr * e, expr_ref & result) {

2
src/util/mpf.cpp
View file

@ -1350,7 +1350,7 @@ bool mpf_manager::is_ninf(mpf const & x) {
}
bool mpf_manager::is_normal(mpf const & x) {
return !has_bot_exp(x) && !has_top_exp(x);
return !is_zero(x) && has_bot_exp(x);
}
bool mpf_manager::is_denormal(mpf const & x) {