mcrl2::data::sort_set Namespace Reference

Namespace for system defined sort set_. More...

Typedefs
typedef std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > >	implementation_map

Functions
container_sort	set_ (const sort_expression &s)
	Constructor for sort expression Set(S)
bool	is_set (const sort_expression &e)
	Recogniser for sort expression Set(s)
const core::identifier_string &	constructor_name ()
	Generate identifier @set.
function_symbol	constructor (const sort_expression &s)
	Constructor for function symbol @set.
bool	is_constructor_function_symbol (const atermpp::aterm &e)
	Recogniser for function @set.
application	constructor (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @set.
void	make_constructor (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol @set.
bool	is_constructor_application (const atermpp::aterm &e)
	Recogniser for application of @set.
function_symbol_vector	set_generate_constructors_code (const sort_expression &s)
	Give all system defined constructors for set_.
function_symbol_vector	set_mCRL2_usable_constructors (const sort_expression &s)
	Give all defined constructors which can be used in mCRL2 specs for set_.
implementation_map	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_.
const core::identifier_string &	set_fset_name ()
	Generate identifier @setfset.
function_symbol	set_fset (const sort_expression &s)
	Constructor for function symbol @setfset.
bool	is_set_fset_function_symbol (const atermpp::aterm &e)
	Recogniser for function @setfset.
application	set_fset (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @setfset.
void	make_set_fset (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @setfset.
bool	is_set_fset_application (const atermpp::aterm &e)
	Recogniser for application of @setfset.
const core::identifier_string &	set_comprehension_name ()
	Generate identifier @setcomp.
function_symbol	set_comprehension (const sort_expression &s)
	Constructor for function symbol @setcomp.
bool	is_set_comprehension_function_symbol (const atermpp::aterm &e)
	Recogniser for function @setcomp.
application	set_comprehension (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @setcomp.
void	make_set_comprehension (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @setcomp.
bool	is_set_comprehension_application (const atermpp::aterm &e)
	Recogniser for application of @setcomp.
const core::identifier_string &	in_name ()
	Generate identifier in.
function_symbol	in (const sort_expression &, const sort_expression &s0, const sort_expression &s1)
bool	is_in_function_symbol (const atermpp::aterm &e)
	Recogniser for function in.
application	in (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol in.
void	make_in (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol in.
bool	is_in_application (const atermpp::aterm &e)
	Recogniser for application of in.
const core::identifier_string &	complement_name ()
	Generate identifier !.
function_symbol	complement (const sort_expression &s)
	Constructor for function symbol !.
bool	is_complement_function_symbol (const atermpp::aterm &e)
	Recogniser for function !.
application	complement (const sort_expression &s, const data_expression &arg0)
	Application of function symbol !.
void	make_complement (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol !.
bool	is_complement_application (const atermpp::aterm &e)
	Recogniser for application of !.
const core::identifier_string &	union_name ()
	Generate identifier +.
function_symbol	union_ (const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
bool	is_union_function_symbol (const atermpp::aterm &e)
	Recogniser for function +.
application	union_ (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol +.
void	make_union_ (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol +.
bool	is_union_application (const atermpp::aterm &e)
	Recogniser for application of +.
const core::identifier_string &	intersection_name ()
	Generate identifier *.
function_symbol	intersection (const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
bool	is_intersection_function_symbol (const atermpp::aterm &e)
	Recogniser for function *.
application	intersection (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol *.
void	make_intersection (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol *.
bool	is_intersection_application (const atermpp::aterm &e)
	Recogniser for application of *.
const core::identifier_string &	difference_name ()
	Generate identifier -.
function_symbol	difference (const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
bool	is_difference_function_symbol (const atermpp::aterm &e)
	Recogniser for function -.
application	difference (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol -.
void	make_difference (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol -.
bool	is_difference_application (const atermpp::aterm &e)
	Recogniser for application of -.
const core::identifier_string &	false_function_name ()
	Generate identifier @false_.
function_symbol	false_function (const sort_expression &s)
	Constructor for function symbol @false_.
bool	is_false_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @false_.
application	false_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @false_.
void	make_false_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @false_.
bool	is_false_function_application (const atermpp::aterm &e)
	Recogniser for application of @false_.
const core::identifier_string &	true_function_name ()
	Generate identifier @true_.
function_symbol	true_function (const sort_expression &s)
	Constructor for function symbol @true_.
bool	is_true_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @true_.
application	true_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @true_.
void	make_true_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @true_.
bool	is_true_function_application (const atermpp::aterm &e)
	Recogniser for application of @true_.
const core::identifier_string &	not_function_name ()
	Generate identifier @not_.
function_symbol	not_function (const sort_expression &s)
	Constructor for function symbol @not_.
bool	is_not_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @not_.
application	not_function (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @not_.
void	make_not_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @not_.
bool	is_not_function_application (const atermpp::aterm &e)
	Recogniser for application of @not_.
const core::identifier_string &	and_function_name ()
	Generate identifier @and_.
function_symbol	and_function (const sort_expression &s)
	Constructor for function symbol @and_.
bool	is_and_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @and_.
application	and_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @and_.
void	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_.
bool	is_and_function_application (const atermpp::aterm &e)
	Recogniser for application of @and_.
const core::identifier_string &	or_function_name ()
	Generate identifier @or_.
function_symbol	or_function (const sort_expression &s)
	Constructor for function symbol @or_.
bool	is_or_function_function_symbol (const atermpp::aterm &e)
	Recogniser for function @or_.
application	or_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol @or_.
void	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_.
bool	is_or_function_application (const atermpp::aterm &e)
	Recogniser for application of @or_.
const core::identifier_string &	fset_union_name ()
	Generate identifier @fset_union.
function_symbol	fset_union (const sort_expression &s)
	Constructor for function symbol @fset_union.
bool	is_fset_union_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_union.
application	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.
void	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.
bool	is_fset_union_application (const atermpp::aterm &e)
	Recogniser for application of @fset_union.
const core::identifier_string &	fset_intersection_name ()
	Generate identifier @fset_inter.
function_symbol	fset_intersection (const sort_expression &s)
	Constructor for function symbol @fset_inter.
bool	is_fset_intersection_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset_inter.
application	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.
void	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.
bool	is_fset_intersection_application (const atermpp::aterm &e)
	Recogniser for application of @fset_inter.
function_symbol_vector	set_generate_functions_code (const sort_expression &s)
	Give all system defined mappings for set_.
function_symbol_vector	set_generate_constructors_and_functions_code (const sort_expression &s)
	Give all system defined mappings and constructors for set_.
function_symbol_vector	set_mCRL2_usable_mappings (const sort_expression &s)
	Give all system defined mappings that can be used in mCRL2 specs for set_.
implementation_map	set_cpp_implementable_mappings (const sort_expression &s)
	Give all system defined mappings that are to be implemented in C++ code for set_.
const data_expression &	left (const data_expression &e)
	Function for projecting out argument. left from an application.
const data_expression &	right (const data_expression &e)
	Function for projecting out argument. right from an application.
const data_expression &	arg (const data_expression &e)
	Function for projecting out argument. arg from an application.
const data_expression &	arg1 (const data_expression &e)
	Function for projecting out argument. arg1 from an application.
const data_expression &	arg2 (const data_expression &e)
	Function for projecting out argument. arg2 from an application.
const data_expression &	arg3 (const data_expression &e)
	Function for projecting out argument. arg3 from an application.
const data_expression &	arg4 (const data_expression &e)
	Function for projecting out argument. arg4 from an application.
data_equation_vector	set_generate_equations_code (const sort_expression &s)
	Give all system defined equations for set_.
core::identifier_string const &	set_enumeration_name ()
	Generate identifier set_enumeration.
function_symbol	set_enumeration (const sort_expression &s)
	Constructor for function symbol set_enumeration.
bool	is_set_enumeration_function_symbol (const atermpp::aterm &e)
	Recogniser for function set_enumeration.
template<typename Sequence >
data_expression	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.
data_expression	set_enumeration (const sort_expression &s, data_expression_list const &range)
	Application of function symbol set_enumeration.
bool	is_set_enumeration_application (const atermpp::aterm &e)
	Recogniser for application of set_enumeration.

Detailed Description

Namespace for system defined sort set_.

Typedef Documentation

implementation_map

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

Definition at line 149 of file set1.h.

Function Documentation

and_function() [1/2]

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

inline

Constructor for function symbol @and_.

Parameters

s	A sort expression.

Returns

Function symbol and_function.

Definition at line 853 of file set1.h.

and_function() [2/2]

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

inline

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.

Definition at line 878 of file set1.h.

and_function_name()

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

inline

Generate identifier @and_.

Returns

Identifier @and_.

Definition at line 843 of file set1.h.

arg()

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

inline

Function for projecting out argument. arg from an application.

Parameters

e	A data expression.

Precondition

arg is defined for e.

Returns

The argument of e that corresponds to arg.

Definition at line 1214 of file set1.h.

arg1()

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

inline

Function for projecting out argument. arg1 from an application.

Parameters

e	A data expression.

Precondition

arg1 is defined for e.

Returns

The argument of e that corresponds to arg1.

Definition at line 1226 of file set1.h.

arg2()

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

inline

Function for projecting out argument. arg2 from an application.

Parameters

e	A data expression.

Precondition

arg2 is defined for e.

Returns

The argument of e that corresponds to arg2.

Definition at line 1238 of file set1.h.

arg3()

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

inline

Function for projecting out argument. arg3 from an application.

Parameters

e	A data expression.

Precondition

arg3 is defined for e.

Returns

The argument of e that corresponds to arg3.

Definition at line 1250 of file set1.h.

arg4()

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

inline

Function for projecting out argument. arg4 from an application.

Parameters

e	A data expression.

Precondition

arg4 is defined for e.

Returns

The argument of e that corresponds to arg4.

Definition at line 1262 of file set1.h.

complement() [1/2]

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

inline

Constructor for function symbol !.

Parameters

s	A sort expression.

Returns

Function symbol complement.

Definition at line 362 of file set1.h.

complement() [2/2]

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

inline

Application of function symbol !.

Parameters

s	A sort expression.
arg0	A data expression.

Returns

Application of ! to a number of arguments.

Definition at line 386 of file set1.h.

complement_name()

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

inline

Generate identifier !.

Returns

Identifier !.

Definition at line 352 of file set1.h.

constructor() [1/2]

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

inline

Constructor for function symbol @set.

Parameters

s	A sort expression.

Returns

Function symbol constructor.

Definition at line 76 of file set1.h.

constructor() [2/2]

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

inline

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.

Definition at line 101 of file set1.h.

constructor_name()

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

inline

Generate identifier @set.

Returns

Identifier @set.

Definition at line 66 of file set1.h.

difference() [1/2]

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

inline

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.

Definition at line 628 of file set1.h.

difference() [2/2]

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

inline

Definition at line 584 of file set1.h.

difference_name()

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

inline

Generate identifier -.

Returns

Identifier -.

Definition at line 576 of file set1.h.

false_function() [1/2]

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

inline

Constructor for function symbol @false_.

Parameters

s	A sort expression.

Returns

Function symbol false_function.

Definition at line 667 of file set1.h.

false_function() [2/2]

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

inline

Application of function symbol @false_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns

Application of @false_ to a number of arguments.

Definition at line 691 of file set1.h.

false_function_name()

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

inline

Generate identifier @false_.

Returns

Identifier @false_.

Definition at line 657 of file set1.h.

fset_intersection() [1/2]

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

inline

Constructor for function symbol @fset_inter.

Parameters

s	A sort expression.

Returns

Function symbol fset_intersection.

Definition at line 1049 of file set1.h.

fset_intersection() [2/2]

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  )

inline

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.

Definition at line 1076 of file set1.h.

fset_intersection_name()

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

inline

Generate identifier @fset_inter.

Returns

Identifier @fset_inter.

Definition at line 1039 of file set1.h.

fset_union() [1/2]

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

inline

Constructor for function symbol @fset_union.

Parameters

s	A sort expression.

Returns

Function symbol fset_union.

Definition at line 981 of file set1.h.

fset_union() [2/2]

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  )

inline

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.

Definition at line 1008 of file set1.h.

fset_union_name()

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

inline

Generate identifier @fset_union.

Returns

Identifier @fset_union.

Definition at line 971 of file set1.h.

in() [1/2]

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

inline

Definition at line 296 of file set1.h.

in() [2/2]

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

inline

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.

Definition at line 323 of file set1.h.

in_name()

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

inline

Generate identifier in.

Returns

Identifier in.

Definition at line 288 of file set1.h.

intersection() [1/2]

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

inline

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.

Definition at line 547 of file set1.h.

intersection() [2/2]

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

inline

Definition at line 499 of file set1.h.

intersection_name()

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

inline

Generate identifier *.

Returns

Identifier *.

Definition at line 491 of file set1.h.

is_and_function_application()

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

inline

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.

Definition at line 899 of file set1.h.

is_and_function_function_symbol()

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

inline

Recogniser for function @and_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @and_.

Definition at line 863 of file set1.h.

is_complement_application()

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

inline

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.

Definition at line 406 of file set1.h.

is_complement_function_symbol()

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

inline

Recogniser for function !.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching !.

Definition at line 372 of file set1.h.

is_constructor_application()

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

inline

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.

Definition at line 122 of file set1.h.

is_constructor_function_symbol()

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

inline

Recogniser for function @set.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @set.

Definition at line 86 of file set1.h.

is_difference_application()

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

inline

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.

Definition at line 649 of file set1.h.

is_difference_function_symbol()

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

inline

Recogniser for function -.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching -.

Definition at line 612 of file set1.h.

is_false_function_application()

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

inline

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.

Definition at line 711 of file set1.h.

is_false_function_function_symbol()

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

inline

Recogniser for function @false_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @false_.

Definition at line 677 of file set1.h.

is_fset_intersection_application()

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

inline

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.

Definition at line 1099 of file set1.h.

is_fset_intersection_function_symbol()

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

inline

Recogniser for function @fset_inter.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_inter.

Definition at line 1059 of file set1.h.

is_fset_union_application()

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

inline

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.

Definition at line 1031 of file set1.h.

is_fset_union_function_symbol()

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

inline

Recogniser for function @fset_union.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset_union.

Definition at line 991 of file set1.h.

is_in_application()

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

inline

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.

Definition at line 344 of file set1.h.

is_in_function_symbol()

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

inline

Recogniser for function in.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching in.

Definition at line 307 of file set1.h.

is_intersection_application()

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

inline

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.

Definition at line 568 of file set1.h.

is_intersection_function_symbol()

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

inline

Recogniser for function *.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching *.

Definition at line 531 of file set1.h.

is_not_function_application()

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

inline

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.

Definition at line 835 of file set1.h.

is_not_function_function_symbol()

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

inline

Recogniser for function @not_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @not_.

Definition at line 801 of file set1.h.

is_or_function_application()

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

inline

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.

Definition at line 963 of file set1.h.

is_or_function_function_symbol()

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

inline

Recogniser for function @or_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @or_.

Definition at line 927 of file set1.h.

is_set()

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

inline

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_

Definition at line 53 of file set1.h.

is_set_comprehension_application()

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

inline

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.

Definition at line 280 of file set1.h.

is_set_comprehension_function_symbol()

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

inline

Recogniser for function @setcomp.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @setcomp.

Definition at line 246 of file set1.h.

is_set_enumeration_application()

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

inline

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

Definition at line 226 of file standard_container_utility.h.

is_set_enumeration_function_symbol()

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

inline

Recogniser for function set_enumeration.

Parameters

e	A data expression

Returns

true iff e is the function symbol matching set_enumeration

Definition at line 167 of file standard_container_utility.h.

is_set_fset_application()

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

inline

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.

Definition at line 218 of file set1.h.

is_set_fset_function_symbol()

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

inline

Recogniser for function @setfset.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @setfset.

Definition at line 184 of file set1.h.

is_true_function_application()

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

inline

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.

Definition at line 773 of file set1.h.

is_true_function_function_symbol()

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

inline

Recogniser for function @true_.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @true_.

Definition at line 739 of file set1.h.

is_union_application()

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

inline

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.

Definition at line 483 of file set1.h.

is_union_function_symbol()

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

inline

Recogniser for function +.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching +.

Definition at line 446 of file set1.h.

left()

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

inline

Function for projecting out argument. left from an application.

Parameters

e	A data expression.

Precondition

left is defined for e.

Returns

The argument of e that corresponds to left.

Definition at line 1190 of file set1.h.

make_and_function()

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

inline

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.

Definition at line 889 of file set1.h.

make_complement()

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

inline

Make an application of function symbol !.

Parameters

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

Definition at line 396 of file set1.h.

make_constructor()

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

inline

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.

Definition at line 112 of file set1.h.

make_difference()

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

inline

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.

Definition at line 639 of file set1.h.

make_false_function()

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

inline

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.

Definition at line 701 of file set1.h.

make_fset_intersection()

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  )

inline

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.

Definition at line 1089 of file set1.h.

make_fset_union()

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  )

inline

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.

Definition at line 1021 of file set1.h.

make_in()

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

inline

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.

Definition at line 334 of file set1.h.

make_intersection()

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

inline

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.

Definition at line 558 of file set1.h.

make_not_function()

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

inline

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.

Definition at line 825 of file set1.h.

make_or_function()

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

inline

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.

Definition at line 953 of file set1.h.

make_set_comprehension()

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

inline

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.

Definition at line 270 of file set1.h.

make_set_fset()

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

inline

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.

Definition at line 208 of file set1.h.

make_true_function()

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

inline

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.

Definition at line 763 of file set1.h.

make_union_()

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

inline

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.

Definition at line 473 of file set1.h.

not_function() [1/2]

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

inline

Constructor for function symbol @not_.

Parameters

s	A sort expression.

Returns

Function symbol not_function.

Definition at line 791 of file set1.h.

not_function() [2/2]

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

inline

Application of function symbol @not_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns

Application of @not_ to a number of arguments.

Definition at line 815 of file set1.h.

not_function_name()

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

inline

Generate identifier @not_.

Returns

Identifier @not_.

Definition at line 781 of file set1.h.

or_function() [1/2]

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

inline

Constructor for function symbol @or_.

Parameters

s	A sort expression.

Returns

Function symbol or_function.

Definition at line 917 of file set1.h.

or_function() [2/2]

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

inline

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.

Definition at line 942 of file set1.h.

or_function_name()

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

inline

Generate identifier @or_.

Returns

Identifier @or_.

Definition at line 907 of file set1.h.

right()

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

inline

Function for projecting out argument. right from an application.

Parameters

e	A data expression.

Precondition

right is defined for e.

Returns

The argument of e that corresponds to right.

Definition at line 1202 of file set1.h.

set_()

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

inline

Constructor for sort expression Set(S)

Parameters

s	A sort expression

Returns

Sort expression set_(s)

Definition at line 42 of file set1.h.

set_comprehension() [1/2]

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

inline

Constructor for function symbol @setcomp.

Parameters

s	A sort expression.

Returns

Function symbol set_comprehension.

Definition at line 236 of file set1.h.

set_comprehension() [2/2]

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

inline

Application of function symbol @setcomp.

Parameters

s	A sort expression.
arg0	A data expression.

Returns

Application of @setcomp to a number of arguments.

Definition at line 260 of file set1.h.

set_comprehension_name()

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

inline

Generate identifier @setcomp.

Returns

Identifier @setcomp.

Definition at line 226 of file set1.h.

set_cpp_implementable_constructors()

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

inline

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_.

Definition at line 154 of file set1.h.

set_cpp_implementable_mappings()

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

inline

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_

Definition at line 1178 of file set1.h.

set_enumeration() [1/3]

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

inline

Constructor for function symbol set_enumeration.

Parameters

s	A sort expression

Returns

Function symbol set_enumeration

Definition at line 157 of file standard_container_utility.h.

set_enumeration() [2/3]

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

inline

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.

Definition at line 206 of file standard_container_utility.h.

set_enumeration() [3/3]

template<typename Sequence >

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  )

inline

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.

Definition at line 185 of file standard_container_utility.h.

set_enumeration_name()

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

inline

Generate identifier set_enumeration.

Returns

Identifier set_enumeration

Definition at line 147 of file standard_container_utility.h.

set_fset() [1/2]

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

inline

Constructor for function symbol @setfset.

Parameters

s	A sort expression.

Returns

Function symbol set_fset.

Definition at line 174 of file set1.h.

set_fset() [2/2]

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

inline

Application of function symbol @setfset.

Parameters

s	A sort expression.
arg0	A data expression.

Returns

Application of @setfset to a number of arguments.

Definition at line 198 of file set1.h.

set_fset_name()

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

inline

Generate identifier @setfset.

Returns

Identifier @setfset.

Definition at line 164 of file set1.h.

set_generate_constructors_and_functions_code()

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

inline

Give all system defined mappings and constructors for set_.

Parameters

s	A sort expression

Returns

All system defined mappings for set_

Definition at line 1134 of file set1.h.

set_generate_constructors_code()

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

inline

Give all system defined constructors for set_.

Parameters

s	A sort expression.

Returns

All system defined constructors for set_.

Definition at line 130 of file set1.h.

set_generate_equations_code()

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

inline

Give all system defined equations for set_.

Parameters

s	A sort expression

Returns

All system defined equations for sort set_

Definition at line 1272 of file set1.h.

set_generate_functions_code()

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

inline

Give all system defined mappings for set_.

Parameters

s	A sort expression

Returns

All system defined mappings for set_

Definition at line 1107 of file set1.h.

set_mCRL2_usable_constructors()

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

inline

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_.

Definition at line 141 of file set1.h.

set_mCRL2_usable_mappings()

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

inline

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_

Definition at line 1148 of file set1.h.

true_function() [1/2]

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

inline

Constructor for function symbol @true_.

Parameters

s	A sort expression.

Returns

Function symbol true_function.

Definition at line 729 of file set1.h.

true_function() [2/2]

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

inline

Application of function symbol @true_.

Parameters

s	A sort expression.
arg0	A data expression.

Returns

Application of @true_ to a number of arguments.

Definition at line 753 of file set1.h.

true_function_name()

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

inline

Generate identifier @true_.

Returns

Identifier @true_.

Definition at line 719 of file set1.h.

union_() [1/2]

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

inline

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.

Definition at line 462 of file set1.h.

union_() [2/2]

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

inline

Definition at line 422 of file set1.h.

union_name()

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

inline

Generate identifier +.

Returns

Identifier +.

Definition at line 414 of file set1.h.