69 return if_exprt(all_zeros, fraction, with_hidden_bit);
108 mult.copy_to_operands(g);
146 if_exprt adjust_for_neg(negative_exp, dec_minus_one, dec_exp);
168 fresh_symbol, res, f.
arguments()[2], array_pool, ns);
221 const mod_exprt fractional_part(shifted, max_non_exponent_notation);
239 fresh_symbol, res, integer_part_str, fractional_part_str);
240 merge(result3.second, std::move(result1.second));
241 merge(result3.second, std::move(result2.second));
243 const auto return_code =
245 return {return_code, std::move(result3.second)};
257 const exprt &int_expr,
285 digit_constraints.push_back(starts_with_dot);
288 for(
size_t j=1; j<max_size; j++)
313 digit_constraints.push_back(no_trailing_zero);
367 exprt bin_significand_int=
381 std::vector<double> two_power_e_over_ten_power_d_table(
382 { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56,
383 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536,
384 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772,
385 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497,
386 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951,
387 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475,
388 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576,
389 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467,
390 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237,
391 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893,
392 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485,
393 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282,
394 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824,
395 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923,
396 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923,
397 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
400 std::vector<double> two_power_e_over_ten_power_d_table_negatives(
401 { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
402 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
403 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
404 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
405 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
406 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
407 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
408 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
409 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
410 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
411 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
412 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
413 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
414 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
415 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
416 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
420 two_power_e_over_ten_power_d_table_negatives.size()+
421 two_power_e_over_ten_power_d_table.size(),
425 for(
const auto &f : two_power_e_over_ten_power_d_table_negatives)
426 conversion_factor_table.copy_to_operands(
constant_float(f, float_spec));
427 for(
const auto &f : two_power_e_over_ten_power_d_table)
428 conversion_factor_table.copy_to_operands(
constant_float(f, float_spec));
435 conversion_factor_table, shifted_index,
float_type);
444 dec_significand_int, ID_ge,
from_integer(10, int_type));
448 dec_exponent_estimate);
459 string_expr_integer_part, dec_significand_int, 3, ns);
474 shifted_float, max_non_exponent_notation);
479 string_fractional_part, fractional_part_shifted, 6);
487 string_expr_with_fractional_part,
488 string_expr_integer_part,
489 string_fractional_part);
500 string_expr_with_fractional_part,
511 fresh_symbol, res, string_expr_with_E, exponent_string);
521 maximum(result5.first,
maximum(result6.first, result7.first))))));
522 merge(result7.second, std::move(result1.second));
523 merge(result7.second, std::move(result2.second));
524 merge(result7.second, std::move(result3.second));
525 merge(result7.second, std::move(result4.second));
526 merge(result7.second, std::move(result5.second));
527 merge(result7.second, std::move(result6.second));
528 return {return_code, std::move(result7.second)};
551 fresh_symbol, res, arg, array_pool, ns);
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
The type of an expression, extends irept.
Fixed-width bit-vector with unsigned binary interpretation.
Semantic type conversion.
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 po...
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Application of (mathematical) function.
constant_exprt to_expr() const
Fixed-width bit-vector with IEEE floating-point interpretation.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
exprt constant_float(const double f, const ieee_float_spect &float_spec)
Create an expression to represent a float or double value.
Generation of fresh symbols of a given type.
The trinary if-then-else operator.
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 decima...
typet & type()
Return the type of the expression.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
static ieee_float_spect double_precision()
class floatbv_typet to_type() const
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const irep_idt & id() const
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.
Fixed-width bit-vector with two's complement interpretation.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static ieee_float_spect single_precision()
#define PRECONDITION(CONDITION)
void from_float(const float f)
The plus expression Associativity is not specified.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
bitvector_typet index_type()
exprt floatbv_mult(const exprt &f, const exprt &g)
Multiplication of expressions representing floating points.
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.
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.
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
exprt maximum(const exprt &a, const exprt &b)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
std::vector< exprt > existential
floatbv_typet float_type()
exprt round_expr_to_zero(const exprt &f)
Round a float expression to an integer closer to 0.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Semantic type conversion from/to floating-point formats.
Base class for all expressions.
void from_double(const double d)
#define UNREACHABLE
This should be used to mark dead code.
exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
Gets the fraction without hidden bit.
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv, signedbv, floatbv or fixedbv.
const typet & subtype() const
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.
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
bitvector_typet char_type()
Array constructor from list of elements.
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...
exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
Gets the unbiased exponent in a floating-point bit-vector.