mcrl2::data::sort_fbag Namespace Reference

Namespace for system defined sort fbag. More...

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

Functions
container_sort	fbag (const sort_expression &s)
	Constructor for sort expression FBag(S)
bool	is_fbag (const sort_expression &e)
	Recogniser for sort expression FBag(s)
const core::identifier_string &	empty_name ()
	Generate identifier {:}.
function_symbol	empty (const sort_expression &s)
	Constructor for function symbol {:}.
bool	is_empty_function_symbol (const atermpp::aterm &e)
	Recogniser for function {:}.
const core::identifier_string &	insert_name ()
	Generate identifier @fbag_insert.
function_symbol	insert (const sort_expression &s)
	Constructor for function symbol @fbag_insert.
bool	is_insert_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_insert.
application	insert (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @fbag_insert.
void	make_insert (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @fbag_insert.
bool	is_insert_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_insert.
function_symbol_vector	fbag_generate_constructors_code (const sort_expression &s)
	Give all system defined constructors for fbag.
function_symbol_vector	fbag_mCRL2_usable_constructors (const sort_expression &s)
	Give all defined constructors which can be used in mCRL2 specs for fbag.
implementation_map	fbag_cpp_implementable_constructors (const sort_expression &)
	Give all system defined constructors which have an implementation in C++ and not in rewrite rules for fbag.
const core::identifier_string &	cons_name ()
	Generate identifier @fbag_cons.
function_symbol	cons_ (const sort_expression &s)
	Constructor for function symbol @fbag_cons.
bool	is_cons_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_cons.
application	cons_ (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @fbag_cons.
void	make_cons (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @fbag_cons.
bool	is_cons_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_cons.
const core::identifier_string &	cinsert_name ()
	Generate identifier @fbag_cinsert.
function_symbol	cinsert (const sort_expression &s)
	Constructor for function symbol @fbag_cinsert.
bool	is_cinsert_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fbag_cinsert.
application	cinsert (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Application of function symbol @fbag_cinsert.
void	make_cinsert (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)
	Make an application of function symbol @fbag_cinsert.
bool	is_cinsert_application (const atermpp::aterm &e)
	Recogniser for application of @fbag_cinsert.
const core::identifier_string &	count_name ()
	Generate identifier count.
function_symbol	count (const sort_expression &s)
	Constructor for function symbol count.
bool	is_count_function_symbol (const atermpp::aterm &e)
	Recogniser for function count.
application	count (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Application of function symbol count.
void	make_count (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
	Make an application of function symbol count.
bool	is_count_application (const atermpp::aterm &e)
	Recogniser for application of count.
const core::identifier_string &	in_name ()
	Generate identifier in.
function_symbol	in (const sort_expression &s)
	Constructor for function symbol in.
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 &	fset2fbag_name ()
	Generate identifier @fset2fbag.
function_symbol	fset2fbag (const sort_expression &s)
	Constructor for function symbol @fset2fbag.
bool	is_fset2fbag_function_symbol (const atermpp::aterm &e)
	Recogniser for function @fset2fbag.
application	fset2fbag (const sort_expression &s, const data_expression &arg0)
	Application of function symbol @fset2fbag.
void	make_fset2fbag (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol @fset2fbag.
bool	is_fset2fbag_application (const atermpp::aterm &e)
	Recogniser for application of @fset2fbag.
const core::identifier_string &	union_name ()
	Generate identifier +.
function_symbol	union_ (const sort_expression &s)
	Constructor for function symbol +.
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)
	Constructor for function symbol *.
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)
	Constructor for function symbol -.
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 &	count_all_name ()
	Generate identifier #.
function_symbol	count_all (const sort_expression &s)
	Constructor for function symbol #.
bool	is_count_all_function_symbol (const atermpp::aterm &e)
	Recogniser for function #.
application	count_all (const sort_expression &s, const data_expression &arg0)
	Application of function symbol #.
void	make_count_all (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol #.
bool	is_count_all_application (const atermpp::aterm &e)
	Recogniser for application of #.
const core::identifier_string &	pick_name ()
	Generate identifier pick.
function_symbol	pick (const sort_expression &s)
	Constructor for function symbol pick.
bool	is_pick_function_symbol (const atermpp::aterm &e)
	Recogniser for function pick.
application	pick (const sort_expression &s, const data_expression &arg0)
	Application of function symbol pick.
void	make_pick (data_expression &result, const sort_expression &s, const data_expression &arg0)
	Make an application of function symbol pick.
bool	is_pick_application (const atermpp::aterm &e)
	Recogniser for application of pick.
function_symbol_vector	fbag_generate_functions_code (const sort_expression &s)
	Give all system defined mappings for fbag.
function_symbol_vector	fbag_generate_constructors_and_functions_code (const sort_expression &s)
	Give all system defined mappings and constructors for fbag.
function_symbol_vector	fbag_mCRL2_usable_mappings (const sort_expression &s)
	Give all system defined mappings that can be used in mCRL2 specs for fbag.
implementation_map	fbag_cpp_implementable_mappings (const sort_expression &)
	Give all system defined mappings that are to be implemented in C++ code for fbag.
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 &	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.
data_equation_vector	fbag_generate_equations_code (const sort_expression &s)
	Give all system defined equations for fbag.
template<typename Sequence >
application	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.
application	fbag (const sort_expression &s, const data_expression_list &range)
	Constructs a finite bag expression from a list of expressions.

Detailed Description

Namespace for system defined sort fbag.

Typedef Documentation

implementation_map

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

Definition at line 183 of file fbag1.h.

Function Documentation

arg()

const data_expression & mcrl2::data::sort_fbag::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 963 of file fbag1.h.

arg1()

const data_expression & mcrl2::data::sort_fbag::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 903 of file fbag1.h.

arg2()

const data_expression & mcrl2::data::sort_fbag::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 915 of file fbag1.h.

arg3()

const data_expression & mcrl2::data::sort_fbag::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 927 of file fbag1.h.

cinsert() [1/2]

function_symbol mcrl2::data::sort_fbag::cinsert ( const sort_expression &  s )

inline

Constructor for function symbol @fbag_cinsert.

Parameters

s	A sort expression.

Returns

Function symbol cinsert.

Definition at line 273 of file fbag1.h.

cinsert() [2/2]

application mcrl2::data::sort_fbag::cinsert ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @fbag_cinsert.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Returns

Application of @fbag_cinsert to a number of arguments.

Definition at line 299 of file fbag1.h.

cinsert_name()

const core::identifier_string & mcrl2::data::sort_fbag::cinsert_name ( )

inline

Generate identifier @fbag_cinsert.

Returns

Identifier @fbag_cinsert.

Definition at line 263 of file fbag1.h.

cons_() [1/2]

function_symbol mcrl2::data::sort_fbag::cons_ ( const sort_expression &  s )

inline

Constructor for function symbol @fbag_cons.

Parameters

s	A sort expression.

Returns

Function symbol cons_.

Definition at line 207 of file fbag1.h.

cons_() [2/2]

application mcrl2::data::sort_fbag::cons_ ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @fbag_cons.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Returns

Application of @fbag_cons to a number of arguments.

Definition at line 233 of file fbag1.h.

cons_name()

const core::identifier_string & mcrl2::data::sort_fbag::cons_name ( )

inline

Generate identifier @fbag_cons.

Returns

Identifier @fbag_cons.

Definition at line 197 of file fbag1.h.

count() [1/2]

function_symbol mcrl2::data::sort_fbag::count ( const sort_expression &  s )

inline

Constructor for function symbol count.

Parameters

s	A sort expression.

Returns

Function symbol count.

Definition at line 339 of file fbag1.h.

count() [2/2]

application mcrl2::data::sort_fbag::count ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Application of function symbol count.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of count to a number of arguments.

Definition at line 364 of file fbag1.h.

count_all() [1/2]

function_symbol mcrl2::data::sort_fbag::count_all ( const sort_expression &  s )

inline

Constructor for function symbol #.

Parameters

s	A sort expression.

Returns

Function symbol count_all.

Definition at line 721 of file fbag1.h.

count_all() [2/2]

application mcrl2::data::sort_fbag::count_all ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol #.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of # to a number of arguments.

Definition at line 745 of file fbag1.h.

count_all_name()

const core::identifier_string & mcrl2::data::sort_fbag::count_all_name ( )

inline

Generate identifier #.

Returns

Identifier #.

Definition at line 711 of file fbag1.h.

count_name()

const core::identifier_string & mcrl2::data::sort_fbag::count_name ( )

inline

Generate identifier count.

Returns

Identifier count.

Definition at line 329 of file fbag1.h.

difference() [1/2]

function_symbol mcrl2::data::sort_fbag::difference ( const sort_expression &  s )

inline

Constructor for function symbol -.

Parameters

s	A sort expression.

Returns

Function symbol difference.

Definition at line 657 of file fbag1.h.

difference() [2/2]

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

inline

Application of function symbol -.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of - to a number of arguments.

Definition at line 682 of file fbag1.h.

difference_name()

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

inline

Generate identifier -.

Returns

Identifier -.

Definition at line 647 of file fbag1.h.

empty()

function_symbol mcrl2::data::sort_fbag::empty ( const sort_expression &  s )

inline

Constructor for function symbol {:}.

Parameters

s	A sort expression.

Returns

Function symbol empty.

Definition at line 74 of file fbag1.h.

empty_name()

const core::identifier_string & mcrl2::data::sort_fbag::empty_name ( )

inline

Generate identifier {:}.

Returns

Identifier {:}.

Definition at line 64 of file fbag1.h.

fbag() [1/3]

container_sort mcrl2::data::sort_fbag::fbag ( const sort_expression &  s )

inline

Constructor for sort expression FBag(S)

Parameters

s	A sort expression

Returns

Sort expression fbag(s)

Definition at line 40 of file fbag1.h.

fbag() [2/3]

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

inline

Constructs a finite bag expression from a list of expressions.

Precondition

range must contain element, count, element, count, ...

Parameters

[in]	s	the sort of list elements
[in]	range	a range of elements of sort s.

Definition at line 419 of file standard_container_utility.h.

fbag() [3/3]

template<typename Sequence >

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

inline

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.

Precondition

range must contain element, count, element, count, ...

Parameters

[in]	s	the sort of list elements
[in]	range	a range of elements of sort s.

Definition at line 397 of file standard_container_utility.h.

fbag_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_fbag::fbag_cpp_implementable_constructors ( const sort_expression &  )

inline

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

Parameters

s	A sort expression.

Returns

All system defined constructors that are to be implemented in C++ for fbag.

Definition at line 188 of file fbag1.h.

fbag_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_fbag::fbag_cpp_implementable_mappings ( const sort_expression &  )

inline

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

Parameters

s	A sort expression

Returns

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

Definition at line 892 of file fbag1.h.

fbag_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_fbag::fbag_generate_constructors_and_functions_code ( const sort_expression &  s )

inline

Give all system defined mappings and constructors for fbag.

Parameters

s	A sort expression

Returns

All system defined mappings for fbag

Definition at line 855 of file fbag1.h.

fbag_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_fbag::fbag_generate_constructors_code ( const sort_expression &  s )

inline

Give all system defined constructors for fbag.

Parameters

s	A sort expression.

Returns

All system defined constructors for fbag.

Definition at line 162 of file fbag1.h.

fbag_generate_equations_code()

data_equation_vector mcrl2::data::sort_fbag::fbag_generate_equations_code ( const sort_expression &  s )

inline

Give all system defined equations for fbag.

Parameters

s	A sort expression

Returns

All system defined equations for sort fbag

Definition at line 973 of file fbag1.h.

fbag_generate_functions_code()

function_symbol_vector mcrl2::data::sort_fbag::fbag_generate_functions_code ( const sort_expression &  s )

inline

Give all system defined mappings for fbag.

Parameters

s	A sort expression

Returns

All system defined mappings for fbag

Definition at line 835 of file fbag1.h.

fbag_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_fbag::fbag_mCRL2_usable_constructors ( const sort_expression &  s )

inline

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

Parameters

s	A sort expression.

Returns

All system defined constructors that can be used in an mCRL2 specification for fbag.

Definition at line 174 of file fbag1.h.

fbag_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_fbag::fbag_mCRL2_usable_mappings ( const sort_expression &  s )

inline

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

Parameters

s	A sort expression

Returns

All system defined mappings for that can be used in mCRL2 specificationis fbag

Definition at line 869 of file fbag1.h.

fset2fbag() [1/2]

function_symbol mcrl2::data::sort_fbag::fset2fbag ( const sort_expression &  s )

inline

Constructor for function symbol @fset2fbag.

Parameters

s	A sort expression.

Returns

Function symbol fset2fbag.

Definition at line 467 of file fbag1.h.

fset2fbag() [2/2]

application mcrl2::data::sort_fbag::fset2fbag ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol @fset2fbag.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of @fset2fbag to a number of arguments.

Definition at line 491 of file fbag1.h.

fset2fbag_name()

const core::identifier_string & mcrl2::data::sort_fbag::fset2fbag_name ( )

inline

Generate identifier @fset2fbag.

Returns

Identifier @fset2fbag.

Definition at line 457 of file fbag1.h.

in() [1/2]

function_symbol mcrl2::data::sort_fbag::in ( const sort_expression &  s )

inline

Constructor for function symbol in.

Parameters

s	A sort expression.

Returns

Function symbol in.

Definition at line 403 of file fbag1.h.

in() [2/2]

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

inline

Application of function symbol in.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of in to a number of arguments.

Definition at line 428 of file fbag1.h.

in_name()

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

inline

Generate identifier in.

Returns

Identifier in.

Definition at line 393 of file fbag1.h.

insert() [1/2]

function_symbol mcrl2::data::sort_fbag::insert ( const sort_expression &  s )

inline

Constructor for function symbol @fbag_insert.

Parameters

s	A sort expression.

Returns

Function symbol insert.

Definition at line 106 of file fbag1.h.

insert() [2/2]

application mcrl2::data::sort_fbag::insert ( const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Application of function symbol @fbag_insert.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Returns

Application of @fbag_insert to a number of arguments.

Definition at line 132 of file fbag1.h.

insert_name()

const core::identifier_string & mcrl2::data::sort_fbag::insert_name ( )

inline

Generate identifier @fbag_insert.

Returns

Identifier @fbag_insert.

Definition at line 96 of file fbag1.h.

intersection() [1/2]

function_symbol mcrl2::data::sort_fbag::intersection ( const sort_expression &  s )

inline

Constructor for function symbol *.

Parameters

s	A sort expression.

Returns

Function symbol intersection.

Definition at line 593 of file fbag1.h.

intersection() [2/2]

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

inline

Application of function symbol *.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of * to a number of arguments.

Definition at line 618 of file fbag1.h.

intersection_name()

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

inline

Generate identifier *.

Returns

Identifier *.

Definition at line 583 of file fbag1.h.

is_cinsert_application()

bool mcrl2::data::sort_fbag::is_cinsert_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fbag_cinsert.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol cinsert to a number of arguments.

Definition at line 321 of file fbag1.h.

is_cinsert_function_symbol()

bool mcrl2::data::sort_fbag::is_cinsert_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fbag_cinsert.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fbag_cinsert.

Definition at line 283 of file fbag1.h.

is_cons_application()

bool mcrl2::data::sort_fbag::is_cons_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fbag_cons.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol cons_ to a number of arguments.

Definition at line 255 of file fbag1.h.

is_cons_function_symbol()

bool mcrl2::data::sort_fbag::is_cons_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fbag_cons.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fbag_cons.

Definition at line 217 of file fbag1.h.

is_count_all_application()

bool mcrl2::data::sort_fbag::is_count_all_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 count_all to a number of arguments.

Definition at line 765 of file fbag1.h.

is_count_all_function_symbol()

bool mcrl2::data::sort_fbag::is_count_all_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 731 of file fbag1.h.

is_count_application()

bool mcrl2::data::sort_fbag::is_count_application ( const atermpp::aterm &  e )

inline

Recogniser for application of count.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol count to a number of arguments.

Definition at line 385 of file fbag1.h.

is_count_function_symbol()

bool mcrl2::data::sort_fbag::is_count_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function count.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching count.

Definition at line 349 of file fbag1.h.

is_difference_application()

bool mcrl2::data::sort_fbag::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 703 of file fbag1.h.

is_difference_function_symbol()

bool mcrl2::data::sort_fbag::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 667 of file fbag1.h.

is_empty_function_symbol()

bool mcrl2::data::sort_fbag::is_empty_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 84 of file fbag1.h.

is_fbag()

bool mcrl2::data::sort_fbag::is_fbag ( const sort_expression &  e )

inline

Recogniser for sort expression FBag(s)

Parameters

e	A sort expression

Returns

true iff e is a container sort of which the name matches fbag

Definition at line 51 of file fbag1.h.

is_fset2fbag_application()

bool mcrl2::data::sort_fbag::is_fset2fbag_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fset2fbag.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol fset2fbag to a number of arguments.

Definition at line 511 of file fbag1.h.

is_fset2fbag_function_symbol()

bool mcrl2::data::sort_fbag::is_fset2fbag_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fset2fbag.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fset2fbag.

Definition at line 477 of file fbag1.h.

is_in_application()

bool mcrl2::data::sort_fbag::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 449 of file fbag1.h.

is_in_function_symbol()

bool mcrl2::data::sort_fbag::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 413 of file fbag1.h.

is_insert_application()

bool mcrl2::data::sort_fbag::is_insert_application ( const atermpp::aterm &  e )

inline

Recogniser for application of @fbag_insert.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol insert to a number of arguments.

Definition at line 154 of file fbag1.h.

is_insert_function_symbol()

bool mcrl2::data::sort_fbag::is_insert_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function @fbag_insert.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching @fbag_insert.

Definition at line 116 of file fbag1.h.

is_intersection_application()

bool mcrl2::data::sort_fbag::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 639 of file fbag1.h.

is_intersection_function_symbol()

bool mcrl2::data::sort_fbag::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 603 of file fbag1.h.

is_pick_application()

bool mcrl2::data::sort_fbag::is_pick_application ( const atermpp::aterm &  e )

inline

Recogniser for application of pick.

Parameters

e	A data expression.

Returns

true iff e is an application of function symbol pick to a number of arguments.

Definition at line 827 of file fbag1.h.

is_pick_function_symbol()

bool mcrl2::data::sort_fbag::is_pick_function_symbol ( const atermpp::aterm &  e )

inline

Recogniser for function pick.

Parameters

e	A data expression.

Returns

true iff e is the function symbol matching pick.

Definition at line 793 of file fbag1.h.

is_union_application()

bool mcrl2::data::sort_fbag::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 575 of file fbag1.h.

is_union_function_symbol()

bool mcrl2::data::sort_fbag::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 539 of file fbag1.h.

left()

const data_expression & mcrl2::data::sort_fbag::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 939 of file fbag1.h.

make_cinsert()

void mcrl2::data::sort_fbag::make_cinsert ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @fbag_cinsert.

Parameters

[out]	result	The data expression where the @fbag_cinsert expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Definition at line 311 of file fbag1.h.

make_cons()

void mcrl2::data::sort_fbag::make_cons ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @fbag_cons.

Parameters

[out]	result	The data expression where the @fbag_cons expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Definition at line 245 of file fbag1.h.

make_count()

void mcrl2::data::sort_fbag::make_count ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1  )

inline

Make an application of function symbol count.

Parameters

[out]	result	The data expression where the count expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 375 of file fbag1.h.

make_count_all()

void mcrl2::data::sort_fbag::make_count_all ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol #.

Parameters

[out]	result	The data expression where the # expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 755 of file fbag1.h.

make_difference()

void mcrl2::data::sort_fbag::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

[out]	result	The data expression where the - expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 693 of file fbag1.h.

make_fset2fbag()

void mcrl2::data::sort_fbag::make_fset2fbag ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol @fset2fbag.

Parameters

[out]	result	The data expression where the @fset2fbag expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 501 of file fbag1.h.

make_in()

void mcrl2::data::sort_fbag::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

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

Definition at line 439 of file fbag1.h.

make_insert()

void mcrl2::data::sort_fbag::make_insert ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0, const data_expression &  arg1, const data_expression &  arg2  )

inline

Make an application of function symbol @fbag_insert.

Parameters

[out]	result	The data expression where the @fbag_insert expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.
[in]	arg2	A data expression.

Definition at line 144 of file fbag1.h.

make_intersection()

void mcrl2::data::sort_fbag::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

[out]	result	The data expression where the * expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 629 of file fbag1.h.

make_pick()

void mcrl2::data::sort_fbag::make_pick ( data_expression &  result, const sort_expression &  s, const data_expression &  arg0  )

inline

Make an application of function symbol pick.

Parameters

[out]	result	The data expression where the pick expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.

Definition at line 817 of file fbag1.h.

make_union()

void mcrl2::data::sort_fbag::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

[out]	result	The data expression where the + expression is put.
[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Definition at line 565 of file fbag1.h.

pick() [1/2]

function_symbol mcrl2::data::sort_fbag::pick ( const sort_expression &  s )

inline

Constructor for function symbol pick.

Parameters

s	A sort expression.

Returns

Function symbol pick.

Definition at line 783 of file fbag1.h.

pick() [2/2]

application mcrl2::data::sort_fbag::pick ( const sort_expression &  s, const data_expression &  arg0  )

inline

Application of function symbol pick.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.

Returns

Application of pick to a number of arguments.

Definition at line 807 of file fbag1.h.

pick_name()

const core::identifier_string & mcrl2::data::sort_fbag::pick_name ( )

inline

Generate identifier pick.

Returns

Identifier pick.

Definition at line 773 of file fbag1.h.

right()

const data_expression & mcrl2::data::sort_fbag::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 951 of file fbag1.h.

union_() [1/2]

function_symbol mcrl2::data::sort_fbag::union_ ( const sort_expression &  s )

inline

Constructor for function symbol +.

Parameters

s	A sort expression.

Returns

Function symbol union_.

Definition at line 529 of file fbag1.h.

union_() [2/2]

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

inline

Application of function symbol +.

Parameters

[in]	s	A sort expression.
[in]	arg0	A data expression.
[in]	arg1	A data expression.

Returns

Application of + to a number of arguments.

Definition at line 554 of file fbag1.h.

union_name()

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

inline

Generate identifier +.

Returns

Identifier +.

Definition at line 519 of file fbag1.h.