mcrl2::data::data_specification

Include file:

#include "mcrl2/data/data_specification.h
class mcrl2::data::data_specification

data specification.

Protected attributes

target_sort_to_function_map m_grouped_normalised_constructors

Cache normalised constructors grouped by target sort.

target_sort_to_function_map m_grouped_normalised_mappings

Cache normalised mappings grouped by target sort.

function_symbol_vector m_normalised_constructors

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

data_equation_vector m_normalised_equations

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

function_symbol_vector m_normalised_mappings

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

function_symbol_vector m_user_defined_constructors

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

std::vector<data_equation> m_user_defined_equations

The equations of the specification.

function_symbol_vector 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_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

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.

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

Indicates that the data specification is type checked.

This builds up internal data structures and allows access to the data specification using all the utility functions.

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

void load(std::istream &stream, bool binary = true, const std::string &source = "")

Reads a data specification from a stream.

Parameters:

  • stream An input stream.
  • binary An boolean that if true means the stream contains a term in binary encoding.
  • source The source from which the stream originates. Used for error messages.
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.

data_specification &operator=(const data_specification &other)
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 save(std::ostream &stream, bool binary = true) const

Writes the data specification to a stream.

Parameters:

  • stream The output stream.
  • binary If binary is true the data specification is saved in compressed binary format. Otherwise an ascii representation is saved. In general the binary format is much more compact than the ascii representation.
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.

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