Go to the documentation of this file.
22 else if(expr.
id()==ID_unary_minus)
24 else if(expr.
id()==ID_ieee_float_equal)
28 equal_expr.lhs(), equal_expr.rhs(),
get_spec(equal_expr.lhs()));
30 else if(expr.
id()==ID_ieee_float_notequal)
34 notequal_expr.lhs(), notequal_expr.rhs(),
get_spec(notequal_expr.lhs())));
36 else if(expr.
id()==ID_floatbv_typecast)
39 const auto &op = floatbv_typecast_expr.op();
40 const typet &src_type = floatbv_typecast_expr.op().type();
41 const typet &dest_type = floatbv_typecast_expr.type();
42 const auto &rounding_mode = floatbv_typecast_expr.rounding_mode();
44 if(dest_type.
id()==ID_signedbv &&
45 src_type.
id()==ID_floatbv)
51 else if(dest_type.
id()==ID_unsignedbv &&
52 src_type.
id()==ID_floatbv)
58 else if(src_type.
id()==ID_signedbv &&
59 dest_type.
id()==ID_floatbv)
61 else if(src_type.
id()==ID_unsignedbv &&
62 dest_type.
id()==ID_floatbv)
66 else if(dest_type.
id()==ID_floatbv &&
67 src_type.
id()==ID_floatbv)
75 expr.
id() == ID_typecast && expr.
type().
id() == ID_bool &&
80 else if(expr.
id()==ID_floatbv_plus)
87 float_expr.rounding_mode(),
90 else if(expr.
id()==ID_floatbv_minus)
97 float_expr.rounding_mode(),
100 else if(expr.
id()==ID_floatbv_mult)
106 float_expr.rounding_mode(),
109 else if(expr.
id()==ID_floatbv_div)
115 float_expr.rounding_mode(),
118 else if(expr.
id()==ID_isnan)
123 else if(expr.
id()==ID_isfinite)
128 else if(expr.
id()==ID_isinf)
133 else if(expr.
id()==ID_isnormal)
138 else if(expr.
id()==ID_lt)
144 else if(expr.
id()==ID_gt)
150 else if(expr.
id()==ID_le)
156 else if(expr.
id()==ID_ge)
162 else if(expr.
id()==ID_sign)
202 const and_exprt both_zero(is_zero0, is_zero1);
263 exprt round_to_plus_inf_const=
265 exprt round_to_minus_inf_const=
303 return rounder(result, rm, spec);
325 return rounder(result, rm, spec);
330 std::size_t dest_width,
334 return to_integer(src, dest_width,
true, rm, spec);
339 std::size_t dest_width,
343 return to_integer(src, dest_width,
false, rm, spec);
348 std::size_t dest_width,
366 exprt result=shift_result;
410 int sourceSmallestNormalExponent = -((1 << (src_spec.
e - 1)) - 1);
411 int sourceSmallestDenormalExponent =
412 sourceSmallestNormalExponent - src_spec.
f;
416 int destSmallestNormalExponent = -((1 << (dest_spec.
e - 1)) - 1);
418 if(dest_spec.
e>=src_spec.
e &&
419 dest_spec.
f>=src_spec.
f &&
420 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
426 std::size_t padding=dest_spec.
f-src_spec.
f;
436 "the exponent needs to have a signed type");
442 if(dest_spec.
e > src_spec.
e)
447 result.
NaN=unpacked_src.
NaN;
451 return pack(
bias(result, dest_spec), dest_spec);
457 return rounder(result, rm, dest_spec);
487 return minus_exprt(extended_exponent1, extended_exponent2);
506 const sign_exprt src2_bigger(exponent_difference);
508 const exprt bigger_exponent=
512 const exprt new_fraction1=
515 const exprt new_fraction2=
519 const exprt distance=
528 const exprt fraction1_padded=
530 const exprt fraction2_padded=
535 const exprt fraction1_shifted=fraction1_padded;
537 fraction2_padded, limited_dist, sticky_bit);
545 fraction2_shifted.
type()));
548 const exprt fraction1_ext=
550 const exprt fraction2_ext=
632 return rounder(result, rm, spec);
643 if(dist_width<=nb_bits)
685 const plus_exprt added_exponent(exponent1, exponent2);
706 return rounder(result, rm, spec);
719 std::size_t fraction_width=
721 std::size_t div_width=fraction_width*2+1;
757 const minus_exprt added_exponent(exponent1, exponent2);
795 return rounder(result, rm, spec);
811 "relation should be equality, less-than, or less-or-equal");
816 const and_exprt both_zero(is_zero1, is_zero2);
857 return std::move(and_bv);
861 or_exprt or_bv{{less_than3, both_zero, bitwise_equal}};
903 src, spec.
f+spec.
e-1, spec.
f,
939 if(exponent_bits<depth)
944 for(
int d=depth-1; d>=0; d--)
946 unsigned distance=(1<<d);
948 fraction_bits > distance,
949 "distance must be within the range of fraction bits");
955 fraction_bits - distance,
961 const shl_exprt shifted(fraction, distance);
964 if_exprt(prefix_is_zero, shifted, fraction);
968 d < (
signed int)exponent_bits,
969 "depth must be smaller than exponent bits");
1019 if(fraction_bits < spec.
f+3)
1028 exprt denormalisedFraction = fraction;
1031 denormalisedFraction =
1034 denormalisedFraction=
1041 denormalisedFraction,
1071 std::size_t exponent_bits = std::max(
address_bits(spec.
f), spec.
e) + 1;
1097 return pack(
bias(result, spec), spec);
1102 const std::size_t dest_bits,
1104 const exprt &fraction,
1107 std::size_t fraction_bits=
1113 std::size_t extra_bits=fraction_bits-dest_bits;
1131 extra_bits >= 1,
"the extra bits contain at least the rounding bit");
1139 rounding_bit,
or_exprt(rounding_least, sticky_bit));
1164 std::size_t fraction_size=spec.
f+1;
1165 std::size_t result_fraction_size=
1169 if(result_fraction_size<fraction_size)
1172 std::size_t padding=fraction_size-result_fraction_size;
1179 else if(result_fraction_size==fraction_size)
1185 std::size_t extra_bits=result_fraction_size-fraction_size;
1187 extra_bits >= 1,
"the extra bits include at least the rounding bit");
1191 fraction_size, result.
sign, result.
fraction, rounding_mode_bits);
1195 result.
fraction, result_fraction_size-1, extra_bits,
1211 bv_utils.incrementer(result.
exponent, overflow);
1216 const or_exprt new_integer_part(integer_part1, integer_part0);
1219 result.
fraction.back()=new_integer_part;
1250 or_exprt(overflow, subnormal_to_normal),
1271 std::size_t result_exponent_size=
1277 if(result_exponent_size == spec.
e)
1310 exprt largest_normal_exponent=
1445 {std::move(
sign_bit), std::move(exponent), std::move(fraction)},
1461 for(std::size_t stage=0; stage<dist_width; stage++)
1481 result=
if_exprt(dist_bit, tmp, result);
void get(const exprt &rm)
#define UNREACHABLE
This should be used to mark dead code.
static exprt isnormal(const exprt &, const ieee_float_spect &)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
std::size_t size() const
Amount of nodes this expression tree contains.
static exprt abs(const exprt &, const ieee_float_spect &)
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
The type of an expression, extends irept.
The trinary if-then-else operator.
bool is_signed(const typet &t)
Convenience function – is the type signed?
Fixed-width bit-vector with IEEE floating-point interpretation.
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
The plus expression Associativity is not specified.
Base class for all expressions.
static 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
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
Sign of an expression Predicate is true if _op is negative, false otherwise.
Concatenation of bit-vector operands.
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
static exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
Fixed-width bit-vector with unsigned binary interpretation.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
static exprt isfinite(const exprt &, const ieee_float_spect &)
static exprt to_signed_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
typet & type()
Return the type of the expression.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
std::size_t width() const
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
static exprt isinf(const exprt &, const ieee_float_spect &)
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
static ieee_float_spect get_spec(const exprt &)
class floatbv_typet to_type() const
#define PRECONDITION(CONDITION)
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
Fixed-width bit-vector with two's complement interpretation.
static exprt add_bias(const exprt &exponent, const ieee_float_spect &)
static void denormalization_shift(exprt &fraction, exprt &exponent, const ieee_float_spect &)
make sure exponent is not too small; the exponent is unbiased
static exprt isnan(const exprt &, const ieee_float_spect &)
Binary multiplication Associativity is not specified.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
The unary minus expression.
static exprt is_zero(const exprt &)
const irep_idt & id() const
static exprt negation(const exprt &, const ieee_float_spect &)
The Boolean constant false.
API to expression classes for floating-point arithmetic.
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
const ieee_float_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
static exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
static exprt pack(const biased_floatt &, const ieee_float_spect &)
std::size_t get_width() const
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
static exprt sign_bit(const exprt &)
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
Base class of fixed-width bit-vector types.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
A base class for relations, i.e., binary predicates whose two operands have the same type.
mp_integer max_exponent() const
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
constant_exprt to_expr() const
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
Semantic type conversion.
A constant literal expression.
exprt convert(const exprt &) const
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
static exprt is_equal(const exprt &, const exprt &, const ieee_float_spect &)
API to expression classes for bitvectors.
Fixed-width bit-vector without numerical interpretation.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const