cprover
|
#include <float_utils.h>
Classes | |
struct | biased_floatt |
struct | rounding_mode_bitst |
struct | unbiased_floatt |
struct | unpacked_floatt |
Public Types | |
enum class | relt { LT , LE , EQ , GT , GE } |
Public Member Functions | |
float_utilst (propt &_prop) | |
float_utilst (propt &_prop, const floatbv_typet &type) | |
void | set_rounding_mode (const bvt &) |
virtual | ~float_utilst () |
bvt | build_constant (const ieee_float_valuet &) |
bvt | get_exponent (const bvt &) |
Gets the unbiased exponent in a floating-point bit-vector. | |
bvt | get_fraction (const bvt &) |
Gets the fraction without hidden bit in a floating-point bit-vector src. | |
literalt | is_normal (const bvt &) |
literalt | is_zero (const bvt &) |
literalt | is_infinity (const bvt &) |
literalt | is_plus_inf (const bvt &) |
literalt | is_minus_inf (const bvt &) |
literalt | is_NaN (const bvt &) |
virtual bvt | add_sub (const bvt &src1, const bvt &src2, bool subtract) |
bvt | add (const bvt &src1, const bvt &src2) |
bvt | sub (const bvt &src1, const bvt &src2) |
virtual bvt | mul (const bvt &src1, const bvt &src2) |
virtual bvt | div (const bvt &src1, const bvt &src2) |
virtual bvt | rem (const bvt &src1, const bvt &src2) |
bvt | abs (const bvt &) |
bvt | negate (const bvt &) |
bvt | from_unsigned_integer (const bvt &) |
bvt | from_signed_integer (const bvt &) |
bvt | to_integer (const bvt &src, std::size_t int_width, bool is_signed) |
bvt | to_signed_integer (const bvt &src, std::size_t int_width) |
bvt | to_unsigned_integer (const bvt &src, std::size_t int_width) |
bvt | conversion (const bvt &src, const ieee_float_spect &dest_spec) |
bvt | round_to_integral (const bvt &) |
literalt | relation (const bvt &src1, relt rel, const bvt &src2) |
ieee_float_valuet | get (const bvt &) const |
literalt | exponent_all_ones (const bvt &) |
literalt | exponent_all_zeros (const bvt &) |
literalt | fraction_all_zeros (const bvt &) |
bvt | debug1 (const bvt &op0, const bvt &op1) |
bvt | debug2 (const bvt &op0, const bvt &op1) |
Static Public Member Functions | |
static literalt | sign_bit (const bvt &src) |
Public Attributes | |
rounding_mode_bitst | rounding_mode_bits |
ieee_float_spect | spec |
Protected Member Functions | |
virtual void | normalization_shift (bvt &fraction, bvt &exponent) |
normalize fraction/exponent pair returns 'zero' if fraction is zero | |
void | denormalization_shift (bvt &fraction, bvt &exponent) |
make sure exponent is not too small; the exponent is unbiased | |
bvt | add_bias (const bvt &exponent) |
bvt | sub_bias (const bvt &exponent) |
bvt | limit_distance (const bvt &dist, mp_integer limit) |
Limits the shift distance. | |
unbiased_floatt | unpack (const bvt &) |
biased_floatt | bias (const unbiased_floatt &) |
takes an unbiased float, and applies the bias | |
unbiased_floatt | rounder (const unbiased_floatt &) |
bvt | round_and_pack (const unbiased_floatt &) |
bvt | pack (const biased_floatt &) |
void | round_fraction (unbiased_floatt &result) |
void | round_exponent (unbiased_floatt &result) |
literalt | fraction_rounding_decision (const std::size_t dest_bits, const literalt sign, const bvt &fraction) |
rounding decision for fraction using sticky bit | |
bvt | subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2) |
Subtracts the exponents. | |
bvt | sticky_right_shift (const bvt &op, const bvt &dist, literalt &sticky) |
Protected Attributes | |
propt & | prop |
bv_utilst | bv_utils |
Definition at line 17 of file float_utils.h.
|
strong |
Enumerator | |
---|---|
LT | |
LE | |
EQ | |
GT | |
GE |
Definition at line 145 of file float_utils.h.
|
inlineexplicit |
Definition at line 75 of file float_utils.h.
|
inline |
Definition at line 81 of file float_utils.h.
|
inlinevirtual |
Definition at line 90 of file float_utils.h.
Definition at line 603 of file float_utils.cpp.
Definition at line 117 of file float_utils.h.
Definition at line 1237 of file float_utils.cpp.
Definition at line 280 of file float_utils.cpp.
|
protected |
takes an unbiased float, and applies the bias
Definition at line 1207 of file float_utils.cpp.
bvt float_utilst::build_constant | ( | const ieee_float_valuet & | src | ) |
Definition at line 142 of file float_utils.cpp.
bvt float_utilst::conversion | ( | const bvt & | src, |
const ieee_float_spect & | dest_spec ) |
Definition at line 185 of file float_utils.cpp.
Definition at line 1364 of file float_utils.cpp.
Definition at line 1371 of file float_utils.cpp.
make sure exponent is not too small; the exponent is unbiased
Definition at line 869 of file float_utils.cpp.
Definition at line 497 of file float_utils.cpp.
Definition at line 744 of file float_utils.cpp.
Definition at line 757 of file float_utils.cpp.
Definition at line 770 of file float_utils.cpp.
|
protected |
rounding decision for fraction using sticky bit
Definition at line 981 of file float_utils.cpp.
Definition at line 35 of file float_utils.cpp.
Definition at line 53 of file float_utils.cpp.
ieee_float_valuet float_utilst::get | ( | const bvt & | src | ) | const |
Definition at line 1315 of file float_utils.cpp.
Gets the unbiased exponent in a floating-point bit-vector.
Definition at line 718 of file float_utils.cpp.
Gets the fraction without hidden bit in a floating-point bit-vector src.
Definition at line 724 of file float_utils.cpp.
Definition at line 710 of file float_utils.cpp.
Definition at line 729 of file float_utils.cpp.
Definition at line 738 of file float_utils.cpp.
Definition at line 256 of file float_utils.cpp.
Definition at line 701 of file float_utils.cpp.
Definition at line 692 of file float_utils.cpp.
|
protected |
Limits the shift distance.
Definition at line 422 of file float_utils.cpp.
Definition at line 445 of file float_utils.cpp.
Definition at line 594 of file float_utils.cpp.
normalize fraction/exponent pair returns 'zero' if fraction is zero
Reimplemented in float_approximationt.
Definition at line 780 of file float_utils.cpp.
|
protected |
Definition at line 1284 of file float_utils.cpp.
Definition at line 611 of file float_utils.cpp.
Definition at line 576 of file float_utils.cpp.
|
protected |
Definition at line 975 of file float_utils.cpp.
|
protected |
Definition at line 1144 of file float_utils.cpp.
|
protected |
Definition at line 1045 of file float_utils.cpp.
Definition at line 155 of file float_utils.cpp.
|
protected |
Definition at line 937 of file float_utils.cpp.
void float_utilst::set_rounding_mode | ( | const bvt & | src | ) |
Definition at line 15 of file float_utils.cpp.
Definition at line 98 of file float_utils.h.
|
protected |
Definition at line 1329 of file float_utils.cpp.
Definition at line 122 of file float_utils.h.
Definition at line 1246 of file float_utils.cpp.
|
protected |
Subtracts the exponents.
Definition at line 264 of file float_utils.cpp.
Definition at line 84 of file float_utils.cpp.
Definition at line 70 of file float_utils.cpp.
Definition at line 77 of file float_utils.cpp.
|
protected |
Definition at line 1255 of file float_utils.cpp.
|
protected |
Definition at line 162 of file float_utils.h.
|
protected |
Definition at line 161 of file float_utils.h.
rounding_mode_bitst float_utilst::rounding_mode_bits |
Definition at line 73 of file float_utils.h.
ieee_float_spect float_utilst::spec |
Definition at line 94 of file float_utils.h.