Go to the documentation of this file.
13 const exprt &return_code,
14 const std::vector<exprt> &fun_args,
19 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
26 const std::function<
exprt(
const exprt &)> &get_value)
40 const auto &array = expr_try_dynamic_cast<array_exprt>(content);
44 const auto &ops = array->operands();
45 std::vector<mp_integer> result;
47 const auto &insert = std::back_inserter(result);
49 ops.begin(), ops.end(), insert, [unknown](
const exprt &e) {
50 if(const auto i = numeric_cast<mp_integer>(e))
57 template <
typename Iter>
63 const auto &insert = std::back_inserter(array_expr.operands());
64 std::transform(begin, end, insert, [&](
const mp_integer &i) {
73 return make_string(array.begin(), array.end(), array_type);
77 const std::function<
exprt(
const exprt &)> &get_value)
const
80 if(!input_opt.has_value())
83 if(
const auto val = numeric_cast<mp_integer>(get_value(
character)))
87 "character valuation should only contain constants and unknown");
90 input_opt.value().push_back(char_val);
111 const exprt upper_bound =
129 const std::function<
exprt(
const exprt &)> &get_value)
const
132 const auto char_opt = numeric_cast<mp_integer>(get_value(
character));
133 const auto position_opt = numeric_cast<mp_integer>(get_value(
position));
134 if(!input_opt || !char_opt || !position_opt)
136 if(0 <= *position_opt && *position_opt < input_opt.value().size())
137 input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
212 return (
'A' <= c && c <=
'Z') || (0xc0 <= c && c <= 0xd6) ||
213 (0xd8 <= c && c <= 0xde);
217 const std::function<
exprt(
const exprt &)> &get_value)
const
292 const exprt conditional_convert = [&] {
295 const typet &char_type = result.type().subtype();
296 const exprt diff = from_integer(0x20, char_type);
297 const exprt converted =
298 equal_exprt(result[idx], plus_exprt(input[idx], diff));
299 const exprt non_converted = equal_exprt(result[idx], input[idx]);
300 return if_exprt(is_upper_case(input[idx]), converted, non_converted);
305 conditional_convert);
311 const std::function<
exprt(
const exprt &)> &get_value)
const
345 const exprt converted =
363 const exprt &return_code,
364 const std::vector<exprt> &fun_args,
374 const std::function<
exprt(
const exprt &)> &get_value)
const
376 const auto arg_value = numeric_cast<mp_integer>(get_value(
arg));
379 static std::string digits =
"0123456789abcdefghijklmnopqrstuvwxyz";
380 const auto radix_value = numeric_cast<mp_integer>(get_value(
radix));
381 if(!radix_value || *radix_value > digits.length())
385 std::vector<mp_integer> right_to_left_characters;
386 if(current_value < 0)
387 current_value = -current_value;
388 if(current_value == 0)
389 right_to_left_characters.emplace_back(
'0');
390 while(current_value > 0)
392 const auto digit_value = (current_value % *radix_value).to_ulong();
393 right_to_left_characters.emplace_back(digits.at(digit_value));
394 current_value /= *radix_value;
397 right_to_left_characters.emplace_back(
'-');
399 const auto length = right_to_left_characters.size();
403 right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
418 const auto radix_opt = numeric_cast<std::size_t>(
radix);
419 const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
420 const std::size_t upper_bound =
422 const exprt negative_arg =
424 const exprt absolute_arg =
429 for(std::size_t current_size = 2; current_size <= upper_bound + 1;
432 min_int_with_current_size =
mult_exprt(
radix, min_int_with_current_size);
433 const exprt at_least_current_size =
436 at_least_current_size,
from_integer(current_size, type), size_expr);
446 const exprt &return_code,
451 const std::vector<exprt> &fun_args = f.
arguments();
453 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
459 for(; i < fun_args.size(); ++i)
461 const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
464 arg && arg->operands().size() == 2 &&
465 arg->op1().type().id() == ID_pointer)
471 args.push_back(fun_args[i]);
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
const typet & length_type() const
const typet & subtype() const
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...
static bool eval_is_upper_case(const mp_integer &c)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
exprt minimum(const exprt &a, const exprt &b)
The type of an expression, extends irept.
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...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Correspondance between arrays and pointers string representations.
The trinary if-then-else operator.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
symbol_generatort fresh_symbol
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
The plus expression Associativity is not specified.
function_application_exprt function_application
Base class for all expressions.
std::vector< array_string_exprt > string_args
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 ...
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > args
bool is_true() const
Return whether the expression is a constant representing true.
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 ...
Expression to hold a symbol (variable)
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.
Generation of fresh symbols of a given type.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
#define CHARACTER_FOR_UNKNOWN
#define PRECONDITION(CONDITION)
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
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...
The unary minus expression.
std::pair< exprt, string_constraintst > add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
const irep_idt & id() const
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< exprt > operandst
array_string_exprt & to_array_string_expr(exprt &expr)
nonstd::optional< T > optionalt
Base class for string functions that are built in the solver.
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
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...
bitvector_typet char_type()
optionalt< 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 ...
optionalt< array_string_exprt > string_res
array_string_exprt result
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates whose two operands have the same type.
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 ...
bool is_refined_string_type(const typet &type)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Generates string constraints to link results from string functions with their arguments.
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)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
Array constructor from list of elements.
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.
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
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.
std::vector< exprt > existential
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 ...
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< string_constraintt > universal