cprover
|
Base class for string functions that are built in the solver. More...
#include <string_builtin_function.h>
Public Member Functions | |
string_builtin_functiont (const string_builtin_functiont &)=delete | |
virtual | ~string_builtin_functiont ()=default |
virtual optionalt< array_string_exprt > | string_result () const |
virtual std::vector< array_string_exprt > | string_arguments () const |
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 builtin function. More... | |
virtual std::string | name () const =0 |
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 the value of the function call. More... | |
virtual exprt | length_constraint () const =0 |
Constraint ensuring that the length of the strings are coherent with the function call. More... | |
virtual bool | maybe_testing_function () const |
Tells whether the builtin function can be a testing function, that is a function that does not return a string, for instance like equals , indexOf or compare . More... | |
Public Attributes | |
exprt | return_code |
Protected Member Functions | |
string_builtin_functiont (exprt return_code) | |
Private Member Functions | |
string_builtin_functiont ()=default | |
Base class for string functions that are built in the solver.
Definition at line 19 of file string_builtin_function.h.
|
delete |
|
virtualdefault |
|
privatedefault |
|
inlineexplicitprotected |
Definition at line 67 of file string_builtin_function.h.
|
pure virtual |
Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.
Implemented in string_builtin_function_with_no_evalt, string_of_int_builtin_functiont, string_concatenation_builtin_functiont, string_insertion_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, and string_concat_char_builtin_functiont.
|
pure virtual |
Given a function get_value
which gives a valuation to expressions, attempt to find the result of the builtin function.
If not enough information can be gathered from get_value
, return an empty optional.
Implemented in string_of_int_builtin_functiont, string_insertion_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, string_concat_char_builtin_functiont, and string_builtin_function_with_no_evalt.
|
pure virtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implemented in string_builtin_function_with_no_evalt, string_of_int_builtin_functiont, string_concatenation_builtin_functiont, string_insertion_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, and string_concat_char_builtin_functiont.
|
inlinevirtual |
Tells whether the builtin function can be a testing function, that is a function that does not return a string, for instance like equals
, indexOf
or compare
.
Reimplemented in string_creation_builtin_functiont, string_insertion_builtin_functiont, and string_transformation_builtin_functiont.
Definition at line 58 of file string_builtin_function.h.
|
pure virtual |
Implemented in string_builtin_function_with_no_evalt, string_of_int_builtin_functiont, string_concatenation_builtin_functiont, string_insertion_builtin_functiont, string_to_upper_case_builtin_functiont, string_to_lower_case_builtin_functiont, string_set_char_builtin_functiont, and string_concat_char_builtin_functiont.
|
inlinevirtual |
Reimplemented in string_builtin_function_with_no_evalt, string_test_builtin_functiont, string_insertion_builtin_functiont, and string_transformation_builtin_functiont.
Definition at line 30 of file string_builtin_function.h.
|
inlinevirtual |
Reimplemented in string_builtin_function_with_no_evalt, string_creation_builtin_functiont, string_insertion_builtin_functiont, and string_transformation_builtin_functiont.
Definition at line 25 of file string_builtin_function.h.
exprt string_builtin_functiont::return_code |
Definition at line 53 of file string_builtin_function.h.