Loading...

Searching...

No Matches

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:

[フレーム]

[legend]

+ Collaboration diagram for float_approximationt:

[フレーム]

[legend]

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 fma (const bvt &multiply_lhs, const bvt &multiply_rhs, const bvt &addend)

Fused multiply-add: round(multiply_lhs * multiply_rhs + addend) with a single rounding step.

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:

/home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_approximation.h
/home/runner/work/cbmc/cbmc/src/solvers/floatbv/float_approximation.cpp