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

Bugfix for fp.to_sbv

Browse source 
Fixes #114.
This commit is contained in:
Christoph M. Wintersteiger 2015-07-14 12:05:45 -07:00
parent 21201371ed
commit f9e2ad76fa
2 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2975,7 +2975,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
m_bv_util.mk_zero_extend(2, lz)); m_bv_util.mk_zero_extend(2, lz));
shift = m_bv_util.mk_bv_sub(exp_m_lz, shift = m_bv_util.mk_bv_sub(exp_m_lz,
m_bv_util.mk_numeral(bv_sz - 1, ebits + 2)); m_bv_util.mk_numeral(bv_sz, ebits + 2));
shift_neg = m_bv_util.mk_bv_neg(shift); shift_neg = m_bv_util.mk_bv_neg(shift);
bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2); bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift); shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
@ -2987,8 +2987,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
// sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long
// [1][ ... sig ... ][r][g][ ... s ...] // [1][ ... sig ... ][r][g][ ... s ...]
// [ ... ubv ... ][r][g][ ... s ... ] // [ ... ubv ... ][r][g][ ... s ... ]
expr_ref max_shift(m); // expr_ref max_shift(m);
max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz); // max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs); shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz); SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs); dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
@ -3440,7 +3440,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 Z3DEBUG #ifdef Z3DEBUG
return; // return;
// CMW: This works only for quantifier-free formulas. // CMW: This works only for quantifier-free formulas.
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));

1
src/ast/fpa_decl_plugin.cpp
View file

@ -629,7 +629,6 @@ func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, par
symbol name("fp.to_sbv"); symbol name("fp.to_sbv");
sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters); sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters);
return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters)); return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters));
} }
func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,