34 if(
const auto i = numeric_cast<unsigned long>(
simplify_expr(expr, ns)))
43 DEPRECATED(
SINCE(2017, 10, 5,
"use add_axioms_for_string_of_int instead"))
48 PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
50 array_pool.
find(f.arguments()[1], f.arguments()[0]);
51 if(f.arguments().size() == 4)
52 return add_axioms_for_string_of_int_with_radix(
53 res, f.arguments()[2], f.arguments()[3], 0);
55 return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
64 DEPRECATED(
SINCE(2017, 10, 5,
"Java specific, should be implemented in Java"))
81 std::string str_true =
"true";
83 eq,
equal_to(array_pool.get_or_create_length(res), str_true.length()));
86 for(std::size_t i = 0; i < str_true.length(); i++)
93 std::string str_false =
"false";
96 equal_to(array_pool.get_or_create_length(res), str_false.length()));
99 for(std::size_t i = 0; i < str_false.length(); i++)
117 std::pair<exprt, string_constraintst>
120 const exprt &input_int,
125 res, input_int, radix, max_size);
137 std::pair<exprt, string_constraintst>
140 const exprt &input_int,
144 PRECONDITION(max_size < std::numeric_limits<size_t>::max());
151 CHECK_RETURN((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
156 CHECK_RETURN(max_size < std::numeric_limits<size_t>::max());
162 const bool strict_formatting =
true;
165 res, radix_as_char, radix_ul, max_size, strict_formatting);
174 result2.existential.push_back(
conjunction(std::move(result1)));
199 DEPRECATED(
SINCE(2017, 10, 5,
"use add_axioms_for_string_of_int_with_radix"))
205 const typet &type = i.type();
222 for(
size_t size = 1; size <= max_size; size++)
228 for(
size_t j = 0; j < size; j++)
244 equal_to(array_pool.get_or_create_length(res), size);
259 std::pair<exprt, string_constraintst>
282 const exprt &radix_as_char,
283 const unsigned long radix_ul,
284 const std::size_t max_size,
285 const bool strict_formatting)
287 std::vector<exprt> conjuncts;
291 const exprt &chr = str[0];
294 const exprt starts_with_digit =
300 conjuncts.push_back(non_empty);
302 if(strict_formatting)
305 const or_exprt correct_first(starts_with_minus, starts_with_digit);
306 conjuncts.push_back(correct_first);
312 starts_with_minus, starts_with_digit, starts_with_plus);
313 conjuncts.push_back(correct_first);
318 or_exprt(starts_with_minus, starts_with_plus),
321 conjuncts.push_back(contains_digit);
330 for(std::size_t index = 1; index < max_size; ++index)
338 str[index], strict_formatting, radix_as_char, radix_ul));
339 conjuncts.push_back(character_at_index_is_digit);
342 if(strict_formatting)
351 conjuncts.push_back(no_leading_zero);
356 conjuncts.push_back(no_leading_zero_after_minus);
375 const exprt &input_int,
377 const bool strict_formatting,
379 const std::size_t max_string_length,
381 const unsigned long radix_ul)
390 str[0],
char_type, type, strict_formatting, radix_ul);
399 for(
size_t size = 2; size <= max_string_length; size++)
419 str[size - 1],
char_type, type, strict_formatting, radix_ul));
426 if(size - 1 >= max_string_length - 2 || radix_ul == 0)
435 if(no_overflow.has_value())
451 and_exprt(string_length_equals_size, starts_with_minus),
461 const typet &target_int_type)
474 PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
476 const std::size_t max_string_length =
479 return {str, radix, radix_ul, max_string_length};
489 std::pair<exprt, string_constraintst>
495 called_function == ID_cprover_string_is_valid_int_func ||
496 called_function == ID_cprover_string_is_valid_long_func);
498 called_function == ID_cprover_string_is_valid_int_func ? 32 : 64)};
503 const bool strict_formatting =
false;
511 args.max_string_length,
524 std::pair<exprt, string_constraintst>
533 const bool strict_formatting =
false;
540 args.max_string_length,
544 return {input_int, std::move(constraints2)};
557 const bool strict_formatting,
558 const exprt &radix_as_char,
559 const unsigned long radix_ul)
561 PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
565 const and_exprt is_digit_when_radix_le_10(
569 if(radix_ul <= 10 && radix_ul != 0)
571 return is_digit_when_radix_le_10;
579 const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
588 chr, ID_lt,
plus_exprt(a_char, radix_minus_ten))));
590 if(!strict_formatting)
596 chr, ID_lt,
plus_exprt(A_char, radix_minus_ten))));
603 is_digit_when_radix_le_10,
604 is_digit_when_radix_gt_10);
608 return std::move(is_digit_when_radix_gt_10);
627 const bool strict_formatting,
628 const unsigned long radix_ul)
635 chr, ID_ge, zero_char);
637 if(radix_ul <= 10 && radix_ul != 0)
642 upper_case_lower_case_or_digit,
655 if(strict_formatting)
664 upper_case_lower_case_or_digit,
679 upper_case_or_lower_case,
682 upper_case_lower_case_or_digit,
704 double radix =
static_cast<double>(radix_ul);
705 bool signed_type = type.
id() == ID_signedbv;
724 double max = signed_type
725 ? floor(
static_cast<double>(n_bits - 1) / log2(radix)) + 2.0
726 : ceil(
static_cast<double>(n_bits) / log2(radix));
727 return static_cast<size_t>(max);