340 const exprt &float_expr)
358 exprt bin_significand_int =
369 exprt dec_exponent_estimate =
373 std::vector<double> two_power_e_over_ten_power_d_table(
374 {1, 2, 4, 8, 1.6, 3.2, 6.4, 1.28,
375 2.56, 5.12, 1.024, 2.048, 4.096, 8.192, 1.6384, 3.2768,
376 6.5536, 1.31072, 2.62144, 5.24288, 1.04858, 2.09715, 4.19430, 8.38861,
377 1.67772, 3.35544, 6.71089, 1.34218, 2.68435, 5.36871, 1.07374, 2.14748,
378 4.29497, 8.58993, 1.71799, 3.43597, 6.87195, 1.37439, 2.74878, 5.49756,
379 1.09951, 2.19902, 4.39805, 8.79609, 1.75922, 3.51844, 7.03687, 1.40737,
380 2.81475, 5.62950, 1.12590, 2.25180, 4.50360, 9.00720, 1.80144, 3.60288,
381 7.20576, 1.44115, 2.88230, 5.76461, 1.15292, 2.30584, 4.61169, 9.22337,
382 1.84467, 3.68935, 7.37870, 1.47574, 2.95148, 5.90296, 1.18059, 2.36118,
383 4.72237, 9.44473, 1.88895, 3.77789, 7.55579, 1.51116, 3.02231, 6.04463,
384 1.20893, 2.41785, 4.83570, 9.67141, 1.93428, 3.86856, 7.73713, 1.54743,
385 3.09485, 6.18970, 1.23794, 2.47588, 4.95176, 9.90352, 1.98070, 3.96141,
386 7.92282, 1.58456, 3.16913, 6.33825, 1.26765, 2.53530, 5.07060, 1.01412,
387 2.02824, 4.05648, 8.11296, 1.62259, 3.24519, 6.49037, 1.29807, 2.59615,
388 5.1923, 1.03846, 2.07692, 4.15384, 8.30767, 1.66153, 3.32307, 6.64614,
389 1.32923, 2.65846, 5.31691, 1.06338, 2.12676, 4.25353, 8.50706, 1.70141});
392 std::vector<double> two_power_e_over_ten_power_d_table_negatives(
393 {2.93874, 5.87747, 1.17549, 2.35099, 4.70198, 9.40395, 1.88079, 3.76158,
394 7.52316, 1.50463, 3.00927, 6.01853, 1.20371, 2.40741, 4.81482, 9.62965,
395 1.92593, 3.85186, 7.70372, 1.54074, 3.08149, 6.16298, 1.23260, 2.46519,
396 4.93038, 9.86076, 1.97215, 3.94430, 7.88861, 1.57772, 3.15544, 6.31089,
397 1.26218, 2.52435, 5.04871, 1.00974, 2.01948, 4.03897, 8.07794, 1.61559,
398 3.23117, 6.46235, 1.29247, 2.58494, 5.16988, 1.03398, 2.06795, 4.13590,
399 8.27181, 1.65436, 3.30872, 6.61744, 1.32349, 2.64698, 5.29396, 1.05879,
400 2.11758, 4.23516, 8.47033, 1.69407, 3.38813, 6.77626, 1.35525, 2.71051,
401 5.42101, 1.08420, 2.16840, 4.33681, 8.67362, 1.73472, 3.46945, 6.93889,
402 1.38778, 2.77556, 5.55112, 1.11022, 2.22045, 4.44089, 8.88178, 1.77636,
403 3.55271, 7.10543, 1.42109, 2.84217, 5.68434, 1.13687, 2.27374, 4.54747,
404 9.09495, 1.81899, 3.63798, 7.27596, 1.45519, 2.91038, 5.82077, 1.16415,
405 2.32831, 4.65661, 9.31323, 1.86265, 3.72529, 7.45058, 1.49012, 2.98023,
406 5.96046, 1.19209, 2.38419, 4.76837, 9.53674, 1.90735, 3.81470, 7.62939,
407 1.52588, 3.05176, 6.10352, 1.22070, 2.44141, 4.88281, 9.76563, 1.95313,
408 3.90625, 7.81250, 1.56250, 3.12500, 6.25000, 1.25000, 2.50000, 5});
412 two_power_e_over_ten_power_d_table_negatives.size() +
413 two_power_e_over_ten_power_d_table.size(),
417 for(
const auto &negative : two_power_e_over_ten_power_d_table_negatives)
420 for(
const auto &positive : two_power_e_over_ten_power_d_table)
421 conversion_factor_table.copy_to_operands(
429 conversion_factor_table, shifted_index,
float_type);
438 dec_significand_int, ID_ge,
from_integer(10, int_type));
442 dec_exponent_estimate);
453 string_expr_integer_part, dec_significand_int, 3);
459 exprt shifted_float =
468 shifted_float, max_non_exponent_notation);
473 string_fractional_part, fractional_part_shifted, 6);
480 string_expr_with_fractional_part,
481 string_expr_integer_part,
482 string_fractional_part);
491 string_expr_with_E, string_expr_with_fractional_part, stringE);
511 maximum(result5.first,
maximum(result6.first, result7.first))))));
512 merge(result7.second, std::move(result1.second));
513 merge(result7.second, std::move(result2.second));
514 merge(result7.second, std::move(result3.second));
515 merge(result7.second, std::move(result4.second));
516 merge(result7.second, std::move(result5.second));
517 merge(result7.second, std::move(result6.second));
518 return {return_code, std::move(result7.second)};