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,
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.
Base class for all expressions.
typet & type()
Return the type of the expression.
Application of (mathematical) function.
const irep_idt & id() const
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
std::vector< array_string_exprt > string_args
std::vector< exprt > args
optionalt< array_string_exprt > string_res
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 ...
optionalt< array_string_exprt > string_result() const override
std::vector< array_string_exprt > string_arguments() 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.
std::string name() const override
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.
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 ...
virtual std::vector< array_string_exprt > string_arguments() const
string_builtin_functiont(const string_builtin_functiont &)=delete
string_builtin_functiont()=delete
string_builtin_functiont(exprt return_code, array_poolt &array_pool)
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
virtual ~string_builtin_functiont()=default
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call.
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 optionalt< array_string_exprt > string_result() const
virtual std::string name() const =0
Adding a character at the end of a string.
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.
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.
std::string name() const override
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
symbol_generatort fresh_symbol
String creation from other types.
optionalt< array_string_exprt > string_result() const override
array_string_exprt result
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
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 creation from integer types.
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
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 ...
std::string name() const override
Setting a character at a particular position of a string.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
std::string name() const override
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 ...
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::vector< exprt > args
std::vector< array_string_exprt > string_arguments() const override
std::vector< array_string_exprt > under_test
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
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...
std::string name() const override
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
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.
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input, array_poolt &array_pool)
std::string name() const override
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, 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 irep_idt & get_identifier() const
Generation of fresh symbols of a given type.
const std::string & id2string(const irep_idt &d)
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
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 ...
Generates string constraints to link results from string functions with their arguments.
String expressions for the string solver.
Collection of constraints of different types: existential formulas, universal formulas,...