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);
156 std::string mask_str(width,
'1');
198 exprt round_to_plus_inf_const=
200 exprt round_to_minus_inf_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);
418 assert(extended_exponent1.
type()==extended_exponent2.
type());
421 return minus_exprt(extended_exponent1, extended_exponent2);
440 const sign_exprt src2_bigger(exponent_difference);
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);
479 fraction2_shifted.
type()));
482 const exprt fraction1_ext=
484 const exprt fraction2_ext=
566 return rounder(result, rm, spec);
577 if(dist_width<=nb_bits)
619 const plus_exprt added_exponent(exponent1, exponent2);
640 return rounder(result, rm, spec);
653 std::size_t fraction_width=
655 std::size_t div_width=fraction_width*2+1;
671 result.fraction=
div_exprt(fraction1, fraction2);
691 const minus_exprt added_exponent(exponent1, exponent2);
729 return rounder(result, rm, spec);
748 const and_exprt both_zero(is_zero1, is_zero2);
843 src, spec.
f+spec.
e-1, spec.
f,
875 assert(fraction_bits!=0);
879 if(exponent_bits<depth)
884 for(
int d=depth-1; d>=0; d--)
886 unsigned distance=(1<<d);
887 assert(fraction_bits>distance);
893 fraction_bits - distance,
899 const shl_exprt shifted(fraction, distance);
902 if_exprt(prefix_is_zero, shifted, fraction);
905 assert(d<(
signed int)exponent_bits);
931 assert(exponent_bits>=spec.
e);
955 if(fraction_bits < spec.
f+3)
964 exprt denormalisedFraction = fraction;
967 denormalisedFraction =
970 denormalisedFraction=
977 denormalisedFraction,
1007 std::size_t exponent_bits = std::max(
address_bits(spec.
f), spec.
e) + 1;
1033 return pack(
bias(result, spec), spec);
1038 const std::size_t dest_bits,
1040 const exprt &fraction,
1043 std::size_t fraction_bits=
1046 assert(dest_bits<fraction_bits);
1049 std::size_t extra_bits=fraction_bits-dest_bits;
1066 assert(extra_bits>=1);
1074 rounding_bit,
or_exprt(rounding_least, sticky_bit));
1099 std::size_t fraction_size=spec.
f+1;
1100 std::size_t result_fraction_size=
1104 if(result_fraction_size<fraction_size)
1107 std::size_t padding=fraction_size-result_fraction_size;
1114 else if(result_fraction_size==fraction_size)
1120 std::size_t extra_bits=result_fraction_size-fraction_size;
1121 assert(extra_bits>=1);
1125 fraction_size, result.
sign, result.
fraction, rounding_mode_bits);
1129 result.
fraction, result_fraction_size-1, extra_bits,
1145 bv_utils.incrementer(result.
exponent, overflow);
1150 const or_exprt new_integer_part(integer_part1, integer_part0);
1153 result.
fraction.back()=new_integer_part;
1184 or_exprt(overflow, subnormal_to_normal),
1205 std::size_t result_exponent_size=
1209 if(result_exponent_size<spec.
e)
1214 else if(result_exponent_size==spec.
e)
1247 exprt largest_normal_exponent=
1398 for(std::size_t stage=0; stage<dist_width; stage++)
1418 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 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)
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 &)
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.
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 &)
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 &)