21 else if(expr.
id()==ID_unary_minus)
23 else if(expr.
id()==ID_ieee_float_equal)
25 else if(expr.
id()==ID_ieee_float_notequal)
27 else if(expr.
id()==ID_floatbv_typecast)
32 if(dest_type.
id()==ID_signedbv &&
33 src_type.
id()==ID_floatbv)
40 else if(dest_type.
id()==ID_unsignedbv &&
41 src_type.
id()==ID_floatbv)
48 else if(src_type.
id()==ID_signedbv &&
49 dest_type.
id()==ID_floatbv)
52 else if(src_type.
id()==ID_unsignedbv &&
53 dest_type.
id()==ID_floatbv)
56 else if(dest_type.
id()==ID_floatbv &&
57 src_type.
id()==ID_floatbv)
64 else if(expr.
id()==ID_typecast &&
65 expr.
type().
id()==ID_bool &&
68 else if(expr.
id()==ID_floatbv_plus)
70 else if(expr.
id()==ID_floatbv_minus)
72 else if(expr.
id()==ID_floatbv_mult)
74 else if(expr.
id()==ID_floatbv_div)
76 else if(expr.
id()==ID_isnan)
78 else if(expr.
id()==ID_isfinite)
80 else if(expr.
id()==ID_isinf)
82 else if(expr.
id()==ID_isnormal)
84 else if(expr.
id()==ID_lt)
86 else if(expr.
id()==ID_gt)
88 else if(expr.
id()==ID_le)
90 else if(expr.
id()==ID_ge)
92 else if(expr.
id()==ID_sign)
107 std::string mask_str(spec.
width(),
'1');
118 std::string mask_str(spec.
width(),
'0');
156 std::string mask_str(width,
'1');
198 exprt round_to_plus_inf_const=
200 exprt round_to_minus_inf_const=
204 round_to_even=
equal_exprt(rm, round_to_even_const);
205 round_to_plus_inf=
equal_exprt(rm, round_to_plus_inf_const);
206 round_to_minus_inf=
equal_exprt(rm, round_to_minus_inf_const);
207 round_to_zero=
equal_exprt(rm, round_to_zero_const);
238 return rounder(result, rm, spec);
260 return rounder(result, rm, spec);
265 std::size_t dest_width,
269 return to_integer(src, dest_width,
true, rm, spec);
274 std::size_t dest_width,
278 return to_integer(src, dest_width,
false, rm, spec);
283 std::size_t dest_width,
301 exprt result=shift_result;
345 int sourceSmallestNormalExponent = -((1 << (src_spec.
e - 1)) - 1);
346 int sourceSmallestDenormalExponent =
347 sourceSmallestNormalExponent - src_spec.
f;
351 int destSmallestNormalExponent = -((1 << (dest_spec.
e - 1)) - 1);
353 if(dest_spec.
e>=src_spec.
e &&
354 dest_spec.
f>=src_spec.
f &&
355 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
361 std::size_t padding=dest_spec.
f-src_spec.
f;
375 if(dest_spec.
e > src_spec.
e)
380 result.
NaN=unpacked_src.
NaN;
384 return pack(
bias(result, dest_spec), dest_spec);
390 return rounder(result, rm, dest_spec);
411 assert(old_width1==old_width2);
413 exprt extended_exponent1=
415 exprt extended_exponent2=
418 assert(extended_exponent1.
type()==extended_exponent2.
type());
421 return minus_exprt(extended_exponent1, extended_exponent2);
442 const exprt bigger_exponent=
446 const exprt new_fraction1=
449 const exprt new_fraction2=
453 const exprt distance=
462 const exprt fraction1_padded=
464 const exprt fraction2_padded=
469 const exprt fraction1_shifted=fraction1_padded;
471 fraction2_padded, limited_dist, sticky_bit);
474 exprt fraction2_stickied=
479 fraction2_shifted.
type()));
482 const exprt fraction1_ext=
484 const exprt fraction2_ext=
568 return rounder(result, rm, spec);
579 if(dist_width<=nb_bits)
585 exprt upper_bits_zero=
650 return rounder(result, rm, spec);
663 std::size_t fraction_width=
665 std::size_t div_width=fraction_width*2+1;
675 const exprt fraction2=
683 result.fraction=
div_exprt(fraction1, fraction2);
697 const exprt exponent1=
699 const exprt exponent2=
742 return rounder(result, rm, spec);
774 exprt signs_different=
858 src, spec.
f+spec.
e-1, spec.
f,
890 assert(fraction_bits!=0);
894 if(exponent_bits<depth)
899 for(
int d=depth-1; d>=0; d--)
901 unsigned distance=(1<<d);
902 assert(fraction_bits>distance);
916 if_exprt(prefix_is_zero, shifted, fraction);
919 assert(d<(
signed int)exponent_bits);
945 assert(exponent_bits>=spec.
e);
970 if(fraction_bits < spec.
f+3)
979 exprt denormalisedFraction = fraction;
982 denormalisedFraction =
985 denormalisedFraction=
992 denormalisedFraction,
1022 std::size_t exponent_bits=
1024 (std::size_t)spec.
e)+1;
1050 return pack(
bias(result, spec), spec);
1055 const std::size_t dest_bits,
1057 const exprt &fraction,
1060 std::size_t fraction_bits=
1063 assert(dest_bits<fraction_bits);
1066 std::size_t extra_bits=fraction_bits-dest_bits;
1084 assert(extra_bits>=1);
1091 exprt round_to_even=
1093 or_exprt(rounding_least, sticky_bit));
1096 exprt round_to_plus_inf=
1098 or_exprt(rounding_bit, sticky_bit));
1101 exprt round_to_minus_inf=
1103 or_exprt(rounding_bit, sticky_bit));
1106 exprt round_to_zero=
1122 std::size_t fraction_size=spec.
f+1;
1123 std::size_t result_fraction_size=
1127 if(result_fraction_size<fraction_size)
1130 std::size_t padding=fraction_size-result_fraction_size;
1137 else if(result_fraction_size==fraction_size)
1143 std::size_t extra_bits=result_fraction_size-fraction_size;
1144 assert(extra_bits>=1);
1148 fraction_size, result.
sign, result.
fraction, rounding_mode_bits);
1152 result.
fraction, result_fraction_size-1, extra_bits,
1168 bv_utils.incrementer(result.
exponent, overflow);
1173 exprt new_integer_part=
or_exprt(integer_part1, integer_part0);
1176 result.
fraction.back()=new_integer_part;
1202 exprt subnormal_to_normal=
1211 or_exprt(overflow, subnormal_to_normal),
1232 std::size_t result_exponent_size=
1236 if(result_exponent_size<spec.
e)
1241 else if(result_exponent_size==spec.
e)
1259 exprt exponent_too_large=
1269 exprt overflow_to_inf=
1280 exprt largest_normal_exponent=
1406 exprt infinity_or_NaN=
1434 for(std::size_t stage=0; stage<dist_width; stage++)
1455 result=
if_exprt(dist_bit, tmp, result);
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
exprt isinf(const exprt &, const ieee_float_spect &)
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
The type of an expression.
bool is_signed(const typet &t)
Convenience function – is the type signed?
exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
ieee_float_spect get_spec(const exprt &)
Fixed-width bit-vector with unsigned binary interpretation.
constant_exprt zero_expr() const
exprt add_bias(const exprt &exponent, const ieee_float_spect &)
exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
A generic base class for relations, i.e., binary predicates.
exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
exprt convert(const exprt &)
Fixed-width bit-vector with IEEE floating-point interpretation.
exprt pack(const biased_floatt &, const ieee_float_spect &)
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
exprt sign_bit(const exprt &)
exprt negation(const exprt &, const ieee_float_spect &)
void copy_to_operands(const exprt &expr)
void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
The trinary if-then-else operator.
mp_integer max_exponent() const
A constant literal expression.
exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
class floatbv_typet to_type() const
Concatenation of bit-vector operands.
exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
const irep_idt & id() const
division (integer and real)
virtual exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &)
Fixed-width bit-vector with two's complement interpretation.
exprt isnormal(const exprt &, const ieee_float_spect &)
API to expression classes.
exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec)
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &)
exprt abs(const exprt &, const ieee_float_spect &)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
The unary minus expression.
Base class of bitvector types.
The boolean constant false.
std::size_t get_width() const
exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
void get(const exprt &rm)
exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
unsigned integer2unsigned(const mp_integer &n)
exprt fraction_rounding_decision(const std::size_t dest_bits, const exprt sign, const exprt &fraction, const rounding_mode_bitst &)
rounding decision for fraction using sticky bit
exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt is_zero(const exprt &, const ieee_float_spect &)
Base class for all expressions.
exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
exprt isfinite(const exprt &, const ieee_float_spect &)
exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
std::size_t width() const
std::size_t integer2size_t(const mp_integer &n)
fixed-width bit-vector without numerical interpretation
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
exprt isnan(const exprt &, const ieee_float_spect &)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.