Public Member Functions |
Public Attributes |
Protected Member Functions |
Private Types |
List of all members
float_approximationt Class Reference
#include <float_approximation.h>
Inheritance diagram for float_approximationt: Collaboration diagram for float_approximationt:Public Member Functions | |
| float_approximationt (propt &_prop) | |
| virtual | ~float_approximationt () |
| Public Member Functions inherited from float_utilst | |
| 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_floatt &) |
| bvt | get_exponent (const bvt &) |
| Gets the unbiased exponent in a floating-point bit-vector. More... | |
| bvt | get_fraction (const bvt &) |
| Gets the fraction without hidden bit in a floating-point bit-vector src. More... | |
| 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) |
| literalt | relation (const bvt &src1, relt rel, const bvt &src2) |
| ieee_floatt | 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) |
Public Attributes | |
| bool | over_approximate |
| bool | partial_interpretation |
| Public Attributes inherited from float_utilst | |
| 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 More... | |
| bvt | overapproximating_left_shift (const bvt &src, unsigned dist) |
| Protected Member Functions inherited from float_utilst | |
| void | denormalization_shift (bvt &fraction, bvt &exponent) |
| make sure exponent is not too small; the exponent is unbiased More... | |
| 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. More... | |
| biased_floatt | bias (const unbiased_floatt &) |
| takes an unbiased float, and applies the bias More... | |
| virtual bvt | rounder (const unbiased_floatt &) |
| bvt | pack (const biased_floatt &) |
| unbiased_floatt | unpack (const bvt &) |
| 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 More... | |
| bvt | subtract_exponents (const unbiased_floatt &src1, const unbiased_floatt &src2) |
| Subtracts the exponents. More... | |
| bvt | sticky_right_shift (const bvt &op, const bvt &dist, literalt &sticky) |
Private Types | |
| typedef float_utilst | SUB |
Additional Inherited Members | |
| Public Types inherited from float_utilst | |
| enum class | relt { LT , LE , EQ , GT , GE } |
| Static Public Member Functions inherited from float_utilst | |
| static literalt | sign_bit (const bvt &src) |
| Protected Attributes inherited from float_utilst | |
| propt & | prop |
| bv_utilst | bv_utils |
Detailed Description
Definition at line 17 of file float_approximation.h.
Member Typedef Documentation
◆ SUB
|
private |
Definition at line 38 of file float_approximation.h.
Constructor & Destructor Documentation
◆ float_approximationt()
|
inlineexplicit |
Definition at line 20 of file float_approximation.h.
◆ ~float_approximationt()
|
virtual |
Definition at line 11 of file float_approximation.cpp.
Member Function Documentation
◆ normalization_shift()
normalize fraction/exponent pair returns 'zero' if fraction is zero
Reimplemented from float_utilst.
Definition at line 15 of file float_approximation.cpp.
◆ overapproximating_left_shift()
Definition at line 66 of file float_approximation.cpp.
Member Data Documentation
◆ over_approximate
| bool float_approximationt::over_approximate |
Definition at line 29 of file float_approximation.h.
◆ partial_interpretation
| bool float_approximationt::partial_interpretation |
Definition at line 30 of file float_approximation.h.
The documentation for this class was generated from the following files:
- /home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_approximation.h
- /home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_approximation.cpp
