cprover
|
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... | |
std::pair< exprt, string_constraintst > | add_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
String representation of a float value. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_double (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
Add axioms corresponding to the String.valueOf(D) java function. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_string_of_float (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns) |
Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '. More... | |
std::pair< exprt, string_constraintst > | add_axioms_for_fractional_part (const array_string_exprt &res, const exprt &int_expr, size_t max_size) |
Add axioms for representing the fractional part of a floating point starting with a dot. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const array_string_exprt &res, const exprt &f, array_poolt &array_pool, const namespacet &ns) |
Add axioms to write the float in scientific notation. More... | |
std::pair< exprt, string_constraintst > | add_axioms_from_float_scientific_notation (symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns) |
Representation of a float value in scientific notation. More... | |
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.
std::pair<exprt, string_constraintst> add_axioms_for_fractional_part | ( | const array_string_exprt & | res, |
const exprt & | int_expr, | ||
size_t | max_size | ||
) |
Add axioms for representing the fractional part of a floating point starting with a dot.
res | string expression for the result |
int_expr | an integer expression |
max_size | a maximal size for the string, this includes the potential minus sign and therefore should be greater than 2 |
Definition at line 255 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_float | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Add axioms corresponding to the integer part of m, in decimal form with no leading zeroes, followed by '.
', followed by one or more decimal digits representing the fractional part of m. This specification is correct for inputs that do not exceed 100000 and the function is unspecified for other values.
fresh_symbol | generator of fresh symbols |
res | string expression corresponding to the result |
f | a float expression, which is positive |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 201 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_for_string_of_float | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
String representation of a float value.
Add axioms corresponding to the String.valueOf(F) java function
fresh_symbol | generator of fresh symbols |
f | function application with one float argument |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 158 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_double | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Add axioms corresponding to the String.valueOf(D) java function.
fresh_symbol | generator of fresh symbols |
f | function application with one double argument |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 177 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation | ( | symbol_generatort & | fresh_symbol, |
const array_string_exprt & | res, | ||
const exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Add axioms to write the float in scientific notation.
A float is represented as \(f = m * 2^e\) where \(0 <= m < 2\) is the significand and \(-126 <= e <= 127\) is the exponent. We want an alternate representation by finding \(n\) and \(d\) such that \(f=n*10^d\). We can estimate \(d\) the following way: \(d ~= log_10(f/n) ~= log_10(m) + log_10(2) * e - log_10(n)\) \(d = floor(log_10(2) * e)\) Then \(n\) can be expressed by the equation: \(log_10(n) = log_10(m) + log_10(2) * e - d\) \(n = f / 10^d = m * 2^e / 10^d = m * 2^e / 10^(floor(log_10(2) * e))\)
fresh_symbol | generator of fresh symbols |
res | string expression representing the float in scientific notation |
f | a float expression, which is positive |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 344 of file string_constraint_generator_float.cpp.
std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation | ( | symbol_generatort & | fresh_symbol, |
const function_application_exprt & | f, | ||
array_poolt & | array_pool, | ||
const namespacet & | ns | ||
) |
Representation of a float value in scientific notation.
Add axioms corresponding to the scientific representation of floating point values
fresh_symbol | generator of fresh symbols |
f | a function application expression |
array_pool | pool of arrays representing strings |
ns | namespace |
Definition at line 540 of file string_constraint_generator_float.cpp.
exprt constant_float | ( | const double | f, |
const ieee_float_spect & | float_spec | ||
) |
Create an expression to represent a float or double value.
f | a floating point value in double precision |
float_spec | a specification for floats |
Definition at line 76 of file string_constraint_generator_float.cpp.
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)
f | a floating point expression |
spec | specification for floating point |
Definition at line 137 of file string_constraint_generator_float.cpp.
Multiplication of expressions representing floating points.
Note that the rounding mode is set to ROUND_TO_EVEN.
f | a floating point expression |
g | a floating point expression |
Definition at line 102 of file string_constraint_generator_float.cpp.
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.
i | an expression representing an integer |
spec | specification for floating point numbers |
Definition at line 119 of file string_constraint_generator_float.cpp.
exprt get_exponent | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Gets the unbiased exponent in a floating-point bit-vector.
src | a floating point expression |
spec | specification for floating points |
Definition at line 27 of file string_constraint_generator_float.cpp.
exprt get_fraction | ( | const exprt & | src, |
const ieee_float_spect & | spec | ||
) |
Gets the fraction without hidden bit.
src | a floating point expression |
spec | specification for floating points |
Definition at line 44 of file string_constraint_generator_float.cpp.
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.
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 |
Definition at line 59 of file string_constraint_generator_float.cpp.
Round a float expression to an integer closer to 0.
f | expression representing a float |
Definition at line 91 of file string_constraint_generator_float.cpp.