33 if(
const auto i = numeric_cast<unsigned long>(
simplify_expr(expr, ns)))
44 DEPRECATED(
"should use add_axioms_for_string_of_int instead")
50 PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
53 if(f.arguments().size() == 4)
55 res, f.arguments()[2], f.arguments()[3], 0, ns);
65 DEPRECATED(
"This is Java specific and should be implemented in Java instead")
82 DEPRECATED(
"This is Java specific and should be implemented in Java instead")
98 std::string str_true=
"true";
102 for(std::size_t i=0; i<str_true.length(); i++)
109 std::string str_false=
"false";
113 for(std::size_t i=0; i<str_false.length(); i++)
134 const exprt &input_int,
140 res, input_int, radix, max_size, ns);
155 const exprt &input_int,
160 PRECONDITION(max_size < std::numeric_limits<size_t>::max());
167 CHECK_RETURN((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
172 CHECK_RETURN(max_size<std::numeric_limits<size_t>::max());
178 const bool strict_formatting=
true;
181 res, radix_as_char, radix_ul, max_size, strict_formatting);
190 merge(result2, std::move(result1));
215 DEPRECATED(
"use add_axioms_for_string_of_int_with_radix instead")
220 const typet &type=i.type();
236 for(
size_t size=1; size<=max_size; size++)
242 for(
size_t j=0; j<size; j++)
331 const exprt &radix_as_char,
332 const unsigned long radix_ul,
333 const std::size_t max_size,
334 const bool strict_formatting)
340 const exprt &chr=str[0];
343 const exprt starts_with_digit=
350 if(strict_formatting)
353 const or_exprt correct_first(starts_with_minus, starts_with_digit);
360 starts_with_minus, starts_with_digit, starts_with_plus);
366 or_exprt(starts_with_minus, starts_with_plus),
376 for(std::size_t index=1; index<max_size; ++index)
382 str[index], strict_formatting, radix_as_char, radix_ul));
383 constraints.
existential.push_back(character_at_index_is_digit);
386 if(strict_formatting)
393 constraints.
existential.push_back(no_leading_zero);
398 constraints.
existential.push_back(no_leading_zero_after_minus);
416 const exprt &input_int,
418 const bool strict_formatting,
420 const std::size_t max_string_length,
422 const unsigned long radix_ul)
432 str[0],
char_type, type, strict_formatting, radix_ul);
440 for(
size_t size=2; size<=max_string_length; size++)
461 str[size-1],
char_type, type, strict_formatting, radix_ul));
467 if(size-1>=max_string_length-2 || radix_ul==0)
472 digit_constraints.push_back(no_overflow);
478 if(!digit_constraints.empty())
523 PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
525 const symbol_exprt input_int=fresh_symbol(
"parsed_int", type);
528 const bool strict_formatting=
false;
537 str, radix_as_char, radix_ul, max_string_length, strict_formatting);
547 merge(constraints2, std::move(constraints1));
549 return {input_int, std::move(constraints2)};
562 const bool strict_formatting,
563 const exprt &radix_as_char,
564 const unsigned long radix_ul)
566 PRECONDITION((radix_ul>=2 && radix_ul<=36) || radix_ul==0);
570 const and_exprt is_digit_when_radix_le_10(
573 chr, ID_lt,
plus_exprt(zero_char, radix_as_char)));
575 if(radix_ul<=10 && radix_ul!=0)
577 return is_digit_when_radix_le_10;
585 const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
594 chr, ID_lt,
plus_exprt(a_char, radix_minus_ten))));
596 if(!strict_formatting)
603 chr, ID_lt,
plus_exprt(A_char, radix_minus_ten))));
610 is_digit_when_radix_le_10,
611 is_digit_when_radix_gt_10);
615 return std::move(is_digit_when_radix_gt_10);
634 const bool strict_formatting,
635 const unsigned long radix_ul)
642 chr, ID_ge, zero_char);
644 if(radix_ul<=10 && radix_ul!=0)
649 upper_case_lower_case_or_digit,
662 if(strict_formatting)
671 upper_case_lower_case_or_digit,
686 upper_case_or_lower_case,
689 upper_case_lower_case_or_digit,
711 double radix=
static_cast<double>(radix_ul);
712 bool signed_type=type.
id()==ID_signedbv;
731 double max=signed_type?
732 floor(
static_cast<double>(n_bits-1)/log2(radix))+2.0:
733 ceil(
static_cast<double>(n_bits)/log2(radix));
734 return static_cast<size_t>(max);