13 const exprt &return_code,
14 const std::vector<exprt> &fun_args,
26 const std::function<
exprt(
const exprt &)> &get_value)
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))
57template <
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())
87 "character valuation should only contain constants and unknown");
90 input_opt.value().push_back(char_val);
112 const exprt upper_bound =
130 const std::function<
exprt(
const exprt &)> &get_value)
const
135 if(!input_opt || !char_opt || !position_opt)
137 if(0 <= *position_opt && *position_opt < input_opt.value().size())
216 return (
'A' <= c && c <=
'Z') || (0xc0 <= c && c <= 0xd6) ||
217 (0xd8 <= c && c <= 0xde);
221 const std::function<
exprt(
const exprt &)> &get_value)
const
297 const exprt conditional_convert = [&] {
302 const exprt converted =
317 const std::function<
exprt(
const exprt &)> &get_value)
const
354 const exprt converted =
373 const exprt &return_code,
374 const std::vector<exprt> &fun_args,
384 const std::function<
exprt(
const exprt &)> &get_value)
const
389 static std::string digits =
"0123456789abcdefghijklmnopqrstuvwxyz";
391 if(!radix_value || *radix_value > digits.length())
395 std::vector<mp_integer> right_to_left_characters;
396 if(current_value < 0)
397 current_value = -current_value;
398 if(current_value == 0)
399 right_to_left_characters.emplace_back(
'0');
400 while(current_value > 0)
402 const auto digit_value = (current_value % *radix_value).to_ulong();
403 right_to_left_characters.emplace_back(digits.at(digit_value));
404 current_value /= *radix_value;
407 right_to_left_characters.emplace_back(
'-');
409 const auto length = right_to_left_characters.size();
414 right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
431 const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
432 const std::size_t upper_bound =
434 const exprt negative_arg =
436 const exprt absolute_arg =
441 for(std::size_t current_size = 2; current_size <= upper_bound + 1;
444 min_int_with_current_size =
mult_exprt(
radix, min_int_with_current_size);
445 const exprt at_least_current_size =
448 at_least_current_size,
from_integer(current_size, type), size_expr);
458 const exprt &return_code,
463 const std::vector<exprt> &fun_args = f.
arguments();
465 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
467 string_res = array_pool.find(fun_args[1], fun_args[0]);
471 for(; i < fun_args.size(); ++i)
473 const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
476 arg && arg->operands().size() == 2 &&
477 arg->op1().type().id() == ID_pointer)
479 INVARIANT(is_refined_string_type(arg->type()),
"should be a string");
480 string_args.push_back(array_pool.find(arg->op1(), arg->op0()));
483 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
const typet & element_type() const
The type of the elements of the array.
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.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
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< exprt > args
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, message_handlert &message_handler) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
function_application_exprt function_application
Base class for string functions that are built in the solver.
std::optional< 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, message_handlert &message_handlert) 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.
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) 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.
std::optional< 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.
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
std::optional< 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.
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
std::optional< 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(class symbol_generatort &fresh_symbol, message_handlert &message_handler) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
std::optional< 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.
const typet & subtype() const
The type of an expression, extends irept.
The unary minus expression.
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.
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.
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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...
std::optional< 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 ...
static bool eval_is_upper_case(const mp_integer &c)
#define CHARACTER_FOR_UNKNOWN
Module: String solver Author: Diffblue Ltd.
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
std::optional< 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 ...
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
const type_with_subtypet & to_type_with_subtype(const typet &type)