Go to the documentation of this file.
31 result.
set(ID_x86_extended,
true);
52 "mantissa bits must be less than "
53 "originating type width");
69 switch(format_spec.
style)
94 if(adjusted_exponent>=format_spec.
precision ||
107 std::size_t trunc_pos=result.find_last_not_of(
'0');
108 if(trunc_pos!=std::string::npos)
109 result.resize(trunc_pos+1);
112 if(!result.empty() && result.back()==
'.')
113 result.resize(result.size()-1);
119 while(result.size()<format_spec.
min_width)
130 while(tmp!=0) { ++result; tmp/=10; }
157 for(std::size_t i=0; i<precision; i++)
175 for(std::size_t i=0; i<precision; i++)
185 _fraction*=
power(5, position);
188 if(position>precision)
202 while(
mp_integer(tmp.size())<=position) tmp=
"0"+tmp;
204 const std::size_t
dot =
205 tmp.size() - numeric_cast_v<std::size_t>(position);
206 result+=std::string(tmp, 0,
dot)+
'.';
207 result+=std::string(tmp,
dot, std::string::npos);
251 for(std::size_t i=0; i<precision; i++)
278 else if(remainder>p/2)
294 while(decimals.size()<precision+1)
297 result+=decimals.substr(1, precision);
303 std::string exponent_str=
306 if(!exponent_str.empty() && exponent_str[0]!=
'-')
309 result+=exponent_str;
414 _fraction=_exponent=0;
425 while((_fraction%2)==0)
438 _fraction=_exponent=0;
451 _fraction*=
power(2, _exponent);
457 _fraction*=
power(5, -_exponent);
461 while((_fraction%10)==0)
548 std::size_t lowPower2=
fraction.floorPow2();
553 exponent_offset-=(
spec.
f-lowPower2);
557 "normalisation result must be >= lower bound");
560 "normalisation result must be < upper bound");
562 else if(lowPower2>
spec.
f)
564 exponent_offset+=(lowPower2-
spec.
f);
568 "normalisation result must be >= lower bound");
571 "normalisation result must be < upper bound");
620 else if(biased_exponent<=0)
624 exponent_offset=new_exponent-
exponent;
629 if(exponent_offset>0)
640 else if(exponent_offset<0)
651 const mp_integer remainder = dividend % divisor;
661 if(remainder < divisor_middle)
665 else if(remainder > divisor_middle)
671 if((dividend % 2) != 0)
873 "prior block equalises the exponents by setting both to the "
874 "minimum of their previous values while adjusting the mantissa");
908 return (*
this)+=_other;
1019 return *
this==other;
1026 return *
this==other;
1031 return !(*
this==other);
1041 return *
this!=other;
1060 build(_fraction, _exponent);
1080 result/=
power(2, -new_exponent);
1082 result*=
power(2, new_exponent);
1097 std::numeric_limits<double>::is_iec559,
1098 "this requires the double layout is according to the ieee754 "
1101 sizeof(
double) ==
sizeof(std::uint64_t),
"ensure double has 64 bit width");
1121 std::numeric_limits<float>::is_iec559,
1122 "this requires the float layout is according to the ieee754 "
1125 sizeof(
float) ==
sizeof(std::uint32_t),
"ensure float has 32 bit width");
1189 union {
double f; uint64_t i; } a;
1194 return -std::numeric_limits<double>::infinity();
1196 return std::numeric_limits<double>::infinity();
1202 return -std::numeric_limits<double>::quiet_NaN();
1204 return std::numeric_limits<double>::quiet_NaN();
1209 CHECK_RETURN(i <= std::numeric_limits<std::uint64_t>::max());
1221 std::numeric_limits<float>::is_iec559,
1222 "this requires the float layout is according to the IEC 559/IEEE 754 "
1225 sizeof(
float) ==
sizeof(uint32_t),
"a 32 bit float type is required");
1227 union {
float f; uint32_t i; } a;
1232 return -std::numeric_limits<float>::infinity();
1234 return std::numeric_limits<float>::infinity();
1240 return -std::numeric_limits<float>::quiet_NaN();
1242 return std::numeric_limits<float>::quiet_NaN();
1245 a.i = numeric_cast_v<uint32_t>(
pack());
#define UNREACHABLE
This should be used to mark dead code.
void set_f(std::size_t b)
bool operator==(const ieee_floatt &other) const
mp_integer max_fraction() const
void set_sign(bool _sign)
void print(std::ostream &out) const
#define CHECK_RETURN(CONDITION)
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
std::size_t get_f() const
std::string to_ansi_c_string() const
void dot(const goto_modelt &src, std::ostream &out)
Fixed-width bit-vector with IEEE floating-point interpretation.
bool operator<(const ieee_floatt &other) const
void unpack(const mp_integer &i)
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
void change_spec(const ieee_float_spect &dest_spec)
mp_integer to_integer() const
bool operator!=(const ieee_floatt &other) const
void from_type(const floatbv_typet &type)
void from_float(const float f)
ieee_floatt & operator+=(const ieee_floatt &other)
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
typet & type()
Return the type of the expression.
bool get_bool(const irep_namet &name) const
bool operator<=(const ieee_floatt &other) const
static ieee_float_spect double_precision()
std::size_t width() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
class floatbv_typet to_type() const
#define PRECONDITION(CONDITION)
bool ieee_equal(const ieee_floatt &other) const
void make_plus_infinity()
bool operator>(const ieee_floatt &other) const
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
void divide_and_round(mp_integer ÷nd, const mp_integer &divisor)
void from_integer(const mp_integer &i)
void set_width(std::size_t width)
rounding_modet rounding_mode
std::string to_string_decimal(std::size_t precision) const
std::size_t get_width() const
bool ieee_not_equal(const ieee_floatt &other) const
void set(const irep_namet &name, const irep_idt &value)
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.
mp_integer max_exponent() const
void make_minus_infinity()
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
constant_exprt to_expr() const
std::string format(const format_spect &format_spec) const
static mp_integer base10_digits(const mp_integer &src)
A constant literal expression.
ieee_floatt & operator-=(const ieee_floatt &other)
bool operator>=(const ieee_floatt &other) const
API to expression classes.
const irep_idt & get_value() const
void next_representable(bool greater)
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinit...
ieee_floatt & operator/=(const ieee_floatt &other)
ieee_floatt & operator*=(const ieee_floatt &other)
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
void from_expr(const constant_exprt &expr)
void build(const mp_integer &exp, const mp_integer &frac)
const std::string integer2string(const mp_integer &n, unsigned base)
void from_double(const double d)