52 "mantissa bits must be less than "
53 "originating type width");
114 std::size_t
trunc_pos=result.find_last_not_of(
'0');
119 if(!result.empty() && result.back()==
'.')
120 result.resize(result.size()-1);
137 while(
tmp!=0) { ++result;
tmp/=10; }
164 for(std::size_t i=0; i<precision; i++)
182 for(std::size_t i=0; i<precision; i++)
195 if(position>precision)
211 const std::size_t
dot =
213 result+=std::string(
tmp, 0,
dot)+
'.';
214 result+=std::string(
tmp,
dot, std::string::npos);
258 for(std::size_t i=0; i<precision; i++)
304 result+=
decimals.substr(1, precision);
479 result.fraction =
power(2, result.spec.f);
502 return -std::numeric_limits<double>::infinity();
504 return std::numeric_limits<double>::infinity();
510 return -std::numeric_limits<double>::quiet_NaN();
512 return std::numeric_limits<double>::quiet_NaN();
517 CHECK_RETURN(i <= std::numeric_limits<std::uint64_t>::max());
529 std::numeric_limits<float>::is_iec559,
530 "this requires the float layout is according to the IEC 559/IEEE 754 "
533 sizeof(
float) ==
sizeof(
uint32_t),
"a 32 bit float type is required");
544 return -std::numeric_limits<float>::infinity();
546 return std::numeric_limits<float>::infinity();
552 return -std::numeric_limits<float>::quiet_NaN();
554 return std::numeric_limits<float>::quiet_NaN();
652 return *
this < other;
657 return other < *
this;
662 return other <= *
this;
695 return *
this == other;
703 return *
this == other;
710 return *
this == other;
717 return *
this == other;
722 return !(*
this == other);
734 return *
this != other;
859 "normalisation result must be >= lower bound");
862 "normalisation result must be < upper bound");
870 "normalisation result must be >= lower bound");
873 "normalisation result must be < upper bound");
978 if((dividend % 2) != 0)
1193 "prior block equalises the exponents by setting both to the "
1194 "minimum of their previous values while adjusting the mantissa");
1199 _other.fraction.negate();
1284 std::numeric_limits<double>::is_iec559,
1285 "this requires the double layout is according to the ieee754 "
1288 sizeof(
double) ==
sizeof(std::uint64_t),
"ensure double has 64 bit width");
1308 std::numeric_limits<float>::is_iec559,
1309 "this requires the float layout is according to the ieee754 "
1312 sizeof(
float) ==
sizeof(std::uint32_t),
"ensure float has 32 bit width");
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
void set_width(std::size_t width)
std::size_t get_width() const
A constant literal expression.
const irep_idt & get_value() const
typet & type()
Return the type of the expression.
Fixed-width bit-vector with IEEE floating-point interpretation.
void set_f(std::size_t b)
std::size_t get_f() const
mp_integer max_fraction() const
class floatbv_typet to_type() const
mp_integer max_exponent() const
void from_type(const floatbv_typet &type)
static ieee_float_spect double_precision()
std::size_t width() const
An IEEE 754 floating-point value, including specificiation.
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
void set_sign(bool _sign)
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
bool ieee_equal(const ieee_float_valuet &) const
bool operator>=(const ieee_float_valuet &) const
bool operator<(const ieee_float_valuet &) const
static ieee_float_valuet one(const floatbv_typet &)
bool operator!=(const ieee_float_valuet &) const
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
void make_minus_infinity()
void from_expr(const constant_exprt &expr)
bool ieee_not_equal(const ieee_float_valuet &) const
constant_exprt to_expr() const
bool operator==(const ieee_float_valuet &) const
ieee_float_valuet abs() const
std::string to_ansi_c_string() const
std::string to_string_decimal(std::size_t precision) const
std::string to_string_scientific(std::size_t precision) const
format as [-]d.ddde+-d Note that printf always produces at least two digits for the exponent.
void print(std::ostream &out) const
void next_representable(bool greater)
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinit...
static mp_integer base10_digits(const mp_integer &src)
bool operator<=(const ieee_float_valuet &) const
std::string format(const format_spect &format_spec) const
void unpack(const mp_integer &)
void make_plus_infinity()
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
bool operator>(const ieee_float_valuet &) const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
ieee_floatt & operator*=(const ieee_floatt &other)
mp_integer to_integer() const
ieee_floatt & operator+=(const ieee_floatt &other)
void divide_and_round(mp_integer ÷nd, const mp_integer &divisor)
static constant_exprt rounding_mode_expr(rounding_modet)
ieee_floatt & operator-=(const ieee_floatt &other)
ieee_floatt & operator/=(const ieee_floatt &other)
rounding_modet _rounding_mode
void from_integer(const mp_integer &i)
rounding_modet rounding_mode() const
void build(const mp_integer &exp, const mp_integer &frac)
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
void change_spec(const ieee_float_spect &dest_spec)
ieee_floatt round_to_integral() const
bool get_bool(const irep_idt &name) const
void set(const irep_idt &name, const irep_idt &value)
void dot(const goto_modelt &src, std::ostream &out)
constant_exprt floatbv_rounding_mode(unsigned rm)
returns the a rounding mode expression for a given IEEE rounding mode, encoded using the recommendati...
API to expression classes for floating-point arithmetic.
double remainder(double x, double y)
const std::string integer2string(const mp_integer &n, unsigned base)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
API to expression classes.