mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

FPA: bugfix for bitblaster.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2013-03-05 14:11:50 +00:00
parent 35906889b6
commit 9a4331995e
1 changed files with 8 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1546,14 +1546,14 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
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);
//SASSERT(tmp_rat.is_int32());
//SASSERT(sz == 3);
//BV_RM_VAL rm = (BV_RM_VAL) tmp_rat.get_unsigned();
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();
/*mpf_rounding_mode rm;
mpf_rounding_mode rm;
switch(bv_rm)
{
case BV_RM_TIES_TO_AWAY: rm = MPF_ROUND_NEAREST_TAWAY; break;
@ -1562,14 +1562,10 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a
case BV_RM_TO_POSITIVE: rm = MPF_ROUND_TOWARD_POSITIVE; break;
case BV_RM_TO_ZERO: rm = MPF_ROUND_TOWARD_ZERO; break;
default: UNREACHABLE();
}*/
}
SASSERT(m_util.au().is_numeral(args[1]));
sort * rm_rng = to_app(args[0])->get_decl()->get_range();
SASSERT(m_util.is_rm(rm_rng));
mpf_rounding_mode rm = static_cast<mpf_rounding_mode>(to_app(args[1])->get_decl_kind());
rational q;
SASSERT(m_util.au().is_numeral(args[1]));
m_util.au().is_numeral(args[1], q);