mcrl2/data/standard_container_utility.h

Include file:

#include "mcrl2/data/standard_container_utility.h"

Provides utilities for working with data expressions of standard container sorts.

Functions

function_symbol mcrl2::data::sort_bag::bag_enumeration(const sort_expression &s)

Constructor for function symbol bag_enumeration.

Parameters:

• s A sort expression

Returns: Function symbol bag_enumeration

data_expression mcrl2::data::sort_bag::bag_enumeration(const sort_expression &s, data_expression_list const &range)

Application of function symbol bag_enumeration.

Parameters:

• s A sort expression
• range A range of data expressions

Returns: Application of bag_enum to the data expressions in range.

data_expression mcrl2::data::sort_bag::bag_enumeration(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container<Sequence, data_expression>::type * = 0)

Application of function symbol bag_enumeration.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters:

• s A sort expression
• range A range of data expressions

Returns: Application of bag_enum to the data expressions in range.

core::identifier_string const &mcrl2::data::sort_bag::bag_enumeration_name()

Generate identifier bag_enumeration.

Returns: Identifier bag_enumeration

bool mcrl2::data::sort_bag::is_bag_enumeration_application(const atermpp::aterm_appl &e)

Recogniser for application of bag_enumeration.

Parameters:

• e A data expression

Returns: true iff e is an application of function symbol bag_enumeration to a number of arguments

bool mcrl2::data::sort_bag::is_bag_enumeration_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function bag_enumeration.

Parameters:

• e A data expression

Returns: true iff e is the function symbol matching bag_enumeration

Functions

application mcrl2::data::sort_fbag::fbag(const sort_expression &s, const data_expression_list &range)

Constructs a finite bag expression from a list of expressions.

Pre: range must contain element, count, element, count, …

Parameters:

• s the sort of list elements
• range a range of elements of sort s.

application mcrl2::data::sort_fbag::fbag(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container<Sequence, data_expression>::type * = nullptr)

Constructs a finite bag expression from a range of expressions Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Pre: range must contain element, count, element, count, …

Parameters:

• s the sort of list elements
• range a range of elements of sort s.

Functions

application mcrl2::data::sort_fset::fset(const sort_expression &s, const data_expression_list &range)

Constructs a finite set expression from a list of expressions.

Parameters:

• s the sort of list elements
• range a sequence of elements

application mcrl2::data::sort_fset::fset(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container<Sequence, data_expression>::type * = nullptr)

Constructs a finite set expression from a range of expressions.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters:

• s the sort of list elements
• range a sequence of elements

Functions

bool mcrl2::data::sort_list::is_list_enumeration_application(const atermpp::aterm_appl &e)

Recogniser for application of list_enumeration.

Parameters:

• e A data expression

Returns: true iff e is an application of function symbol list_enumeration to a number of arguments

bool mcrl2::data::sort_list::is_list_enumeration_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function list_enumeration.

Parameters:

• e A data expression

Returns: true iff e is the function symbol matching list_enumeration

application mcrl2::data::sort_list::list(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container<Sequence, data_expression>::type * = nullptr)

Constructs a list expression from a range of expressions.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters:

• s the sort of list elements
• range an iterator range of elements of sort s

function_symbol mcrl2::data::sort_list::list_enumeration(const sort_expression &s)

Constructor for function symbol list_enumeration.

Parameters:

• s A sort expression

Returns: Function symbol list_enumeration

data_expression mcrl2::data::sort_list::list_enumeration(const sort_expression &s, data_expression_list const &range)

Application of function symbol list_enumeration.

Parameters:

• s A sort expression
• range A range of data expressions

Returns: Application of list_enum to the data expressions in range.

data_expression mcrl2::data::sort_list::list_enumeration(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container<Sequence, data_expression>::type * = nullptr)

Application of function symbol list_enumeration.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters:

• s A sort expression
• range A range of data expressions

Returns: Application of list_enum to the data expressions in range.

core::identifier_string const &mcrl2::data::sort_list::list_enumeration_name()

Generate identifier list_enumeration.

Returns: Identifier list_enumeration

Functions

bool mcrl2::data::sort_set::is_set_enumeration_application(const atermpp::aterm_appl &e)

Recogniser for application of set_enumeration.

Parameters:

• e A data expression

Returns: true iff e is an application of function symbol set_enumeration to a number of arguments

bool mcrl2::data::sort_set::is_set_enumeration_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function set_enumeration.

Parameters:

• e A data expression

Returns: true iff e is the function symbol matching set_enumeration

function_symbol mcrl2::data::sort_set::set_enumeration(const sort_expression &s)

Constructor for function symbol set_enumeration.

Parameters:

• s A sort expression

Returns: Function symbol set_enumeration

data_expression mcrl2::data::sort_set::set_enumeration(const sort_expression &s, data_expression_list const &range)

Application of function symbol set_enumeration.

Parameters:

• s A sort expression
• range A range of data expressions

Returns: Application of set_enum to the data expressions in range.

data_expression mcrl2::data::sort_set::set_enumeration(const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container<Sequence, data_expression>::type * = 0)

Application of function symbol set_enumeration.

Type Sequence must be a model of the Forward Traversal Iterator concept; with value_type convertible to data_expression.

Parameters:

• s A sort expression
• range A range of data expressions

Returns: Application of set_enum to the data expressions in range.

core::identifier_string const &mcrl2::data::sort_set::set_enumeration_name()

Generate identifier set_enumeration.

Returns: Identifier set_enumeration