mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Bugfix for fpa2bv_converter_prec

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-06-02 17:19:31 +01:00
parent 599e5b6838
commit 65a6845945
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/fpa/fpa2bv_converter_prec.cpp
View file

@ -35,8 +35,8 @@ fpa2bv_converter_prec::fpa2bv_converter_prec(ast_manager & m, fpa_approximation_
void fpa2bv_converter_prec::fix_bits(unsigned prec, expr_ref rounded, unsigned sbits, unsigned ebits)//expr_ref& fixed,
{ //AZ: TODO: revise! minimal number of legal bits is 3!!!! Remove magic numbers
unsigned szeroes=((sbits-2)*(MAX_PRECISION - prec +0.0)/MAX_PRECISION);//3 bits are minimum for the significand
unsigned ezeroes=((ebits-2)*(MAX_PRECISION - prec+0.0)/MAX_PRECISION);//2 bits are minimum for the exponent
unsigned szeroes = (unsigned) ((sbits-2)*(MAX_PRECISION - prec +0.0) / MAX_PRECISION);//3 bits are minimum for the significand
unsigned ezeroes = (unsigned) ((ebits - 2)*(MAX_PRECISION - prec + 0.0) / MAX_PRECISION);//2 bits are minimum for the exponent
expr_ref fix_sig(m), fix_exp(m);
expr * sgn, *sig, *expn;
@ -226,8 +226,8 @@ void fpa2bv_converter_prec::mk_cast_small_to_big(unsigned sbits, unsigned ebits,
void fpa2bv_converter_prec::match_sorts(expr * a, expr * b, expr_ref & n_a, expr_ref & n_b)
{
//Check if the sorts of lhs and rhs match, otherwise cast them to appropriate size?
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_TO_FP));
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_TO_FP));
SASSERT(is_app_of(a, m_plugin->get_family_id(), OP_FPA_FP));
SASSERT(is_app_of(b, m_plugin->get_family_id(), OP_FPA_FP));
func_decl * a_decl = to_app(a)->get_decl();
func_decl * b_decl = to_app(b)->get_decl();