mcrl2::data::identifier_generator

Include file:

#include "mcrl2/data/identifier_generator.h

class mcrl2::data::identifier_generator

Abstract base class for identifier generators. Identifier generators generate fresh names that do not appear in a given context. A context is maintained containing already used identifiers. Using the operator()() and operator()(std::string) fresh identifiers are generated that do not appear in the context.

Protected attributes

Generator mcrl2::data::identifier_generator::m_generator

Public member functions

virtual void add_identifier(const core::identifier_string &s) = 0

Adds the identifier s to the context.

Parameters:

• s An identifier.

void add_identifiers(const std::set<core::identifier_string> &ids)

Add a set of identifiers to the context.

virtual void clear_context() = 0

Clears the context.

virtual bool has_identifier(const core::identifier_string &s) const = 0

Returns true if the identifier s appears in the context.

Parameters:

• s An identifier.

Returns: True if the identifier appears in the context.

identifier_generator() = default

Constructor.

virtual core::identifier_string operator()(const std::string &hint, bool add_to_context = true)

Returns a fresh identifier, with the given hint as prefix. The returned identifier is added to the context.

Parameters:

• hint A string
• add_to_context If true, the freshly generated identifier is added to the context to make sure no duplicates are generated.

Returns: A fresh identifier.

virtual void remove_identifier(const core::identifier_string &s) = 0

Removes the identifier s from the context.

Parameters:

• s An identifier.

void remove_identifiers(const std::set<core::identifier_string> &ids)

Remove a set of identifiers from the context.

virtual ~identifier_generator() = default

Destructor.