Loading...

Searching...

No Matches

string_constraint_generator_float.cpp File Reference

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool. More...

#include "string_constraint_generator.h"
#include <util/bitvector_expr.h>
#include <util/floatbv_expr.h>
#include <util/ieee_float.h>
#include <util/mathematical_expr.h>

+ Include dependency graph for string_constraint_generator_float.cpp:

[フレーム]

Go to the source code of this file.

Functions

exprt get_exponent (const exprt &src, const ieee_float_spect &spec)

Gets the unbiased exponent in a floating-point bit-vector.

exprt get_fraction (const exprt &src, const ieee_float_spect &spec)

Gets the fraction without hidden bit.

exprt get_significand (const exprt &src, const ieee_float_spect &spec, const typet &type)

Gets the significand as a java integer, looking for the hidden bit.

exprt constant_float (const double f, const ieee_float_spect &float_spec)

Create an expression to represent a float or double value.

exprt round_expr_to_zero (const exprt &f)

Round a float expression to an integer closer to 0.

exprt floatbv_mult (const exprt &f, const exprt &g)

Multiplication of expressions representing floating points.

exprt floatbv_of_int_expr (const exprt &i, const ieee_float_spect &spec)

Convert integers to floating point to be used in operations with other values that are in floating point representation.

exprt estimate_decimal_exponent (const exprt &f, const ieee_float_spect &spec)

Estimate the decimal exponent that should be used to represent a given floating point value in decimal.

Detailed Description

Generates string constraints for functions generating strings from other types, in particular int, long, float, double, char, bool.

Definition in file string_constraint_generator_float.cpp.

Function Documentation

◆ constant_float()

exprt constant_float ( const double f,

const ieee_float_spect & float_spec

)

Create an expression to represent a float or double value.

Parameters: f a floating point value in double precision

float_spec a specification for floats

Returns: an expression representing this floating point

Definition at line 78 of file string_constraint_generator_float.cpp.

◆ estimate_decimal_exponent()

exprt estimate_decimal_exponent ( const exprt & f,

const ieee_float_spect & spec

)

Estimate the decimal exponent that should be used to represent a given floating point value in decimal.

We are looking for \(d\) such that \(n * 10^d = m * 2^e\), so: \(d = log_10(m) + log_10(2) * e - log_10(n)\) m – the fraction – should be between 1 and 2 so log_10(m) in [0,log_10(2)]. n – the fraction in base 10 – should be between 1 and 10 so log_10(n) in [0, 1]. So the estimate is given by: d ~=~ floor(log_10(2) * e)

Parameters: f a floating point expression

spec specification for floating point

Definition at line 141 of file string_constraint_generator_float.cpp.

◆ floatbv_mult()

exprt floatbv_mult ( const exprt & f,

const exprt & g

)

Multiplication of expressions representing floating points.

Note that the rounding mode is set to ROUND_TO_EVEN.

Parameters: f a floating point expression

g a floating point expression

Returns: An expression representing floating point multiplication.

Definition at line 105 of file string_constraint_generator_float.cpp.

◆ floatbv_of_int_expr()

exprt floatbv_of_int_expr ( const exprt & i,

const ieee_float_spect & spec

)

Convert integers to floating point to be used in operations with other values that are in floating point representation.

Parameters: i an expression representing an integer

spec specification for floating point numbers

Returns: An expression representing the value of the input integer as a float.

Definition at line 122 of file string_constraint_generator_float.cpp.

◆ get_exponent()

exprt get_exponent ( const exprt & src,

const ieee_float_spect & spec

)

Gets the unbiased exponent in a floating-point bit-vector.

Parameters: src a floating point expression

spec specification for floating points

Returns: A new 32 bit integer expression representing the exponent. Note that 32 bits are sufficient for the exponent even in octuple precision.

Definition at line 29 of file string_constraint_generator_float.cpp.

◆ get_fraction()

exprt get_fraction ( const exprt & src,

const ieee_float_spect & spec

)

Gets the fraction without hidden bit.

Parameters: src a floating point expression

spec specification for floating points

Returns: An unsigned value representing the fractional part.

Definition at line 44 of file string_constraint_generator_float.cpp.

◆ get_significand()

exprt get_significand ( const exprt & src,

const ieee_float_spect & spec,

const typet & type

)

Gets the significand as a java integer, looking for the hidden bit.

Since the most significant bit is 1 for normalized number, it is not part of the encoding of the significand and is 0 only if all the bits of the exponent are 0, that is why it is called the hidden bit.

Parameters: src a floating point expression

spec specification for floating points

type type of the output, should be unsigned with width greater than the width of the significand in the given spec

Returns: An integer expression of the given type representing the significand.

Definition at line 59 of file string_constraint_generator_float.cpp.

◆ round_expr_to_zero()

exprt round_expr_to_zero ( const exprt & f )

Round a float expression to an integer closer to 0.

Parameters: f expression representing a float

Returns: expression representing a 32 bit integer

Definition at line 93 of file string_constraint_generator_float.cpp.