mCRL2
Loading...
Searching...
No Matches
mcrl2::data::data_specification Class Reference

data specification. More...

#include <data_specification.h>

Inheritance diagram for mcrl2::data::data_specification:
mcrl2::data::sort_specification

Public Types

typedef std::map< function_symbol, std::pair< std::function< 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_appl &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_vectorconstructors () const
 Gets all constructors including those that are system defined.
 
const function_symbol_vectoruser_defined_constructors () const
 Gets the constructors defined by the user, excluding those that are system defined.
 
const function_symbol_vectorconstructors (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_vectormappings () const
 Gets all mappings in this specification including those that are system defined.
 
const function_symbol_vectoruser_defined_mappings () const
 Gets all user defined mappings in this specification.
 
const function_symbol_vectormappings (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_mapcpp_implemented_functions () const
 Gets all equations in this specification including those that are system defined.
 
const data_equation_vectoruser_defined_equations () const
 Gets all user defined equations.
 
data_equation_vectoruser_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_vectoruser_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_vectoruser_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_equationm_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_expressionm_normalised_sorts
 Set containing all the sorts, including the system defined ones.
 
std::set< sort_expressionm_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_expressionm_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<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_appl t)
inline

Constructor from an aterm.

Parameters
[in]ta 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 821 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]fA 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]eAn 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]fA 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]fA 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]eAn 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]fA 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]sA 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]s1A sort expression
[in]s2A 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 516 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 721 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]sortA sort expression that is representing the structured sort.
[out]constructorsTo this set the new constructors are added.
[out]mappingsNew mappings are added to this set.
[out]equationsNew equations for the structured sort are added to this set.
[in]skip_equationsThis 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]sA sort expression
Returns
true if s can be determined to be finite, false otherwise.
Parameters
[in]sA 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]sA 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 747 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]sA 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]fA 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]eAn 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]fA 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: