56 constraints.existential.push_back(
length_eq(res, k));
63 constraints.universal.push_back(a2);
71 constraints.universal.push_back(a3);
104 const exprt &i = args[3];
105 const exprt j = args.size() == 5 ? args[4] : str.length();
140 constraints.existential.push_back(
144 constraints.universal.push_back([&] {
199 constraints.existential.push_back(
203 constraints.existential.push_back(a2);
206 constraints.existential.push_back(a3);
209 constraints.existential.push_back(a4);
212 constraints.existential.push_back(a5);
217 constraints.universal.push_back(a6);
220 constraints.universal.push_back([&] {
231 constraints.universal.push_back(a8);
234 constraints.existential.push_back([&] {
238 str[index_before], ID_gt, space_char);
262 if((expr1.
type().
id()==ID_unsignedbv
263 || expr1.
type().
id()==ID_char)
264 && (expr2.
type().
id()==ID_char
265 || expr2.
type().
id()==ID_unsignedbv))
266 return std::make_pair(expr1, expr2);
269 const auto expr1_length =
numeric_cast<std::size_t>(expr1_str.length());
270 const auto expr2_length =
numeric_cast<std::size_t>(expr2_str.length());
271 if(expr1_length && expr2_length && *expr1_length==1 && *expr2_length==1)
272 return std::make_pair(
exprt(expr1_str[0]),
exprt(expr2_str[0]));
308 const auto maybe_chars =
313 const auto old_char=maybe_chars->first;
314 const auto new_char=maybe_chars->second;
327 constraints.universal.push_back(a2);
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
The type of an expression, extends irept.
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
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.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Generation of fresh symbols of a given type.
typet & type()
Return the type of the expression.
signedbv_typet get_return_code_type()
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
exprt minimum(const exprt &a, const exprt &b)
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
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...
nonstd::optional< T > optionalt
exprt::operandst argumentst
#define PRECONDITION(CONDITION)
The plus expression Associativity is not specified.
bitvector_typet index_type()
exprt maximum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
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.
Universally quantified string constraint
Expression to hold a symbol (variable)
const typet & subtype() const
binary_relation_exprt length_le(const T &lhs, const exprt &rhs)
bitvector_typet char_type()