10#ifndef CPROVER_UTIL_IEEE_FLOAT_H
11#define CPROVER_UTIL_IEEE_FLOAT_H
111 return !(*
this==other);
205 c.make_plus_infinity();
212 c.make_minus_infinity();
279 void print(std::ostream &out)
const;
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A constant literal expression.
Fixed-width bit-vector with IEEE floating-point interpretation.
mp_integer max_fraction() const
ieee_float_spect(std::size_t _f, std::size_t _e)
static ieee_float_spect half_precision()
ieee_float_spect(const floatbv_typet &type)
bool operator!=(const ieee_float_spect &other) const
static ieee_float_spect x86_80()
static ieee_float_spect single_precision()
static ieee_float_spect quadruple_precision()
bool operator==(const ieee_float_spect &other) const
class floatbv_typet to_type() const
mp_integer max_exponent() const
static ieee_float_spect x86_96()
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.
ieee_float_valuet(const ieee_float_spect &_spec)
void set_sign(bool _sign)
static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
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
ieee_float_valuet(const constant_exprt &expr)
constant_exprt to_expr() const
static ieee_float_valuet fltmin(const ieee_float_spect &_spec)
bool operator==(const ieee_float_valuet &) const
static ieee_float_valuet fltmax(const ieee_float_spect &_spec)
std::string to_ansi_c_string() const
std::string to_string_decimal(std::size_t precision) const
const mp_integer & get_fraction() 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 ieee_float_valuet zero(const floatbv_typet &type)
static mp_integer base10_digits(const mp_integer &src)
static ieee_float_valuet NaN(const ieee_float_spect &_spec)
bool operator<=(const ieee_float_valuet &) const
mp_integer to_integer() const
void decrement(bool distinguish_zero=false)
std::string format(const format_spect &format_spec) const
static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
void unpack(const mp_integer &)
void make_plus_infinity()
void increment(bool distinguish_zero=false)
ieee_float_valuet(const floatbv_typet &type)
void extract_base2(mp_integer &_exponent, mp_integer &_fraction) const
bool operator>(const ieee_float_valuet &) const
static ieee_float_valuet zero(const ieee_float_spect &spec)
const mp_integer & get_exponent() const
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
ieee_floatt & operator*=(const ieee_floatt &other)
ieee_floatt(ieee_float_valuet __value, rounding_modet __rounding_mode)
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(const floatbv_typet &type, rounding_modet __rounding_mode)
ieee_floatt & operator-=(const ieee_floatt &other)
ieee_floatt & operator/=(const ieee_floatt &other)
ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)
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)
ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
void change_spec(const ieee_float_spect &dest_spec)
std::ostream & operator<<(std::ostream &out, const ieee_float_valuet &f)