14 const std::function<
exprt(
const exprt &)> &get_value);
18 const std::vector<mp_integer> &array,
23 const exprt &return_code,
24 const std::vector<exprt> &fun_args,
30 input = array_pool.
find(arg1.op1(), arg1.op0());
31 result = array_pool.
find(fun_args[1], fun_args[0]);
32 args.insert(
args.end(), fun_args.begin() + 3, fun_args.end());
36 const std::function<
exprt(
const exprt &)> &get_value)
const 39 if(!input_value.has_value())
42 std::vector<mp_integer> arg_values;
43 const auto &insert = std::back_inserter(arg_values);
47 if(
const auto val = numeric_cast<mp_integer>(get_value(e)))
50 get_value(e).
id() == ID_unknown,
51 "array valuation should only contain constants and unknown");
55 const auto result_value =
eval(*input_value, arg_values);
62 const exprt &return_code,
63 const std::vector<exprt> &fun_args,
69 input1 = array_pool.
find(arg1.op1(), arg1.op0());
71 input2 = array_pool.
find(arg2.op1(), arg2.op0());
72 result = array_pool.
find(fun_args[1], fun_args[0]);
73 args.push_back(fun_args[3]);
74 args.insert(
args.end(), fun_args.begin() + 5, fun_args.end());
78 const exprt &return_code,
79 const std::vector<exprt> &fun_args,
83 PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
85 input1 = array_pool.
find(arg1.op1(), arg1.op0());
87 input2 = array_pool.
find(arg2.op1(), arg2.op0());
88 result = array_pool.
find(fun_args[1], fun_args[0]);
89 args.insert(
args.end(), fun_args.begin() + 4, fun_args.end());
94 const std::function<
exprt(
const exprt &)> &get_value)
112 const auto &ops = array->
operands();
113 std::vector<mp_integer> result;
115 const auto &insert = std::back_inserter(result);
117 ops.begin(), ops.end(), insert, [unknown](
const exprt &e) {
118 if(
const auto i = numeric_cast<mp_integer>(e))
130 const auto &insert = std::back_inserter(array_expr.
operands());
132 array.begin(), array.end(), insert, [&](
const mp_integer &i) {
139 const std::vector<mp_integer> &input1_value,
140 const std::vector<mp_integer> &input2_value,
141 const std::vector<mp_integer> &args_value)
const 143 const auto start_index =
144 args_value.size() > 0 && args_value[0] > 0 ? args_value[0] :
mp_integer(0);
145 const mp_integer input2_size(input2_value.size());
146 const auto end_index =
147 args_value.size() > 1
148 ? std::max(std::min(args_value[1], input2_size), start_index)
151 std::vector<mp_integer>
result(input1_value);
154 input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
155 input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
160 const std::vector<mp_integer> &input_value,
161 const std::vector<mp_integer> &args_value)
const 164 std::vector<mp_integer>
result(input_value);
165 result.push_back(args_value[0]);
170 const std::vector<mp_integer> &input1_value,
171 const std::vector<mp_integer> &input2_value,
172 const std::vector<mp_integer> &args_value)
const 174 PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
175 const auto offset = std::min(
177 const auto start = args_value.size() > 1
181 const mp_integer input2_size(input2_value.size());
183 args_value.size() > 2
184 ? std::max(std::min(args_value[2], input2_size),
mp_integer(0))
187 std::vector<mp_integer>
result(input1_value);
189 result.begin() + numeric_cast_v<std::size_t>(offset),
190 input2_value.begin() + numeric_cast_v<std::size_t>(start),
191 input2_value.begin() + numeric_cast_v<std::size_t>(end));
196 const std::function<
exprt(
const exprt &)> &get_value)
const 200 if(!input2_value.has_value() || !input1_value.has_value())
203 std::vector<mp_integer> arg_values;
204 const auto &insert = std::back_inserter(arg_values);
208 if(
const auto val = numeric_cast<mp_integer>(get_value(e)))
213 const auto result_value =
eval(*input1_value, *input2_value, arg_values);
220 const exprt &return_code,
225 const std::vector<exprt> &fun_args = f.
arguments();
227 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
233 for(; i < fun_args.size(); ++i)
238 arg && arg->operands().size() == 2 &&
239 arg->op1().type().id() == ID_pointer)
245 args.push_back(fun_args[i]);
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
Generates string constraints to link results from string functions with their arguments.
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.
application of (mathematical) function
string_concatenation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
String inserting a string into another one.
std::vector< array_string_exprt > string_args
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.
static optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Module: String solver Author: Diffblue Ltd.
The trinary if-then-else operator.
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
static array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
#define INVARIANT(CONDITION, REASON)
const irep_idt & id() const
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
array_string_exprt input1
std::vector< exprt > args
nonstd::optional< T > optionalt
std::vector< mp_integer > eval(const std::vector< mp_integer > &input_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
#define PRECONDITION(CONDITION)
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
array_string_exprt result
array_string_exprt input2
Base class for all expressions.
bool is_refined_string_type(const typet &type)
std::vector< exprt > args
optionalt< array_string_exprt > string_res
const typet & subtype() const
struct constructor from list of elements
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 override
Evaluate the result from a concrete valuation of the arguments.
bitvector_typet char_type()
array constructor from list of elements
array_string_exprt & to_array_string_expr(exprt &expr)
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.