CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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_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)
 

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
 
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
 
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)
 

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

typedef float_utilst float_approximationt::SUB
private

Definition at line 38 of file float_approximation.h.

Constructor & Destructor Documentation

◆ float_approximationt()

float_approximationt::float_approximationt ( propt &  _prop)
inlineexplicit

Definition at line 20 of file float_approximation.h.

◆ ~float_approximationt()

float_approximationt::~float_approximationt ( )
virtual

Definition at line 11 of file float_approximation.cpp.

Member Function Documentation

◆ normalization_shift()

void float_approximationt::normalization_shift ( bvt &  fraction,
bvt &  exponent 
)
protectedvirtual

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()

bvt float_approximationt::overapproximating_left_shift ( const bvt &  src,
unsigned  dist 
)
protected

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: