mcrl2::utilities::number_postfix_generator

Include file:

#include "mcrl2/utilities/number_postfix_generator.h

class mcrl2::utilities::number_postfix_generator

Identifier generator that generates names consisting of a prefix followed by a number. For each prefix an index is maintained, that is incremented after each call to operator()(prefix).

Protected attributes

std::string mcrl2::utilities::number_postfix_generator::m_hint

The default hint.

std::map<std::string, std::size_t> mcrl2::utilities::number_postfix_generator::m_index

A map that maintains the highest index for each prefix.

Public member functions

void add_identifier(const std::string &id)

Adds the strings in the range [first, last) to the context.

Parameters:

• id A string

void add_identifiers(Iter first, Iter last)

Adds the strings in the range [first, last) to the context.

Parameters:

• first
• last [first, last) is a sequence of strings that is used as context.

void clear()

Clear the context of the generator.

std::string &hint()

Returns the default hint.

const std::string &hint() const

Returns the default hint.

number_postfix_generator(Iter first, Iter last, std::string hint = "FRESH_VAR")

Constructor.

Parameters:

• first
• last
• hint String hint to use as prefix for generated strings. [first, last) is a sequence of strings that is used as context.

number_postfix_generator(std::string hint = "FRESH_VAR")

Constructor.

std::string operator()() const

Generates a fresh identifier that doesn’t appear in the context.

Returns: A fresh identifier.

std::string operator()(std::string hint, bool add_to_context = true) const

Generates a fresh identifier that doesn’t appear in the context.

Returns: A fresh identifier.