Go to the documentation of this file.
4 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
5 #define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
16 #define CHARACTER_FOR_UNKNOWN '?'
97 virtual std::string
name()
const = 0;
156 const std::vector<exprt> &fun_args,
186 const std::vector<exprt> &fun_args,
195 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
197 std::string
name()
const override
199 return "concat_char";
222 const std::vector<exprt> &fun_args,
232 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
234 std::string
name()
const override
255 const std::vector<exprt> &fun_args,
262 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
264 std::string
name()
const override
266 return "to_lower_case";
290 const std::vector<exprt> &fun_args,
310 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
312 std::string
name()
const override
314 return "to_upper_case";
344 const std::vector<exprt> &fun_args,
364 const std::vector<exprt> &fun_args,
369 if(fun_args.size() == 4)
376 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
378 std::string
name()
const override
380 return "string_of_int";
422 std::string
name()
const override
430 return std::vector<array_string_exprt>(
string_args);
459 const std::function<
exprt(
const exprt &)> &get_value);
463 const std::vector<mp_integer> &array,
466 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
virtual ~string_builtin_functiont()=default
std::string name() const override
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
std::string name() const override
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Correspondance between arrays and pointers string representations.
string_builtin_functiont(const string_builtin_functiont &)=delete
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.
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
function_application_exprt function_application
String creation from other types.
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 ...
string_concat_char_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > args
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
virtual optionalt< array_string_exprt > string_result() 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 ...
virtual string_constraintst constraints(string_constraint_generatort &constraint_generator) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
virtual std::vector< array_string_exprt > string_arguments() const
string_set_char_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::string name() const override
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.
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
std::string name() const override
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.
const std::string & id2string(const irep_idt &d)
std::vector< exprt > args
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
std::vector< array_string_exprt > string_arguments() const override
std::vector< array_string_exprt > under_test
string_builtin_functiont(exprt return_code, array_poolt &array_pool)
Application of (mathematical) function.
String creation from integer types.
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
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...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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...
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 ...
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_result() const override
string_builtin_functiont()=delete
nonstd::optional< T > optionalt
Base class for string functions that are built in the solver.
virtual optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const =0
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
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::string name() const override
std::string name() const override
Setting a character at a particular position of a string.
optionalt< array_string_exprt > string_res
array_string_exprt result
Adding a character at the end of a string.
virtual exprt length_constraint() const =0
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 ...
virtual std::string name() const =0
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Generates string constraints to link results from string functions with their arguments.
String expressions for the string solver.
optionalt< array_string_exprt > string_result() const override
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &) 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...
std::vector< array_string_exprt > string_arguments() const override
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) 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 ...