69 return if_exprt(all_zeros, fraction, with_hidden_bit);
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)
427 for(
const auto &f : two_power_e_over_ten_power_d_table)
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);