cprover
|
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values. More...
#include <ieee_float.h>
Public Types | |
enum | rounding_modet { ROUND_TO_EVEN = 0 , ROUND_TO_MINUS_INF = 1 , ROUND_TO_PLUS_INF = 2 , ROUND_TO_ZERO = 3 , ROUND_TO_AWAY = 4 , UNKNOWN , NONDETERMINISTIC } |
Public Member Functions | |
rounding_modet | rounding_mode () const |
ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode) | |
ieee_floatt (ieee_float_spect __spec, rounding_modet __rounding_mode, const mp_integer &value) | |
ieee_floatt (const floatbv_typet &type, rounding_modet __rounding_mode) | |
ieee_floatt (const constant_exprt &expr, rounding_modet __rounding_mode) | |
ieee_floatt (ieee_float_valuet __value, rounding_modet __rounding_mode) | |
void | from_integer (const mp_integer &i) |
void | from_base10 (const mp_integer &exp, const mp_integer &frac) |
compute f * (10^e) | |
void | build (const mp_integer &exp, const mp_integer &frac) |
double | to_double () const |
float | to_float () const |
mp_integer | to_integer () const |
void | change_spec (const ieee_float_spect &dest_spec) |
ieee_floatt | round_to_integral () const |
ieee_floatt & | operator/= (const ieee_floatt &other) |
ieee_floatt & | operator*= (const ieee_floatt &other) |
ieee_floatt & | operator+= (const ieee_floatt &other) |
ieee_floatt & | operator-= (const ieee_floatt &other) |
Public Member Functions inherited from ieee_float_valuet | |
ieee_float_valuet (const ieee_float_spect &_spec) | |
ieee_float_valuet (const floatbv_typet &type) | |
ieee_float_valuet (const constant_exprt &expr) | |
ieee_float_valuet () | |
void | negate () |
void | set_sign (bool _sign) |
void | make_zero () |
void | make_NaN () |
void | make_plus_infinity () |
void | make_minus_infinity () |
void | make_fltmax () |
void | make_fltmin () |
void | increment (bool distinguish_zero=false) |
void | decrement (bool distinguish_zero=false) |
bool | is_zero () const |
bool | get_sign () const |
bool | is_negative () const |
bool | is_NaN () const |
bool | is_infinity () const |
bool | is_normal () const |
const mp_integer & | get_exponent () const |
const mp_integer & | get_fraction () const |
void | unpack (const mp_integer &) |
void | from_double (double) |
void | from_float (float) |
double | to_double () const |
Note that calling from_double -> to_double can return different bit patterns for NaN. | |
float | to_float () const |
Note that calling from_float -> to_float can return different bit patterns for NaN. | |
bool | is_double () const |
bool | is_float () const |
mp_integer | pack () const |
void | extract_base2 (mp_integer &_exponent, mp_integer &_fraction) const |
void | extract_base10 (mp_integer &_exponent, mp_integer &_fraction) const |
mp_integer | to_integer () const |
void | print (std::ostream &out) 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. | |
std::string | format (const format_spect &format_spec) const |
constant_exprt | to_expr () const |
void | from_expr (const constant_exprt &expr) |
bool | operator< (const ieee_float_valuet &) const |
bool | operator<= (const ieee_float_valuet &) const |
bool | operator> (const ieee_float_valuet &) const |
bool | operator>= (const ieee_float_valuet &) const |
ieee_float_valuet | abs () const |
bool | operator== (const ieee_float_valuet &) const |
bool | operator!= (const ieee_float_valuet &) const |
bool | operator== (int) const |
bool | operator== (double) const |
bool | operator== (float) const |
bool | ieee_equal (const ieee_float_valuet &) const |
bool | ieee_not_equal (const ieee_float_valuet &) const |
Static Public Member Functions | |
static constant_exprt | rounding_mode_expr (rounding_modet) |
Static Public Member Functions inherited from ieee_float_valuet | |
static ieee_float_valuet | zero (const floatbv_typet &type) |
static ieee_float_valuet | zero (const ieee_float_spect &spec) |
static ieee_float_valuet | one (const floatbv_typet &) |
static ieee_float_valuet | one (const ieee_float_spect &) |
static ieee_float_valuet | NaN (const ieee_float_spect &_spec) |
static ieee_float_valuet | plus_infinity (const ieee_float_spect &_spec) |
static ieee_float_valuet | minus_infinity (const ieee_float_spect &_spec) |
static ieee_float_valuet | fltmax (const ieee_float_spect &_spec) |
static ieee_float_valuet | fltmin (const ieee_float_spect &_spec) |
Protected Member Functions | |
void | divide_and_round (mp_integer ÷nd, const mp_integer &divisor) |
void | align () |
Protected Member Functions inherited from ieee_float_valuet | |
void | next_representable (bool greater) |
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false). |
Protected Attributes | |
rounding_modet | _rounding_mode |
Protected Attributes inherited from ieee_float_valuet | |
bool | sign_flag |
mp_integer | exponent |
mp_integer | fraction |
bool | NaN_flag |
bool | infinity_flag |
Additional Inherited Members | |
Public Attributes inherited from ieee_float_valuet | |
ieee_float_spect | spec |
Static Protected Member Functions inherited from ieee_float_valuet | |
static mp_integer | base10_digits (const mp_integer &src) |
An IEEE 754 value plus a rounding mode, enabling operations with rounding on values.
Definition at line 337 of file ieee_float.h.
Enumerator | |
---|---|
ROUND_TO_EVEN | |
ROUND_TO_MINUS_INF | |
ROUND_TO_PLUS_INF | |
ROUND_TO_ZERO | |
ROUND_TO_AWAY | |
UNKNOWN | |
NONDETERMINISTIC |
Definition at line 346 of file ieee_float.h.
|
inline |
Definition at line 365 of file ieee_float.h.
|
inline |
Definition at line 370 of file ieee_float.h.
|
inline |
Definition at line 379 of file ieee_float.h.
|
inline |
Definition at line 384 of file ieee_float.h.
|
inline |
Definition at line 389 of file ieee_float.h.
|
protected |
Definition at line 821 of file ieee_float.cpp.
void ieee_floatt::build | ( | const mp_integer & | exp, |
const mp_integer & | frac ) |
Definition at line 566 of file ieee_float.cpp.
void ieee_floatt::change_spec | ( | const ieee_float_spect & | dest_spec | ) |
Definition at line 1231 of file ieee_float.cpp.
|
protected |
Definition at line 954 of file ieee_float.cpp.
void ieee_floatt::from_base10 | ( | const mp_integer & | exp, |
const mp_integer & | frac ) |
compute f * (10^e)
Definition at line 784 of file ieee_float.cpp.
void ieee_floatt::from_integer | ( | const mp_integer & | i | ) |
Definition at line 813 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator*= | ( | const ieee_floatt & | other | ) |
Definition at line 1097 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator+= | ( | const ieee_floatt & | other | ) |
Definition at line 1133 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator-= | ( | const ieee_floatt & | other | ) |
Definition at line 1224 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator/= | ( | const ieee_floatt & | other | ) |
Definition at line 1023 of file ieee_float.cpp.
ieee_floatt ieee_floatt::round_to_integral | ( | ) | const |
Definition at line 1371 of file ieee_float.cpp.
|
inline |
Definition at line 357 of file ieee_float.h.
|
static |
Definition at line 561 of file ieee_float.cpp.
double ieee_floatt::to_double | ( | ) | const |
float ieee_floatt::to_float | ( | ) | const |
mp_integer ieee_floatt::to_integer | ( | ) | const |
Definition at line 1256 of file ieee_float.cpp.
|
protected |
Definition at line 419 of file ieee_float.h.