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