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,
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 ...
string_builtin_functiont(const string_builtin_functiont &)=delete
virtual optionalt< array_string_exprt > string_result() const
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 std::string name() const =0
virtual std::vector< array_string_exprt > string_arguments() const
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.
array_string_exprt result
optionalt< array_string_exprt > string_result() const override
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)
API to expression classes for 'mathematical' expressions.
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,...