296 std::size_t width=
bv_type.get_width();
454 "the exponent needs to have a signed type");
544 const exprt distance=
744 std::size_t fraction_width=
746 std::size_t
div_width=fraction_width*2+1;
836 "relation should be equality, less-than, or less-or-equal");
928 src, spec.
f+spec.
e-1, spec.
f,
969 for(
int d=depth-1; d>=0; d--)
971 unsigned distance=(1<<d);
974 "distance must be within the range of fraction bits");
994 "depth must be smaller than exponent bits");
1122 return pack(
bias(result, spec), spec);
1129 const exprt &fraction,
1156 extra_bits >= 1,
"the extra bits contain at least the rounding bit");
1212 extra_bits >= 1,
"the extra bits include at least the rounding bit");
1470 {std::move(
sign_bit), std::move(exponent), std::move(fraction)},
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
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
The trinary if-then-else operator.
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.
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.
#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?