data specification. More...

#include <data_specification.h>

Inheritance diagram for mcrl2::data::data_specification:

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

Public Member Functions
	data_specification ()=default
	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_certainly_finite (const sort_expression_list &l) const
	Checks whether all sorts are certainly finite in a sort_expression_list.

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, 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, 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 49 of file data_specification.h.

Member Typedef Documentation

◆ implementation_map

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

Definition at line 52 of file data_specification.h.

Constructor & Destructor Documentation

◆ data_specification() [1/3]

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

default

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

◆ data_specification() [2/3]

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

inlineexplicit

Constructor from an aterm.

Parameters

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

Definition at line 316 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 855 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 450 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 508 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 480 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 465 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 178 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 216 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 242 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 210 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 234 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 194 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 225 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 333 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 354 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 420 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 163 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 648 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 408 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,
		bool	skip_equations = `false`
	)		const

private

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

Definition at line 529 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 752 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 575 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() [1/2]

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_certainly_finite() [2/2]

bool mcrl2::data::data_specification::is_certainly_finite ( const sort_expression_list & l ) const

inline

Checks whether all sorts are certainly finite in a sort_expression_list.

Parameters

[in] l A sort expression list

Returns: true if all sorts in the list l can be determined to be finite. false otherwise.

Definition at line 668 of file data_specification.h.

◆ 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 684 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 781 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 372 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 395 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 548 of file data_specification.h.

◆ operator==()

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

inline

Definition at line 699 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 611 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 636 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 624 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 493 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 343 of file data_specification.h.

◆ user_defined_equations() [1/2]

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

inline

Definition at line 439 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 432 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 384 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 159 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 136 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 143 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 133 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 150 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 140 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 123 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 129 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 126 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() [1/2]

◆ is_certainly_finite() [2/2]

◆ 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