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');
134 const and_exprt both_zero(is_zero0, is_zero1);
154 std::string mask_str(width,
'1');
196 exprt round_to_plus_inf_const=
198 exprt round_to_minus_inf_const=
236 return rounder(result, rm, spec);
258 return rounder(result, rm, spec);
263 std::size_t dest_width,
267 return to_integer(src, dest_width,
true, rm, spec);
272 std::size_t dest_width,
276 return to_integer(src, dest_width,
false, rm, spec);
281 std::size_t dest_width,
299 exprt result=shift_result;
343 int sourceSmallestNormalExponent = -((1 << (src_spec.
e - 1)) - 1);
344 int sourceSmallestDenormalExponent =
345 sourceSmallestNormalExponent - src_spec.
f;
349 int destSmallestNormalExponent = -((1 << (dest_spec.
e - 1)) - 1);
351 if(dest_spec.
e>=src_spec.
e &&
352 dest_spec.
f>=src_spec.
f &&
353 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
359 std::size_t padding=dest_spec.
f-src_spec.
f;
373 if(dest_spec.
e > src_spec.
e)
378 result.
NaN=unpacked_src.
NaN;
382 return pack(
bias(result, dest_spec), dest_spec);
388 return rounder(result, rm, dest_spec);
409 assert(old_width1==old_width2);
416 assert(extended_exponent1.
type()==extended_exponent2.
type());
419 return minus_exprt(extended_exponent1, extended_exponent2);
438 const sign_exprt src2_bigger(exponent_difference);
440 const exprt bigger_exponent=
444 const exprt new_fraction1=
447 const exprt new_fraction2=
451 const exprt distance=
460 const exprt fraction1_padded=
462 const exprt fraction2_padded=
467 const exprt fraction1_shifted=fraction1_padded;
469 fraction2_padded, limited_dist, sticky_bit);
477 fraction2_shifted.
type()));
480 const exprt fraction1_ext=
482 const exprt fraction2_ext=
564 return rounder(result, rm, spec);
575 if(dist_width<=nb_bits)
617 const plus_exprt added_exponent(exponent1, exponent2);
638 return rounder(result, rm, spec);
651 std::size_t fraction_width=
653 std::size_t div_width=fraction_width*2+1;
669 result.fraction=
div_exprt(fraction1, fraction2);
689 const minus_exprt added_exponent(exponent1, exponent2);
727 return rounder(result, rm, spec);
746 const and_exprt both_zero(is_zero1, is_zero2);
841 src, spec.
f+spec.
e-1, spec.
f,
873 assert(fraction_bits!=0);
877 if(exponent_bits<depth)
882 for(
int d=depth-1; d>=0; d--)
884 unsigned distance=(1<<d);
885 assert(fraction_bits>distance);
891 fraction_bits - distance,
897 const shl_exprt shifted(fraction, distance);
900 if_exprt(prefix_is_zero, shifted, fraction);
903 assert(d<(
signed int)exponent_bits);
929 assert(exponent_bits>=spec.
e);
953 if(fraction_bits < spec.
f+3)
962 exprt denormalisedFraction = fraction;
965 denormalisedFraction =
968 denormalisedFraction=
975 denormalisedFraction,
1005 std::size_t exponent_bits = std::max(
address_bits(spec.
f), spec.
e) + 1;
1031 return pack(
bias(result, spec), spec);
1036 const std::size_t dest_bits,
1038 const exprt &fraction,
1041 std::size_t fraction_bits=
1044 assert(dest_bits<fraction_bits);
1047 std::size_t extra_bits=fraction_bits-dest_bits;
1064 assert(extra_bits>=1);
1072 rounding_bit,
or_exprt(rounding_least, sticky_bit));
1097 std::size_t fraction_size=spec.
f+1;
1098 std::size_t result_fraction_size=
1102 if(result_fraction_size<fraction_size)
1105 std::size_t padding=fraction_size-result_fraction_size;
1112 else if(result_fraction_size==fraction_size)
1118 std::size_t extra_bits=result_fraction_size-fraction_size;
1119 assert(extra_bits>=1);
1123 fraction_size, result.
sign, result.
fraction, rounding_mode_bits);
1127 result.
fraction, result_fraction_size-1, extra_bits,
1143 bv_utils.incrementer(result.
exponent, overflow);
1148 const or_exprt new_integer_part(integer_part1, integer_part0);
1151 result.
fraction.back()=new_integer_part;
1182 or_exprt(overflow, subnormal_to_normal),
1203 std::size_t result_exponent_size=
1207 if(result_exponent_size<spec.
e)
1212 else if(result_exponent_size==spec.
e)
1245 exprt largest_normal_exponent=
1396 for(std::size_t stage=0; stage<dist_width; stage++)
1416 result=
if_exprt(dist_bit, tmp, result);
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.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
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 &)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Fixed-width bit-vector with IEEE floating-point interpretation.
exprt is_zero(const exprt &)
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 &)
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)
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 &)
The unary minus expression.
Base class of bitvector types.
The boolean constant false.
std::size_t get_width() const
exprt disjunction(const exprt::operandst &op)
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 &)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
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)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
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 &)
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &)
exprt isfinite(const exprt &, const ieee_float_spect &)
const abs_exprt & to_abs_expr(const exprt &expr)
Cast a generic exprt to a abs_exprt.
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
fixed-width bit-vector without numerical interpretation
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
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast a generic exprt to a unary_minus_exprt.
void reserve_operands(operandst::size_type n)
exprt isnan(const exprt &, const ieee_float_spect &)