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";
100 constraints.existential.push_back(a1);
102 for(std::size_t i=0; i<str_true.length(); i++)
106 constraints.existential.push_back(a2);
109 std::string str_false=
"false";
111 constraints.existential.push_back(a3);
113 for(std::size_t i=0; i<str_false.length(); i++)
117 constraints.existential.push_back(a4);
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();
233 constraints.existential.push_back(
236 for(
size_t size=1; size<=max_size; size++)
242 for(
size_t j=0; j<size; j++)
258 constraints.existential.push_back(
263 constraints.existential.push_back(
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);
The type of an expression, extends irept.
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
Semantic type conversion.
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the String.valueOf(Z) java function.
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Application of (mathematical) function.
exprt simplify_expr(const exprt &src, const namespacet &ns)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
string_constraintst add_axioms_for_correct_number_format(const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
Add axioms making the return value true if the given string is a correct number in the given radix.
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Generation of fresh symbols of a given type.
The trinary if-then-else operator.
typet & type()
Return the type of the expression.
signedbv_typet get_return_code_type()
A constant literal expression.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
#define CHECK_RETURN(CONDITION)
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas,...
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const irep_idt & id() const
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
The Boolean constant true.
static unsigned long to_integer_or_default(const exprt &expr, unsigned long def, const namespacet &ns)
If the expression is a constant expression then we get the value of it as an unsigned long.
size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
Calculate the string length needed to represent any value of the given type using the given radix.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
The plus expression Associativity is not specified.
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
exprt is_digit_with_radix(const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
Check if a character is a digit with respect to the given radix, e.g.
bitvector_typet index_type()
The unary minus expression.
string_constraintst add_axioms_for_characters_in_integer_string(const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
Add axioms connecting the characters in the input string to the value of the output integer.
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
std::vector< exprt > existential
equal_exprt length_eq(const T &lhs, const exprt &rhs)
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Base class for all expressions.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
exprt get_numeric_value_from_character(const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, const unsigned long radix_ul)
Get the numeric value of a character, assuming that the radix is large enough.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Expression to hold a symbol (variable)
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
std::pair< exprt, string_constraintst > add_axioms_from_long(const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the String.valueOf(J) java function.
std::pair< exprt, string_constraintst > add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.
const typet & subtype() const
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Integer value represented by a string.
bitvector_typet char_type()