24 const exprt &return_code,
42 const std::vector<mp_integer> &
args_value)
const
45 const auto offset = std::min(
66 const std::function<
exprt(
const exprt &)> &get_value)
const
74 const auto &insert = std::back_inserter(
arg_values);
78 if(const auto val = numeric_cast<mp_integer>(get_value(e)))
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Correspondance between arrays and pointers string representations.
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
Base class for all expressions.
typet & type()
Return the type of the expression.
The plus expression Associativity is not specified.
Base class for string functions that are built in the solver.
symbol_generatort fresh_symbol
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Constraints ensuring the result corresponds to input1 where we inserted input2 at position offset giv...
string_insertion_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
exprt length_constraint() const override
array_string_exprt input1
array_string_exprt result
array_string_exprt input2
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const
Evaluate the result from a concrete valuation of the arguments.
std::vector< exprt > args
Expression to hold a symbol (variable)
The type of an expression, extends irept.
#define PRECONDITION(CONDITION)
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
std::optional< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
exprt maximum(const exprt &a, const exprt &b)
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal
const type_with_subtypet & to_type_with_subtype(const typet &type)