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 '?'
40 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const = 0;
42 virtual std::string
name()
const = 0;
97 const std::vector<exprt> &fun_args,
127 const std::vector<exprt> &fun_args,
136 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
138 std::string
name()
const override
140 return "concat_char";
163 const std::vector<exprt> &fun_args,
173 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
175 std::string
name()
const override
196 const std::vector<exprt> &fun_args,
203 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
205 std::string
name()
const override
207 return "to_lower_case";
229 const std::vector<exprt> &fun_args,
247 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
249 std::string
name()
const override
251 return "to_upper_case";
287 const std::vector<exprt> &fun_args,
300 virtual std::vector<mp_integer>
eval(
301 const std::vector<mp_integer> &input1_value,
302 const std::vector<mp_integer> &input2_value,
303 const std::vector<mp_integer> &args_value)
const;
306 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
308 std::string
name()
const override
342 const std::vector<exprt> &fun_args,
345 std::vector<mp_integer>
eval(
346 const std::vector<mp_integer> &input1_value,
347 const std::vector<mp_integer> &input2_value,
348 const std::vector<mp_integer> &args_value)
const override;
350 std::string
name()
const override
370 const std::vector<exprt> &fun_args,
390 const std::vector<exprt> &fun_args,
395 if(fun_args.size() == 4)
402 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
404 std::string
name()
const override
406 return "string_of_int";
448 std::string
name()
const override
454 return std::vector<array_string_exprt>(
string_args);
478 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H
string_builtin_functiont(exprt return_code)
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.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
#define PRECONDITION(CONDITION)
string_concatenation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
String inserting a string into another one.
virtual ~string_builtin_functiont()=default
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
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 ...
Correspondance between arrays and pointers string representations.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
symbol_generatort fresh_symbol
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 ...
std::string name() const override
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.
array_string_exprt input1
std::string name() const override
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const
Evaluate the result from a concrete valuation of the arguments.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
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.
array_string_exprt result
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)
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< array_string_exprt > string_result() const override
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
string_insertion_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.
const irep_idt & get_identifier() const
std::vector< array_string_exprt > string_arguments() const override
string_insertion_builtin_functiont(const exprt &return_code)
std::vector< array_string_exprt > under_test
Application of (mathematical) function.
String creation from integer types.
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...
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 ...
optionalt< array_string_exprt > string_result() const override
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...
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
std::string name() const override
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 ...
symbol_exprt & function()
virtual std::string name() const =0
array_string_exprt input2
std::vector< exprt > args
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)
std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
std::vector< array_string_exprt > string_arguments() const override
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 ...