#include <lpsparunfoldlib.h>

Public Member Functions
	unfold_data_manager (std::map< mcrl2::data::sort_expression, unfold_cache_element > &cache, data::data_specification &dataspec, bool possibly_inconsistent)

const data::data_specification &	dataspec () const

void	add_used_identifier (const core::identifier_string &id)

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

data::set_identifier_generator &	id_gen ()

unfold_cache_element &	get_cache_element (const data::sort_expression &sort)

bool	is_cached (const data::sort_expression &sort) const

bool	is_constructor (const data::function_symbol &f) const

const std::vector< data::function_symbol > &	get_constructors (const data::sort_expression &sort)

data::data_expression	create_cases (const data::data_expression &target, const data::data_expression_vector &rhss)

const data::function_symbol_vector &	get_projection_funcs (const data::function_symbol &f)

mcrl2::data::basic_sort	generate_fresh_basic_sort (const data::sort_expression &sort)
	Generates a fresh basic sort given a sort expression.

mcrl2::core::identifier_string	generate_fresh_function_symbol_name (const std::string &str)
	Generates a fresh name for a constructor or mapping.

mcrl2::data::variable	generate_fresh_variable (std::string str, const data::sort_expression &sort)
	Generates variable of type sort based on a given string str.

void	create_determine_function (const data::sort_expression &sort)
	Creates the determine function.

void	create_projection_functions (const data::sort_expression &sort)
	Creates projection functions for the unfolded process parameter.

void	determine_affected_constructors (const data::sort_expression &sort)
	Determines the constructors that are affected with the unfold process parameter.

void	create_new_constructors (const data::sort_expression &sort)
	Creates a set of constructors for the fresh basic sort.

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..

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	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.

void	generate_projection_function_equations (const data::sort_expression &sort)
	Create the data equations for the projection functions.

std::string	filter_illegal_characters (std::string in) const

Static Public Member Functions
static bool	char_filter (char c)

Private Attributes
std::map< mcrl2::data::sort_expression, unfold_cache_element > &	m_cache
	cache for previously unfolded sorts. facilitates reuse of previously introduced sorts and function symbols.

data::data_specification &	m_dataspec

mcrl2::data::set_identifier_generator	m_identifier_generator
	set of identifiers to use during fresh variable generation

detail::data_equation_argument_generator	m_data_equation_argument_generator
	generator for arguments in left hand side of data equations

mcrl2::data::representative_generator	m_representative_generator
	a generator for default data expressions of a given sort;

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

Detailed Description

Definition at line 90 of file lpsparunfoldlib.h.

Constructor & Destructor Documentation

◆ unfold_data_manager()

mcrl2::lps::detail::unfold_data_manager::unfold_data_manager	(	std::map< mcrl2::data::sort_expression, unfold_cache_element > &	cache,
		data::data_specification &	dataspec,
		bool	possibly_inconsistent
	)

inline

Definition at line 113 of file lpsparunfoldlib.h.

Member Function Documentation

◆ add_used_identifier()

void mcrl2::lps::detail::unfold_data_manager::add_used_identifier ( const core::identifier_string & id )

inline

Definition at line 124 of file lpsparunfoldlib.h.

◆ add_used_identifiers()

void mcrl2::lps::detail::unfold_data_manager::add_used_identifiers ( const std::set< core::identifier_string > & ids )

inline

Definition at line 129 of file lpsparunfoldlib.h.

◆ char_filter()

static bool mcrl2::lps::detail::unfold_data_manager::char_filter ( char c )

inlinestatic

Definition at line 256 of file lpsparunfoldlib.h.

◆ create_case_function()

data::function_symbol mcrl2::lps::detail::unfold_data_manager::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.

Definition at line 142 of file lpsparunfoldlib.cpp.

◆ create_cases()

data::data_expression mcrl2::lps::detail::unfold_data_manager::create_cases	(	const data::data_expression &	target,
		const data::data_expression_vector &	rhss
	)

inline

Definition at line 156 of file lpsparunfoldlib.h.

◆ create_determine_function()

void mcrl2::lps::detail::unfold_data_manager::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

Definition at line 181 of file lpsparunfoldlib.cpp.

◆ create_distribution_law_over_case()

void mcrl2::lps::detail::unfold_data_manager::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.

Definition at line 294 of file lpsparunfoldlib.cpp.

◆ create_new_constructors()

void mcrl2::lps::detail::unfold_data_manager::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

Definition at line 124 of file lpsparunfoldlib.cpp.

◆ create_projection_functions()

void mcrl2::lps::detail::unfold_data_manager::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.

Definition at line 196 of file lpsparunfoldlib.cpp.

◆ dataspec()

const data::data_specification & mcrl2::lps::detail::unfold_data_manager::dataspec ( ) const

inline

Definition at line 122 of file lpsparunfoldlib.h.

◆ determine_affected_constructors()

void mcrl2::lps::detail::unfold_data_manager::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

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

Definition at line 105 of file lpsparunfoldlib.cpp.

◆ filter_illegal_characters()

std::string mcrl2::lps::detail::unfold_data_manager::filter_illegal_characters ( std::string in ) const

inline

Definition at line 267 of file lpsparunfoldlib.h.

◆ generate_case_function_equations()

void mcrl2::lps::detail::unfold_data_manager::generate_case_function_equations	(	const data::sort_expression &	sort,
		const data::function_symbol &	case_function
	)

Create the data equations for case functions.

Definition at line 338 of file lpsparunfoldlib.cpp.

◆ generate_determine_function_equations()

void mcrl2::lps::detail::unfold_data_manager::generate_determine_function_equations ( const data::sort_expression & sort )

Create the data equations for the determine function.

Definition at line 423 of file lpsparunfoldlib.cpp.

◆ generate_fresh_basic_sort()

data::basic_sort mcrl2::lps::detail::unfold_data_manager::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.

Definition at line 74 of file lpsparunfoldlib.cpp.

◆ generate_fresh_function_symbol_name()

core::identifier_string mcrl2::lps::detail::unfold_data_manager::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.

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

Returns: A fresh name for a constructor or mapping.

Definition at line 92 of file lpsparunfoldlib.cpp.

◆ generate_fresh_variable()

data::variable mcrl2::lps::detail::unfold_data_manager::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.

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

Returns: A fresh variable.

Definition at line 100 of file lpsparunfoldlib.cpp.

◆ generate_projection_function_equations()

void mcrl2::lps::detail::unfold_data_manager::generate_projection_function_equations ( const data::sort_expression & sort )

Create the data equations for the projection functions.

Definition at line 229 of file lpsparunfoldlib.cpp.

◆ get_cache_element()

unfold_cache_element & mcrl2::lps::detail::unfold_data_manager::get_cache_element ( const data::sort_expression & sort )

Definition at line 35 of file lpsparunfoldlib.cpp.

◆ get_constructors()

const std::vector< data::function_symbol > & mcrl2::lps::detail::unfold_data_manager::get_constructors ( const data::sort_expression & sort )

inline

Definition at line 151 of file lpsparunfoldlib.h.

◆ get_projection_funcs()

const data::function_symbol_vector & mcrl2::lps::detail::unfold_data_manager::get_projection_funcs ( const data::function_symbol & f )

inline

Definition at line 171 of file lpsparunfoldlib.h.

◆ id_gen()

data::set_identifier_generator & mcrl2::lps::detail::unfold_data_manager::id_gen ( )

inline

Definition at line 134 of file lpsparunfoldlib.h.

◆ is_cached()

bool mcrl2::lps::detail::unfold_data_manager::is_cached ( const data::sort_expression & sort ) const

inline

Definition at line 141 of file lpsparunfoldlib.h.

◆ is_constructor()

bool mcrl2::lps::detail::unfold_data_manager::is_constructor ( const data::function_symbol & f ) const

inline

Definition at line 146 of file lpsparunfoldlib.h.

Member Data Documentation

◆ m_cache

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

private

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

Definition at line 95 of file lpsparunfoldlib.h.

◆ m_data_equation_argument_generator

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

private

generator for arguments in left hand side of data equations

Definition at line 103 of file lpsparunfoldlib.h.

◆ m_dataspec

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

private

Definition at line 97 of file lpsparunfoldlib.h.

◆ m_identifier_generator

mcrl2::data::set_identifier_generator mcrl2::lps::detail::unfold_data_manager::m_identifier_generator

private

set of identifiers to use during fresh variable generation

Definition at line 100 of file lpsparunfoldlib.h.

◆ m_possibly_inconsistent

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

private

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

Definition at line 110 of file lpsparunfoldlib.h.

◆ m_representative_generator

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

private

a generator for default data expressions of a given sort;

Definition at line 106 of file lpsparunfoldlib.h.

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

lps/include/mcrl2/lps/lpsparunfoldlib.h
lps/source/lpsparunfoldlib.cpp

Public Member Functions

Static Public Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ unfold_data_manager()

Member Function Documentation

◆ add_used_identifier()

◆ add_used_identifiers()

◆ char_filter()

◆ create_case_function()

◆ create_cases()

◆ create_determine_function()

◆ create_distribution_law_over_case()

◆ create_new_constructors()

◆ create_projection_functions()

◆ dataspec()

◆ determine_affected_constructors()

◆ filter_illegal_characters()

◆ generate_case_function_equations()

◆ generate_determine_function_equations()

◆ generate_fresh_basic_sort()

◆ generate_fresh_function_symbol_name()

◆ generate_fresh_variable()

◆ generate_projection_function_equations()

◆ get_cache_element()

◆ get_constructors()

◆ get_projection_funcs()

◆ id_gen()

◆ is_cached()

◆ is_constructor()

Member Data Documentation

◆ m_cache

◆ m_data_equation_argument_generator

◆ m_dataspec

◆ m_identifier_generator

◆ m_possibly_inconsistent

◆ m_representative_generator