32 result.
set(ID_x86_extended,
true);
60 out << to_ansi_c_string();
67 switch(format_spec.
style)
70 result+=to_string_decimal(format_spec.
precision);
74 result+=to_string_scientific(format_spec.
precision);
88 extract_base10(_fraction, _exponent);
90 mp_integer adjusted_exponent=base10_digits(_fraction)+_exponent;
92 if(adjusted_exponent>=format_spec.
precision ||
95 result+=to_string_scientific(format_spec.
precision);
99 result+=to_string_decimal(format_spec.
precision);
105 std::size_t trunc_pos=result.find_last_not_of(
'0');
106 if(trunc_pos!=std::string::npos)
107 result.resize(trunc_pos+1);
110 if(!result.empty() && result.back()==
'.')
111 result.resize(result.size()-1);
117 while(result.size()<format_spec.
min_width)
128 while(tmp!=0) { ++result; tmp/=10; }
139 if((NaN_flag || infinity_flag) && !sign_flag)
145 else if(infinity_flag)
155 for(std::size_t i=0; i<precision; i++)
162 extract_base2(_fraction, _exponent);
173 for(std::size_t i=0; i<precision; i++)
183 _fraction*=
power(5, position);
186 if(position>precision)
200 while(
mp_integer(tmp.size())<=position) tmp=
"0"+tmp;
203 result+=std::string(tmp, 0, dot)+
'.';
204 result+=std::string(tmp, dot, std::string::npos);
232 if((NaN_flag || infinity_flag) && !sign_flag)
238 else if(infinity_flag)
248 for(std::size_t i=0; i<precision; i++)
257 extract_base10(_fraction, _exponent);
261 if(base10_digits(_fraction)>precision+1)
264 mp_integer distance=base10_digits(_fraction)-(precision+1);
275 else if(remainder>p/2)
281 assert(!decimals.empty());
291 while(decimals.size()<precision+1)
294 result+=decimals.substr(1, precision);
300 std::string exponent_str=
303 if(!exponent_str.empty() && exponent_str[0]!=
'-')
306 result+=exponent_str;
333 if(exponent==spec.max_exponent() && fraction!=0)
337 else if(exponent==spec.max_exponent() && fraction==0)
342 else if(exponent==0 && fraction==0)
351 exponent=-spec.bias()+1;
357 fraction+=
power(2, spec.f);
358 exponent-=spec.bias();
364 return fraction>=
power(2, spec.f);
373 result+=
power(2, spec.e+spec.f);
377 result+=
power(2, spec.f)*spec.max_exponent();
380 else if(infinity_flag)
382 result+=
power(2, spec.f)*spec.max_exponent();
384 else if(fraction==0 && exponent==0)
391 result+=fraction-
power(2, spec.f);
394 result+=
power(2, spec.f)*(exponent+spec.bias());
409 if(is_zero() || is_NaN() || is_infinity())
411 _fraction=_exponent=0;
422 while((_fraction%2)==0)
433 if(is_zero() || is_NaN() || is_infinity())
435 _fraction=_exponent=0;
448 _fraction*=
power(2, _exponent);
454 _fraction*=
power(5, -_exponent);
458 while((_fraction%10)==0)
469 sign_flag=_fraction<0;
483 NaN_flag=infinity_flag=
false;
484 sign_flag=_fraction<0;
495 fraction*=
power(2, e_power);
497 fraction/=
power(5, -_exponent);
502 fraction*=
power(5, _exponent);
510 NaN_flag=infinity_flag=sign_flag=
false;
530 sign_flag=!sign_flag;
545 std::size_t lowPower2=fraction.floorPow2();
550 exponent_offset-=(spec.f-lowPower2);
552 assert(fraction*
power(2, (spec.f-lowPower2))>=f_power);
553 assert(fraction*
power(2, (spec.f-lowPower2))<f_power_next);
555 else if(lowPower2>spec.f)
557 exponent_offset+=(lowPower2-spec.f);
559 assert(fraction/
power(2, (lowPower2-spec.f))>=f_power);
560 assert(fraction/
power(2, (lowPower2-spec.f))<f_power_next);
563 mp_integer biased_exponent=exponent+exponent_offset+spec.bias();
566 if(biased_exponent>=spec.max_exponent())
569 switch(rounding_mode)
572 case NONDETERMINISTIC:
577 case ROUND_TO_MINUS_INF:
585 case ROUND_TO_PLUS_INF:
609 else if(biased_exponent<=0)
613 exponent_offset=new_exponent-exponent;
616 exponent+=exponent_offset;
618 if(exponent_offset>0)
620 divide_and_round(fraction,
power(2, exponent_offset));
623 if(fraction==f_power_next)
629 else if(exponent_offset<0)
630 fraction*=
power(2, -exponent_offset);
645 switch(rounding_mode)
650 if(remainder<factor_middle)
654 else if(remainder>factor_middle)
670 case ROUND_TO_MINUS_INF:
675 case ROUND_TO_PLUS_INF:
695 assert(other.
spec.
f==spec.f);
709 if(is_zero() && other.
is_zero())
733 bool old_sign=sign_flag;
742 else if(infinity_flag)
751 fraction*=
power(2, spec.f);
754 fraction*=
power(2, spec.f);
769 assert(other.
spec.
f==spec.f);
778 if(is_zero() || other.
is_zero())
807 assert(_other.
spec==spec);
821 else if(infinity_flag)
831 if(is_zero() && other.
is_zero())
837 if(rounding_mode==ROUND_TO_MINUS_INF)
875 if(rounding_mode==ROUND_TO_MINUS_INF)
882 sign_flag=(fraction<0);
896 return (*
this)+=_other;
905 if(is_zero() && other.
is_zero())
951 if(is_zero() && other.
is_zero())
1004 if(is_zero() && other.
is_zero())
1006 assert(spec==other.
spec);
1007 return *
this==other;
1014 return *
this==other;
1019 return !(*
this==other);
1026 if(is_zero() && other.
is_zero())
1028 assert(spec==other.
spec);
1029 return *
this!=other;
1048 build(_fraction, _exponent);
1059 if(NaN_flag || infinity_flag || is_zero())
1068 result/=
power(2, -new_exponent);
1070 result*=
power(2, new_exponent);
1082 assert(spec.width()==64);
1085 assert(
sizeof(
double)==
sizeof(
long long unsigned int));
1090 long long unsigned int i;
1102 assert(spec.width()==32);
1104 assert(
sizeof(
float)==
sizeof(
unsigned int));
1123 infinity_flag=
false;
1130 unpack(bit_pattern);
1135 unpack(
power(2, spec.f));
1149 make_plus_infinity();
1155 return spec.f==52 && spec.e==11;
1160 return spec.f==23 && spec.e==8;
1167 union {
double f; uint64_t i; } a;
1172 return -std::numeric_limits<double>::infinity();
1174 return std::numeric_limits<double>::infinity();
1180 return -std::numeric_limits<double>::quiet_NaN();
1182 return std::numeric_limits<double>::quiet_NaN();
1186 assert(i.is_ulong());
1196 if(
sizeof(
unsigned)!=
sizeof(
float))
1198 throw "ieee_floatt::to_float not supported on this architecture";
1201 union {
float f; uint32_t i; } a;
1206 return -std::numeric_limits<float>::infinity();
1208 return std::numeric_limits<float>::infinity();
1214 return -std::numeric_limits<float>::quiet_NaN();
1216 return std::numeric_limits<float>::quiet_NaN();
1220 assert(i.is_ulong());
1233 bool old_sign=get_sign();
1245 if(get_sign()==greater)
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...
const std::string & id2string(const irep_idt &d)
ieee_floatt & operator-=(const ieee_floatt &other)
bool operator>=(const ieee_floatt &other) const
bool operator!=(const ieee_floatt &other) const
const std::string integer2string(const mp_integer &n, unsigned base)
constant_exprt to_expr() const
Fixed-width bit-vector with IEEE floating-point interpretation.
ieee_floatt & operator+=(const ieee_floatt &other)
void from_expr(const constant_exprt &expr)
void build(const mp_integer &exp, const mp_integer &frac)
bool operator==(const ieee_floatt &other) const
const irep_idt & get_value() const
void from_type(const floatbv_typet &type)
void next_representable(bool greater)
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinit...
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
void print(std::ostream &out) const
mp_integer max_exponent() const
A constant literal expression.
bool get_bool(const irep_namet &name) const
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
mp_integer max_fraction() const
void divide_and_round(mp_integer &fraction, const mp_integer &factor)
class floatbv_typet to_type() const
void change_spec(const ieee_float_spect &dest_spec)
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
void set_value(const irep_idt &value)
mp_integer to_integer() const
bool ieee_equal(const ieee_floatt &other) const
void unpack(const mp_integer &i)
API to expression classes.
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
bool operator<=(const ieee_floatt &other) const
void from_float(const float f)
std::size_t get_width() const
std::string format(const format_spect &format_spec) const
void make_minus_infinity()
std::size_t get_f() const
static mp_integer base10_digits(const mp_integer &src)
void make_plus_infinity()
void from_double(const double d)
bool operator>(const ieee_floatt &other) const
const std::string integer2binary(const mp_integer &n, std::size_t width)
ieee_floatt & operator/=(const ieee_floatt &other)
std::string to_string_decimal(std::size_t precision) const
void from_integer(const mp_integer &i)
void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const
void dot(const goto_functionst &src, const namespacet &ns, std::ostream &out)
bool ieee_not_equal(const ieee_floatt &other) const
void set_f(std::size_t b)
std::size_t width() const
ieee_floatt & operator*=(const ieee_floatt &other)
std::size_t integer2size_t(const mp_integer &n)
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
void set(const irep_namet &name, const irep_idt &value)
bool operator<(const ieee_floatt &other) const
void set_width(std::size_t width)