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