mcrl2::lps::detail::unfold_data_manager

Include file:

#include "mcrl2/lps/lpsparunfoldlib.h
class mcrl2::lps::detail::unfold_data_manager

Private attributes

std::map<mcrl2::data::sort_expression, unfold_cache_element> &mcrl2::lps::detail::unfold_data_manager::m_cache

cache for previously unfolded sorts. facilitates reuse of previously introduced sorts and function symbols.

detail::data_equation_argument_generator mcrl2::lps::detail::unfold_data_manager::m_data_equation_argument_generator

generator for arguments in left hand side of data equations

data::data_specification &mcrl2::lps::detail::unfold_data_manager::m_dataspec
mcrl2::data::set_identifier_generator mcrl2::lps::detail::unfold_data_manager::m_identifier_generator

set of identifiers to use during fresh variable generation

bool mcrl2::lps::detail::unfold_data_manager::m_possibly_inconsistent

Boolean indicating whether rewrite rules may be added that could make the data specification inconsistent.

mcrl2::data::representative_generator mcrl2::lps::detail::unfold_data_manager::m_representative_generator

a generator for default data expressions of a given sort;

Public member functions

void add_used_identifier(const core::identifier_string &id)
void add_used_identifiers(const std::set<core::identifier_string> &ids)
data::function_symbol create_case_function(const data::sort_expression &det_sort, const data::sort_expression &output_sort)

Creates the case function with number of arguments determined by the number of affected constructors, the sort of the arguments and result are determined by sort..

Parameters:

  • det_sort The sort whose constructor is determined in the first argument
  • output_sort The sort of the arguments and return sort of the case function

Returns: A function that returns the corresponding constructor given the case selector and constructors.

data::data_expression create_cases(const data::data_expression &target, const data::data_expression_vector &rhss)
void create_determine_function(const data::sort_expression &sort)

Creates the determine function.

Parameters:

  • sort The sort on which this function operates

Returns: A function that maps constructors to the fresh basic sort

void create_distribution_law_over_case(const data::sort_expression &sort, const data::function_symbol &function_for_distribution, const data::function_symbol case_function)

Create distribution rules for distribution_functions over case_functions.

void create_new_constructors(const data::sort_expression &sort)

Creates a set of constructors for the fresh basic sort.

Parameters:

  • sort The sort for which to create analogous constructors

Returns: The constructors that are created for the fresh basic sort

void create_projection_functions(const data::sort_expression &sort)

Creates projection functions for the unfolded process parameter.

Parameters:

  • sort The sort on which these functions operate

Returns: A function that returns the projection functions for the constructors of the unfolded process parameter.

const data::data_specification &dataspec() const
void determine_affected_constructors(const data::sort_expression &sort)

Determines the constructors that are affected with the unfold process parameter.

Parameters:

  • sort The sort for which to find constructors

Post: The constructors that are affected with the unfold process parameter are stored in m_affected_constructors

std::string filter_illegal_characters(std::string in) const
void generate_case_function_equations(const data::sort_expression &sort, const data::function_symbol &case_function)

Create the data equations for case functions.

void generate_determine_function_equations(const data::sort_expression &sort)

Create the data equations for the determine function.

data::basic_sort generate_fresh_basic_sort(const data::sort_expression &sort)

Generates a fresh basic sort given a sort expression.

Parameters:

  • sort This sort’s name will be used to derive a name for the new sort

Returns: A fresh basic sort.

core::identifier_string generate_fresh_function_symbol_name(const std::string &str)

Generates a fresh name for a constructor or mapping.

Parameters:

  • str a string value. The value is used to generate a fresh name for a constructor or mapping.

Post: A fresh name for a constructor or mapping is generated.

Returns: A fresh name for a constructor or mapping.

data::variable generate_fresh_variable(std::string str, const data::sort_expression &sort)

Generates variable of type sort based on a given string str.

Parameters:

  • str a string value. The value is used to generate a fresh variable name.
  • sort The sort of the variable to generate.

Post: A fresh variable is generated, which has an unique name.

Returns: A fresh variable.

void generate_projection_function_equations(const data::sort_expression &sort)

Create the data equations for the projection functions.

unfold_cache_element &get_cache_element(const data::sort_expression &sort)
const std::vector<data::function_symbol> &get_constructors(const data::sort_expression &sort)
const data::function_symbol_vector &get_projection_funcs(const data::function_symbol &f)
data::set_identifier_generator &id_gen()
bool is_cached(const data::sort_expression &sort) const
bool is_constructor(const data::function_symbol &f) const
unfold_data_manager(std::map<mcrl2::data::sort_expression, unfold_cache_element> &cache, data::data_specification &dataspec, bool possibly_inconsistent)

Public static member functions

static bool char_filter(char c)