#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:

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

Public Member Functions

Public Attributes

Protected Member Functions

Private Types

Additional Inherited Members