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 std::vector< array_string_exprt > string_arguments() const override
string_builtin_functiont()=default
Adding a character at the end of a string.
Generates string constraints to link results from string functions with their arguments.
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.
const std::string & id2string(const irep_idt &d)
Application of (mathematical) function.
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.
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 ...
function_application_exprt function_application
std::vector< array_string_exprt > under_test
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.
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...
string_to_lower_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
virtual ~string_builtin_functiont()=default
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 ...
std::vector< array_string_exprt > string_arguments() const override
const irep_idt & get_identifier() 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 ...
Generation of fresh symbols of a given type.
virtual optionalt< array_string_exprt > string_result() const
String inserting a string into another one.
std::vector< array_string_exprt > string_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.
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.
String creation from integer types.
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.
Base class for string functions that are built in the solver.
std::string name() const override
Collection of constraints of different types: existential formulas, universal formulas,...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
string_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
std::vector< exprt > args
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
string_to_upper_case_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input)
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 creation from other types.
string_to_upper_case_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
virtual exprt length_constraint() const =0
Constraint ensuring that the length of the strings are coherent with the function call.
virtual std::vector< array_string_exprt > string_arguments() const
array_string_exprt input1
optionalt< array_string_exprt > string_result() const override
std::vector< exprt > args
optionalt< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code)
nonstd::optional< T > optionalt
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...
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)
std::string name() const override
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 ...
std::vector< array_string_exprt > string_arguments() const override
exprt length_constraint() const override
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 ...
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.
std::string name() const override
array_string_exprt result
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
symbol_exprt & function()
std::string name() const override
array_string_exprt result
String expressions for the string solver.
array_string_exprt input2
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.
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
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 all expressions.
std::vector< exprt > args
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...
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< array_string_exprt > string_res
Converting each uppercase character of Basic Latin and Latin-1 supplement to the corresponding lowerc...
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...
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 ...
Setting a character at a particular position of a string.
optionalt< array_string_exprt > string_result() const override
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
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::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.
virtual std::string name() const =0
string_builtin_functiont(exprt return_code)
symbol_generatort fresh_symbol