10 #ifndef CPROVER_UTIL_IEEE_FLOAT_H 11 #define CPROVER_UTIL_IEEE_FLOAT_H 46 f(_f), e(_e), x86_extended(false)
54 return f+e+1+(x86_extended?1:0);
99 return f==other.
f && e==other.
e && x86_extended==other.
x86_extended;
104 return !(*
this==other);
116 ROUND_TO_EVEN=0, ROUND_TO_MINUS_INF=1,
117 ROUND_TO_PLUS_INF=2, ROUND_TO_ZERO=3,
126 rounding_mode(ROUND_TO_EVEN),
127 spec(_spec), sign_flag(false), exponent(0), fraction(0),
128 NaN_flag(false), infinity_flag(false)
133 rounding_mode(ROUND_TO_EVEN),
144 rounding_mode(ROUND_TO_EVEN),
145 sign_flag(false), exponent(0), fraction(0),
146 NaN_flag(false), infinity_flag(false)
151 rounding_mode(ROUND_TO_EVEN)
158 sign_flag=!sign_flag;
162 { sign_flag = _sign; }
181 void make_plus_infinity();
182 void make_minus_infinity();
206 if(is_zero() && get_sign() && distinguish_zero)
209 next_representable(
true);
215 if(is_zero() && !get_sign() && distinguish_zero)
218 next_representable(
false);
223 return !NaN_flag && !infinity_flag && fraction==0 && exponent==0;
228 bool is_normal()
const;
238 void from_double(
const double d);
239 void from_float(
const float f);
243 double to_double()
const;
244 float to_float()
const;
245 bool is_double()
const;
246 bool is_float()
const;
256 void print(std::ostream &out)
const;
263 std::string to_string_decimal(std::size_t precision)
const;
264 std::string to_string_scientific(std::size_t precision)
const;
265 std::string format(
const format_spect &format_spec)
const;
290 bool ieee_not_equal(
const ieee_floatt &other)
const;
295 void next_representable(
bool greater);
314 #endif // CPROVER_UTIL_IEEE_FLOAT_H
void decrement(bool distinguish_zero=false)
exprt to_expr(const namespacet &ns, const irep_idt &identifier, const std::string &src)
std::ostream & operator<<(std::ostream &out, const ieee_floatt &f)
guardt & operator-=(guardt &g1, const guardt &g2)
static ieee_floatt NaN(const ieee_float_spect &_spec)
Fixed-width bit-vector with IEEE floating-point interpretation.
static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void from_type(const floatbv_typet &type)
void set_sign(bool _sign)
mp_integer max_exponent() const
A constant literal expression.
const mp_integer & get_exponent() const
tvt operator>(const interval_templatet< T > &a, const interval_templatet< T > &b)
mp_integer max_fraction() const
ieee_floatt(const ieee_float_spect &_spec)
static ieee_float_spect double_precision()
static ieee_float_spect x86_96()
tvt operator<=(const interval_templatet< T > &a, const interval_templatet< T > &b)
ieee_floatt(const floatbv_typet &type)
static ieee_float_spect quadruple_precision()
static ieee_float_spect single_precision()
bool operator!=(const ieee_float_spect &other) const
ieee_floatt(const constant_exprt &expr)
static ieee_floatt fltmax(const ieee_float_spect &_spec)
void make_minus_infinity()
bool operator==(const ieee_float_spect &other) const
void make_plus_infinity()
static ieee_float_spect x86_80()
void increment(bool distinguish_zero=false)
ieee_float_spect(const floatbv_typet &type)
static ieee_floatt fltmin(const ieee_float_spect &_spec)
tvt operator>=(const interval_templatet< T > &a, const interval_templatet< T > &b)
rounding_modet rounding_mode
ieee_float_spect(std::size_t _f, std::size_t _e)
static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
std::size_t width() const
tvt operator<(const interval_templatet< T > &a, const interval_templatet< T > &b)
std::string to_ansi_c_string() const
const mp_integer & get_fraction() const
static ieee_floatt zero(const floatbv_typet &type)