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);
202 const mod_exprt fractional_part(shifted, max_non_exponent_notation);
205 const exprt return_code1 =
216 const exprt return_code2 =
231 const exprt &int_expr,
259 digit_constraints.push_back(starts_with_dot);
262 for(
size_t j=1; j<max_size; j++)
287 digit_constraints.push_back(no_trailing_zero);
334 exprt bin_significand_int=
348 std::vector<double> two_power_e_over_ten_power_d_table(
349 { 1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28, 2.56,
350 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768, 6.5536,
351 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861, 1.67772,
352 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748, 4.29497,
353 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756, 1.09951,
354 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737, 2.81475,
355 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288, 7.20576,
356 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337, 1.84467,
357 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118, 4.72237,
358 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463, 1.20893,
359 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743, 3.09485,
360 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141, 7.92282,
361 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412, 2.02824,
362 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615, 5.1923,
363 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614, 1.32923,
364 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
367 std::vector<double> two_power_e_over_ten_power_d_table_negatives(
368 { 2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
369 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
370 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
371 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
372 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
373 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
374 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
375 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
376 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
377 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
378 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
379 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
380 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
381 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
382 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
383 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
387 two_power_e_over_ten_power_d_table_negatives.size()+
388 two_power_e_over_ten_power_d_table.size(),
392 for(
const auto &f : two_power_e_over_ten_power_d_table_negatives)
393 conversion_factor_table.copy_to_operands(
constant_float(f, float_spec));
394 for(
const auto &f : two_power_e_over_ten_power_d_table)
395 conversion_factor_table.copy_to_operands(
constant_float(f, float_spec));
402 conversion_factor_table, shifted_index,
float_type);
411 dec_significand_int, ID_ge,
from_integer(10, int_type));
415 dec_exponent_estimate);
442 shifted_float, max_non_exponent_notation);
447 string_fractional_part, fractional_part_shifted, 6);
454 string_expr_with_fractional_part,
455 string_expr_integer_part,
456 string_fractional_part);
464 string_expr_with_E, string_expr_with_fractional_part, stringE);
469 const exprt return_code6 =
The type of an expression.
Fixed-width bit-vector with unsigned binary interpretation.
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 generic base class for relations, i.e., binary predicates.
application of (mathematical) function
constant_exprt to_expr() const
exprt add_axioms_from_int(const function_application_exprt &f)
Convert an integer to a string.
Fixed-width bit-vector with IEEE floating-point interpretation.
void copy_to_operands(const exprt &expr)
exprt constant_float(const double f, const ieee_float_spect &float_spec)
Create an expression to represent a float or double value.
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...
static ieee_float_spect double_precision()
class floatbv_typet to_type() const
exprt conjunction(const exprt::operandst &op)
exprt add_axioms_from_double(const function_application_exprt &f)
Add axioms corresponding to the String.valueOf(D) java function.
const irep_idt & id() const
exprt add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
exprt 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.
bitvector_typet float_type()
Fixed-width bit-vector with two's complement interpretation.
binary_relation_exprt axiom_for_length_le(const string_exprt &rhs) const
static ieee_float_spect single_precision()
#define PRECONDITION(CONDITION)
void from_float(const float f)
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::vector< exprt > operandst
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
exprt round_expr_to_zero(const exprt &f)
Round a float expression to an integer closer to 0.
bool is_number(const typet &type)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
semantic type conversion from/to floating-point formats
Base class for all expressions.
void from_double(const double d)
binary_relation_exprt axiom_for_length_gt(const exprt &rhs) const
exprt add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
exprt get_fraction(const exprt &src, const ieee_float_spect &spec)
Gets the fraction without hidden bit.
std::vector< exprt > lemmas
exprt add_axioms_for_fractional_part(const array_string_exprt &res, const exprt &i, size_t max_size)
Add axioms for representing the fractional part of a floating point starting with a dot...
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
bitvector_typet char_type()
exprt add_axioms_for_concat(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.
array constructor from list of elements
exprt get_exponent(const exprt &src, const ieee_float_spect &spec)
Gets the unbiased exponent in a floating-point bit-vector.