Functions that are not yet supported in this class but are supported by string_constraint_generatort. More...
#include <string_builtin_function.h>
Public Member Functions | |
| string_builtin_function_with_no_evalt (const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool) | |
| std::string | name () const override |
| std::vector< array_string_exprt > | string_arguments () const override |
| optionalt< array_string_exprt > | string_result () const override |
| 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 builtin function. More... | |
| exprt | add_constraints (string_constraint_generatort &generator) const override |
| Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call. More... | |
| exprt | length_constraint () const override |
| Constraint ensuring that the length of the strings are coherent with the function call. More... | |
 Public Member Functions inherited from string_builtin_functiont | |
| string_builtin_functiont (const string_builtin_functiont &)=delete | |
| virtual | ~string_builtin_functiont ()=default |
| 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 | |
| function_application_exprt | function_application |
| optionalt< array_string_exprt > | string_res |
| std::vector< array_string_exprt > | string_args |
| std::vector< exprt > | args |
| Public Attributes inherited from string_builtin_functiont | |
| exprt | return_code |
Additional Inherited Members | |
| Protected Member Functions inherited from string_builtin_functiont | |
| string_builtin_functiont (const exprt &return_code) | |
Detailed Description
Functions that are not yet supported in this class but are supported by string_constraint_generatort.
- Note
- Ultimately this should be disappear, once all builtin function have a corresponding string_builtin_functiont class.
Definition at line 446 of file string_builtin_function.h.
Constructor & Destructor Documentation
◆ string_builtin_function_with_no_evalt()
| string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt | ( | const exprt & | return_code, |
| const function_application_exprt & | f, | ||
| array_poolt & | array_pool | ||
| ) |
Definition at line 365 of file string_builtin_function.cpp.
References args, function_application_exprt::arguments(), expr_try_dynamic_cast(), array_poolt::find(), INVARIANT, is_refined_string_type(), string_args, and string_res.
Member Function Documentation
◆ add_constraints()
|
inlineoverridevirtual |
Add constraints ensuring that the value of result expression of the builtin function corresponds to the value of the function call.
Implements string_builtin_functiont.
Definition at line 478 of file string_builtin_function.h.
References string_constraint_generatort::add_axioms_for_function_application(), and function_application.
◆ eval()
|
inlineoverridevirtual |
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.
Implements string_builtin_functiont.
Definition at line 473 of file string_builtin_function.h.
◆ length_constraint()
|
inlineoverridevirtual |
Constraint ensuring that the length of the strings are coherent with the function call.
Implements string_builtin_functiont.
Definition at line 483 of file string_builtin_function.h.
References UNIMPLEMENTED.
◆ name()
|
inlineoverridevirtual |
Implements string_builtin_functiont.
Definition at line 459 of file string_builtin_function.h.
References function_application_exprt::function(), function_application, symbol_exprt::get_identifier(), and id2string().
◆ string_arguments()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 463 of file string_builtin_function.h.
References string_args.
◆ string_result()
|
inlineoverridevirtual |
Reimplemented from string_builtin_functiont.
Definition at line 467 of file string_builtin_function.h.
References string_res.
Member Data Documentation
◆ args
| std::vector<exprt> string_builtin_function_with_no_evalt::args |
Definition at line 452 of file string_builtin_function.h.
Referenced by string_builtin_function_with_no_evalt().
◆ function_application
| function_application_exprt string_builtin_function_with_no_evalt::function_application |
Definition at line 449 of file string_builtin_function.h.
Referenced by add_constraints(), and name().
◆ string_args
| std::vector<array_string_exprt> string_builtin_function_with_no_evalt::string_args |
Definition at line 451 of file string_builtin_function.h.
Referenced by string_arguments(), and string_builtin_function_with_no_evalt().
◆ string_res
| optionalt<array_string_exprt> string_builtin_function_with_no_evalt::string_res |
Definition at line 450 of file string_builtin_function.h.
Referenced by string_builtin_function_with_no_evalt(), and string_result().
The documentation for this class was generated from the following files:
- solvers/refinement/string_builtin_function.h
- solvers/refinement/string_builtin_function.cpp
