set.h¶

Include file:

#include "mcrl2/data/set.h"

The standard sort set_.

This file was generated from the data sort specification mcrl2/data/build/set.spec.

Typedefs¶

type mcrl2::data::sort_set::implementation_map¶: typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >

Functions¶

function_symbol mcrl2::data::sort_set::and_function(const sort_expression &s)¶

Constructor for function symbol @and_.

Parameters:

s A sort expression.

Returns: Function symbol and_function.

application mcrl2::data::sort_set::and_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol @and_.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of @and_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::and_function_name()¶

Generate identifier @and_.

Returns: Identifier @and_.

const data_expression &mcrl2::data::sort_set::arg(const data_expression &e)¶

Function for projecting out argument. arg from an application.

Parameters:

e A data expression.

Pre: arg is defined for e.

Returns: The argument of e that corresponds to arg.

const data_expression &mcrl2::data::sort_set::arg1(const data_expression &e)¶

Function for projecting out argument. arg1 from an application.

Parameters:

e A data expression.

Pre: arg1 is defined for e.

Returns: The argument of e that corresponds to arg1.

const data_expression &mcrl2::data::sort_set::arg2(const data_expression &e)¶

Function for projecting out argument. arg2 from an application.

Parameters:

e A data expression.

Pre: arg2 is defined for e.

Returns: The argument of e that corresponds to arg2.

const data_expression &mcrl2::data::sort_set::arg3(const data_expression &e)¶

Function for projecting out argument. arg3 from an application.

Parameters:

e A data expression.

Pre: arg3 is defined for e.

Returns: The argument of e that corresponds to arg3.

const data_expression &mcrl2::data::sort_set::arg4(const data_expression &e)¶

Function for projecting out argument. arg4 from an application.

Parameters:

e A data expression.

Pre: arg4 is defined for e.

Returns: The argument of e that corresponds to arg4.

function_symbol mcrl2::data::sort_set::complement(const sort_expression &s)¶

Constructor for function symbol !.

Parameters:

s A sort expression.

Returns: Function symbol complement.

application mcrl2::data::sort_set::complement(const sort_expression &s, const data_expression &arg0)¶

Application of function symbol !.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of ! to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::complement_name()¶

Generate identifier !.

Returns: Identifier !.

function_symbol mcrl2::data::sort_set::constructor(const sort_expression &s)¶

Constructor for function symbol @set.

Parameters:

s A sort expression.

Returns: Function symbol constructor.

application mcrl2::data::sort_set::constructor(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol @set.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of @set to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::constructor_name()¶

Generate identifier @set.

Returns: Identifier @set.

application mcrl2::data::sort_set::difference(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol -.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of - to a number of arguments.

function_symbol mcrl2::data::sort_set::difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_set::difference_name()¶

Generate identifier -.

Returns: Identifier -.

function_symbol mcrl2::data::sort_set::false_function(const sort_expression &s)¶

Constructor for function symbol @false_.

Parameters:

s A sort expression.

Returns: Function symbol false_function.

application mcrl2::data::sort_set::false_function(const sort_expression &s, const data_expression &arg0)¶

Application of function symbol @false_.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of @false_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::false_function_name()¶

Generate identifier @false_.

Returns: Identifier @false_.

function_symbol mcrl2::data::sort_set::fset_intersection(const sort_expression &s)¶

Constructor for function symbol @fset_inter.

Parameters:

s A sort expression.

Returns: Function symbol fset_intersection.

application mcrl2::data::sort_set::fset_intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)¶

Application of function symbol @fset_inter.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.
arg2 A data expression.
arg3 A data expression.

Returns: Application of @fset_inter to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::fset_intersection_name()¶

Generate identifier @fset_inter.

Returns: Identifier @fset_inter.

function_symbol mcrl2::data::sort_set::fset_union(const sort_expression &s)¶

Constructor for function symbol @fset_union.

Parameters:

s A sort expression.

Returns: Function symbol fset_union.

application mcrl2::data::sort_set::fset_union(const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)¶

Application of function symbol @fset_union.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.
arg2 A data expression.
arg3 A data expression.

Returns: Application of @fset_union to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::fset_union_name()¶

Generate identifier @fset_union.

Returns: Identifier @fset_union.

function_symbol mcrl2::data::sort_set::in(const sort_expression&, const sort_expression &s0, const sort_expression &s1)¶

application mcrl2::data::sort_set::in(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol in.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of in to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::in_name()¶

Generate identifier in.

Returns: Identifier in.

application mcrl2::data::sort_set::intersection(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol *.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of * to a number of arguments.

function_symbol mcrl2::data::sort_set::intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_set::intersection_name()¶

Generate identifier *.

Returns: Identifier *.

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

Recogniser for application of @and_.

Parameters:

e A data expression.

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

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

Recogniser for function @and_.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @and_.

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

Recogniser for application of !.

Parameters:

e A data expression.

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

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

Recogniser for function !.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching !.

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

Recogniser for application of @set.

Parameters:

e A data expression.

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

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

Recogniser for function @set.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @set.

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

Recogniser for application of -.

Parameters:

e A data expression.

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

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

Recogniser for function -.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching -.

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

Recogniser for application of @false_.

Parameters:

e A data expression.

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

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

Recogniser for function @false_.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @false_.

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

Recogniser for application of @fset_inter.

Parameters:

e A data expression.

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

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

Recogniser for function @fset_inter.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @fset_inter.

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

Recogniser for application of @fset_union.

Parameters:

e A data expression.

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

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

Recogniser for function @fset_union.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @fset_union.

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

Recogniser for application of in.

Parameters:

e A data expression.

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

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

Recogniser for function in.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching in.

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

Recogniser for application of *.

Parameters:

e A data expression.

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

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

Recogniser for function *.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching *.

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

Recogniser for application of @not_.

Parameters:

e A data expression.

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

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

Recogniser for function @not_.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @not_.

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

Recogniser for application of @or_.

Parameters:

e A data expression.

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

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

Recogniser for function @or_.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @or_.

bool mcrl2::data::sort_set::is_set(const sort_expression &e)¶

Recogniser for sort expression Set(s)

Parameters:

e A sort expression

Returns: true iff e is a container sort of which the name matches set_

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

Recogniser for application of @setcomp.

Parameters:

e A data expression.

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

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

Recogniser for function @setcomp.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @setcomp.

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

Recogniser for application of @setfset.

Parameters:

e A data expression.

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

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

Recogniser for function @setfset.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @setfset.

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

Recogniser for application of @true_.

Parameters:

e A data expression.

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

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

Recogniser for function @true_.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching @true_.

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

Recogniser for application of +.

Parameters:

e A data expression.

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

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

Recogniser for function +.

Parameters:

e A data expression.

Returns: true iff e is the function symbol matching +.

const data_expression &mcrl2::data::sort_set::left(const data_expression &e)¶

Function for projecting out argument. left from an application.

Parameters:

e A data expression.

Pre: left is defined for e.

Returns: The argument of e that corresponds to left.

void mcrl2::data::sort_set::make_and_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol @and_.

Parameters:

result The data expression where the @and_ expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_set::make_complement(data_expression &result, const sort_expression &s, const data_expression &arg0)¶

Make an application of function symbol !.

Parameters:

result The data expression where the ! expression is put.
s A sort expression.
arg0 A data expression.

void mcrl2::data::sort_set::make_constructor(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol @set.

Parameters:

result The data expression where the @set expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_set::make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol -.

Parameters:

result The data expression where the - expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_set::make_false_function(data_expression &result, const sort_expression &s, const data_expression &arg0)¶

Make an application of function symbol @false_.

Parameters:

result The data expression where the @false_ expression is put.
s A sort expression.
arg0 A data expression.

void mcrl2::data::sort_set::make_fset_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)¶

Make an application of function symbol @fset_inter.

Parameters:

result The data expression where the @fset_inter expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.
arg2 A data expression.
arg3 A data expression.

void mcrl2::data::sort_set::make_fset_union(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)¶

Make an application of function symbol @fset_union.

Parameters:

result The data expression where the @fset_union expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.
arg2 A data expression.
arg3 A data expression.

void mcrl2::data::sort_set::make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol in.

Parameters:

result The data expression where the in expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_set::make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol *.

Parameters:

result The data expression where the * expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_set::make_not_function(data_expression &result, const sort_expression &s, const data_expression &arg0)¶

Make an application of function symbol @not_.

Parameters:

result The data expression where the @not_ expression is put.
s A sort expression.
arg0 A data expression.

void mcrl2::data::sort_set::make_or_function(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol @or_.

Parameters:

result The data expression where the @or_ expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_set::make_set_comprehension(data_expression &result, const sort_expression &s, const data_expression &arg0)¶

Make an application of function symbol @setcomp.

Parameters:

result The data expression where the @setcomp expression is put.
s A sort expression.
arg0 A data expression.

void mcrl2::data::sort_set::make_set_fset(data_expression &result, const sort_expression &s, const data_expression &arg0)¶

Make an application of function symbol @setfset.

Parameters:

result The data expression where the @setfset expression is put.
s A sort expression.
arg0 A data expression.

void mcrl2::data::sort_set::make_true_function(data_expression &result, const sort_expression &s, const data_expression &arg0)¶

Make an application of function symbol @true_.

Parameters:

result The data expression where the @true_ expression is put.
s A sort expression.
arg0 A data expression.

void mcrl2::data::sort_set::make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol +.

Parameters:

result The data expression where the + expression is put.
s A sort expression.
arg0 A data expression.
arg1 A data expression.

function_symbol mcrl2::data::sort_set::not_function(const sort_expression &s)¶

Constructor for function symbol @not_.

Parameters:

s A sort expression.

Returns: Function symbol not_function.

application mcrl2::data::sort_set::not_function(const sort_expression &s, const data_expression &arg0)¶

Application of function symbol @not_.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of @not_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::not_function_name()¶

Generate identifier @not_.

Returns: Identifier @not_.

function_symbol mcrl2::data::sort_set::or_function(const sort_expression &s)¶

Constructor for function symbol @or_.

Parameters:

s A sort expression.

Returns: Function symbol or_function.

application mcrl2::data::sort_set::or_function(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol @or_.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of @or_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::or_function_name()¶

Generate identifier @or_.

Returns: Identifier @or_.

const data_expression &mcrl2::data::sort_set::right(const data_expression &e)¶

Function for projecting out argument. right from an application.

Parameters:

e A data expression.

Pre: right is defined for e.

Returns: The argument of e that corresponds to right.

container_sort mcrl2::data::sort_set::set_(const sort_expression &s)¶

Constructor for sort expression Set(S)

Parameters:

s A sort expression

Returns: Sort expression set_(s)

function_symbol mcrl2::data::sort_set::set_comprehension(const sort_expression &s)¶

Constructor for function symbol @setcomp.

Parameters:

s A sort expression.

Returns: Function symbol set_comprehension.

application mcrl2::data::sort_set::set_comprehension(const sort_expression &s, const data_expression &arg0)¶

Application of function symbol @setcomp.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of @setcomp to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::set_comprehension_name()¶

Generate identifier @setcomp.

Returns: Identifier @setcomp.

implementation_map mcrl2::data::sort_set::set_cpp_implementable_constructors(const sort_expression &s)¶

Give all system defined constructors which have an implementation in C++ and not in rewrite rules for set_.

Parameters:

s A sort expression.

Returns: All system defined constructors that are to be implemented in C++ for set_.

implementation_map mcrl2::data::sort_set::set_cpp_implementable_mappings(const sort_expression &s)¶

Give all system defined mappings that are to be implemented in C++ code for set_.

Parameters:

s A sort expression

Returns: A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for set_

function_symbol mcrl2::data::sort_set::set_fset(const sort_expression &s)¶

Constructor for function symbol @setfset.

Parameters:

s A sort expression.

Returns: Function symbol set_fset.

application mcrl2::data::sort_set::set_fset(const sort_expression &s, const data_expression &arg0)¶

Application of function symbol @setfset.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of @setfset to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::set_fset_name()¶

Generate identifier @setfset.

Returns: Identifier @setfset.

function_symbol_vector mcrl2::data::sort_set::set_generate_constructors_and_functions_code(const sort_expression &s)¶

Give all system defined mappings and constructors for set_.

Parameters:

s A sort expression

Returns: All system defined mappings for set_

function_symbol_vector mcrl2::data::sort_set::set_generate_constructors_code(const sort_expression &s)¶

Give all system defined constructors for set_.

Parameters:

s A sort expression.

Returns: All system defined constructors for set_.

data_equation_vector mcrl2::data::sort_set::set_generate_equations_code(const sort_expression &s)¶

Give all system defined equations for set_.

Parameters:

s A sort expression

Returns: All system defined equations for sort set_

function_symbol_vector mcrl2::data::sort_set::set_generate_functions_code(const sort_expression &s)¶

Give all system defined mappings for set_.

Parameters:

s A sort expression

Returns: All system defined mappings for set_

function_symbol_vector mcrl2::data::sort_set::set_mCRL2_usable_constructors(const sort_expression &s)¶

Give all defined constructors which can be used in mCRL2 specs for set_.

Parameters:

s A sort expression.

Returns: All system defined constructors that can be used in an mCRL2 specification for set_.

function_symbol_vector mcrl2::data::sort_set::set_mCRL2_usable_mappings(const sort_expression &s)¶

Give all system defined mappings that can be used in mCRL2 specs for set_.

Parameters:

s A sort expression

Returns: All system defined mappings for that can be used in mCRL2 specificationis set_

function_symbol mcrl2::data::sort_set::true_function(const sort_expression &s)¶

Constructor for function symbol @true_.

Parameters:

s A sort expression.

Returns: Function symbol true_function.

application mcrl2::data::sort_set::true_function(const sort_expression &s, const data_expression &arg0)¶

Application of function symbol @true_.

Parameters:

s A sort expression.
arg0 A data expression.

Returns: Application of @true_ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_set::true_function_name()¶

Generate identifier @true_.

Returns: Identifier @true_.

application mcrl2::data::sort_set::union_(const sort_expression &s, const data_expression &arg0, const data_expression &arg1)¶

Application of function symbol +.

Parameters:

s A sort expression.
arg0 A data expression.
arg1 A data expression.

Returns: Application of + to a number of arguments.

function_symbol mcrl2::data::sort_set::union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_set::union_name()¶

Generate identifier +.

Returns: Identifier +.

mcrl2/data/set.h¶

Typedefs¶

Functions¶

Table of Contents

Previous topic

Next topic

This page