string_builtin_functiont Class Reference

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_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

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

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.

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

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.

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()

virtual std::string string_builtin_functiont::name ( ) const

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.

string_arguments()

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

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.

string_result()

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

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.

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:

• solvers/refinement/string_builtin_function.h