mcrl2/data/function_sort.h

Include file:

#include "mcrl2/data/function_sort.h"

The class function_sort.

Typedefs

type mcrl2::data::function_sort_list

typedef for atermpp::term_list< function_sort >

list of function sorts

type mcrl2::data::function_sort_vector

typedef for std::vector< function_sort >

vector of function sorts

Functions

function_sort mcrl2::data::make_function_sort(const sort_expression &dom1, const sort_expression &codomain)

Convenience constructor for function sort with domain size 1.

Parameters:

  • dom1 The first sort of the domain.
  • codomain The codomain of the sort.

Post: *this represents dom1 -> codomain

function_sort mcrl2::data::make_function_sort(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &codomain)

Convenience constructor for function sort with domain size 2.

Parameters:

  • dom1 The first sort of the domain.
  • dom2 The second sort of the domain.
  • codomain The codomain of the sort.

Post: *this represents dom1 # dom2 -> codomain

function_sort mcrl2::data::make_function_sort(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &codomain)

Convenience constructor for function sort with domain size 3.

Parameters:

  • dom1 The first sort of the domain.
  • dom2 The second sort of the domain.
  • dom3 The third sort of the domain.
  • codomain The codomain of the sort.

Post: *this represents dom1 # dom2 # dom3 -> codomain

function_sort mcrl2::data::make_function_sort(const sort_expression &dom1, const sort_expression &dom2, const sort_expression &dom3, const sort_expression &dom4, const sort_expression &codomain)

Convenience constructor for function sort with domain size 4.

Parameters:

  • dom1 The first sort of the domain.
  • dom2 The second sort of the domain.
  • dom3 The third sort of the domain.
  • dom4 The fourth sort of the domain.
  • codomain The codomain of the sort.

Post: *this represents dom1 # dom2 # dom3 # dom4 -> codomain

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

Outputs the object to a stream.

Parameters:

  • out An output stream
  • x Object x

Returns: The output stream

void mcrl2::data::swap(function_sort &t1, function_sort &t2)

swap overload