mCRL2
Loading...
Searching...
No Matches
mcrl2::data::sort_bag Namespace Reference

Namespace for system defined sort bag. More...

Typedefs

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

Functions

container_sort bag (const sort_expression &s)
 Constructor for sort expression Bag(S)
 
bool is_bag (const sort_expression &e)
 Recogniser for sort expression Bag(s)
 
const core::identifier_stringconstructor_name ()
 Generate identifier @bag.
 
function_symbol constructor (const sort_expression &s)
 Constructor for function symbol @bag.
 
bool is_constructor_function_symbol (const atermpp::aterm &e)
 Recogniser for function @bag.
 
application constructor (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @bag.
 
void make_constructor (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @bag.
 
bool is_constructor_application (const atermpp::aterm &e)
 Recogniser for application of @bag.
 
function_symbol_vector bag_generate_constructors_code (const sort_expression &s)
 Give all system defined constructors for bag.
 
function_symbol_vector bag_mCRL2_usable_constructors (const sort_expression &s)
 Give all defined constructors which can be used in mCRL2 specs for bag.
 
implementation_map bag_cpp_implementable_constructors (const sort_expression &s)
 Give all system defined constructors which have an implementation in C++ and not in rewrite rules for bag.
 
const core::identifier_stringbag_fbag_name ()
 Generate identifier @bagfbag.
 
function_symbol bag_fbag (const sort_expression &s)
 Constructor for function symbol @bagfbag.
 
bool is_bag_fbag_function_symbol (const atermpp::aterm &e)
 Recogniser for function @bagfbag.
 
application bag_fbag (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @bagfbag.
 
void make_bag_fbag (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @bagfbag.
 
bool is_bag_fbag_application (const atermpp::aterm &e)
 Recogniser for application of @bagfbag.
 
const core::identifier_stringbag_comprehension_name ()
 Generate identifier @bagcomp.
 
function_symbol bag_comprehension (const sort_expression &s)
 Constructor for function symbol @bagcomp.
 
bool is_bag_comprehension_function_symbol (const atermpp::aterm &e)
 Recogniser for function @bagcomp.
 
application bag_comprehension (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @bagcomp.
 
void make_bag_comprehension (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @bagcomp.
 
bool is_bag_comprehension_application (const atermpp::aterm &e)
 Recogniser for application of @bagcomp.
 
const core::identifier_stringcount_name ()
 Generate identifier count.
 
function_symbol count (const sort_expression &, const sort_expression &s0, const sort_expression &s1)
 
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_stringin_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_stringunion_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_stringintersection_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_stringdifference_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_stringbag2set_name ()
 Generate identifier Bag2Set.
 
function_symbol bag2set (const sort_expression &s)
 Constructor for function symbol Bag2Set.
 
bool is_bag2set_function_symbol (const atermpp::aterm &e)
 Recogniser for function Bag2Set.
 
application bag2set (const sort_expression &s, const data_expression &arg0)
 Application of function symbol Bag2Set.
 
void make_bag2set (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol Bag2Set.
 
bool is_bag2set_application (const atermpp::aterm &e)
 Recogniser for application of Bag2Set.
 
const core::identifier_stringset2bag_name ()
 Generate identifier Set2Bag.
 
function_symbol set2bag (const sort_expression &s)
 Constructor for function symbol Set2Bag.
 
bool is_set2bag_function_symbol (const atermpp::aterm &e)
 Recogniser for function Set2Bag.
 
application set2bag (const sort_expression &s, const data_expression &arg0)
 Application of function symbol Set2Bag.
 
void make_set2bag (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol Set2Bag.
 
bool is_set2bag_application (const atermpp::aterm &e)
 Recogniser for application of Set2Bag.
 
const core::identifier_stringzero_function_name ()
 Generate identifier @zero_.
 
function_symbol zero_function (const sort_expression &s)
 Constructor for function symbol @zero_.
 
bool is_zero_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @zero_.
 
application zero_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @zero_.
 
void make_zero_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @zero_.
 
bool is_zero_function_application (const atermpp::aterm &e)
 Recogniser for application of @zero_.
 
const core::identifier_stringone_function_name ()
 Generate identifier @one_.
 
function_symbol one_function (const sort_expression &s)
 Constructor for function symbol @one_.
 
bool is_one_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @one_.
 
application one_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @one_.
 
void make_one_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @one_.
 
bool is_one_function_application (const atermpp::aterm &e)
 Recogniser for application of @one_.
 
const core::identifier_stringadd_function_name ()
 Generate identifier @add_.
 
function_symbol add_function (const sort_expression &s)
 Constructor for function symbol @add_.
 
bool is_add_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @add_.
 
application add_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @add_.
 
void make_add_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @add_.
 
bool is_add_function_application (const atermpp::aterm &e)
 Recogniser for application of @add_.
 
const core::identifier_stringmin_function_name ()
 Generate identifier @min_.
 
function_symbol min_function (const sort_expression &s)
 Constructor for function symbol @min_.
 
bool is_min_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @min_.
 
application min_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @min_.
 
void make_min_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @min_.
 
bool is_min_function_application (const atermpp::aterm &e)
 Recogniser for application of @min_.
 
const core::identifier_stringmonus_function_name ()
 Generate identifier @monus_.
 
function_symbol monus_function (const sort_expression &s)
 Constructor for function symbol @monus_.
 
bool is_monus_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @monus_.
 
application monus_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @monus_.
 
void make_monus_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @monus_.
 
bool is_monus_function_application (const atermpp::aterm &e)
 Recogniser for application of @monus_.
 
const core::identifier_stringnat2bool_function_name ()
 Generate identifier @Nat2Bool_.
 
function_symbol nat2bool_function (const sort_expression &s)
 Constructor for function symbol @Nat2Bool_.
 
bool is_nat2bool_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @Nat2Bool_.
 
application nat2bool_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @Nat2Bool_.
 
void make_nat2bool_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @Nat2Bool_.
 
bool is_nat2bool_function_application (const atermpp::aterm &e)
 Recogniser for application of @Nat2Bool_.
 
const core::identifier_stringbool2nat_function_name ()
 Generate identifier @Bool2Nat_.
 
function_symbol bool2nat_function (const sort_expression &s)
 Constructor for function symbol @Bool2Nat_.
 
bool is_bool2nat_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @Bool2Nat_.
 
application bool2nat_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @Bool2Nat_.
 
void make_bool2nat_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @Bool2Nat_.
 
bool is_bool2nat_function_application (const atermpp::aterm &e)
 Recogniser for application of @Bool2Nat_.
 
const core::identifier_stringfbag_join_name ()
 Generate identifier @fbag_join.
 
function_symbol fbag_join (const sort_expression &s)
 Constructor for function symbol @fbag_join.
 
bool is_fbag_join_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fbag_join.
 
application fbag_join (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @fbag_join.
 
void make_fbag_join (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 @fbag_join.
 
bool is_fbag_join_application (const atermpp::aterm &e)
 Recogniser for application of @fbag_join.
 
const core::identifier_stringfbag_intersect_name ()
 Generate identifier @fbag_inter.
 
function_symbol fbag_intersect (const sort_expression &s)
 Constructor for function symbol @fbag_inter.
 
bool is_fbag_intersect_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fbag_inter.
 
application fbag_intersect (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @fbag_inter.
 
void make_fbag_intersect (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 @fbag_inter.
 
bool is_fbag_intersect_application (const atermpp::aterm &e)
 Recogniser for application of @fbag_inter.
 
const core::identifier_stringfbag_difference_name ()
 Generate identifier @fbag_diff.
 
function_symbol fbag_difference (const sort_expression &s)
 Constructor for function symbol @fbag_diff.
 
bool is_fbag_difference_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fbag_diff.
 
application fbag_difference (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @fbag_diff.
 
void make_fbag_difference (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 @fbag_diff.
 
bool is_fbag_difference_application (const atermpp::aterm &e)
 Recogniser for application of @fbag_diff.
 
const core::identifier_stringfbag2fset_name ()
 Generate identifier @fbag2fset.
 
function_symbol fbag2fset (const sort_expression &s)
 Constructor for function symbol @fbag2fset.
 
bool is_fbag2fset_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fbag2fset.
 
application fbag2fset (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @fbag2fset.
 
void make_fbag2fset (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @fbag2fset.
 
bool is_fbag2fset_application (const atermpp::aterm &e)
 Recogniser for application of @fbag2fset.
 
function_symbol_vector bag_generate_functions_code (const sort_expression &s)
 Give all system defined mappings for bag.
 
function_symbol_vector bag_generate_constructors_and_functions_code (const sort_expression &s)
 Give all system defined mappings and constructors for bag.
 
function_symbol_vector bag_mCRL2_usable_mappings (const sort_expression &s)
 Give all system defined mappings that can be used in mCRL2 specs for bag.
 
implementation_map bag_cpp_implementable_mappings (const sort_expression &s)
 Give all system defined mappings that are to be implemented in C++ code for bag.
 
const data_expressionleft (const data_expression &e)
 Function for projecting out argument. left from an application.
 
const data_expressionright (const data_expression &e)
 Function for projecting out argument. right from an application.
 
const data_expressionarg (const data_expression &e)
 Function for projecting out argument. arg from an application.
 
const data_expressionarg1 (const data_expression &e)
 Function for projecting out argument. arg1 from an application.
 
const data_expressionarg2 (const data_expression &e)
 Function for projecting out argument. arg2 from an application.
 
const data_expressionarg3 (const data_expression &e)
 Function for projecting out argument. arg3 from an application.
 
const data_expressionarg4 (const data_expression &e)
 Function for projecting out argument. arg4 from an application.
 
data_equation_vector bag_generate_equations_code (const sort_expression &s)
 Give all system defined equations for bag.
 
const core::identifier_stringjoin_name ()
 Generate identifier @fbag_join.
 
function_symbol join (const sort_expression &s)
 Constructor for function symbol @fbag_join.
 
bool is_join_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fbag_join.
 
application join (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @fbag_join.
 
void make_join (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 @fbag_join.
 
bool is_join_application (const atermpp::aterm &e)
 Recogniser for application of @fbag_join.
 
const core::identifier_stringfset2fbag_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.
 
core::identifier_string const & bag_enumeration_name ()
 Generate identifier bag_enumeration.
 
function_symbol bag_enumeration (const sort_expression &s)
 Constructor for function symbol bag_enumeration.
 
bool is_bag_enumeration_function_symbol (const atermpp::aterm &e)
 Recogniser for function bag_enumeration.
 
template<typename Sequence >
data_expression bag_enumeration (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=0)
 Application of function symbol bag_enumeration.
 
data_expression bag_enumeration (const sort_expression &s, data_expression_list const &range)
 Application of function symbol bag_enumeration.
 
bool is_bag_enumeration_application (const atermpp::aterm &e)
 Recogniser for application of bag_enumeration.
 

Detailed Description

Namespace for system defined sort bag.

Typedef Documentation

◆ implementation_map

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

Definition at line 151 of file bag1.h.

Function Documentation

◆ add_function() [1/2]

function_symbol mcrl2::data::sort_bag::add_function ( const sort_expression s)
inline

Constructor for function symbol @add_.

Parameters
sA sort expression.
Returns
Function symbol add_function.

Definition at line 931 of file bag1.h.

◆ add_function() [2/2]

application mcrl2::data::sort_bag::add_function ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @add_.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of @add_ to a number of arguments.

Definition at line 956 of file bag1.h.

◆ add_function_name()

const core::identifier_string & mcrl2::data::sort_bag::add_function_name ( )
inline

Generate identifier @add_.

Returns
Identifier @add_.

Definition at line 921 of file bag1.h.

◆ arg()

const data_expression & mcrl2::data::sort_bag::arg ( const data_expression e)
inline

Function for projecting out argument. arg from an application.

Parameters
eA data expression.
Precondition
arg is defined for e.
Returns
The argument of e that corresponds to arg.

Definition at line 1618 of file bag1.h.

◆ arg1()

const data_expression & mcrl2::data::sort_bag::arg1 ( const data_expression e)
inline

Function for projecting out argument. arg1 from an application.

Parameters
eA data expression.
Precondition
arg1 is defined for e.
Returns
The argument of e that corresponds to arg1.

Definition at line 1630 of file bag1.h.

◆ arg2()

const data_expression & mcrl2::data::sort_bag::arg2 ( const data_expression e)
inline

Function for projecting out argument. arg2 from an application.

Parameters
eA data expression.
Precondition
arg2 is defined for e.
Returns
The argument of e that corresponds to arg2.

Definition at line 1642 of file bag1.h.

◆ arg3()

const data_expression & mcrl2::data::sort_bag::arg3 ( const data_expression e)
inline

Function for projecting out argument. arg3 from an application.

Parameters
eA data expression.
Precondition
arg3 is defined for e.
Returns
The argument of e that corresponds to arg3.

Definition at line 1654 of file bag1.h.

◆ arg4()

const data_expression & mcrl2::data::sort_bag::arg4 ( const data_expression e)
inline

Function for projecting out argument. arg4 from an application.

Parameters
eA data expression.
Precondition
arg4 is defined for e.
Returns
The argument of e that corresponds to arg4.

Definition at line 1666 of file bag1.h.

◆ bag()

container_sort mcrl2::data::sort_bag::bag ( const sort_expression s)
inline

Constructor for sort expression Bag(S)

Parameters
sA sort expression
Returns
Sort expression bag(s)

Definition at line 44 of file bag1.h.

◆ bag2set() [1/2]

function_symbol mcrl2::data::sort_bag::bag2set ( const sort_expression s)
inline

Constructor for function symbol Bag2Set.

Parameters
sA sort expression.
Returns
Function symbol bag2set.

Definition at line 683 of file bag1.h.

◆ bag2set() [2/2]

application mcrl2::data::sort_bag::bag2set ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol Bag2Set.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of Bag2Set to a number of arguments.

Definition at line 707 of file bag1.h.

◆ bag2set_name()

const core::identifier_string & mcrl2::data::sort_bag::bag2set_name ( )
inline

Generate identifier Bag2Set.

Returns
Identifier Bag2Set.

Definition at line 673 of file bag1.h.

◆ bag_comprehension() [1/2]

function_symbol mcrl2::data::sort_bag::bag_comprehension ( const sort_expression s)
inline

Constructor for function symbol @bagcomp.

Parameters
sA sort expression.
Returns
Function symbol bag_comprehension.

Definition at line 238 of file bag1.h.

◆ bag_comprehension() [2/2]

application mcrl2::data::sort_bag::bag_comprehension ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @bagcomp.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @bagcomp to a number of arguments.

Definition at line 262 of file bag1.h.

◆ bag_comprehension_name()

const core::identifier_string & mcrl2::data::sort_bag::bag_comprehension_name ( )
inline

Generate identifier @bagcomp.

Returns
Identifier @bagcomp.

Definition at line 228 of file bag1.h.

◆ bag_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_bag::bag_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 bag.

Parameters
sA sort expression.
Returns
All system defined constructors that are to be implemented in C++ for bag.

Definition at line 156 of file bag1.h.

◆ bag_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_bag::bag_cpp_implementable_mappings ( const sort_expression s)
inline

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

Parameters
sA sort expression
Returns
A mapping from C++ implementable function symbols to system defined mappings implemented in C++ code for bag

Definition at line 1582 of file bag1.h.

◆ bag_enumeration() [1/3]

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

Constructor for function symbol bag_enumeration.

Parameters
sA sort expression
Returns
Function symbol bag_enumeration

Definition at line 291 of file standard_container_utility.h.

◆ bag_enumeration() [2/3]

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

Application of function symbol bag_enumeration.

Parameters
sA sort expression
rangeA range of data expressions
Returns
Application of bag_enum to the data expressions in range.

Definition at line 349 of file standard_container_utility.h.

◆ bag_enumeration() [3/3]

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

Application of function symbol bag_enumeration.

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

Parameters
sA sort expression
rangeA range of data expressions
Returns
Application of bag_enum to the data expressions in range.

Definition at line 319 of file standard_container_utility.h.

◆ bag_enumeration_name()

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

Generate identifier bag_enumeration.

Returns
Identifier bag_enumeration

Definition at line 281 of file standard_container_utility.h.

◆ bag_fbag() [1/2]

function_symbol mcrl2::data::sort_bag::bag_fbag ( const sort_expression s)
inline

Constructor for function symbol @bagfbag.

Parameters
sA sort expression.
Returns
Function symbol bag_fbag.

Definition at line 176 of file bag1.h.

◆ bag_fbag() [2/2]

application mcrl2::data::sort_bag::bag_fbag ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @bagfbag.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @bagfbag to a number of arguments.

Definition at line 200 of file bag1.h.

◆ bag_fbag_name()

const core::identifier_string & mcrl2::data::sort_bag::bag_fbag_name ( )
inline

Generate identifier @bagfbag.

Returns
Identifier @bagfbag.

Definition at line 166 of file bag1.h.

◆ bag_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_bag::bag_generate_constructors_and_functions_code ( const sort_expression s)
inline

Give all system defined mappings and constructors for bag.

Parameters
sA sort expression
Returns
All system defined mappings for bag

Definition at line 1535 of file bag1.h.

◆ bag_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_bag::bag_generate_constructors_code ( const sort_expression s)
inline

Give all system defined constructors for bag.

Parameters
sA sort expression.
Returns
All system defined constructors for bag.

Definition at line 132 of file bag1.h.

◆ bag_generate_equations_code()

data_equation_vector mcrl2::data::sort_bag::bag_generate_equations_code ( const sort_expression s)
inline

Give all system defined equations for bag.

Parameters
sA sort expression
Returns
All system defined equations for sort bag

Definition at line 1676 of file bag1.h.

◆ bag_generate_functions_code()

function_symbol_vector mcrl2::data::sort_bag::bag_generate_functions_code ( const sort_expression s)
inline

Give all system defined mappings for bag.

Parameters
sA sort expression
Returns
All system defined mappings for bag

Definition at line 1505 of file bag1.h.

◆ bag_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_bag::bag_mCRL2_usable_constructors ( const sort_expression s)
inline

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

Parameters
sA sort expression.
Returns
All system defined constructors that can be used in an mCRL2 specification for bag.

Definition at line 143 of file bag1.h.

◆ bag_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_bag::bag_mCRL2_usable_mappings ( const sort_expression s)
inline

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

Parameters
sA sort expression
Returns
All system defined mappings for that can be used in mCRL2 specificationis bag

Definition at line 1549 of file bag1.h.

◆ bool2nat_function() [1/2]

function_symbol mcrl2::data::sort_bag::bool2nat_function ( const sort_expression s)
inline

Constructor for function symbol @Bool2Nat_.

Parameters
sA sort expression.
Returns
Function symbol bool2nat_function.

Definition at line 1185 of file bag1.h.

◆ bool2nat_function() [2/2]

application mcrl2::data::sort_bag::bool2nat_function ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @Bool2Nat_.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @Bool2Nat_ to a number of arguments.

Definition at line 1209 of file bag1.h.

◆ bool2nat_function_name()

const core::identifier_string & mcrl2::data::sort_bag::bool2nat_function_name ( )
inline

Generate identifier @Bool2Nat_.

Returns
Identifier @Bool2Nat_.

Definition at line 1175 of file bag1.h.

◆ constructor() [1/2]

function_symbol mcrl2::data::sort_bag::constructor ( const sort_expression s)
inline

Constructor for function symbol @bag.

Parameters
sA sort expression.
Returns
Function symbol constructor.

Definition at line 78 of file bag1.h.

◆ constructor() [2/2]

application mcrl2::data::sort_bag::constructor ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @bag.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of @bag to a number of arguments.

Definition at line 103 of file bag1.h.

◆ constructor_name()

const core::identifier_string & mcrl2::data::sort_bag::constructor_name ( )
inline

Generate identifier @bag.

Returns
Identifier @bag.

Definition at line 68 of file bag1.h.

◆ count() [1/2]

function_symbol mcrl2::data::sort_bag::count ( const sort_expression ,
const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 298 of file bag1.h.

◆ count() [2/2]

application mcrl2::data::sort_bag::count ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol count.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of count to a number of arguments.

Definition at line 325 of file bag1.h.

◆ count_name()

const core::identifier_string & mcrl2::data::sort_bag::count_name ( )
inline

Generate identifier count.

Returns
Identifier count.

Definition at line 290 of file bag1.h.

◆ difference() [1/2]

application mcrl2::data::sort_bag::difference ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol -.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of - to a number of arguments.

Definition at line 644 of file bag1.h.

◆ difference() [2/2]

function_symbol mcrl2::data::sort_bag::difference ( const sort_expression s,
const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 596 of file bag1.h.

◆ difference_name()

const core::identifier_string & mcrl2::data::sort_bag::difference_name ( )
inline

Generate identifier -.

Returns
Identifier -.

Definition at line 588 of file bag1.h.

◆ fbag2fset() [1/2]

function_symbol mcrl2::data::sort_bag::fbag2fset ( const sort_expression s)
inline

Constructor for function symbol @fbag2fset.

Parameters
sA sort expression.
Returns
Function symbol fbag2fset.

Definition at line 1451 of file bag1.h.

◆ fbag2fset() [2/2]

application mcrl2::data::sort_bag::fbag2fset ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @fbag2fset.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of @fbag2fset to a number of arguments.

Definition at line 1476 of file bag1.h.

◆ fbag2fset_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag2fset_name ( )
inline

Generate identifier @fbag2fset.

Returns
Identifier @fbag2fset.

Definition at line 1441 of file bag1.h.

◆ fbag_difference() [1/2]

function_symbol mcrl2::data::sort_bag::fbag_difference ( const sort_expression s)
inline

Constructor for function symbol @fbag_diff.

Parameters
sA sort expression.
Returns
Function symbol fbag_difference.

Definition at line 1383 of file bag1.h.

◆ fbag_difference() [2/2]

application mcrl2::data::sort_bag::fbag_difference ( 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 @fbag_diff.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @fbag_diff to a number of arguments.

Definition at line 1410 of file bag1.h.

◆ fbag_difference_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag_difference_name ( )
inline

Generate identifier @fbag_diff.

Returns
Identifier @fbag_diff.

Definition at line 1373 of file bag1.h.

◆ fbag_intersect() [1/2]

function_symbol mcrl2::data::sort_bag::fbag_intersect ( const sort_expression s)
inline

Constructor for function symbol @fbag_inter.

Parameters
sA sort expression.
Returns
Function symbol fbag_intersect.

Definition at line 1315 of file bag1.h.

◆ fbag_intersect() [2/2]

application mcrl2::data::sort_bag::fbag_intersect ( 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 @fbag_inter.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @fbag_inter to a number of arguments.

Definition at line 1342 of file bag1.h.

◆ fbag_intersect_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag_intersect_name ( )
inline

Generate identifier @fbag_inter.

Returns
Identifier @fbag_inter.

Definition at line 1305 of file bag1.h.

◆ fbag_join() [1/2]

function_symbol mcrl2::data::sort_bag::fbag_join ( const sort_expression s)
inline

Constructor for function symbol @fbag_join.

Parameters
sA sort expression.
Returns
Function symbol fbag_join.

Definition at line 1247 of file bag1.h.

◆ fbag_join() [2/2]

application mcrl2::data::sort_bag::fbag_join ( 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 @fbag_join.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @fbag_join to a number of arguments.

Definition at line 1274 of file bag1.h.

◆ fbag_join_name()

const core::identifier_string & mcrl2::data::sort_bag::fbag_join_name ( )
inline

Generate identifier @fbag_join.

Returns
Identifier @fbag_join.

Definition at line 1237 of file bag1.h.

◆ fset2fbag() [1/2]

function_symbol mcrl2::data::sort_bag::fset2fbag ( const sort_expression s)
inline

Constructor for function symbol @fset2fbag.

Parameters
sA sort expression.
Returns
Function symbol fset2fbag.

Definition at line 1515 of file bag64.h.

◆ fset2fbag() [2/2]

application mcrl2::data::sort_bag::fset2fbag ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @fset2fbag.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @fset2fbag to a number of arguments.

Definition at line 1539 of file bag64.h.

◆ fset2fbag_name()

const core::identifier_string & mcrl2::data::sort_bag::fset2fbag_name ( )
inline

Generate identifier @fset2fbag.

Returns
Identifier @fset2fbag.

Definition at line 1505 of file bag64.h.

◆ in() [1/2]

function_symbol mcrl2::data::sort_bag::in ( const sort_expression ,
const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 362 of file bag1.h.

◆ in() [2/2]

application mcrl2::data::sort_bag::in ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol in.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of in to a number of arguments.

Definition at line 389 of file bag1.h.

◆ in_name()

const core::identifier_string & mcrl2::data::sort_bag::in_name ( )
inline

Generate identifier in.

Returns
Identifier in.

Definition at line 354 of file bag1.h.

◆ intersection() [1/2]

application mcrl2::data::sort_bag::intersection ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol *.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of * to a number of arguments.

Definition at line 559 of file bag1.h.

◆ intersection() [2/2]

function_symbol mcrl2::data::sort_bag::intersection ( const sort_expression s,
const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 511 of file bag1.h.

◆ intersection_name()

const core::identifier_string & mcrl2::data::sort_bag::intersection_name ( )
inline

Generate identifier *.

Returns
Identifier *.

Definition at line 503 of file bag1.h.

◆ is_add_function_application()

bool mcrl2::data::sort_bag::is_add_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @add_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol add_function to a number of arguments.

Definition at line 977 of file bag1.h.

◆ is_add_function_function_symbol()

bool mcrl2::data::sort_bag::is_add_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @add_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @add_.

Definition at line 941 of file bag1.h.

◆ is_bag()

bool mcrl2::data::sort_bag::is_bag ( const sort_expression e)
inline

Recogniser for sort expression Bag(s)

Parameters
eA sort expression
Returns
true iff e is a container sort of which the name matches bag

Definition at line 55 of file bag1.h.

◆ is_bag2set_application()

bool mcrl2::data::sort_bag::is_bag2set_application ( const atermpp::aterm e)
inline

Recogniser for application of Bag2Set.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol bag2set to a number of arguments.

Definition at line 727 of file bag1.h.

◆ is_bag2set_function_symbol()

bool mcrl2::data::sort_bag::is_bag2set_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function Bag2Set.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching Bag2Set.

Definition at line 693 of file bag1.h.

◆ is_bag_comprehension_application()

bool mcrl2::data::sort_bag::is_bag_comprehension_application ( const atermpp::aterm e)
inline

Recogniser for application of @bagcomp.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol bag_comprehension to a number of arguments.

Definition at line 282 of file bag1.h.

◆ is_bag_comprehension_function_symbol()

bool mcrl2::data::sort_bag::is_bag_comprehension_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @bagcomp.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @bagcomp.

Definition at line 248 of file bag1.h.

◆ is_bag_enumeration_application()

bool mcrl2::data::sort_bag::is_bag_enumeration_application ( const atermpp::aterm e)
inline

Recogniser for application of bag_enumeration.

Parameters
eA data expression
Returns
true iff e is an application of function symbol bag_enumeration to a number of arguments

Definition at line 377 of file standard_container_utility.h.

◆ is_bag_enumeration_function_symbol()

bool mcrl2::data::sort_bag::is_bag_enumeration_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function bag_enumeration.

Parameters
eA data expression
Returns
true iff e is the function symbol matching bag_enumeration

Definition at line 301 of file standard_container_utility.h.

◆ is_bag_fbag_application()

bool mcrl2::data::sort_bag::is_bag_fbag_application ( const atermpp::aterm e)
inline

Recogniser for application of @bagfbag.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol bag_fbag to a number of arguments.

Definition at line 220 of file bag1.h.

◆ is_bag_fbag_function_symbol()

bool mcrl2::data::sort_bag::is_bag_fbag_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @bagfbag.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @bagfbag.

Definition at line 186 of file bag1.h.

◆ is_bool2nat_function_application()

bool mcrl2::data::sort_bag::is_bool2nat_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @Bool2Nat_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol bool2nat_function to a number of arguments.

Definition at line 1229 of file bag1.h.

◆ is_bool2nat_function_function_symbol()

bool mcrl2::data::sort_bag::is_bool2nat_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @Bool2Nat_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @Bool2Nat_.

Definition at line 1195 of file bag1.h.

◆ is_constructor_application()

bool mcrl2::data::sort_bag::is_constructor_application ( const atermpp::aterm e)
inline

Recogniser for application of @bag.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol constructor to a number of arguments.

Definition at line 124 of file bag1.h.

◆ is_constructor_function_symbol()

bool mcrl2::data::sort_bag::is_constructor_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @bag.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @bag.

Definition at line 88 of file bag1.h.

◆ is_count_application()

bool mcrl2::data::sort_bag::is_count_application ( const atermpp::aterm e)
inline

Recogniser for application of count.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol count to a number of arguments.

Definition at line 346 of file bag1.h.

◆ is_count_function_symbol()

bool mcrl2::data::sort_bag::is_count_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function count.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching count.

Definition at line 309 of file bag1.h.

◆ is_difference_application()

bool mcrl2::data::sort_bag::is_difference_application ( const atermpp::aterm e)
inline

Recogniser for application of -.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol difference to a number of arguments.

Definition at line 665 of file bag1.h.

◆ is_difference_function_symbol()

bool mcrl2::data::sort_bag::is_difference_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function -.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching -.

Definition at line 628 of file bag1.h.

◆ is_fbag2fset_application()

bool mcrl2::data::sort_bag::is_fbag2fset_application ( const atermpp::aterm e)
inline

Recogniser for application of @fbag2fset.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol fbag2fset to a number of arguments.

Definition at line 1497 of file bag1.h.

◆ is_fbag2fset_function_symbol()

bool mcrl2::data::sort_bag::is_fbag2fset_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @fbag2fset.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @fbag2fset.

Definition at line 1461 of file bag1.h.

◆ is_fbag_difference_application()

bool mcrl2::data::sort_bag::is_fbag_difference_application ( const atermpp::aterm e)
inline

Recogniser for application of @fbag_diff.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol fbag_difference to a number of arguments.

Definition at line 1433 of file bag1.h.

◆ is_fbag_difference_function_symbol()

bool mcrl2::data::sort_bag::is_fbag_difference_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @fbag_diff.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @fbag_diff.

Definition at line 1393 of file bag1.h.

◆ is_fbag_intersect_application()

bool mcrl2::data::sort_bag::is_fbag_intersect_application ( const atermpp::aterm e)
inline

Recogniser for application of @fbag_inter.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol fbag_intersect to a number of arguments.

Definition at line 1365 of file bag1.h.

◆ is_fbag_intersect_function_symbol()

bool mcrl2::data::sort_bag::is_fbag_intersect_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @fbag_inter.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @fbag_inter.

Definition at line 1325 of file bag1.h.

◆ is_fbag_join_application()

bool mcrl2::data::sort_bag::is_fbag_join_application ( const atermpp::aterm e)
inline

Recogniser for application of @fbag_join.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol fbag_join to a number of arguments.

Definition at line 1297 of file bag1.h.

◆ is_fbag_join_function_symbol()

bool mcrl2::data::sort_bag::is_fbag_join_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @fbag_join.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @fbag_join.

Definition at line 1257 of file bag1.h.

◆ is_fset2fbag_application()

bool mcrl2::data::sort_bag::is_fset2fbag_application ( const atermpp::aterm e)
inline

Recogniser for application of @fset2fbag.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol fset2fbag to a number of arguments.

Definition at line 1559 of file bag64.h.

◆ is_fset2fbag_function_symbol()

bool mcrl2::data::sort_bag::is_fset2fbag_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @fset2fbag.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @fset2fbag.

Definition at line 1525 of file bag64.h.

◆ is_in_application()

bool mcrl2::data::sort_bag::is_in_application ( const atermpp::aterm e)
inline

Recogniser for application of in.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol in to a number of arguments.

Definition at line 410 of file bag1.h.

◆ is_in_function_symbol()

bool mcrl2::data::sort_bag::is_in_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function in.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching in.

Definition at line 373 of file bag1.h.

◆ is_intersection_application()

bool mcrl2::data::sort_bag::is_intersection_application ( const atermpp::aterm e)
inline

Recogniser for application of *.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol intersection to a number of arguments.

Definition at line 580 of file bag1.h.

◆ is_intersection_function_symbol()

bool mcrl2::data::sort_bag::is_intersection_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function *.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching *.

Definition at line 543 of file bag1.h.

◆ is_join_application()

bool mcrl2::data::sort_bag::is_join_application ( const atermpp::aterm e)
inline

Recogniser for application of @fbag_join.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol join to a number of arguments.

Definition at line 1297 of file bag64.h.

◆ is_join_function_symbol()

bool mcrl2::data::sort_bag::is_join_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @fbag_join.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @fbag_join.

Definition at line 1257 of file bag64.h.

◆ is_min_function_application()

bool mcrl2::data::sort_bag::is_min_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @min_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol min_function to a number of arguments.

Definition at line 1041 of file bag1.h.

◆ is_min_function_function_symbol()

bool mcrl2::data::sort_bag::is_min_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @min_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @min_.

Definition at line 1005 of file bag1.h.

◆ is_monus_function_application()

bool mcrl2::data::sort_bag::is_monus_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @monus_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol monus_function to a number of arguments.

Definition at line 1105 of file bag1.h.

◆ is_monus_function_function_symbol()

bool mcrl2::data::sort_bag::is_monus_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @monus_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @monus_.

Definition at line 1069 of file bag1.h.

◆ is_nat2bool_function_application()

bool mcrl2::data::sort_bag::is_nat2bool_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @Nat2Bool_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol nat2bool_function to a number of arguments.

Definition at line 1167 of file bag1.h.

◆ is_nat2bool_function_function_symbol()

bool mcrl2::data::sort_bag::is_nat2bool_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @Nat2Bool_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @Nat2Bool_.

Definition at line 1133 of file bag1.h.

◆ is_one_function_application()

bool mcrl2::data::sort_bag::is_one_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @one_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol one_function to a number of arguments.

Definition at line 913 of file bag1.h.

◆ is_one_function_function_symbol()

bool mcrl2::data::sort_bag::is_one_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @one_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @one_.

Definition at line 879 of file bag1.h.

◆ is_set2bag_application()

bool mcrl2::data::sort_bag::is_set2bag_application ( const atermpp::aterm e)
inline

Recogniser for application of Set2Bag.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol set2bag to a number of arguments.

Definition at line 789 of file bag1.h.

◆ is_set2bag_function_symbol()

bool mcrl2::data::sort_bag::is_set2bag_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function Set2Bag.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching Set2Bag.

Definition at line 755 of file bag1.h.

◆ is_union_application()

bool mcrl2::data::sort_bag::is_union_application ( const atermpp::aterm e)
inline

Recogniser for application of +.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol union_ to a number of arguments.

Definition at line 495 of file bag1.h.

◆ is_union_function_symbol()

bool mcrl2::data::sort_bag::is_union_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function +.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching +.

Definition at line 458 of file bag1.h.

◆ is_zero_function_application()

bool mcrl2::data::sort_bag::is_zero_function_application ( const atermpp::aterm e)
inline

Recogniser for application of @zero_.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol zero_function to a number of arguments.

Definition at line 851 of file bag1.h.

◆ is_zero_function_function_symbol()

bool mcrl2::data::sort_bag::is_zero_function_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function @zero_.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching @zero_.

Definition at line 817 of file bag1.h.

◆ join() [1/2]

function_symbol mcrl2::data::sort_bag::join ( const sort_expression s)
inline

Constructor for function symbol @fbag_join.

Parameters
sA sort expression.
Returns
Function symbol join.

Definition at line 1247 of file bag64.h.

◆ join() [2/2]

application mcrl2::data::sort_bag::join ( 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 @fbag_join.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.
Returns
Application of @fbag_join to a number of arguments.

Definition at line 1274 of file bag64.h.

◆ join_name()

const core::identifier_string & mcrl2::data::sort_bag::join_name ( )
inline

Generate identifier @fbag_join.

Returns
Identifier @fbag_join.

Definition at line 1237 of file bag64.h.

◆ left()

const data_expression & mcrl2::data::sort_bag::left ( const data_expression e)
inline

Function for projecting out argument. left from an application.

Parameters
eA data expression.
Precondition
left is defined for e.
Returns
The argument of e that corresponds to left.

Definition at line 1594 of file bag1.h.

◆ make_add_function()

void mcrl2::data::sort_bag::make_add_function ( data_expression result,
const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @add_.

Parameters
resultThe data expression where the @add_ expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 967 of file bag1.h.

◆ make_bag2set()

void mcrl2::data::sort_bag::make_bag2set ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol Bag2Set.

Parameters
resultThe data expression where the Bag2Set expression is put.
sA sort expression.
arg0A data expression.

Definition at line 717 of file bag1.h.

◆ make_bag_comprehension()

void mcrl2::data::sort_bag::make_bag_comprehension ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @bagcomp.

Parameters
resultThe data expression where the @bagcomp expression is put.
sA sort expression.
arg0A data expression.

Definition at line 272 of file bag1.h.

◆ make_bag_fbag()

void mcrl2::data::sort_bag::make_bag_fbag ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @bagfbag.

Parameters
resultThe data expression where the @bagfbag expression is put.
sA sort expression.
arg0A data expression.

Definition at line 210 of file bag1.h.

◆ make_bool2nat_function()

void mcrl2::data::sort_bag::make_bool2nat_function ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @Bool2Nat_.

Parameters
resultThe data expression where the @Bool2Nat_ expression is put.
sA sort expression.
arg0A data expression.

Definition at line 1219 of file bag1.h.

◆ make_constructor()

void mcrl2::data::sort_bag::make_constructor ( data_expression result,
const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @bag.

Parameters
resultThe data expression where the @bag expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 114 of file bag1.h.

◆ make_count()

void mcrl2::data::sort_bag::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
resultThe data expression where the count expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 336 of file bag1.h.

◆ make_difference()

void mcrl2::data::sort_bag::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
resultThe data expression where the - expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 655 of file bag1.h.

◆ make_fbag2fset()

void mcrl2::data::sort_bag::make_fbag2fset ( data_expression result,
const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @fbag2fset.

Parameters
resultThe data expression where the @fbag2fset expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 1487 of file bag1.h.

◆ make_fbag_difference()

void mcrl2::data::sort_bag::make_fbag_difference ( 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 @fbag_diff.

Parameters
resultThe data expression where the @fbag_diff expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1423 of file bag1.h.

◆ make_fbag_intersect()

void mcrl2::data::sort_bag::make_fbag_intersect ( 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 @fbag_inter.

Parameters
resultThe data expression where the @fbag_inter expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1355 of file bag1.h.

◆ make_fbag_join()

void mcrl2::data::sort_bag::make_fbag_join ( 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 @fbag_join.

Parameters
resultThe data expression where the @fbag_join expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1287 of file bag1.h.

◆ make_fset2fbag()

void mcrl2::data::sort_bag::make_fset2fbag ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @fset2fbag.

Parameters
resultThe data expression where the @fset2fbag expression is put.
sA sort expression.
arg0A data expression.

Definition at line 1549 of file bag64.h.

◆ make_in()

void mcrl2::data::sort_bag::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
resultThe data expression where the in expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 400 of file bag1.h.

◆ make_intersection()

void mcrl2::data::sort_bag::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
resultThe data expression where the * expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 570 of file bag1.h.

◆ make_join()

void mcrl2::data::sort_bag::make_join ( 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 @fbag_join.

Parameters
resultThe data expression where the @fbag_join expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.
arg2A data expression.
arg3A data expression.

Definition at line 1287 of file bag64.h.

◆ make_min_function()

void mcrl2::data::sort_bag::make_min_function ( data_expression result,
const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @min_.

Parameters
resultThe data expression where the @min_ expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 1031 of file bag1.h.

◆ make_monus_function()

void mcrl2::data::sort_bag::make_monus_function ( data_expression result,
const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol @monus_.

Parameters
resultThe data expression where the @monus_ expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 1095 of file bag1.h.

◆ make_nat2bool_function()

void mcrl2::data::sort_bag::make_nat2bool_function ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @Nat2Bool_.

Parameters
resultThe data expression where the @Nat2Bool_ expression is put.
sA sort expression.
arg0A data expression.

Definition at line 1157 of file bag1.h.

◆ make_one_function()

void mcrl2::data::sort_bag::make_one_function ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @one_.

Parameters
resultThe data expression where the @one_ expression is put.
sA sort expression.
arg0A data expression.

Definition at line 903 of file bag1.h.

◆ make_set2bag()

void mcrl2::data::sort_bag::make_set2bag ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol Set2Bag.

Parameters
resultThe data expression where the Set2Bag expression is put.
sA sort expression.
arg0A data expression.

Definition at line 779 of file bag1.h.

◆ make_union_()

void mcrl2::data::sort_bag::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
resultThe data expression where the + expression is put.
sA sort expression.
arg0A data expression.
arg1A data expression.

Definition at line 485 of file bag1.h.

◆ make_zero_function()

void mcrl2::data::sort_bag::make_zero_function ( data_expression result,
const sort_expression s,
const data_expression arg0 
)
inline

Make an application of function symbol @zero_.

Parameters
resultThe data expression where the @zero_ expression is put.
sA sort expression.
arg0A data expression.

Definition at line 841 of file bag1.h.

◆ min_function() [1/2]

function_symbol mcrl2::data::sort_bag::min_function ( const sort_expression s)
inline

Constructor for function symbol @min_.

Parameters
sA sort expression.
Returns
Function symbol min_function.

Definition at line 995 of file bag1.h.

◆ min_function() [2/2]

application mcrl2::data::sort_bag::min_function ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @min_.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of @min_ to a number of arguments.

Definition at line 1020 of file bag1.h.

◆ min_function_name()

const core::identifier_string & mcrl2::data::sort_bag::min_function_name ( )
inline

Generate identifier @min_.

Returns
Identifier @min_.

Definition at line 985 of file bag1.h.

◆ monus_function() [1/2]

function_symbol mcrl2::data::sort_bag::monus_function ( const sort_expression s)
inline

Constructor for function symbol @monus_.

Parameters
sA sort expression.
Returns
Function symbol monus_function.

Definition at line 1059 of file bag1.h.

◆ monus_function() [2/2]

application mcrl2::data::sort_bag::monus_function ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol @monus_.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of @monus_ to a number of arguments.

Definition at line 1084 of file bag1.h.

◆ monus_function_name()

const core::identifier_string & mcrl2::data::sort_bag::monus_function_name ( )
inline

Generate identifier @monus_.

Returns
Identifier @monus_.

Definition at line 1049 of file bag1.h.

◆ nat2bool_function() [1/2]

function_symbol mcrl2::data::sort_bag::nat2bool_function ( const sort_expression s)
inline

Constructor for function symbol @Nat2Bool_.

Parameters
sA sort expression.
Returns
Function symbol nat2bool_function.

Definition at line 1123 of file bag1.h.

◆ nat2bool_function() [2/2]

application mcrl2::data::sort_bag::nat2bool_function ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @Nat2Bool_.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @Nat2Bool_ to a number of arguments.

Definition at line 1147 of file bag1.h.

◆ nat2bool_function_name()

const core::identifier_string & mcrl2::data::sort_bag::nat2bool_function_name ( )
inline

Generate identifier @Nat2Bool_.

Returns
Identifier @Nat2Bool_.

Definition at line 1113 of file bag1.h.

◆ one_function() [1/2]

function_symbol mcrl2::data::sort_bag::one_function ( const sort_expression s)
inline

Constructor for function symbol @one_.

Parameters
sA sort expression.
Returns
Function symbol one_function.

Definition at line 869 of file bag1.h.

◆ one_function() [2/2]

application mcrl2::data::sort_bag::one_function ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @one_.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @one_ to a number of arguments.

Definition at line 893 of file bag1.h.

◆ one_function_name()

const core::identifier_string & mcrl2::data::sort_bag::one_function_name ( )
inline

Generate identifier @one_.

Returns
Identifier @one_.

Definition at line 859 of file bag1.h.

◆ right()

const data_expression & mcrl2::data::sort_bag::right ( const data_expression e)
inline

Function for projecting out argument. right from an application.

Parameters
eA data expression.
Precondition
right is defined for e.
Returns
The argument of e that corresponds to right.

Definition at line 1606 of file bag1.h.

◆ set2bag() [1/2]

function_symbol mcrl2::data::sort_bag::set2bag ( const sort_expression s)
inline

Constructor for function symbol Set2Bag.

Parameters
sA sort expression.
Returns
Function symbol set2bag.

Definition at line 745 of file bag1.h.

◆ set2bag() [2/2]

application mcrl2::data::sort_bag::set2bag ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol Set2Bag.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of Set2Bag to a number of arguments.

Definition at line 769 of file bag1.h.

◆ set2bag_name()

const core::identifier_string & mcrl2::data::sort_bag::set2bag_name ( )
inline

Generate identifier Set2Bag.

Returns
Identifier Set2Bag.

Definition at line 735 of file bag1.h.

◆ union_() [1/2]

application mcrl2::data::sort_bag::union_ ( const sort_expression s,
const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol +.

Parameters
sA sort expression.
arg0A data expression.
arg1A data expression.
Returns
Application of + to a number of arguments.

Definition at line 474 of file bag1.h.

◆ union_() [2/2]

function_symbol mcrl2::data::sort_bag::union_ ( const sort_expression s,
const sort_expression s0,
const sort_expression s1 
)
inline

Definition at line 426 of file bag1.h.

◆ union_name()

const core::identifier_string & mcrl2::data::sort_bag::union_name ( )
inline

Generate identifier +.

Returns
Identifier +.

Definition at line 418 of file bag1.h.

◆ zero_function() [1/2]

function_symbol mcrl2::data::sort_bag::zero_function ( const sort_expression s)
inline

Constructor for function symbol @zero_.

Parameters
sA sort expression.
Returns
Function symbol zero_function.

Definition at line 807 of file bag1.h.

◆ zero_function() [2/2]

application mcrl2::data::sort_bag::zero_function ( const sort_expression s,
const data_expression arg0 
)
inline

Application of function symbol @zero_.

Parameters
sA sort expression.
arg0A data expression.
Returns
Application of @zero_ to a number of arguments.

Definition at line 831 of file bag1.h.

◆ zero_function_name()

const core::identifier_string & mcrl2::data::sort_bag::zero_function_name ( )
inline

Generate identifier @zero_.

Returns
Identifier @zero_.

Definition at line 797 of file bag1.h.