mcrl2::data::enumerator_identifier_generator Class Reference

#include <enumerator_identifier_generator.h>

Public Member Functions
	enumerator_identifier_generator (const std::string &prefix="x_")
	Constructor.
core::identifier_string	operator() ()
	Generates a unique function symbol with the given prefix followed by a number.
core::identifier_string	operator() (const std::string &prefix)
	Generates a unique constant function symbol with the given prefix followed by a number.
void	clear ()

Protected Attributes
atermpp::function_symbol_generator	f

Detailed Description

Definition at line 27 of file enumerator_identifier_generator.h.

Constructor & Destructor Documentation

enumerator_identifier_generator()

mcrl2::data::enumerator_identifier_generator::enumerator_identifier_generator ( const std::string &  prefix = "x_" )

inlineexplicit

Constructor.

Parameters

prefix

The prefix of the generated generated strings

Precondition

The prefix may not be empty, and it may not have trailing digits

Definition at line 36 of file enumerator_identifier_generator.h.

Member Function Documentation

clear()

void mcrl2::data::enumerator_identifier_generator::clear ( )

inline

Definition at line 54 of file enumerator_identifier_generator.h.

operator()() [1/2]

core::identifier_string mcrl2::data::enumerator_identifier_generator::operator() ( )

inline

Generates a unique function symbol with the given prefix followed by a number.

Definition at line 41 of file enumerator_identifier_generator.h.

operator()() [2/2]

core::identifier_string mcrl2::data::enumerator_identifier_generator::operator() ( const std::string &  prefix )

inline

Generates a unique constant function symbol with the given prefix followed by a number.

This is not as efficient as iteratively generating a string with a fixed prefix.

Parameters

prefix

The prefix used to generate this function symbol

Definition at line 49 of file enumerator_identifier_generator.h.

Member Data Documentation

f

atermpp::function_symbol_generator mcrl2::data::enumerator_identifier_generator::f

protected

Definition at line 30 of file enumerator_identifier_generator.h.

---

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

• data/include/mcrl2/data/detail/enumerator_identifier_generator.h