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
15 #define CHARACTER_FOR_UNKNOWN '?'
96 virtual std::string
name()
const = 0;
155 const std::vector<exprt> &fun_args,
185 const std::vector<exprt> &fun_args,
194 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
196 std::string
name()
const override
198 return "concat_char";
221 const std::vector<exprt> &fun_args,
231 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
233 std::string
name()
const override
254 const std::vector<exprt> &fun_args,
261 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
263 std::string
name()
const override
265 return "to_lower_case";
289 const std::vector<exprt> &fun_args,
309 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
311 std::string
name()
const override
313 return "to_upper_case";
343 const std::vector<exprt> &fun_args,
363 const std::vector<exprt> &fun_args,
368 if(fun_args.size() == 4)
375 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
377 std::string
name()
const override
379 return "string_of_int";
421 std::string
name()
const override
429 return std::vector<array_string_exprt>(
string_args);
458 const std::function<
exprt(
const exprt &)> &get_value);
462 const std::vector<mp_integer> &array,
465 #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 ...
API to expression classes for 'mathematical' expressions.
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 ...