4 #ifndef CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H 5 #define CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H 14 #define CHARACTER_FOR_UNKNOWN '?' 38 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const = 0;
40 virtual std::string
name()
const = 0;
85 const std::vector<exprt> &fun_args,
115 const std::vector<exprt> &fun_args,
124 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
126 std::string
name()
const override 128 return "concat_char";
156 const std::vector<exprt> &fun_args,
166 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
168 std::string
name()
const override 192 const std::vector<exprt> &fun_args,
199 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
201 std::string
name()
const override 203 return "to_lower_case";
225 const std::vector<exprt> &fun_args,
232 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
234 std::string
name()
const override 236 return "to_upper_case";
267 const std::vector<exprt> &fun_args,
280 virtual std::vector<mp_integer>
eval(
281 const std::vector<mp_integer> &input1_value,
282 const std::vector<mp_integer> &input2_value,
283 const std::vector<mp_integer> &args_value)
const;
286 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
288 std::string
name()
const override 335 const std::vector<exprt> &fun_args,
338 std::vector<mp_integer>
eval(
339 const std::vector<mp_integer> &input1_value,
340 const std::vector<mp_integer> &input2_value,
341 const std::vector<mp_integer> &args_value)
const override;
343 std::string
name()
const override 378 const std::vector<exprt> &fun_args,
398 const std::vector<exprt> &fun_args,
403 if(fun_args.size() == 4)
410 eval(
const std::function<
exprt(
const exprt &)> &get_value)
const override;
412 std::string
name()
const override 414 return "string_of_int";
459 std::string
name()
const override 465 return std::vector<array_string_exprt>(
string_args);
491 #endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H std::vector< array_string_exprt > string_arguments() const override
string_builtin_functiont()=default
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2...
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.
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.
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
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.
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 ...
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
exprt add_axioms_for_to_upper_case(const array_string_exprt &res, const array_string_exprt &expr)
Add axioms ensuring res corresponds to str in which lowercase characters of Basic Latin and Latin-1 s...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
String creation from integer types.
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_of_int_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
string_builtin_functiont(const exprt &return_code)
std::vector< exprt > args
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.
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...
exprt add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size=0)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String...
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
exprt add_axioms_for_to_lower_case(const array_string_exprt &res, const array_string_exprt &str)
Add axioms ensuring res corresponds to str in which uppercase characters have been converted to lower...
array_string_exprt input1
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 add_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 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< array_string_exprt > string_result() const override
string_insertion_builtin_functiont(const exprt &return_code)
nonstd::optional< T > optionalt
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...
#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
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...
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...
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...
exprt add_axioms_for_set_char(const array_string_exprt &res, const array_string_exprt &str, const exprt &position, const exprt &character)
Add axioms ensuring that the result res is similar to input string str where the character at index p...
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...
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 ...
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...
Setting a character at a particular position of a string.
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...
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...
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...
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
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.