23 else if(expr.
id()==ID_unary_minus)
25 else if(expr.
id()==ID_ieee_float_equal)
29 equal_expr.lhs(), equal_expr.rhs(),
get_spec(equal_expr.lhs()));
31 else if(expr.
id()==ID_ieee_float_notequal)
35 notequal_expr.lhs(), notequal_expr.rhs(),
get_spec(notequal_expr.lhs())));
37 else if(expr.
id()==ID_floatbv_typecast)
40 const auto &op = floatbv_typecast_expr.op();
41 const typet &src_type = floatbv_typecast_expr.op().type();
42 const typet &dest_type = floatbv_typecast_expr.type();
43 const auto &rounding_mode = floatbv_typecast_expr.rounding_mode();
45 if(dest_type.
id()==ID_signedbv &&
46 src_type.
id()==ID_floatbv)
52 else if(dest_type.
id()==ID_unsignedbv &&
53 src_type.
id()==ID_floatbv)
59 else if(src_type.
id()==ID_signedbv &&
60 dest_type.
id()==ID_floatbv)
62 else if(src_type.
id()==ID_unsignedbv &&
63 dest_type.
id()==ID_floatbv)
67 else if(dest_type.
id()==ID_floatbv &&
68 src_type.
id()==ID_floatbv)
82 expr.
id() == ID_typecast && expr.
type().
id() == ID_bv &&
97 else if(expr.
id()==ID_floatbv_plus)
104 float_expr.rounding_mode(),
107 else if(expr.
id()==ID_floatbv_minus)
114 float_expr.rounding_mode(),
117 else if(expr.
id()==ID_floatbv_mult)
123 float_expr.rounding_mode(),
126 else if(expr.
id()==ID_floatbv_div)
132 float_expr.rounding_mode(),
135 else if(expr.
id()==ID_isnan)
140 else if(expr.
id()==ID_isfinite)
145 else if(expr.
id()==ID_isinf)
150 else if(expr.
id()==ID_isnormal)
155 else if(expr.
id()==ID_lt)
161 else if(expr.
id()==ID_gt)
167 else if(expr.
id()==ID_le)
173 else if(expr.
id()==ID_ge)
179 else if(expr.
id()==ID_sign)
219 const and_exprt both_zero(is_zero0, is_zero1);
280 exprt round_to_plus_inf_const=
282 exprt round_to_minus_inf_const=
285 exprt round_to_away_const =
323 return rounder(result, rm, spec);
345 return rounder(result, rm, spec);
350 std::size_t dest_width,
354 return to_integer(src, dest_width,
true, rm, spec);
359 std::size_t dest_width,
363 return to_integer(src, dest_width,
false, rm, spec);
368 std::size_t dest_width,
386 exprt result=shift_result;
430 int sourceSmallestNormalExponent = -((1 << (src_spec.
e - 1)) - 1);
431 int sourceSmallestDenormalExponent =
432 sourceSmallestNormalExponent - src_spec.
f;
436 int destSmallestNormalExponent = -((1 << (dest_spec.
e - 1)) - 1);
438 if(dest_spec.
e>=src_spec.
e &&
439 dest_spec.
f>=src_spec.
f &&
440 !(sourceSmallestDenormalExponent < destSmallestNormalExponent))
446 std::size_t padding=dest_spec.
f-src_spec.
f;
456 "the exponent needs to have a signed type");
462 if(dest_spec.
e > src_spec.
e)
474 result.
NaN=unpacked_src.
NaN;
478 return pack(
bias(result, dest_spec), dest_spec);
484 return rounder(result, rm, dest_spec);
514 return minus_exprt(extended_exponent1, extended_exponent2);
533 const sign_exprt src2_bigger(exponent_difference);
535 const exprt bigger_exponent=
539 const exprt new_fraction1=
542 const exprt new_fraction2=
546 const exprt distance=
555 const exprt fraction1_padded=
557 const exprt fraction2_padded=
562 const exprt fraction1_shifted=fraction1_padded;
564 fraction2_padded, limited_dist, sticky_bit);
572 fraction2_shifted.
type()));
575 const exprt fraction1_ext=
577 const exprt fraction2_ext=
659 return rounder(result, rm, spec);
670 if(dist_width<=nb_bits)
698 const exprt fraction1 =
700 const exprt fraction2 =
713 const plus_exprt added_exponent(exponent1, exponent2);
734 return rounder(result, rm, spec);
747 std::size_t fraction_width=
749 std::size_t div_width=fraction_width*2+1;
785 const minus_exprt added_exponent(exponent1, exponent2);
823 return rounder(result, rm, spec);
839 "relation should be equality, less-than, or less-or-equal");
844 const and_exprt both_zero(is_zero1, is_zero2);
885 return std::move(and_bv);
889 or_exprt or_bv{{less_than3, both_zero, bitwise_equal}};
968 for(
int d=depth-1; d>=0; d--)
970 unsigned distance=(1<<d);
972 fraction_bits > distance,
973 "distance must be within the range of fraction bits");
982 const shl_exprt shifted(fraction, distance);
985 if_exprt(prefix_is_zero, shifted, fraction);
989 d < (
signed int)exponent_bits,
990 "depth must be smaller than exponent bits");
1040 if(fraction_bits < spec.
f+3)
1049 exprt denormalisedFraction = fraction;
1052 denormalisedFraction =
1055 denormalisedFraction=
1062 denormalisedFraction,
1092 std::size_t exponent_bits = std::max(
address_bits(spec.
f), spec.
e) + 1;
1118 return pack(
bias(result, spec), spec);
1123 const std::size_t dest_bits,
1125 const exprt &fraction,
1128 std::size_t fraction_bits=
1134 std::size_t extra_bits=fraction_bits-dest_bits;
1152 extra_bits >= 1,
"the extra bits contain at least the rounding bit");
1160 rounding_bit,
or_exprt(rounding_least, sticky_bit));
1173 const auto round_to_away =
or_exprt(rounding_bit, sticky_bit);
1191 std::size_t fraction_size=spec.
f+1;
1192 std::size_t result_fraction_size=
1196 if(result_fraction_size<fraction_size)
1199 std::size_t padding=fraction_size-result_fraction_size;
1206 else if(result_fraction_size==fraction_size)
1212 std::size_t extra_bits=result_fraction_size-fraction_size;
1214 extra_bits >= 1,
"the extra bits include at least the rounding bit");
1218 fraction_size, result.
sign, result.
fraction, rounding_mode_bits);
1237 bv_utils.incrementer(result.
exponent, overflow);
1242 const or_exprt new_integer_part(integer_part1, integer_part0);
1245 result.
fraction.back()=new_integer_part;
1276 or_exprt(overflow, subnormal_to_normal),
1297 std::size_t result_exponent_size=
1303 if(result_exponent_size == spec.
e)
1336 exprt largest_normal_exponent=
1469 {std::move(
sign_bit), std::move(exponent), std::move(fraction)},
1485 for(std::size_t stage=0; stage<dist_width; stage++)
1505 result=
if_exprt(dist_bit, tmp, result);
API to expression classes for bitvectors.
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
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.
Base class of fixed-width bit-vector types.
std::size_t get_width() const
Fixed-width bit-vector without numerical interpretation.
Concatenation of bit-vector operands.
A constant literal expression.
Base class for all expressions.
bool is_boolean() const
Return whether the expression represents a Boolean.
typet & type()
Return the type of the expression.
The Boolean constant false.
static unbiased_floatt unpack(const exprt &, const ieee_float_spect &)
static void normalization_shift(exprt &fraction, exprt &exponent)
normalize fraction/exponent pair returns 'zero' if fraction is zero
static exprt get_fraction(const exprt &, const ieee_float_spect &)
Gets the fraction without hidden bit in a floating-point bit-vector src.
static exprt sub_bias(const exprt &exponent, const ieee_float_spect &)
static exprt exponent_all_ones(const exprt &, const ieee_float_spect &)
static exprt to_integer(const exprt &src, std::size_t dest_width, bool is_signed, const exprt &rm, const ieee_float_spect &)
exprt from_unsigned_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
static exprt isfinite(const exprt &, const ieee_float_spect &)
static exprt isnormal(const exprt &, const ieee_float_spect &)
exprt from_signed_integer(const exprt &, const exprt &rm, const ieee_float_spect &) const
exprt add_sub(bool subtract, const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
static exprt is_zero(const exprt &)
static exprt abs(const exprt &, const ieee_float_spect &)
static void round_fraction(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
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
exprt conversion(const exprt &src, const exprt &rm, const ieee_float_spect &src_spec, const ieee_float_spect &dest_spec) const
static exprt isnan(const exprt &, const ieee_float_spect &)
static biased_floatt bias(const unbiased_floatt &, const ieee_float_spect &)
takes an unbiased float, and applies the bias
static exprt get_exponent(const exprt &, const ieee_float_spect &)
Gets the unbiased exponent in a floating-point bit-vector.
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 add_bias(const exprt &exponent, const ieee_float_spect &)
static exprt sticky_right_shift(const exprt &op, const exprt &dist, exprt &sticky)
exprt rounder(const unbiased_floatt &, const exprt &rm, const ieee_float_spect &) const
static exprt subtract_exponents(const unbiased_floatt &src1, const unbiased_floatt &src2)
Subtracts the exponents.
exprt div(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
exprt convert(const exprt &) const
static ieee_float_spect get_spec(const exprt &)
static exprt to_unsigned_integer(const exprt &src, std::size_t dest_width, const exprt &rm, const ieee_float_spect &)
static exprt negation(const exprt &, const ieee_float_spect &)
static exprt relation(const exprt &, relt rel, const exprt &, const ieee_float_spect &)
static exprt isinf(const exprt &, const ieee_float_spect &)
static exprt sign_bit(const exprt &)
exprt mul(const exprt &, const exprt &, const exprt &rm, const ieee_float_spect &) const
static exprt fraction_all_zeros(const exprt &, const ieee_float_spect &)
static exprt exponent_all_zeros(const exprt &, const ieee_float_spect &)
static exprt is_equal(const exprt &, 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 &)
static exprt limit_distance(const exprt &dist, mp_integer limit)
Limits the shift distance.
static exprt pack(const biased_floatt &, const ieee_float_spect &)
static void round_exponent(unbiased_floatt &result, const rounding_mode_bitst &, const ieee_float_spect &)
Fixed-width bit-vector with IEEE floating-point interpretation.
class floatbv_typet to_type() const
mp_integer max_exponent() const
std::size_t width() const
An IEEE 754 floating-point value, including specificiation.
constant_exprt to_expr() const
The trinary if-then-else operator.
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
constant_exprt zero_expr() const
Return an expression representing the zero value of this type.
const irep_idt & id() const
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Binary multiplication Associativity is not specified.
The plus expression Associativity is not specified.
Sign of an expression Predicate is true if _op is negative, false otherwise.
Fixed-width bit-vector with two's complement interpretation.
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
Fixed-width bit-vector with unsigned binary interpretation.
zero extension The operand is converted to the given type by either a) truncating if the new type is ...
API to expression classes for floating-point arithmetic.
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_notequal_exprt & to_ieee_float_notequal_expr(const exprt &expr)
Cast an exprt to an ieee_float_notequal_exprt.
const ieee_float_equal_exprt & to_ieee_float_equal_expr(const exprt &expr)
Cast an exprt to an ieee_float_equal_exprt.
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
const std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::mask
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const abs_exprt & to_abs_expr(const exprt &expr)
Cast an exprt to a abs_exprt.
const unary_minus_exprt & to_unary_minus_expr(const exprt &expr)
Cast an exprt to a unary_minus_exprt.
void get(const exprt &rm)
bool is_signed(const typet &t)
Convenience function – is the type signed?