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

void mcrl2::data::make_function_sort(atermpp::aterm_appl &t, const ARGUMENTS&... args)

brief Make_function_sort constructs a new term into a given address.

Parameters:

  • t The reference into which the new function_sort is constructed.
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)

brief Outputs the object to a stream param out An output stream param x Object x return The output stream

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

brief swap overload