37 std::pair<exprt, string_constraintst>
82 strings_differ_at_witness);
86 return {isprefix, std::move(constraints)};
104 std::pair<exprt, string_constraintst>
127 DEPRECATED(
SINCE(2017, 10, 5,
"should use `string_length s == 0` instead"))
190 array_pool.get_or_create_length(
s1),
191 array_pool.get_or_create_length(s0)));
198 array_pool.get_or_create_length(
s1),
199 array_pool.get_or_create_length(s0)));
210 array_pool.get_or_create_length(
s1),
211 array_pool.get_or_create_length(s0)));
215 array_pool.get_or_create_length(s0),
216 array_pool.get_or_create_length(
s1)),
221 greater_than(array_pool.get_or_create_length(s0), witness),
226 return {tc_issuffix, std::move(constraints)};
247 std::pair<exprt, string_constraintst>
279 const plus_exprt qvar_shifted(qvar, startpos);
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
bitvector_typet index_type()
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
const typet & length_type() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
typet & type()
Return the type of the expression.
std::size_t size() const
Amount of nodes this expression tree contains.
Application of (mathematical) function.
exprt::operandst argumentst
const irep_idt & id() const
The plus expression Associativity is not specified.
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
symbol_generatort fresh_symbol
Expression to hold a symbol (variable)
Semantic type conversion.
The type of an expression, extends irept.
#define SINCE(year, month, day, msg)
bool is_empty(const std::string &s)
#define PRECONDITION(CONDITION)
Generates string constraints to link results from string functions with their arguments.
exprt is_positive(const exprt &x)
exprt maximum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
equal_exprt equal_to(exprt lhs, exprt rhs)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.