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

#include <solvers/floatbv/float_bv.h>
#include "string_constraint_generator.h"

Include dependency graph for string_constraint_generator_float.cpp:

Functions
exprt	get_exponent (const exprt &src, const ieee_float_spect &spec)
	Gets the unbiased exponent in a floating-point bit-vector. More...

exprt	get_fraction (const exprt &src, const ieee_float_spect &spec)
	Gets the fraction without hidden bit. More...

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. More...

exprt	constant_float (const double f, const ieee_float_spect &float_spec)
	Create an expression to represent a float or double value. More...

exprt	round_expr_to_zero (const exprt &f)
	Round a float expression to an integer closer to 0. More...

exprt	floatbv_mult (const exprt &f, const exprt &g)
	Multiplication of expressions representing floating points. More...

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. More...

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. More...

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 76 of file string_constraint_generator_float.cpp.

References ieee_float_spect::double_precision(), ieee_floatt::from_double(), ieee_floatt::from_float(), ieee_float_spect::single_precision(), ieee_floatt::to_expr(), and UNREACHABLE.

Referenced by string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().

◆ 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 137 of file string_constraint_generator_float.cpp.

References constant_float(), floatbv_mult(), floatbv_of_int_expr(), get_exponent(), and round_expr_to_zero().

Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation().

◆ 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 102 of file string_constraint_generator_float.cpp.

References exprt::copy_to_operands(), from_integer(), PRECONDITION, ieee_floatt::ROUND_TO_EVEN, and exprt::type().

Referenced by string_constraint_generatort::add_axioms_for_string_of_float(), string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().

◆ 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 119 of file string_constraint_generator_float.cpp.

References from_integer(), ieee_floatt::ROUND_TO_ZERO, and ieee_float_spect::to_type().

Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation(), and estimate_decimal_exponent().

◆ 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 27 of file string_constraint_generator_float.cpp.

References ieee_float_spect::bias(), ieee_float_spect::e, ieee_float_spect::f, and from_integer().

Referenced by string_constraint_generatort::add_axioms_from_float_scientific_notation(), estimate_decimal_exponent(), and get_significand().

◆ 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.

References ieee_float_spect::f.

Referenced by get_significand().

◆ 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