data specification. More...

#include <data_specification.h>

Inheritance diagram for mcrl2::data::data_specification:

Public Types
typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > >	implementation_map

Public Member Functions
	data_specification ()
	Default constructor. Generate a data specification that contains only booleans and positive numbers.

	data_specification (const atermpp::aterm &t)
	Constructor from an aterm.

	data_specification (const basic_sort_vector &sorts, const alias_vector &aliases, const function_symbol_vector &constructors, const function_symbol_vector &user_defined_mappings, const data_equation_vector &user_defined_equations)
	Constructor from its members.

const function_symbol_vector &	constructors () const
	Gets all constructors including those that are system defined.

const function_symbol_vector &	user_defined_constructors () const
	Gets the constructors defined by the user, excluding those that are system defined.

const function_symbol_vector &	constructors (const sort_expression &s, const bool do_not_normalize=false) const
	Gets all constructors of a sort including those that are system defined.

const function_symbol_vector &	mappings () const
	Gets all mappings in this specification including those that are system defined.

const function_symbol_vector &	user_defined_mappings () const
	Gets all user defined mappings in this specification.

const function_symbol_vector &	mappings (const sort_expression &s) const
	Gets all mappings of a sort including those that are system defined.

const std::set< data_equation > &	equations () const
	Gets all equations in this specification including those that are system defined.

const implementation_map &	cpp_implemented_functions () const
	Gets all equations in this specification including those that are system defined.

const data_equation_vector &	user_defined_equations () const
	Gets all user defined equations.

data_equation_vector &	user_defined_equations ()

void	add_constructor (const function_symbol &f)
	Adds a constructor to this specification.

void	add_mapping (const function_symbol &f)
	Adds a mapping to this specification.

void	add_equation (const data_equation &e)
	Adds an equation to this specification.

void	translate_user_notation ()
	Translate user notation within the equations of the data specification.

void	get_system_defined_sorts_constructors_and_mappings (std::set< sort_expression > &sorts, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings) const
	This function provides a sample of all system defined sorts, constructors and mappings that contains at least one specimen of each sort and function symbol. Because types can be parameterised not all function symbols for all types are provided.

void	remove_constructor (const function_symbol &f)
	Removes constructor from specification.

void	remove_mapping (const function_symbol &f)
	Removes mapping from specification.

void	remove_equation (const data_equation &e)
	Removes equation from specification.

bool	equal_sorts (sort_expression const &s1, sort_expression const &s2) const
	Checks whether two sort expressions represent the same sort.

bool	is_certainly_finite (const sort_expression &s) const
	Checks whether a sort is certainly finite.

bool	is_constructor_sort (const sort_expression &s) const
	Checks whether a sort is a constructor sort.

bool	is_well_typed () const
	Returns true if.

bool	operator== (const data_specification &other) const

Public Member Functions inherited from mcrl2::data::sort_specification
	sort_specification ()
	Default constructor.

	sort_specification (const basic_sort_vector &sorts, const alias_vector &aliases)

void	add_sort (const basic_sort &s)
	Adds a sort to this specification.

void	add_system_defined_sort (const sort_expression &s)
	Adds a sort to this specification, and marks it as system defined.

void	add_context_sort (const sort_expression &s)
	Adds the sort s to the context sorts.

template<typename Container >
void	add_context_sorts (const Container &c, typename atermpp::enable_if_container< Container >::type *=nullptr)
	Adds the sorts in c to the context sorts.

void	remove_sort (const sort_expression &s)
	Removes sort from the user defined sorts in the specification. Note that this does not remove aliases for the sort, and it does not remove constructors, mappings and equations, and also keeps the sort as defined in the context.

const std::set< sort_expression > &	sorts () const
	Gets the normalised sort declarations including those that are system defined. This is the set with all sorts that occur in a data_specification, or that have been registered as sorts used in the context.

const std::set< sort_expression > &	context_sorts () const
	Return the user defined context sorts of the current specification.

const basic_sort_vector &	user_defined_sorts () const
	Gets all sorts defined by a user (excluding the system defined sorts).

void	add_alias (const alias &a)
	Adds an alias (new name for a sort) to this specification.

void	remove_alias (const alias &a)
	Removes a user defined //alias from specification.

const alias_vector &	user_defined_aliases () const
	Gets the user defined aliases.

const std::map< sort_expression, sort_expression > &	sort_alias_map () const
	Gets a normalisation mapping that maps each sort to its unique normalised sort.

bool	operator== (const sort_specification &other) const

Protected Member Functions
void	data_is_not_necessarily_normalised_anymore () const

void	add_normalised_constructor (const function_symbol &f) const
	Adds a constructor to this specification, and marks it as system defined.

void	add_normalised_mapping (const function_symbol &f) const
	Adds a mapping to this specification, and marks it as system defined.

void	add_normalised_equation (const data_equation &e) const
	Adds an equation to this specification, and marks it as system defined.

template<class Iterator >
void	add_normalised_constructors (Iterator begin, Iterator end) const

template<class Iterator >
void	add_normalised_mappings (Iterator begin, Iterator end) const

template<class Iterator >
void	add_normalised_equations (Iterator begin, Iterator end) const

void	add_normalised_cpp_implemented_functions (const implementation_map &c) const

void	insert_mappings_constructors_for_structured_sort (const structured_sort &sort, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
	Adds constructors, mappings and equations for a structured sort to this specification, and marks them as system defined.

void	add_standard_mappings_and_equations (const sort_expression &sort, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const

Protected Member Functions inherited from mcrl2::data::sort_specification
void	sorts_are_not_necessarily_normalised_anymore () const

void	data_is_not_necessarily_normalised_anymore () const

void	normalise_sort_specification_if_required () const

void	add_predefined_basic_sorts ()

template<class CONTAINER >
void	import_system_defined_sorts (const CONTAINER &sorts)

void	import_system_defined_sort (const sort_expression &sort)
	Adds the system defined sorts in a sequence. The second argument is used to check which sorts are added, to prevent useless repetitions of additions of sorts.

void	reconstruct_m_normalised_aliases () const

void	check_for_alias_loop (const sort_expression &s, std::set< sort_expression > sorts_already_seen, const bool toplevel=true) const

Protected Attributes
function_symbol_vector	m_user_defined_constructors
	A mapping of sort expressions to the constructors corresponding to that sort.

function_symbol_vector	m_user_defined_mappings
	The mappings of the specification.

data_equation_vector	m_user_defined_equations
	The equations of the specification.

function_symbol_vector	m_normalised_constructors
	Set containing all constructors, including the system defined ones. The types in these constructors are normalised.

target_sort_to_function_map	m_grouped_normalised_constructors
	Cache normalised constructors grouped by target sort.

function_symbol_vector	m_normalised_mappings
	Set containing system defined all mappings, including the system defined ones. The types in these mappings are normalised.

target_sort_to_function_map	m_grouped_normalised_mappings
	Cache normalised mappings grouped by target sort.

std::set< data_equation >	m_normalised_equations
	Table containing all equations, including the system defined ones. The sorts in these equations are normalised.

implementation_map	m_cpp_implemented_functions
	A map that for function symbols gives how it can be implemented.

Protected Attributes inherited from mcrl2::data::sort_specification
bool	m_normalised_sorts_are_up_to_date
	This boolean indicates whether the variables m_normalised_constructors, m_mappings, m_equations, m_normalised_sorts, m_normalised_aliases are up to date with respect to changes of this sort specification.

bool	m_normalised_data_is_up_to_date
	The variable below indicates whether a surrounding data specification is up to data with respect to sort normalisation and available sorts. This is set to false if an alias or a new sort is added.

basic_sort_vector	m_user_defined_sorts
	The basic sorts and structured sorts in the specification.

std::set< sort_expression >	m_normalised_sorts
	Set containing all the sorts, including the system defined ones.

std::set< sort_expression >	m_sorts_in_context
	The sorts that occur are needed in this sort specification but are not explicitly defined as user defined sorts. An example is the sort Nat when declaring the use of a sort List(Nat). The normalised sorts, constructors, mappings and equations are complete with respect to these sorts.

alias_vector	m_user_defined_aliases
	The basic sorts and structured sorts in the specification.

std::map< sort_expression, sort_expression >	m_normalised_aliases
	Table containing how sorts should be mapped to normalised sorts.

Private Member Functions
void	add_data_types_for_sorts () const
	Puts the constructors, functions and equations in normalised form in de data type.

void	normalise_data_specification_if_required () const

void	find_associated_system_defined_data_types_for_a_sort (const sort_expression &sort, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings, std::set< data_equation > &equations, implementation_map &cpp_implemented_functions, const bool skip_equations=false) const
	Adds the system defined sorts to the sets with constructors, mappings, and equations for.

void	import_data_type_for_system_defined_sort (const sort_expression &sort) const
	Adds the system defined sorts in a sequence. The second argument is used to check which sorts are added, to prevent useless repetitions of additions of sorts. The function normalise_sorts imports for the given sort_expression sort all sorts, constructors, mappings and equations that belong to this sort to the ‘normalised’ sets in this data type. E.g. for the sort Nat of natural numbers, it is required that Pos (positive numbers) are defined.

Detailed Description

data specification.

Definition at line 47 of file data_specification.h.

Member Typedef Documentation

◆ implementation_map

typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > mcrl2::data::data_specification::implementation_map

Definition at line 50 of file data_specification.h.

Constructor & Destructor Documentation

◆ data_specification() [1/3]

mcrl2::data::data_specification::data_specification ( )

inline

Default constructor. Generate a data specification that contains only booleans and positive numbers.

Definition at line 312 of file data_specification.h.

◆ data_specification() [2/3]

mcrl2::data::data_specification::data_specification ( const atermpp::aterm & t )

inline

Constructor from an aterm.

Parameters

[in] t a term adhering to the internal format.

Definition at line 318 of file data_specification.h.

◆ data_specification() [3/3]

mcrl2::data::data_specification::data_specification	(	const basic_sort_vector &	sorts,
		const alias_vector &	aliases,
		const function_symbol_vector &	constructors,
		const function_symbol_vector &	user_defined_mappings,
		const data_equation_vector &	user_defined_equations
	)

Constructor from its members.

Definition at line 852 of file data_specification.cpp.

Member Function Documentation

◆ add_constructor()

void mcrl2::data::data_specification::add_constructor ( const function_symbol & f )

inline

Adds a constructor to this specification.

Parameters

[in] f A function symbol.

Precondition: a mapping f does not yet occur in this specification.

Note: this operation does not invalidate iterators of constructors_const_range

Definition at line 452 of file data_specification.h.

◆ add_data_types_for_sorts()

void mcrl2::data::data_specification::add_data_types_for_sorts ( ) const

inlineprivate

Puts the constructors, functions and equations in normalised form in de data type.

See the function normalise_sorts on arbitrary objects for a more detailed description. All sorts in the constructors, mappings and equations are normalised.

Definition at line 510 of file data_specification.h.

◆ add_equation()

void mcrl2::data::data_specification::add_equation ( const data_equation & e )

inline

Adds an equation to this specification.

Parameters

[in] e An equation.

Precondition: e does not yet occur in this specification.

Note: this operation does not invalidate iterators of equations_const_range

Definition at line 482 of file data_specification.h.

◆ add_mapping()

void mcrl2::data::data_specification::add_mapping ( const function_symbol & f )

inline

Adds a mapping to this specification.

Parameters

[in] f A function symbol.

Precondition: a constructor f does not yet occur in this specification.

Note: this operation does not invalidate iterators of mappings_const_range

Definition at line 467 of file data_specification.h.

◆ add_normalised_constructor()

void mcrl2::data::data_specification::add_normalised_constructor ( const function_symbol & f ) const

inlineprotected

Adds a constructor to this specification, and marks it as system defined.

Parameters

[in] f A function symbol.

Precondition: f does not yet occur in this specification.

Postcondition: is_system_defined(f) == true

Note: this operation does not invalidate iterators of constructors_const_range

Definition at line 179 of file data_specification.h.

◆ add_normalised_constructors()

template<class Iterator >

void mcrl2::data::data_specification::add_normalised_constructors	(	Iterator	begin,
		Iterator	end
	)		const

inlineprotected

Definition at line 217 of file data_specification.h.

◆ add_normalised_cpp_implemented_functions()

void mcrl2::data::data_specification::add_normalised_cpp_implemented_functions ( const implementation_map & c ) const

inlineprotected

Definition at line 243 of file data_specification.h.

◆ add_normalised_equation()

void mcrl2::data::data_specification::add_normalised_equation ( const data_equation & e ) const

inlineprotected

Adds an equation to this specification, and marks it as system defined.

Parameters

[in] e An equation.

Precondition: e does not yet occur in this specification.

Postcondition: is_system_defined(f) == true

Note: this operation does not invalidate iterators of equations_const_range

Definition at line 211 of file data_specification.h.

◆ add_normalised_equations()

template<class Iterator >

void mcrl2::data::data_specification::add_normalised_equations	(	Iterator	begin,
		Iterator	end
	)		const

inlineprotected

Definition at line 235 of file data_specification.h.

◆ add_normalised_mapping()

void mcrl2::data::data_specification::add_normalised_mapping ( const function_symbol & f ) const

inlineprotected

Adds a mapping to this specification, and marks it as system defined.

Parameters

[in] f A function symbol.

Precondition: f does not yet occur in this specification.

Postcondition: is_system_defined(f) == true

Note: this operation does not invalidate iterators of mappings_const_range

Definition at line 195 of file data_specification.h.

◆ add_normalised_mappings()

template<class Iterator >

void mcrl2::data::data_specification::add_normalised_mappings	(	Iterator	begin,
		Iterator	end
	)		const

inlineprotected

Definition at line 226 of file data_specification.h.

◆ add_standard_mappings_and_equations()

void mcrl2::data::data_specification::add_standard_mappings_and_equations	(	const sort_expression &	sort,
		std::set< function_symbol > &	mappings,
		std::set< data_equation > &	equations,
		const bool	skip_equations
	)		const

inlineprotected

Definition at line 292 of file data_specification.h.

◆ constructors() [1/2]

const function_symbol_vector & mcrl2::data::data_specification::constructors ( ) const

inline

Gets all constructors including those that are system defined.

The time complexity is the same as for sorts().

Returns: All constructors in this specification, including those for structured sorts.

Definition at line 335 of file data_specification.h.

◆ constructors() [2/2]

const function_symbol_vector & mcrl2::data::data_specification::constructors	(	const sort_expression &	s,
		const bool	do_not_normalize = `false`
	)		const

inline

Gets all constructors of a sort including those that are system defined.

The time complexity is the same as for sorts().

Parameters

[in] s A sort expression.

Returns: The constructors for sort s in this specification.

Definition at line 356 of file data_specification.h.

◆ cpp_implemented_functions()

const implementation_map & mcrl2::data::data_specification::cpp_implemented_functions ( ) const

inline

Gets all equations in this specification including those that are system defined.

The time complexity of this operation is the same as that for sort().

Returns: All equations in this specification, including those for structured sorts.

Definition at line 422 of file data_specification.h.

◆ data_is_not_necessarily_normalised_anymore()

void mcrl2::data::data_specification::data_is_not_necessarily_normalised_anymore ( ) const

inlineprotected

Definition at line 164 of file data_specification.h.

◆ equal_sorts()

bool mcrl2::data::data_specification::equal_sorts	(	sort_expression const &	s1,
		sort_expression const &	s2
	)		const

inline

Checks whether two sort expressions represent the same sort.

Parameters

[in]	s1	A sort expression
[in]	s2	A sort expression

Definition at line 651 of file data_specification.h.

◆ equations()

const std::set< data_equation > & mcrl2::data::data_specification::equations ( ) const

inline

Gets all equations in this specification including those that are system defined.

The time complexity of this operation is the same as that for sort().

Returns: All equations in this specification, including those for structured sorts.

Definition at line 410 of file data_specification.h.

◆ find_associated_system_defined_data_types_for_a_sort()

void mcrl2::data::data_specification::find_associated_system_defined_data_types_for_a_sort	(	const sort_expression &	sort,
		std::set< function_symbol > &	constructors,
		std::set< function_symbol > &	mappings,
		std::set< data_equation > &	equations,
		implementation_map &	cpp_implemented_functions,
		const bool	skip_equations = `false`
	)		const

private

Adds the system defined sorts to the sets with constructors, mappings, and equations for.

Definition at line 526 of file data_specification.cpp.

◆ get_system_defined_sorts_constructors_and_mappings()

void mcrl2::data::data_specification::get_system_defined_sorts_constructors_and_mappings	(	std::set< sort_expression > &	sorts,
		std::set< function_symbol > &	constructors,
		std::set< function_symbol > &	mappings
	)		const

This function provides a sample of all system defined sorts, constructors and mappings that contains at least one specimen of each sort and function symbol. Because types can be parameterised not all function symbols for all types are provided.

The sorts, constructors and mappings for the following types are added: Bool, Pos, Int, Nat, Real, List(Pos), FSet(Pos), FBag(Pos), Set(Pos), Bag(Pos). How to deal with struct...

Definition at line 749 of file data_specification.cpp.

◆ import_data_type_for_system_defined_sort()

void mcrl2::data::data_specification::import_data_type_for_system_defined_sort ( const sort_expression & sort ) const

inlineprivate

Adds the system defined sorts in a sequence. The second argument is used to check which sorts are added, to prevent useless repetitions of additions of sorts. The function normalise_sorts imports for the given sort_expression sort all sorts, constructors, mappings and equations that belong to this sort to the ‘normalised’ sets in this data type. E.g. for the sort Nat of natural numbers, it is required that Pos (positive numbers) are defined.

Definition at line 578 of file data_specification.h.

◆ insert_mappings_constructors_for_structured_sort()

void mcrl2::data::data_specification::insert_mappings_constructors_for_structured_sort	(	const structured_sort &	sort,
		std::set< function_symbol > &	constructors,
		std::set< function_symbol > &	mappings,
		std::set< data_equation > &	equations,
		const bool	skip_equations
	)		const

inlineprotected

Adds constructors, mappings and equations for a structured sort to this specification, and marks them as system defined.

Parameters

[in]	sort	A sort expression that is representing the structured sort.
[out]	constructors	To this set the new constructors are added.
[out]	mappings	New mappings are added to this set.
[out]	equations	New equations for the structured sort are added to this set.
[in]	skip_equations	This boolean indicates whether equations are added.

Definition at line 262 of file data_specification.h.

◆ is_certainly_finite()

bool mcrl2::data::data_specification::is_certainly_finite ( const sort_expression & s ) const

Checks whether a sort is certainly finite.

Parameters

[in] s A sort expression

Returns: true if s can be determined to be finite, false otherwise.

Parameters

[in] s A sort expression

Returns: true if s can be determined to be finite, false otherwise.

Definition at line 137 of file data_specification.cpp.

◆ is_constructor_sort()

bool mcrl2::data::data_specification::is_constructor_sort ( const sort_expression & s ) const

inline

Checks whether a sort is a constructor sort.

Parameters

[in] s A sort expression

Returns: true if s is a constructor sort

Definition at line 670 of file data_specification.h.

◆ is_well_typed()

bool mcrl2::data::data_specification::is_well_typed ( ) const

Returns true if.

the domain and range sorts of constructors are contained in the list of sorts
the domain and range sorts of mappings are contained in the list of sorts

Returns: True if the data specification is well typed.

Definition at line 778 of file data_specification.cpp.

◆ mappings() [1/2]

const function_symbol_vector & mcrl2::data::data_specification::mappings ( ) const

inline

Gets all mappings in this specification including those that are system defined.

The time complexity is the same as for sorts().

Returns: All mappings in this specification, including recognisers and projection functions from structured sorts.

Definition at line 374 of file data_specification.h.

◆ mappings() [2/2]

const function_symbol_vector & mcrl2::data::data_specification::mappings ( const sort_expression & s ) const

inline

Gets all mappings of a sort including those that are system defined.

Parameters

[in] s A sort expression.

Returns: All mappings in this specification, for which s occurs as a right-hand side of the mapping's sort.

Definition at line 397 of file data_specification.h.

◆ normalise_data_specification_if_required()

void mcrl2::data::data_specification::normalise_data_specification_if_required ( ) const

inlineprivate

Definition at line 550 of file data_specification.h.

◆ operator==()

bool mcrl2::data::data_specification::operator== ( const data_specification & other ) const

inline

Definition at line 685 of file data_specification.h.

◆ remove_constructor()

void mcrl2::data::data_specification::remove_constructor ( const function_symbol & f )

inline

Removes constructor from specification.

Note that this does not remove equations containing the constructor.

Parameters

[in] f A constructor.

Precondition: f occurs in the specification as constructor.

Postcondition: f does not occur as constructor.

Note: this operation does not invalidate iterators of constructors_const_range, only if they point to the element that is removed

Definition at line 614 of file data_specification.h.

◆ remove_equation()

void mcrl2::data::data_specification::remove_equation ( const data_equation & e )

inline

Removes equation from specification.

Parameters

[in] e An equation.

Postcondition: e is removed from this specification.

Note: this operation does not invalidate iterators of equations_const_range, only if they point to the element that is removed

Definition at line 639 of file data_specification.h.

◆ remove_mapping()

void mcrl2::data::data_specification::remove_mapping ( const function_symbol & f )

inline

Removes mapping from specification.

Note that this does not remove equations in which the mapping occurs.

Parameters

[in] f A function.

Postcondition: f does not occur as constructor.

Note: this operation does not invalidate iterators of mappings_const_range, only if they point to the element that is removed

Definition at line 627 of file data_specification.h.

◆ translate_user_notation()

void mcrl2::data::data_specification::translate_user_notation ( )

inline

Translate user notation within the equations of the data specification.

This function replaces explicit numbers, lists, sets and bags by their counterpart in the data types. This function is to be invoked after type checking.

Definition at line 495 of file data_specification.h.

◆ user_defined_constructors()

const function_symbol_vector & mcrl2::data::data_specification::user_defined_constructors ( ) const

inline

Gets the constructors defined by the user, excluding those that are system defined.

The time complexity for this operation is constant.

Definition at line 345 of file data_specification.h.

◆ user_defined_equations() [1/2]

data_equation_vector & mcrl2::data::data_specification::user_defined_equations ( )

inline

Definition at line 441 of file data_specification.h.

◆ user_defined_equations() [2/2]

const data_equation_vector & mcrl2::data::data_specification::user_defined_equations ( ) const

inline

Gets all user defined equations.

The time complexity of this operation is constant.

Returns: All equations in this specification, including those for structured sorts.

Definition at line 434 of file data_specification.h.

◆ user_defined_mappings()

const function_symbol_vector & mcrl2::data::data_specification::user_defined_mappings ( ) const

inline

Gets all user defined mappings in this specification.

The time complexity is constant.

Returns: All mappings in this specification, including recognisers and projection functions from structured sorts.

Definition at line 386 of file data_specification.h.

Member Data Documentation

◆ m_cpp_implemented_functions

implementation_map mcrl2::data::data_specification::m_cpp_implemented_functions

mutableprotected

A map that for function symbols gives how it can be implemented.

For each function symbol there is a function : application -> data_expression that when applied to a term in normal form with the function symbol as head symbol returns a function that can be applied to calculate this term. Furthermore, it provides the name of a function that when applied to the number of arguments that the function expects can be used to rewrite the term. This last string can be used for code generation.

Definition at line 160 of file data_specification.h.

◆ m_grouped_normalised_constructors

target_sort_to_function_map mcrl2::data::data_specification::m_grouped_normalised_constructors

mutableprotected

Cache normalised constructors grouped by target sort.

Definition at line 137 of file data_specification.h.

◆ m_grouped_normalised_mappings

target_sort_to_function_map mcrl2::data::data_specification::m_grouped_normalised_mappings

mutableprotected

Cache normalised mappings grouped by target sort.

Definition at line 144 of file data_specification.h.

◆ m_normalised_constructors

function_symbol_vector mcrl2::data::data_specification::m_normalised_constructors

mutableprotected

Set containing all constructors, including the system defined ones. The types in these constructors are normalised.

Definition at line 134 of file data_specification.h.

◆ m_normalised_equations

std::set<data_equation> mcrl2::data::data_specification::m_normalised_equations

mutableprotected

Table containing all equations, including the system defined ones. The sorts in these equations are normalised.

The normalised equations are a set as the number of equations can become large, in which case removing duplicates while inserting equations can be very time consuming.

Definition at line 151 of file data_specification.h.

◆ m_normalised_mappings

function_symbol_vector mcrl2::data::data_specification::m_normalised_mappings

mutableprotected

Set containing system defined all mappings, including the system defined ones. The types in these mappings are normalised.

Definition at line 141 of file data_specification.h.

◆ m_user_defined_constructors

function_symbol_vector mcrl2::data::data_specification::m_user_defined_constructors

protected

A mapping of sort expressions to the constructors corresponding to that sort.

Definition at line 124 of file data_specification.h.

◆ m_user_defined_equations

data_equation_vector mcrl2::data::data_specification::m_user_defined_equations

protected

The equations of the specification.

Definition at line 130 of file data_specification.h.

◆ m_user_defined_mappings

function_symbol_vector mcrl2::data::data_specification::m_user_defined_mappings

protected

The mappings of the specification.

Definition at line 127 of file data_specification.h.

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

data/include/mcrl2/data/data_specification.h
data/source/data_specification.cpp

Public Types

Public Member Functions

Protected Member Functions

Protected Attributes

Private Member Functions

Detailed Description

Member Typedef Documentation

◆ implementation_map

Constructor & Destructor Documentation

◆ data_specification() [1/3]

◆ data_specification() [2/3]

◆ data_specification() [3/3]

Member Function Documentation

◆ add_constructor()

◆ add_data_types_for_sorts()

◆ add_equation()

◆ add_mapping()

◆ add_normalised_constructor()

◆ add_normalised_constructors()

◆ add_normalised_cpp_implemented_functions()

◆ add_normalised_equation()

◆ add_normalised_equations()

◆ add_normalised_mapping()

◆ add_normalised_mappings()

◆ add_standard_mappings_and_equations()

◆ constructors() [1/2]

◆ constructors() [2/2]

◆ cpp_implemented_functions()

◆ data_is_not_necessarily_normalised_anymore()

◆ equal_sorts()

◆ equations()

◆ find_associated_system_defined_data_types_for_a_sort()

◆ get_system_defined_sorts_constructors_and_mappings()

◆ import_data_type_for_system_defined_sort()

◆ insert_mappings_constructors_for_structured_sort()

◆ is_certainly_finite()

◆ is_constructor_sort()

◆ is_well_typed()

◆ mappings() [1/2]

◆ mappings() [2/2]

◆ normalise_data_specification_if_required()

◆ operator==()

◆ remove_constructor()

◆ remove_equation()

◆ remove_mapping()

◆ translate_user_notation()

◆ user_defined_constructors()

◆ user_defined_equations() [1/2]

◆ user_defined_equations() [2/2]

◆ user_defined_mappings()

Member Data Documentation

◆ m_cpp_implemented_functions

◆ m_grouped_normalised_constructors

◆ m_grouped_normalised_mappings

◆ m_normalised_constructors

◆ m_normalised_equations

◆ m_normalised_mappings

◆ m_user_defined_constructors

◆ m_user_defined_equations

◆ m_user_defined_mappings