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]);
bitvector_typet char_type()
Array constructor from list of elements.
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
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
Application of (mathematical) function.
The trinary if-then-else operator.
const irep_idt & id() const
Binary multiplication Associativity is not specified.
The plus expression Associativity is not specified.
std::vector< array_string_exprt > string_args
std::vector< exprt > args
optionalt< array_string_exprt > string_res
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
function_application_exprt function_application
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 string functions that are built in the solver.
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_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.
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....
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.
symbol_generatort fresh_symbol
array_string_exprt result
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.
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...
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.
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_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 ...
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.
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
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.
Expression to hold a symbol (variable)
Generation of fresh symbols of a given type.
The type of an expression, extends irept.
const typet & subtype() const
The unary minus expression.
nonstd::optional< T > optionalt
bool is_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
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 array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
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...
static bool eval_is_upper_case(const mp_integer &c)
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 ...
#define CHARACTER_FOR_UNKNOWN
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.
Generates string constraints to link results from string functions with their arguments.
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
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.
array_string_exprt & to_array_string_expr(exprt &expr)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal