cprover
string_builtin_functiont Class Referenceabstract

Base class for string functions that are built in the solver. More...

#include <string_builtin_function.h>

+ Inheritance diagram for string_builtin_functiont:
+ Collaboration diagram for string_builtin_functiont:

Public Member Functions

 string_builtin_functiont (const string_builtin_functiont &)=delete
 
virtual ~string_builtin_functiont ()=default
 
virtual optionalt< array_string_exprtstring_result () const
 
virtual std::vector< array_string_exprtstring_arguments () const
 
virtual optionalt< exprteval (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
 

Detailed Description

Base class for string functions that are built in the solver.

Definition at line 19 of file string_builtin_function.h.

Constructor & Destructor Documentation

◆ string_builtin_functiont() [1/3]

string_builtin_functiont::string_builtin_functiont ( const string_builtin_functiont )
delete

◆ ~string_builtin_functiont()

virtual string_builtin_functiont::~string_builtin_functiont ( )
virtualdefault

◆ string_builtin_functiont() [2/3]

string_builtin_functiont::string_builtin_functiont ( )
privatedefault

◆ string_builtin_functiont() [3/3]

string_builtin_functiont::string_builtin_functiont ( exprt  return_code)
inlineexplicitprotected

Definition at line 67 of file string_builtin_function.h.

Member Function Documentation

◆ constraints()

virtual string_constraintst string_builtin_functiont::constraints ( string_constraint_generatort constraint_generator) const
pure virtual

◆ eval()

virtual optionalt<exprt> string_builtin_functiont::eval ( const std::function< exprt(const exprt &)> &  get_value) const
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_builtin_function_with_no_evalt, 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, and string_concat_char_builtin_functiont.

◆ length_constraint()

virtual exprt string_builtin_functiont::length_constraint ( ) const
pure virtual

◆ maybe_testing_function()

virtual bool string_builtin_functiont::maybe_testing_function ( ) const
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.

◆ name()

◆ string_arguments()

virtual std::vector<array_string_exprt> string_builtin_functiont::string_arguments ( ) const
inlinevirtual

◆ string_result()

virtual optionalt<array_string_exprt> string_builtin_functiont::string_result ( ) const
inlinevirtual

Member Data Documentation

◆ return_code

exprt string_builtin_functiont::return_code

Definition at line 53 of file string_builtin_function.h.


The documentation for this class was generated from the following file: