Namespace for system defined sort fbag. More...

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

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 &s)
	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 #.

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 &s)
	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 186 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 904 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 844 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 856 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 868 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 277 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

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

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

Definition at line 303 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 267 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 211 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

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

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

Definition at line 237 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 201 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 343 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

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

Returns: Application of count to a number of arguments.

Definition at line 368 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 725 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

s	A sort expression.
arg0	A data expression.

Returns: Application of # to a number of arguments.

Definition at line 749 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 715 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 333 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 661 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

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

Returns: Application of - to a number of arguments.

Definition at line 686 of file fbag1.h.

◆ difference_name()

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

inline

Generate identifier -.

Returns: Identifier -.

Definition at line 651 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 77 of file fbag1.h.

◆ empty_name()

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

inline

Generate identifier {:}.

Returns: Identifier {:}.

Definition at line 67 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 43 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 420 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 398 of file standard_container_utility.h.

◆ fbag_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_fbag::fbag_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 fbag.

Parameters

s	A sort expression.

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

Definition at line 191 of file fbag1.h.

◆ fbag_cpp_implementable_mappings()

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

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 832 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 796 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 165 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 914 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 777 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 177 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 810 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 471 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

s	A sort expression.
arg0	A data expression.

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

Definition at line 495 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 461 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 407 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

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

Returns: Application of in to a number of arguments.

Definition at line 432 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 397 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 109 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

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

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

Definition at line 135 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 99 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 597 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

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

Returns: Application of * to a number of arguments.

Definition at line 622 of file fbag1.h.

◆ intersection_name()

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

inline

Generate identifier *.

Returns: Identifier *.

Definition at line 587 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 325 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 287 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 259 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 221 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 769 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 735 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 389 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 353 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 707 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 671 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 87 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 54 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 515 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 481 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 453 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 417 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 157 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 119 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 643 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 607 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 579 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 543 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 880 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

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

Definition at line 315 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

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

Definition at line 249 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

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

Definition at line 379 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

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

Definition at line 759 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

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

Definition at line 697 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

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

Definition at line 505 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

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 443 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

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

Definition at line 147 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

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

Definition at line 633 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

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

Definition at line 569 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 892 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 533 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

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

Returns: Application of + to a number of arguments.

Definition at line 558 of file fbag1.h.

◆ union_name()

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

inline

Generate identifier +.

Returns: Identifier +.

Definition at line 523 of file fbag1.h.

Typedefs

Functions

Detailed Description

Typedef Documentation

◆ implementation_map

Function Documentation

◆ arg()

◆ arg1()

◆ arg2()

◆ arg3()

◆ cinsert() [1/2]

◆ cinsert() [2/2]

◆ cinsert_name()

◆ cons_() [1/2]

◆ cons_() [2/2]

◆ cons_name()

◆ count() [1/2]

◆ count() [2/2]

◆ count_all() [1/2]

◆ count_all() [2/2]

◆ count_all_name()

◆ count_name()

◆ difference() [1/2]

◆ difference() [2/2]

◆ difference_name()

◆ empty()

◆ empty_name()

◆ fbag() [1/3]

◆ fbag() [2/3]

◆ fbag() [3/3]

◆ fbag_cpp_implementable_constructors()

◆ fbag_cpp_implementable_mappings()

◆ fbag_generate_constructors_and_functions_code()

◆ fbag_generate_constructors_code()

◆ fbag_generate_equations_code()

◆ fbag_generate_functions_code()

◆ fbag_mCRL2_usable_constructors()

◆ fbag_mCRL2_usable_mappings()

◆ fset2fbag() [1/2]

◆ fset2fbag() [2/2]

◆ fset2fbag_name()

◆ in() [1/2]

◆ in() [2/2]

◆ in_name()

◆ insert() [1/2]

◆ insert() [2/2]

◆ insert_name()

◆ intersection() [1/2]

◆ intersection() [2/2]

◆ intersection_name()

◆ is_cinsert_application()

◆ is_cinsert_function_symbol()

◆ is_cons_application()

◆ is_cons_function_symbol()

◆ is_count_all_application()

◆ is_count_all_function_symbol()

◆ is_count_application()

◆ is_count_function_symbol()

◆ is_difference_application()

◆ is_difference_function_symbol()

◆ is_empty_function_symbol()

◆ is_fbag()

◆ is_fset2fbag_application()

◆ is_fset2fbag_function_symbol()

◆ is_in_application()

◆ is_in_function_symbol()

◆ is_insert_application()

◆ is_insert_function_symbol()

◆ is_intersection_application()

◆ is_intersection_function_symbol()

◆ is_union_application()

◆ is_union_function_symbol()

◆ left()

◆ make_cinsert()

◆ make_cons_()

◆ make_count()

◆ make_count_all()

◆ make_difference()

◆ make_fset2fbag()

◆ make_in()