cprover
|
#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, UNKNOWN, NONDETERMINISTIC } |
Public Member Functions | |
ieee_floatt (const ieee_float_spect &_spec) | |
ieee_floatt (const floatbv_typet &type) | |
ieee_floatt () | |
ieee_floatt (const constant_exprt &expr) | |
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_NaN () const |
bool | is_infinity () const |
bool | is_normal () const |
const mp_integer & | get_exponent () const |
const mp_integer & | get_fraction () const |
void | from_integer (const mp_integer &i) |
void | from_base10 (const mp_integer &exp, const mp_integer &frac) |
compute f * (10^e) More... | |
void | build (const mp_integer &exp, const mp_integer &frac) |
void | unpack (const mp_integer &i) |
void | from_double (const double d) |
void | from_float (const float f) |
double | to_double () const |
Note that calling from_double -> to_double can return different bit patterns for NaN. More... | |
float | to_float () const |
Note that calling from_float -> to_float can return different bit patterns for NaN. More... | |
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 | change_spec (const ieee_float_spect &dest_spec) |
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. More... | |
std::string | format (const format_spect &format_spec) const |
constant_exprt | to_expr () const |
void | from_expr (const constant_exprt &expr) |
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) |
bool | operator< (const ieee_floatt &other) const |
bool | operator<= (const ieee_floatt &other) const |
bool | operator> (const ieee_floatt &other) const |
bool | operator>= (const ieee_floatt &other) const |
bool | operator== (const ieee_floatt &other) const |
bool | operator!= (const ieee_floatt &other) const |
bool | operator== (int i) const |
bool | ieee_equal (const ieee_floatt &other) const |
bool | ieee_not_equal (const ieee_floatt &other) const |
Static Public Member Functions | |
static ieee_floatt | zero (const floatbv_typet &type) |
static ieee_floatt | NaN (const ieee_float_spect &_spec) |
static ieee_floatt | plus_infinity (const ieee_float_spect &_spec) |
static ieee_floatt | minus_infinity (const ieee_float_spect &_spec) |
static ieee_floatt | fltmax (const ieee_float_spect &_spec) |
static ieee_floatt | fltmin (const ieee_float_spect &_spec) |
Public Attributes | |
rounding_modet | rounding_mode |
ieee_float_spect | spec |
Protected Member Functions | |
void | divide_and_round (mp_integer &fraction, const mp_integer &factor) |
void | align () |
void | next_representable (bool greater) |
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false). More... | |
Static Protected Member Functions | |
static mp_integer | base10_digits (const mp_integer &src) |
Protected Attributes | |
bool | sign_flag |
mp_integer | exponent |
mp_integer | fraction |
bool | NaN_flag |
bool | infinity_flag |
Definition at line 108 of file ieee_float.h.
Enumerator | |
---|---|
ROUND_TO_EVEN | |
ROUND_TO_MINUS_INF | |
ROUND_TO_PLUS_INF | |
ROUND_TO_ZERO | |
UNKNOWN | |
NONDETERMINISTIC |
Definition at line 114 of file ieee_float.h.
|
inlineexplicit |
Definition at line 125 of file ieee_float.h.
|
inlineexplicit |
Definition at line 132 of file ieee_float.h.
|
inline |
Definition at line 143 of file ieee_float.h.
|
inlineexplicit |
Definition at line 150 of file ieee_float.h.
References from_expr().
|
protected |
Definition at line 516 of file ieee_float.cpp.
References ieee_float_spect::bias(), divide_and_round(), exponent, ieee_float_spect::f, fraction, infinity_flag, make_fltmax(), ieee_float_spect::max_exponent(), NaN_flag, NONDETERMINISTIC, power(), ROUND_TO_EVEN, ROUND_TO_MINUS_INF, ROUND_TO_PLUS_INF, ROUND_TO_ZERO, rounding_mode, sign_flag, spec, and UNKNOWN.
Referenced by build(), from_base10(), from_integer(), operator*=(), operator+=(), and operator/=().
|
staticprotected |
Definition at line 123 of file ieee_float.cpp.
Referenced by format(), and to_string_scientific().
void ieee_floatt::build | ( | const mp_integer & | exp, |
const mp_integer & | frac | ||
) |
Definition at line 465 of file ieee_float.cpp.
References align(), exponent, ieee_float_spect::f, fraction, sign_flag, and spec.
Referenced by change_spec(), convert_float_literal(), and smt2_convt::convert_typecast().
void ieee_floatt::change_spec | ( | const ieee_float_spect & | dest_spec | ) |
Definition at line 1032 of file ieee_float.cpp.
References build(), exponent, ieee_float_spect::f, fraction, sign_flag, and spec.
Referenced by simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_inequality_constant(), and simplify_exprt::simplify_typecast().
|
inline |
Definition at line 213 of file ieee_float.h.
References get_sign(), is_zero(), negate(), and next_representable().
Referenced by interval_domaint::assume_rec().
|
protected |
Definition at line 636 of file ieee_float.cpp.
References fraction, ROUND_TO_EVEN, ROUND_TO_MINUS_INF, ROUND_TO_PLUS_INF, ROUND_TO_ZERO, rounding_mode, and sign_flag.
Referenced by align().
void ieee_floatt::extract_base10 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction | ||
) | const |
Definition at line 429 of file ieee_float.cpp.
References exponent, ieee_float_spect::f, fraction, is_infinity(), is_NaN(), is_zero(), power(), and spec.
Referenced by format(), and to_string_scientific().
void ieee_floatt::extract_base2 | ( | mp_integer & | _exponent, |
mp_integer & | _fraction | ||
) | const |
Definition at line 405 of file ieee_float.cpp.
References exponent, ieee_float_spect::f, fraction, is_infinity(), is_NaN(), is_zero(), and spec.
Referenced by to_string_decimal().
|
inlinestatic |
Definition at line 196 of file ieee_float.h.
References make_fltmax().
|
inlinestatic |
Definition at line 200 of file ieee_float.h.
References make_fltmin().
std::string ieee_floatt::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 63 of file ieee_float.cpp.
References format_spect::AUTOMATIC, base10_digits(), format_spect::DECIMAL, extract_base10(), format_spect::min_width, format_spect::precision, format_spect::SCIENTIFIC, format_spect::style, to_string_decimal(), and to_string_scientific().
Referenced by format_constantt::operator()(), and to_ansi_c_string().
void ieee_floatt::from_base10 | ( | const mp_integer & | exp, |
const mp_integer & | frac | ||
) |
compute f * (10^e)
Definition at line 479 of file ieee_float.cpp.
References align(), ieee_float_spect::e, exponent, ieee_float_spect::f, fraction, infinity_flag, NaN_flag, power(), sign_flag, and spec.
Referenced by convert_float_literal().
void ieee_floatt::from_double | ( | const double | d | ) |
Definition at line 1078 of file ieee_float.cpp.
References ieee_float_spect::e, ieee_float_spect::f, spec, unpack(), and ieee_float_spect::width().
void ieee_floatt::from_expr | ( | const constant_exprt & | expr | ) |
Definition at line 1051 of file ieee_float.cpp.
References binary2integer(), constant_exprt::get_value(), id2string(), spec, to_floatbv_type(), exprt::type(), and unpack().
Referenced by java_bytecode_convert_methodt::convert_instructions(), interpretert::evaluate(), and ieee_floatt().
void ieee_floatt::from_float | ( | const float | f | ) |
Definition at line 1098 of file ieee_float.cpp.
References ieee_float_spect::e, ieee_float_spect::f, spec, unpack(), and ieee_float_spect::width().
void ieee_floatt::from_integer | ( | const mp_integer & | i | ) |
Definition at line 508 of file ieee_float.cpp.
References align(), exponent, ieee_float_spect::f, fraction, infinity_flag, NaN_flag, sign_flag, and spec.
Referenced by goto_checkt::conversion_check(), java_bytecode_convert_methodt::convert_instructions(), interpretert::evaluate(), from_integer(), operator==(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_typecast(), and boolbvt::type_conversion().
|
inline |
Definition at line 230 of file ieee_float.h.
References exponent.
Referenced by float_utilst::build_constant().
|
inline |
Definition at line 231 of file ieee_float.h.
References fraction.
Referenced by float_utilst::build_constant().
|
inline |
Definition at line 225 of file ieee_float.h.
References sign_flag.
Referenced by float_utilst::build_constant(), smt2_convt::convert_constant(), decrement(), increment(), next_representable(), operator+=(), and simplify_exprt::simplify_sign().
bool ieee_floatt::ieee_equal | ( | const ieee_floatt & | other | ) | const |
Definition at line 1000 of file ieee_float.cpp.
References is_zero(), NaN_flag, and spec.
Referenced by simplify_exprt::simplify_ieee_float_relation().
bool ieee_floatt::ieee_not_equal | ( | const ieee_floatt & | other | ) | const |
Definition at line 1022 of file ieee_float.cpp.
References is_zero(), NaN_flag, and spec.
Referenced by simplify_exprt::simplify_ieee_float_relation().
|
inline |
Definition at line 204 of file ieee_float.h.
References get_sign(), is_zero(), negate(), and next_representable().
Referenced by interval_domaint::assume_rec().
bool ieee_floatt::is_double | ( | ) | const |
Definition at line 1153 of file ieee_float.cpp.
References ieee_float_spect::e, ieee_float_spect::f, and spec.
bool ieee_floatt::is_float | ( | ) | const |
Definition at line 1158 of file ieee_float.cpp.
References ieee_float_spect::e, ieee_float_spect::f, and spec.
|
inline |
Definition at line 227 of file ieee_float.h.
References infinity_flag, and NaN_flag.
Referenced by float_utilst::build_constant(), goto_program2codet::cleanup_expr(), smt2_convt::convert_constant(), extract_base10(), extract_base2(), next_representable(), and simplify_exprt::simplify_isinf().
|
inline |
Definition at line 226 of file ieee_float.h.
References NaN_flag.
Referenced by float_utilst::build_constant(), goto_program2codet::cleanup_expr(), smt2_convt::convert_constant(), extract_base10(), extract_base2(), next_representable(), and simplify_exprt::simplify_isnan().
bool ieee_floatt::is_normal | ( | ) | const |
Definition at line 362 of file ieee_float.cpp.
References ieee_float_spect::f, fraction, power(), and spec.
Referenced by pack(), and simplify_exprt::simplify_isnormal().
|
inline |
Definition at line 221 of file ieee_float.h.
References exponent, fraction, infinity_flag, and NaN_flag.
Referenced by decrement(), extract_base10(), extract_base2(), ieee_equal(), ieee_not_equal(), increment(), next_representable(), operator*=(), operator+=(), operator/=(), operator<(), operator<=(), to_integer(), to_string_decimal(), and to_string_scientific().
void ieee_floatt::make_fltmax | ( | ) |
Definition at line 1126 of file ieee_float.cpp.
References ieee_float_spect::e, ieee_float_spect::f, power(), spec, and unpack().
Referenced by align(), fltmax(), and next_representable().
void ieee_floatt::make_fltmin | ( | ) |
Definition at line 1133 of file ieee_float.cpp.
References ieee_float_spect::f, power(), spec, and unpack().
Referenced by fltmin().
void ieee_floatt::make_minus_infinity | ( | ) |
Definition at line 1147 of file ieee_float.cpp.
References make_plus_infinity(), and sign_flag.
Referenced by minus_infinity().
void ieee_floatt::make_NaN | ( | ) |
Definition at line 1117 of file ieee_float.cpp.
References exponent, fraction, infinity_flag, and NaN_flag.
Referenced by NaN(), operator*=(), operator+=(), operator/=(), and unpack().
void ieee_floatt::make_plus_infinity | ( | ) |
Definition at line 1138 of file ieee_float.cpp.
References exponent, fraction, infinity_flag, NaN_flag, and sign_flag.
Referenced by make_minus_infinity(), and plus_infinity().
|
inline |
Definition at line 164 of file ieee_float.h.
References exponent, fraction, infinity_flag, NaN_flag, and sign_flag.
Referenced by operator/=(), and zero().
|
inlinestatic |
Definition at line 192 of file ieee_float.h.
References make_minus_infinity().
Referenced by goto_checkt::nan_check(), and smt2_convt::parse_literal().
|
inlinestatic |
Definition at line 186 of file ieee_float.h.
References make_NaN().
Referenced by java_bytecode_convert_methodt::convert_instructions(), and smt2_convt::parse_literal().
|
inline |
Definition at line 156 of file ieee_float.h.
References sign_flag.
Referenced by decrement(), increment(), exprt::negate(), operator*=(), operator/=(), and simplify_exprt::simplify_unary_minus().
|
protected |
Sets *this to the next representable number closer to plus infinity (greater = true) or minus infinity (greater = false).
Definition at line 1228 of file ieee_float.cpp.
References get_sign(), is_infinity(), is_NaN(), is_zero(), make_fltmax(), pack(), set_sign(), and unpack().
Referenced by decrement(), and increment().
bool ieee_floatt::operator!= | ( | const ieee_floatt & | other | ) | const |
Definition at line 1017 of file ieee_float.cpp.
ieee_floatt & ieee_floatt::operator*= | ( | const ieee_floatt & | other | ) |
Definition at line 767 of file ieee_float.cpp.
References align(), exponent, ieee_float_spect::f, fraction, infinity_flag, is_zero(), make_NaN(), NaN_flag, negate(), sign_flag, and spec.
ieee_floatt & ieee_floatt::operator+= | ( | const ieee_floatt & | other | ) |
Definition at line 803 of file ieee_float.cpp.
References align(), exponent, fraction, get_sign(), infinity_flag, is_zero(), make_NaN(), NaN_flag, power(), ROUND_TO_MINUS_INF, rounding_mode, set_sign(), sign_flag, and spec.
ieee_floatt & ieee_floatt::operator-= | ( | const ieee_floatt & | other | ) |
Definition at line 892 of file ieee_float.cpp.
References sign_flag.
ieee_floatt & ieee_floatt::operator/= | ( | const ieee_floatt & | other | ) |
Definition at line 693 of file ieee_float.cpp.
References align(), exponent, ieee_float_spect::f, fraction, infinity_flag, is_zero(), make_NaN(), make_zero(), NaN_flag, negate(), power(), sign_flag, and spec.
bool ieee_floatt::operator< | ( | const ieee_floatt & | other | ) | const |
Definition at line 899 of file ieee_float.cpp.
References exponent, fraction, infinity_flag, is_zero(), NaN_flag, and sign_flag.
bool ieee_floatt::operator<= | ( | const ieee_floatt & | other | ) | const |
Definition at line 945 of file ieee_float.cpp.
References exponent, fraction, infinity_flag, is_zero(), NaN_flag, and sign_flag.
bool ieee_floatt::operator== | ( | const ieee_floatt & | other | ) | const |
Definition at line 978 of file ieee_float.cpp.
References exponent, fraction, infinity_flag, NaN_flag, and sign_flag.
bool ieee_floatt::operator== | ( | int | i | ) | const |
Definition at line 1010 of file ieee_float.cpp.
References from_integer(), and spec.
bool ieee_floatt::operator> | ( | const ieee_floatt & | other | ) | const |
Definition at line 968 of file ieee_float.cpp.
bool ieee_floatt::operator>= | ( | const ieee_floatt & | other | ) | const |
Definition at line 973 of file ieee_float.cpp.
mp_integer ieee_floatt::pack | ( | ) | const |
Definition at line 367 of file ieee_float.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, exponent, ieee_float_spect::f, fraction, infinity_flag, is_normal(), ieee_float_spect::max_exponent(), NaN_flag, power(), sign_flag, and spec.
Referenced by smt2_convt::convert_constant(), convert_float_literal(), smt2_convt::convert_typecast(), interpretert::evaluate(), next_representable(), to_double(), to_expr(), and to_float().
|
inlinestatic |
Definition at line 189 of file ieee_float.h.
References make_plus_infinity().
Referenced by c_typecheck_baset::do_special_functions(), goto_checkt::nan_check(), and smt2_convt::parse_literal().
void ieee_floatt::print | ( | std::ostream & | out | ) | const |
Definition at line 58 of file ieee_float.cpp.
References to_ansi_c_string().
|
inline |
Definition at line 161 of file ieee_float.h.
References sign_flag.
Referenced by next_representable(), operator+=(), and simplify_exprt::simplify_abs().
|
inline |
Definition at line 258 of file ieee_float.h.
References format().
Referenced by expr2ct::convert_constant(), operator<<(), print(), and xml().
double ieee_floatt::to_double | ( | ) | const |
Note that calling from_double -> to_double can return different bit patterns for NaN.
Definition at line 1165 of file ieee_float.cpp.
References infinity_flag, NaN_flag, pack(), and sign_flag.
constant_exprt ieee_floatt::to_expr | ( | ) | const |
Definition at line 686 of file ieee_float.cpp.
References integer2binary(), pack(), constant_exprt::set_value(), spec, ieee_float_spect::to_type(), and ieee_float_spect::width().
Referenced by goto_checkt::conversion_check(), java_bytecode_convert_methodt::convert_instructions(), c_typecheck_baset::do_special_functions(), from_integer(), exprt::mul(), goto_checkt::nan_check(), exprt::negate(), smt2_convt::parse_literal(), java_bytecode_parsert::rconstant_pool(), simplify_exprt::simplify_abs(), simplify_exprt::simplify_floatbv_op(), simplify_exprt::simplify_floatbv_typecast(), simplify_exprt::simplify_inequality_constant(), simplify_exprt::simplify_typecast(), simplify_exprt::simplify_unary_minus(), exprt::sum(), and boolbvt::type_conversion().
float ieee_floatt::to_float | ( | ) | const |
Note that calling from_float -> to_float can return different bit patterns for NaN.
Definition at line 1194 of file ieee_float.cpp.
References infinity_flag, NaN_flag, pack(), and sign_flag.
mp_integer ieee_floatt::to_integer | ( | ) | const |
Definition at line 1057 of file ieee_float.cpp.
References exponent, ieee_float_spect::f, fraction, infinity_flag, is_zero(), NaN_flag, power(), sign_flag, and spec.
Referenced by simplify_exprt::simplify_floatbv_typecast(), and simplify_exprt::simplify_typecast().
std::string ieee_floatt::to_string_decimal | ( | std::size_t | precision | ) | const |
Definition at line 132 of file ieee_float.cpp.
References dot(), extract_base2(), infinity_flag, integer2size_t(), integer2string(), is_zero(), NaN_flag, power(), r, and sign_flag.
Referenced by format().
std::string ieee_floatt::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.
Definition at line 225 of file ieee_float.cpp.
References base10_digits(), extract_base10(), infinity_flag, integer2string(), is_zero(), NaN_flag, power(), and sign_flag.
Referenced by format().
void ieee_floatt::unpack | ( | const mp_integer & | i | ) |
Definition at line 312 of file ieee_float.cpp.
References ieee_float_spect::bias(), ieee_float_spect::e, exponent, ieee_float_spect::f, fraction, infinity_flag, make_NaN(), ieee_float_spect::max_exponent(), NaN_flag, power(), sign_flag, and spec.
Referenced by bv_refinementt::check_SAT(), interpretert::evaluate(), from_double(), from_expr(), from_float(), float_utilst::get(), make_fltmax(), make_fltmin(), next_representable(), and java_bytecode_parsert::rconstant_pool().
|
inlinestatic |
Definition at line 173 of file ieee_float.h.
References make_zero().
|
protected |
Definition at line 299 of file ieee_float.h.
Referenced by align(), build(), change_spec(), extract_base10(), extract_base2(), from_base10(), from_integer(), get_exponent(), is_zero(), make_NaN(), make_plus_infinity(), make_zero(), operator*=(), operator+=(), operator/=(), operator<(), operator<=(), operator==(), pack(), to_integer(), and unpack().
|
protected |
Definition at line 300 of file ieee_float.h.
Referenced by align(), build(), change_spec(), divide_and_round(), extract_base10(), extract_base2(), from_base10(), from_integer(), get_fraction(), is_normal(), is_zero(), make_NaN(), make_plus_infinity(), make_zero(), operator*=(), operator+=(), operator/=(), operator<(), operator<=(), operator==(), pack(), to_integer(), and unpack().
|
protected |
Definition at line 301 of file ieee_float.h.
Referenced by align(), from_base10(), from_integer(), is_infinity(), is_zero(), make_NaN(), make_plus_infinity(), make_zero(), operator*=(), operator+=(), operator/=(), operator<(), operator<=(), operator==(), pack(), to_double(), to_float(), to_integer(), to_string_decimal(), to_string_scientific(), and unpack().
|
protected |
Definition at line 301 of file ieee_float.h.
Referenced by align(), from_base10(), from_integer(), ieee_equal(), ieee_not_equal(), is_infinity(), is_NaN(), is_zero(), make_NaN(), make_plus_infinity(), make_zero(), operator*=(), operator+=(), operator/=(), operator<(), operator<=(), operator==(), pack(), to_double(), to_float(), to_integer(), to_string_decimal(), to_string_scientific(), and unpack().
rounding_modet ieee_floatt::rounding_mode |
Definition at line 121 of file ieee_float.h.
Referenced by align(), bv_refinementt::check_SAT(), divide_and_round(), operator+=(), simplify_exprt::simplify_floatbv_op(), and simplify_exprt::simplify_floatbv_typecast().
|
protected |
Definition at line 298 of file ieee_float.h.
Referenced by align(), build(), change_spec(), divide_and_round(), from_base10(), from_integer(), get_sign(), make_minus_infinity(), make_plus_infinity(), make_zero(), negate(), operator*=(), operator+=(), operator-=(), operator/=(), operator<(), operator<=(), operator==(), pack(), set_sign(), to_double(), to_float(), to_integer(), to_string_decimal(), to_string_scientific(), and unpack().
ieee_float_spect ieee_floatt::spec |
Definition at line 123 of file ieee_float.h.
Referenced by align(), build(), change_spec(), smt2_convt::convert_constant(), convert_float_literal(), smt2_convt::convert_typecast(), extract_base10(), extract_base2(), from_base10(), from_double(), from_expr(), from_float(), from_integer(), float_utilst::get(), ieee_equal(), ieee_not_equal(), is_double(), is_float(), is_normal(), make_fltmax(), make_fltmin(), operator*=(), operator+=(), operator/=(), operator==(), pack(), simplify_exprt::simplify_typecast(), to_expr(), to_integer(), and unpack().