mcrl2::lps::data_expression_index

Include file:

#include "mcrl2/lps/symbolic_reachability.h
class mcrl2::lps::data_expression_index

A bidirectional mapping between data expressions of a given sort and numbers.

Protected attributes

data::sort_expression mcrl2::lps::data_expression_index::m_sort
mcrl2::utilities::indexed_set<data::data_expression> mcrl2::lps::data_expression_index::m_values

Friends

friend std::ostream & mcrl2::lps::data_expression_index::operator<<

Public member functions

auto begin() const
data_expression_index(const data::sort_expression &sort)
auto end() const
bool has_index(std::uint32_t i) const
bool has_value(const data::data_expression &value) const
std::uint32_t index(const data::data_expression &value)

Returns the index of the given value. If the value is not present yet, it will be added.

std::size_t size() const
const data::sort_expression &sort() const
const data::data_expression &value(std::uint32_t i) const

Returns the value corresponding to index.