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));
144 auto pair = [&]() -> std::pair<exprt, string_constraintst> {
170 const std::function<
exprt(
const exprt &)> &get_value)
const 173 if(!input_opt.has_value())
176 if(
const auto val = numeric_cast<mp_integer>(get_value(
character)))
180 "character valuation should only contain constants and unknown");
183 input_opt.value().push_back(char_val);
221 const std::function<
exprt(
const exprt &)> &get_value)
const 226 if(!input_opt || !char_opt || !position_opt)
228 if(0 <= *position_opt && *position_opt < input_opt.value().size())
229 input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
297 return (
'A' <= c && c <=
'Z') || (0xc0 <= c && c <= 0xd6) ||
298 (0xd8 <= c && c <= 0xde);
302 const std::function<
exprt(
const exprt &)> &get_value)
const 326 upper_case.push_back(
333 upper_case.push_back(
342 upper_case.push_back(
380 const exprt conditional_convert = [&] {
385 const exprt converted =
397 const std::function<
exprt(
const exprt &)> &get_value)
const 431 const exprt converted =
444 const std::vector<mp_integer> &input1_value,
445 const std::vector<mp_integer> &input2_value,
446 const std::vector<mp_integer> &args_value)
const 448 PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
449 const auto offset = std::min(
451 const auto start = args_value.size() > 1
455 const mp_integer input2_size(input2_value.size());
457 args_value.size() > 2
458 ? std::max(std::min(args_value[2], input2_size),
mp_integer(0))
461 std::vector<mp_integer>
result(input1_value);
463 result.begin() + numeric_cast_v<std::size_t>(offset),
464 input2_value.begin() + numeric_cast_v<std::size_t>(start),
465 input2_value.begin() + numeric_cast_v<std::size_t>(end));
470 const std::function<
exprt(
const exprt &)> &get_value)
const 474 if(!input2_value.has_value() || !input1_value.has_value())
477 std::vector<mp_integer> arg_values;
478 const auto &insert = std::back_inserter(arg_values);
482 if(
const auto val = numeric_cast<mp_integer>(get_value(e)))
487 const auto result_value =
eval(*input1_value, *input2_value, arg_values);
523 const exprt &return_code,
524 const std::vector<exprt> &fun_args,
529 result = array_pool.
find(fun_args[1], fun_args[0]);
534 const std::function<
exprt(
const exprt &)> &get_value)
const 539 static std::string digits =
"0123456789abcdefghijklmnopqrstuvwxyz";
541 if(!radix_value || *radix_value > digits.length())
545 std::vector<mp_integer> right_to_left_characters;
546 if(current_value < 0)
547 current_value = -current_value;
548 if(current_value == 0)
549 right_to_left_characters.emplace_back(
'0');
550 while(current_value > 0)
552 const auto digit_value = (current_value % *radix_value).to_ulong();
553 right_to_left_characters.emplace_back(digits.at(digit_value));
554 current_value /= *radix_value;
557 right_to_left_characters.emplace_back(
'-');
559 const auto length = right_to_left_characters.size();
563 right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
579 const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
580 const std::size_t upper_bound =
582 const exprt negative_arg =
584 const exprt absolute_arg =
589 for(std::size_t current_size = 2; current_size <= upper_bound + 1;
592 min_int_with_current_size =
mult_exprt(
radix, min_int_with_current_size);
593 const exprt at_least_current_size =
596 at_least_current_size,
from_integer(current_size, type), size_expr);
605 const exprt &return_code,
610 const std::vector<exprt> &fun_args = f.
arguments();
612 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
618 for(; i < fun_args.size(); ++i)
623 arg && arg->operands().size() == 2 &&
624 arg->op1().type().id() == ID_pointer)
630 args.push_back(fun_args[i]);
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
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.
static exprt is_lower_case(const exprt &character)
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unico...
The type of an expression, extends irept.
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2...
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 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 ...
function_application_exprt function_application
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
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 ...
Generation of fresh symbols of a given type.
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.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
static exprt is_upper_case(const exprt &character)
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicod...
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
std::pair< exprt, string_constraintst > add_axioms_for_concat_substr(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
exprt minimum(const exprt &a, const exprt &b)
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
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 input1
#define CHARACTER_FOR_UNKNOWN
std::pair< exprt, string_constraintst > add_axioms_for_function_application(symbol_generatort &fresh_symbol, const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
std::vector< exprt > args
nonstd::optional< T > optionalt
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 ...
#define PRECONDITION(CONDITION)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
The plus expression Associativity is not specified.
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
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
bool is_constant() const
Return whether the expression is a constant.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
array_string_exprt result
std::vector< exprt > existential
array_string_exprt input2
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
Base class for all expressions.
bool is_refined_string_type(const typet &type)
std::vector< exprt > args
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
std::vector< string_constraintt > universal
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...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
#define UNREACHABLE
This should be used to mark dead code.
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 ...
Universally quantified string constraint
Expression to hold a symbol (variable)
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
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.
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
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.
std::pair< exprt, string_constraintst > add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
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.
symbol_generatort fresh_symbol