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