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

Namespace for system defined sort set_. More...

Typedefs

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

Functions

container_sort set_ (const sort_expression &s)
 Constructor for sort expression Set(S)
 
bool is_set (const sort_expression &e)
 Recogniser for sort expression Set(s)
 
const core::identifier_stringconstructor_name ()
 Generate identifier @set.
 
function_symbol constructor (const sort_expression &s)
 Constructor for function symbol @set.
 
bool is_constructor_function_symbol (const atermpp::aterm &e)
 Recogniser for function @set.
 
application constructor (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @set.
 
void make_constructor (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @set.
 
bool is_constructor_application (const atermpp::aterm &e)
 Recogniser for application of @set.
 
function_symbol_vector set_generate_constructors_code (const sort_expression &s)
 Give all system defined constructors for set_.
 
function_symbol_vector set_mCRL2_usable_constructors (const sort_expression &s)
 Give all defined constructors which can be used in mCRL2 specs for set_.
 
implementation_map set_cpp_implementable_constructors (const sort_expression &s)
 Give all system defined constructors which have an implementation in C++ and not in rewrite rules for set_.
 
const core::identifier_stringset_fset_name ()
 Generate identifier @setfset.
 
function_symbol set_fset (const sort_expression &s)
 Constructor for function symbol @setfset.
 
bool is_set_fset_function_symbol (const atermpp::aterm &e)
 Recogniser for function @setfset.
 
application set_fset (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @setfset.
 
void make_set_fset (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @setfset.
 
bool is_set_fset_application (const atermpp::aterm &e)
 Recogniser for application of @setfset.
 
const core::identifier_stringset_comprehension_name ()
 Generate identifier @setcomp.
 
function_symbol set_comprehension (const sort_expression &s)
 Constructor for function symbol @setcomp.
 
bool is_set_comprehension_function_symbol (const atermpp::aterm &e)
 Recogniser for function @setcomp.
 
application set_comprehension (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @setcomp.
 
void make_set_comprehension (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @setcomp.
 
bool is_set_comprehension_application (const atermpp::aterm &e)
 Recogniser for application of @setcomp.
 
const core::identifier_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_stringcomplement_name ()
 Generate identifier !.
 
function_symbol complement (const sort_expression &s)
 Constructor for function symbol !.
 
bool is_complement_function_symbol (const atermpp::aterm &e)
 Recogniser for function !.
 
application complement (const sort_expression &s, const data_expression &arg0)
 Application of function symbol !.
 
void make_complement (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol !.
 
bool is_complement_application (const atermpp::aterm &e)
 Recogniser for application of !.
 
const core::identifier_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_stringfalse_function_name ()
 Generate identifier @false_.
 
function_symbol false_function (const sort_expression &s)
 Constructor for function symbol @false_.
 
bool is_false_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @false_.
 
application false_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @false_.
 
void make_false_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @false_.
 
bool is_false_function_application (const atermpp::aterm &e)
 Recogniser for application of @false_.
 
const core::identifier_stringtrue_function_name ()
 Generate identifier @true_.
 
function_symbol true_function (const sort_expression &s)
 Constructor for function symbol @true_.
 
bool is_true_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @true_.
 
application true_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @true_.
 
void make_true_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @true_.
 
bool is_true_function_application (const atermpp::aterm &e)
 Recogniser for application of @true_.
 
const core::identifier_stringnot_function_name ()
 Generate identifier @not_.
 
function_symbol not_function (const sort_expression &s)
 Constructor for function symbol @not_.
 
bool is_not_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @not_.
 
application not_function (const sort_expression &s, const data_expression &arg0)
 Application of function symbol @not_.
 
void make_not_function (data_expression &result, const sort_expression &s, const data_expression &arg0)
 Make an application of function symbol @not_.
 
bool is_not_function_application (const atermpp::aterm &e)
 Recogniser for application of @not_.
 
const core::identifier_stringand_function_name ()
 Generate identifier @and_.
 
function_symbol and_function (const sort_expression &s)
 Constructor for function symbol @and_.
 
bool is_and_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @and_.
 
application and_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @and_.
 
void make_and_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @and_.
 
bool is_and_function_application (const atermpp::aterm &e)
 Recogniser for application of @and_.
 
const core::identifier_stringor_function_name ()
 Generate identifier @or_.
 
function_symbol or_function (const sort_expression &s)
 Constructor for function symbol @or_.
 
bool is_or_function_function_symbol (const atermpp::aterm &e)
 Recogniser for function @or_.
 
application or_function (const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @or_.
 
void make_or_function (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol @or_.
 
bool is_or_function_application (const atermpp::aterm &e)
 Recogniser for application of @or_.
 
const core::identifier_stringfset_union_name ()
 Generate identifier @fset_union.
 
function_symbol fset_union (const sort_expression &s)
 Constructor for function symbol @fset_union.
 
bool is_fset_union_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fset_union.
 
application fset_union (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @fset_union.
 
void make_fset_union (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @fset_union.
 
bool is_fset_union_application (const atermpp::aterm &e)
 Recogniser for application of @fset_union.
 
const core::identifier_stringfset_intersection_name ()
 Generate identifier @fset_inter.
 
function_symbol fset_intersection (const sort_expression &s)
 Constructor for function symbol @fset_inter.
 
bool is_fset_intersection_function_symbol (const atermpp::aterm &e)
 Recogniser for function @fset_inter.
 
application fset_intersection (const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Application of function symbol @fset_inter.
 
void make_fset_intersection (data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2, const data_expression &arg3)
 Make an application of function symbol @fset_inter.
 
bool is_fset_intersection_application (const atermpp::aterm &e)
 Recogniser for application of @fset_inter.
 
function_symbol_vector set_generate_functions_code (const sort_expression &s)
 Give all system defined mappings for set_.
 
function_symbol_vector set_generate_constructors_and_functions_code (const sort_expression &s)
 Give all system defined mappings and constructors for set_.
 
function_symbol_vector set_mCRL2_usable_mappings (const sort_expression &s)
 Give all system defined mappings that can be used in mCRL2 specs for set_.
 
implementation_map set_cpp_implementable_mappings (const sort_expression &s)
 Give all system defined mappings that are to be implemented in C++ code for set_.
 
const data_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 set_generate_equations_code (const sort_expression &s)
 Give all system defined equations for set_.
 
core::identifier_string const & set_enumeration_name ()
 Generate identifier set_enumeration.
 
function_symbol set_enumeration (const sort_expression &s)
 Constructor for function symbol set_enumeration.
 
bool is_set_enumeration_function_symbol (const atermpp::aterm &e)
 Recogniser for function set_enumeration.
 
template<typename Sequence >
data_expression set_enumeration (const sort_expression &s, Sequence const &range, typename atermpp::enable_if_container< Sequence, data_expression >::type *=0)
 Application of function symbol set_enumeration.
 
data_expression set_enumeration (const sort_expression &s, data_expression_list const &range)
 Application of function symbol set_enumeration.
 
bool is_set_enumeration_application (const atermpp::aterm &e)
 Recogniser for application of set_enumeration.
 

Detailed Description

Namespace for system defined sort set_.

Typedef Documentation

◆ implementation_map

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

Definition at line 149 of file set1.h.

Function Documentation

◆ and_function() [1/2]

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

Constructor for function symbol @and_.

Parameters
sA sort expression.
Returns
Function symbol and_function.

Definition at line 841 of file set1.h.

◆ and_function() [2/2]

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

Application of function symbol @and_.

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

Definition at line 866 of file set1.h.

◆ and_function_name()

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

Generate identifier @and_.

Returns
Identifier @and_.

Definition at line 831 of file set1.h.

◆ arg()

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

Function for projecting out argument. arg from an application.

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

Definition at line 1196 of file set1.h.

◆ arg1()

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

Function for projecting out argument. arg1 from an application.

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

Definition at line 1208 of file set1.h.

◆ arg2()

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

Function for projecting out argument. arg2 from an application.

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

Definition at line 1220 of file set1.h.

◆ arg3()

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

Function for projecting out argument. arg3 from an application.

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

Definition at line 1232 of file set1.h.

◆ arg4()

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

Function for projecting out argument. arg4 from an application.

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

Definition at line 1244 of file set1.h.

◆ complement() [1/2]

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

Constructor for function symbol !.

Parameters
sA sort expression.
Returns
Function symbol complement.

Definition at line 362 of file set1.h.

◆ complement() [2/2]

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

Application of function symbol !.

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

Definition at line 386 of file set1.h.

◆ complement_name()

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

Generate identifier !.

Returns
Identifier !.

Definition at line 352 of file set1.h.

◆ constructor() [1/2]

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

Constructor for function symbol @set.

Parameters
sA sort expression.
Returns
Function symbol constructor.

Definition at line 76 of file set1.h.

◆ constructor() [2/2]

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

Application of function symbol @set.

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

Definition at line 101 of file set1.h.

◆ constructor_name()

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

Generate identifier @set.

Returns
Identifier @set.

Definition at line 66 of file set1.h.

◆ difference() [1/2]

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

Application of function symbol -.

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

Definition at line 616 of file set1.h.

◆ difference() [2/2]

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

Definition at line 576 of file set1.h.

◆ difference_name()

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

Generate identifier -.

Returns
Identifier -.

Definition at line 568 of file set1.h.

◆ false_function() [1/2]

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

Constructor for function symbol @false_.

Parameters
sA sort expression.
Returns
Function symbol false_function.

Definition at line 655 of file set1.h.

◆ false_function() [2/2]

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

Application of function symbol @false_.

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

Definition at line 679 of file set1.h.

◆ false_function_name()

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

Generate identifier @false_.

Returns
Identifier @false_.

Definition at line 645 of file set1.h.

◆ fset_intersection() [1/2]

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

Constructor for function symbol @fset_inter.

Parameters
sA sort expression.
Returns
Function symbol fset_intersection.

Definition at line 1037 of file set1.h.

◆ fset_intersection() [2/2]

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

Application of function symbol @fset_inter.

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

Definition at line 1064 of file set1.h.

◆ fset_intersection_name()

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

Generate identifier @fset_inter.

Returns
Identifier @fset_inter.

Definition at line 1027 of file set1.h.

◆ fset_union() [1/2]

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

Constructor for function symbol @fset_union.

Parameters
sA sort expression.
Returns
Function symbol fset_union.

Definition at line 969 of file set1.h.

◆ fset_union() [2/2]

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

Application of function symbol @fset_union.

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

Definition at line 996 of file set1.h.

◆ fset_union_name()

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

Generate identifier @fset_union.

Returns
Identifier @fset_union.

Definition at line 959 of file set1.h.

◆ in() [1/2]

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

Definition at line 296 of file set1.h.

◆ in() [2/2]

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

Application of function symbol in.

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

Definition at line 323 of file set1.h.

◆ in_name()

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

Generate identifier in.

Returns
Identifier in.

Definition at line 288 of file set1.h.

◆ intersection() [1/2]

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

Application of function symbol *.

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

Definition at line 539 of file set1.h.

◆ intersection() [2/2]

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

Definition at line 499 of file set1.h.

◆ intersection_name()

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

Generate identifier *.

Returns
Identifier *.

Definition at line 491 of file set1.h.

◆ is_and_function_application()

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

Recogniser for application of @and_.

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

Definition at line 887 of file set1.h.

◆ is_and_function_function_symbol()

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

Recogniser for function @and_.

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

Definition at line 851 of file set1.h.

◆ is_complement_application()

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

Recogniser for application of !.

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

Definition at line 406 of file set1.h.

◆ is_complement_function_symbol()

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

Recogniser for function !.

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

Definition at line 372 of file set1.h.

◆ is_constructor_application()

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

Recogniser for application of @set.

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

Definition at line 122 of file set1.h.

◆ is_constructor_function_symbol()

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

Recogniser for function @set.

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

Definition at line 86 of file set1.h.

◆ is_difference_application()

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

Recogniser for application of -.

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

Definition at line 637 of file set1.h.

◆ is_difference_function_symbol()

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

Recogniser for function -.

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

Definition at line 600 of file set1.h.

◆ is_false_function_application()

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

Recogniser for application of @false_.

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

Definition at line 699 of file set1.h.

◆ is_false_function_function_symbol()

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

Recogniser for function @false_.

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

Definition at line 665 of file set1.h.

◆ is_fset_intersection_application()

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

Recogniser for application of @fset_inter.

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

Definition at line 1087 of file set1.h.

◆ is_fset_intersection_function_symbol()

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

Recogniser for function @fset_inter.

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

Definition at line 1047 of file set1.h.

◆ is_fset_union_application()

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

Recogniser for application of @fset_union.

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

Definition at line 1019 of file set1.h.

◆ is_fset_union_function_symbol()

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

Recogniser for function @fset_union.

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

Definition at line 979 of file set1.h.

◆ is_in_application()

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

Recogniser for application of in.

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

Definition at line 344 of file set1.h.

◆ is_in_function_symbol()

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

Recogniser for function in.

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

Definition at line 307 of file set1.h.

◆ is_intersection_application()

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

Recogniser for application of *.

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

Definition at line 560 of file set1.h.

◆ is_intersection_function_symbol()

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

Recogniser for function *.

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

Definition at line 523 of file set1.h.

◆ is_not_function_application()

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

Recogniser for application of @not_.

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

Definition at line 823 of file set1.h.

◆ is_not_function_function_symbol()

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

Recogniser for function @not_.

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

Definition at line 789 of file set1.h.

◆ is_or_function_application()

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

Recogniser for application of @or_.

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

Definition at line 951 of file set1.h.

◆ is_or_function_function_symbol()

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

Recogniser for function @or_.

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

Definition at line 915 of file set1.h.

◆ is_set()

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

Recogniser for sort expression Set(s)

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

Definition at line 53 of file set1.h.

◆ is_set_comprehension_application()

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

Recogniser for application of @setcomp.

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

Definition at line 280 of file set1.h.

◆ is_set_comprehension_function_symbol()

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

Recogniser for function @setcomp.

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

Definition at line 246 of file set1.h.

◆ is_set_enumeration_application()

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

Recogniser for application of set_enumeration.

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

Definition at line 226 of file standard_container_utility.h.

◆ is_set_enumeration_function_symbol()

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

Recogniser for function set_enumeration.

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

Definition at line 167 of file standard_container_utility.h.

◆ is_set_fset_application()

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

Recogniser for application of @setfset.

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

Definition at line 218 of file set1.h.

◆ is_set_fset_function_symbol()

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

Recogniser for function @setfset.

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

Definition at line 184 of file set1.h.

◆ is_true_function_application()

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

Recogniser for application of @true_.

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

Definition at line 761 of file set1.h.

◆ is_true_function_function_symbol()

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

Recogniser for function @true_.

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

Definition at line 727 of file set1.h.

◆ is_union_application()

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

Recogniser for application of +.

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

Definition at line 483 of file set1.h.

◆ is_union_function_symbol()

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

Recogniser for function +.

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

Definition at line 446 of file set1.h.

◆ left()

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

Function for projecting out argument. left from an application.

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

Definition at line 1172 of file set1.h.

◆ make_and_function()

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

Make an application of function symbol @and_.

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

Definition at line 877 of file set1.h.

◆ make_complement()

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

Make an application of function symbol !.

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

Definition at line 396 of file set1.h.

◆ make_constructor()

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

Make an application of function symbol @set.

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

Definition at line 112 of file set1.h.

◆ make_difference()

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

Make an application of function symbol -.

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

Definition at line 627 of file set1.h.

◆ make_false_function()

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

Make an application of function symbol @false_.

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

Definition at line 689 of file set1.h.

◆ make_fset_intersection()

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

Make an application of function symbol @fset_inter.

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

Definition at line 1077 of file set1.h.

◆ make_fset_union()

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

Make an application of function symbol @fset_union.

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

Definition at line 1009 of file set1.h.

◆ make_in()

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

Make an application of function symbol in.

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

Definition at line 334 of file set1.h.

◆ make_intersection()

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

Make an application of function symbol *.

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

Definition at line 550 of file set1.h.

◆ make_not_function()

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

Make an application of function symbol @not_.

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

Definition at line 813 of file set1.h.

◆ make_or_function()

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

Make an application of function symbol @or_.

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

Definition at line 941 of file set1.h.

◆ make_set_comprehension()

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

Make an application of function symbol @setcomp.

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

Definition at line 270 of file set1.h.

◆ make_set_fset()

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

Make an application of function symbol @setfset.

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

Definition at line 208 of file set1.h.

◆ make_true_function()

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

Make an application of function symbol @true_.

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

Definition at line 751 of file set1.h.

◆ make_union_()

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

Make an application of function symbol +.

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

Definition at line 473 of file set1.h.

◆ not_function() [1/2]

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

Constructor for function symbol @not_.

Parameters
sA sort expression.
Returns
Function symbol not_function.

Definition at line 779 of file set1.h.

◆ not_function() [2/2]

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

Application of function symbol @not_.

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

Definition at line 803 of file set1.h.

◆ not_function_name()

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

Generate identifier @not_.

Returns
Identifier @not_.

Definition at line 769 of file set1.h.

◆ or_function() [1/2]

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

Constructor for function symbol @or_.

Parameters
sA sort expression.
Returns
Function symbol or_function.

Definition at line 905 of file set1.h.

◆ or_function() [2/2]

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

Application of function symbol @or_.

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

Definition at line 930 of file set1.h.

◆ or_function_name()

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

Generate identifier @or_.

Returns
Identifier @or_.

Definition at line 895 of file set1.h.

◆ right()

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

Function for projecting out argument. right from an application.

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

Definition at line 1184 of file set1.h.

◆ set_()

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

Constructor for sort expression Set(S)

Parameters
sA sort expression
Returns
Sort expression set_(s)

Definition at line 42 of file set1.h.

◆ set_comprehension() [1/2]

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

Constructor for function symbol @setcomp.

Parameters
sA sort expression.
Returns
Function symbol set_comprehension.

Definition at line 236 of file set1.h.

◆ set_comprehension() [2/2]

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

Application of function symbol @setcomp.

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

Definition at line 260 of file set1.h.

◆ set_comprehension_name()

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

Generate identifier @setcomp.

Returns
Identifier @setcomp.

Definition at line 226 of file set1.h.

◆ set_cpp_implementable_constructors()

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

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

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

Definition at line 154 of file set1.h.

◆ set_cpp_implementable_mappings()

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

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

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

Definition at line 1160 of file set1.h.

◆ set_enumeration() [1/3]

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

Constructor for function symbol set_enumeration.

Parameters
sA sort expression
Returns
Function symbol set_enumeration

Definition at line 157 of file standard_container_utility.h.

◆ set_enumeration() [2/3]

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

Application of function symbol set_enumeration.

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

Definition at line 206 of file standard_container_utility.h.

◆ set_enumeration() [3/3]

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

Application of function symbol set_enumeration.

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

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

Definition at line 185 of file standard_container_utility.h.

◆ set_enumeration_name()

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

Generate identifier set_enumeration.

Returns
Identifier set_enumeration

Definition at line 147 of file standard_container_utility.h.

◆ set_fset() [1/2]

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

Constructor for function symbol @setfset.

Parameters
sA sort expression.
Returns
Function symbol set_fset.

Definition at line 174 of file set1.h.

◆ set_fset() [2/2]

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

Application of function symbol @setfset.

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

Definition at line 198 of file set1.h.

◆ set_fset_name()

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

Generate identifier @setfset.

Returns
Identifier @setfset.

Definition at line 164 of file set1.h.

◆ set_generate_constructors_and_functions_code()

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

Give all system defined mappings and constructors for set_.

Parameters
sA sort expression
Returns
All system defined mappings for set_

Definition at line 1119 of file set1.h.

◆ set_generate_constructors_code()

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

Give all system defined constructors for set_.

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

Definition at line 130 of file set1.h.

◆ set_generate_equations_code()

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

Give all system defined equations for set_.

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

Definition at line 1254 of file set1.h.

◆ set_generate_functions_code()

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

Give all system defined mappings for set_.

Parameters
sA sort expression
Returns
All system defined mappings for set_

Definition at line 1095 of file set1.h.

◆ set_mCRL2_usable_constructors()

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

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

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

Definition at line 141 of file set1.h.

◆ set_mCRL2_usable_mappings()

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

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

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

Definition at line 1133 of file set1.h.

◆ true_function() [1/2]

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

Constructor for function symbol @true_.

Parameters
sA sort expression.
Returns
Function symbol true_function.

Definition at line 717 of file set1.h.

◆ true_function() [2/2]

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

Application of function symbol @true_.

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

Definition at line 741 of file set1.h.

◆ true_function_name()

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

Generate identifier @true_.

Returns
Identifier @true_.

Definition at line 707 of file set1.h.

◆ union_() [1/2]

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

Application of function symbol +.

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

Definition at line 462 of file set1.h.

◆ union_() [2/2]

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

Definition at line 422 of file set1.h.

◆ union_name()

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

Generate identifier +.

Returns
Identifier +.

Definition at line 414 of file set1.h.