16 const std::function<
exprt(
const exprt &)> &get_value);
20 const std::vector<mp_integer> &array,
25 const exprt &return_code,
26 const std::vector<exprt> &fun_args,
32 input = array_pool.
find(arg1.op1(), arg1.op0());
33 result = array_pool.
find(fun_args[1], fun_args[0]);
37 const exprt &return_code,
38 const std::vector<exprt> &fun_args,
44 input1 = array_pool.
find(arg1.op1(), arg1.op0());
46 input2 = array_pool.
find(arg2.op1(), arg2.op0());
47 result = array_pool.
find(fun_args[1], fun_args[0]);
48 args.push_back(fun_args[3]);
49 args.insert(
args.end(), fun_args.begin() + 5, fun_args.end());
53 const exprt &return_code,
54 const std::vector<exprt> &fun_args,
58 PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
60 input1 = array_pool.
find(arg1.op1(), arg1.op0());
62 input2 = array_pool.
find(arg2.op1(), arg2.op0());
63 result = array_pool.
find(fun_args[1], fun_args[0]);
64 args.insert(
args.end(), fun_args.begin() + 4, fun_args.end());
69 const std::function<
exprt(
const exprt &)> &get_value)
88 std::vector<mp_integer> result;
90 const auto &insert = std::back_inserter(result);
92 ops.begin(), ops.end(), insert, [unknown](
const exprt &e) {
93 if(
const auto i = numeric_cast<mp_integer>(e))
100 template <
typename Iter>
106 const auto &insert = std::back_inserter(array_expr.
operands());
107 std::transform(begin, end, insert, [&](
const mp_integer &i) {
116 return make_string(array.begin(), array.end(), array_type);
120 const std::vector<mp_integer> &input1_value,
121 const std::vector<mp_integer> &input2_value,
122 const std::vector<mp_integer> &args_value)
const 124 const auto start_index =
125 args_value.size() > 0 && args_value[0] > 0 ? args_value[0] :
mp_integer(0);
126 const mp_integer input2_size(input2_value.size());
127 const auto end_index =
128 args_value.size() > 1
129 ? std::max(std::min(args_value[1], input2_size), start_index)
132 std::vector<mp_integer>
result(input1_value);
135 input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
136 input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
141 const std::function<
exprt(
const exprt &)> &get_value)
const 144 if(!input_opt.has_value())
147 if(
const auto val = numeric_cast<mp_integer>(get_value(
character)))
151 "character valuation should only contain constants and unknown");
154 input_opt.value().push_back(char_val);
162 const std::function<
exprt(
const exprt &)> &get_value)
const 167 if(!input_opt || !char_opt || !position_opt)
169 if(0 <= *position_opt && *position_opt < input_opt.value().size())
170 input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
199 return (
'A' <= c && c <=
'Z') || (0xc0 <= c && c <= 0xd6) ||
200 (0xd8 <= c && c <= 0xde);
204 const std::function<
exprt(
const exprt &)> &get_value)
const 221 const std::function<
exprt(
const exprt &)> &get_value)
const 238 const std::vector<mp_integer> &input1_value,
239 const std::vector<mp_integer> &input2_value,
240 const std::vector<mp_integer> &args_value)
const 242 PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
243 const auto offset = std::min(
245 const auto start = args_value.size() > 1
249 const mp_integer input2_size(input2_value.size());
251 args_value.size() > 2
252 ? std::max(std::min(args_value[2], input2_size),
mp_integer(0))
255 std::vector<mp_integer>
result(input1_value);
257 result.begin() + numeric_cast_v<std::size_t>(offset),
258 input2_value.begin() + numeric_cast_v<std::size_t>(start),
259 input2_value.begin() + numeric_cast_v<std::size_t>(end));
264 const std::function<
exprt(
const exprt &)> &get_value)
const 268 if(!input2_value.has_value() || !input1_value.has_value())
271 std::vector<mp_integer> arg_values;
272 const auto &insert = std::back_inserter(arg_values);
276 if(
const auto val = numeric_cast<mp_integer>(get_value(e)))
281 const auto result_value =
eval(*input1_value, *input2_value, arg_values);
293 const exprt &return_code,
294 const std::vector<exprt> &fun_args,
299 result = array_pool.
find(fun_args[1], fun_args[0]);
304 const std::function<
exprt(
const exprt &)> &get_value)
const 309 static std::string digits =
"0123456789abcdefghijklmnopqrstuvwxyz";
311 if(!radix_value || *radix_value > digits.length())
315 std::vector<mp_integer> right_to_left_characters;
316 if(current_value < 0)
317 current_value = -current_value;
318 if(current_value == 0)
319 right_to_left_characters.emplace_back(
'0');
320 while(current_value > 0)
322 const auto digit_value = (current_value % *radix_value).to_ulong();
323 right_to_left_characters.emplace_back(digits.at(digit_value));
324 current_value /= *radix_value;
327 right_to_left_characters.emplace_back(
'-');
329 const auto length = right_to_left_characters.size();
333 right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
340 const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
341 const std::size_t upper_bound =
343 const exprt negative_arg =
345 const exprt absolute_arg =
350 for(std::size_t current_size = 2; current_size <= upper_bound + 1;
353 min_int_with_current_size =
mult_exprt(
radix, min_int_with_current_size);
354 const exprt at_least_current_size =
357 at_least_current_size,
from_integer(current_size, type), size_expr);
366 const exprt &return_code,
371 const std::vector<exprt> &fun_args = f.
arguments();
373 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
379 for(; i < fun_args.size(); ++i)
384 arg && arg->operands().size() == 2 &&
385 arg->op1().type().id() == ID_pointer)
391 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.
A generic base class for relations, i.e., binary predicates.
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.
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
String inserting a string into another one.
static array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
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)
#define INVARIANT(CONDITION, REASON)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
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
#define CHARACTER_FOR_UNKNOWN
std::vector< exprt > args
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_creation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
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.
The unary minus expression.
array_string_exprt result
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
size_t max_printed_string_length(const typet &type, unsigned long ul_radix)
Calculate the string length needed to represent any value of the given type using the given radix...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
const typet & subtype() const
struct constructor from list of elements
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
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()
static bool eval_is_upper_case(const mp_integer &c)
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.