mcrl2/data/data_specification.h

Include file:

#include "mcrl2/data/data_specification.h"

The class data_specification.

Functions

function_symbol mcrl2::data::find_constructor(data_specification const &data, std::string const &s)

Finds a constructor in a data specification.

Parameters:

  • data A data specification

  • s A string

Returns: The found constructor

data_equation_vector mcrl2::data::find_equations(data_specification const &specification, const data_expression &d)

Gets all equations with a data expression as head on one of its sides.

Parameters:

  • specification A data specification.

  • d A data expression.

Returns: All equations with d as head in one of its sides.

function_symbol mcrl2::data::find_mapping(data_specification const &data, std::string const &s)

Finds a mapping in a data specification.

Parameters:

  • data A data specification

  • s A string

Returns: The found mapping

sort_expression mcrl2::data::find_sort(data_specification const &data, std::string const &s)

Finds a sort in a data specification.

Parameters:

  • data A data specification

  • s A string

Returns: The found sort

std::set<core::identifier_string> mcrl2::data::function_and_mapping_identifiers(const data_specification &dataspec)

Returns the names of functions and mappings that occur in a data specification.

Parameters:

  • dataspec A data specification

bool mcrl2::data::is_data_specification(const atermpp::aterm_appl &x)

Test for a data specification expression.

Parameters:

  • x A term

Returns: True if x is a data specification expression

data::data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
data::variable_list normalize_sorts(const variable_list &x, const data::sort_specification &sortspec)
data::data_equation normalize_sorts(const data::data_equation &x, const data::sort_specification &sortspec)
data::data_equation_list normalize_sorts(const data_equation_list &x, const data::sort_specification &sortspec)
void normalize_sorts(data_equation_vector &x, const data::sort_specification &sortspec)
data_specification mcrl2::data::operator+(data_specification spec1, const data_specification &spec2)

Merges two data specifications into one.

It is assumed that the two specs can be merged. I.e. that the second is a safe extension of the first.

Parameters:

  • spec1 One of the input specifications.

  • spec2 The second input specification.

Returns: A specification that is merged.

std::ostream &mcrl2::data::operator<<(std::ostream &out, const data_specification &x)

Outputs the object to a stream.

Parameters:

  • out An output stream

  • x Object x

Returns: The output stream

variable_list mcrl2::data::order_variables_to_optimise_enumeration(const variable_list &l, const data_specification &data_spec)

Order the variables in a variable list such that enumeration over these variables becomes more efficient.

Parameters:

  • l A list of variables that are to be sorted.

  • data_spec A data specification containing the constructors that are used to determine efficiency.

Returns: The same list of variables but ordered in such a way that

std::string pp(const data::data_specification &x)