4 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H 5 #define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H 32 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const = 0;
34 virtual std::string
name()
const = 0;
80 const std::vector<exprt> &fun_args,
93 virtual std::vector<mp_integer>
eval(
94 const std::vector<mp_integer> &input_value,
95 const std::vector<mp_integer> &args_value)
const = 0;
98 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
117 const std::vector<exprt> &fun_args,
123 std::vector<mp_integer>
eval(
124 const std::vector<mp_integer> &input_value,
125 const std::vector<mp_integer> &args_value)
const override;
127 std::string
name()
const override 129 return "concat_char";
160 const std::vector<exprt> &fun_args,
173 virtual std::vector<mp_integer>
eval(
174 const std::vector<mp_integer> &input1_value,
175 const std::vector<mp_integer> &input2_value,
176 const std::vector<mp_integer> &args_value)
const;
179 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
181 std::string
name()
const override 228 const std::vector<exprt> &fun_args,
231 std::vector<mp_integer>
eval(
232 const std::vector<mp_integer> &input1_value,
233 const std::vector<mp_integer> &input2_value,
234 const std::vector<mp_integer> &args_value)
const override;
236 std::string
name()
const override 311 std::string
name()
const override 317 return std::vector<array_string_exprt>(
string_args);
343 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H std::vector< array_string_exprt > string_arguments() const override
string_builtin_functiont()=default
exprt add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
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
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
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.
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_builtin_functiont()=default
std::vector< array_string_exprt > string_arguments() const override
const irep_idt & get_identifier() const
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
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
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
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_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
string_builtin_functiont(const exprt &return_code)
std::vector< exprt > args
String creation from other types.
exprt add_axioms_for_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms...
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
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::vector< exprt > args
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
optionalt< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code)
nonstd::optional< T > optionalt
std::vector< mp_integer > eval(const std::vector< mp_integer > &input_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
virtual exprt add_constraints(string_constraint_generatort &constraint_generator) const =0
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt add_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_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 ...
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 optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const =0
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...
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset...
std::string name() const override
exprt add_axioms_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
array_string_exprt result
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
exprt add_constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
symbol_exprt & function()
std::string name() const override
array_string_exprt result
String expressions for the string solver.
array_string_exprt input2
bool maybe_testing_function() const override
Tells whether the builtin function can be a testing function, that is a function that does not return...
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...
optionalt< array_string_exprt > string_res
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
optionalt< array_string_exprt > string_result() const override
std::vector< exprt > args
Functions that are not yet supported in this class but are supported by string_constraint_generatort...
exprt add_axioms_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c)
Add axioms enforcing that res is the concatenation of s1 with character c.
virtual bool maybe_testing_function() const
Tells whether the builtin function can be a testing function, that is a function that does not return...
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
exprt add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.