mcrl2::data::data_specification

Include file:

#include "mcrl2/data/data_specification.h

class mcrl2::data::data_specification

data specification.

Public types

type mcrl2::data::data_specification::implementation_map

typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >

Protected attributes

implementation_map mcrl2::data::data_specification::m_cpp_implemented_functions

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.

target_sort_to_function_map mcrl2::data::data_specification::m_grouped_normalised_constructors

Cache normalised constructors grouped by target sort.

target_sort_to_function_map mcrl2::data::data_specification::m_grouped_normalised_mappings

Cache normalised mappings grouped by target sort.

function_symbol_vector mcrl2::data::data_specification::m_normalised_constructors

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

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

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.

function_symbol_vector mcrl2::data::data_specification::m_normalised_mappings

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

function_symbol_vector mcrl2::data::data_specification::m_user_defined_constructors

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

data_equation_vector mcrl2::data::data_specification::m_user_defined_equations

The equations of the specification.

function_symbol_vector mcrl2::data::data_specification::m_user_defined_mappings

The mappings of the specification.

Protected member functions

void add_normalised_constructor(const function_symbol &f) const

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

Parameters:

• f A function symbol.

Pre: f does not yet occur in this specification.

Post: is_system_defined(f) == true .. note:: this operation does not invalidate iterators of constructors_const_range

void add_normalised_constructors(Iterator begin, Iterator end) const

void add_normalised_cpp_implemented_functions(const implementation_map &c) const

void add_normalised_equation(const data_equation &e) const

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

Parameters:

• e An equation.

Pre: e does not yet occur in this specification.

Post: is_system_defined(f) == true .. note:: this operation does not invalidate iterators of equations_const_range

void add_normalised_equations(Iterator begin, Iterator end) const

void add_normalised_mapping(const function_symbol &f) const

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

Parameters:

• f A function symbol.

Pre: f does not yet occur in this specification.

Post: is_system_defined(f) == true .. note:: this operation does not invalidate iterators of mappings_const_range

void add_normalised_mappings(Iterator begin, Iterator end) const

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

void data_is_not_necessarily_normalised_anymore() 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.

Parameters:

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

Public member functions

void add_constructor(const function_symbol &f)

Adds a constructor to this specification.

Parameters:

• f A function symbol.

Pre: a mapping f does not yet occur in this specification. .. note:: this operation does not invalidate iterators of constructors_const_range

void add_equation(const data_equation &e)

Adds an equation to this specification.

Parameters:

• e An equation.

Pre: e does not yet occur in this specification. .. note:: this operation does not invalidate iterators of equations_const_range

void add_mapping(const function_symbol &f)

Adds a mapping to this specification.

Parameters:

• f A function symbol.

Pre: a constructor f does not yet occur in this specification. .. note:: this operation does not invalidate iterators of mappings_const_range

const function_symbol_vector &constructors() const

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.

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.

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

Parameters:

• s A sort expression.

Returns: The constructors for sort s in this specification.

const implementation_map &cpp_implemented_functions() const

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.

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.

Parameters:

• t a term adhering to the internal format.

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.

bool equal_sorts(sort_expression const &s1, sort_expression const &s2) const

Checks whether two sort expressions represent the same sort.

Parameters:

• s1 A sort expression
• s2 A sort expression

const std::set<data_equation> &equations() const

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.

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.

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…

bool is_certainly_finite(const sort_expression &s) const

Checks whether a sort is certainly finite.

Parameters:

• s A sort expression

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

bool is_constructor_sort(const sort_expression &s) const

Checks whether a sort is a constructor sort.

Parameters:

• s A sort expression

Returns: true if s is a constructor sort

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

const function_symbol_vector &mappings() const

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.

const function_symbol_vector &mappings(const sort_expression &s) const

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

Parameters:

• s A sort expression.

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

bool operator==(const data_specification &other) const

void remove_constructor(const function_symbol &f)

Removes constructor from specification.

Note that this does not remove equations containing the constructor.

Parameters:

• f A constructor.

Pre: f occurs in the specification as constructor.

Post: 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

void remove_equation(const data_equation &e)

Removes equation from specification.

Parameters:

• e An equation.

Post: 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

void remove_mapping(const function_symbol &f)

Removes mapping from specification.

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

Parameters:

• f A function.

Post: 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

void translate_user_notation()

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.

const function_symbol_vector &user_defined_constructors() const

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

The time complexity for this operation is constant.

data_equation_vector &user_defined_equations()

const data_equation_vector &user_defined_equations() const

Gets all user defined equations.

The time complexity of this operation is constant.

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

const function_symbol_vector &user_defined_mappings() const

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.

Private member functions

void add_data_types_for_sorts() const

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.

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.

void normalise_data_specification_if_required() const