mcrl2/data/fbag.h

Include file:

#include "mcrl2/data/fbag.h"

The standard sort fbag.

This file was generated from the data sort specification mcrl2/data/build/fbag.spec.

Typedefs

type mcrl2::data::sort_fbag::implementation_map

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

Functions

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

Function for projecting out argument. arg from an application.

Parameters:

  • e A data expression.

Pre: arg is defined for e.

Returns: The argument of e that corresponds to arg.

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

Function for projecting out argument. arg1 from an application.

Parameters:

  • e A data expression.

Pre: arg1 is defined for e.

Returns: The argument of e that corresponds to arg1.

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

Function for projecting out argument. arg2 from an application.

Parameters:

  • e A data expression.

Pre: arg2 is defined for e.

Returns: The argument of e that corresponds to arg2.

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

Function for projecting out argument. arg3 from an application.

Parameters:

  • e A data expression.

Pre: arg3 is defined for e.

Returns: The argument of e that corresponds to arg3.

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

Constructor for function symbol @fbag_cinsert.

Parameters:

  • s A sort expression.

Returns: Function symbol cinsert.

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

Application of function symbol @fbag_cinsert.

Parameters:

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

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

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

Generate identifier @fbag_cinsert.

Returns: Identifier @fbag_cinsert.

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

Constructor for function symbol @fbag_cons.

Parameters:

  • s A sort expression.

Returns: Function symbol cons_.

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

Application of function symbol @fbag_cons.

Parameters:

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

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

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

Generate identifier @fbag_cons.

Returns: Identifier @fbag_cons.

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

Constructor for function symbol count.

Parameters:

  • s A sort expression.

Returns: Function symbol count.

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

Application of function symbol count.

Parameters:

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

Returns: Application of count to a number of arguments.

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

Constructor for function symbol #.

Parameters:

  • s A sort expression.

Returns: Function symbol count_all.

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

Application of function symbol #.

Parameters:

  • s A sort expression.
  • arg0 A data expression.

Returns: Application of # to a number of arguments.

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

Generate identifier #.

Returns: Identifier #.

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

Generate identifier count.

Returns: Identifier count.

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

Constructor for function symbol -.

Parameters:

  • s A sort expression.

Returns: Function symbol difference.

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

Application of function symbol -.

Parameters:

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

Returns: Application of - to a number of arguments.

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

Generate identifier -.

Returns: Identifier -.

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

Constructor for function symbol {:}.

Parameters:

  • s A sort expression.

Returns: Function symbol empty.

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

Generate identifier {:}.

Returns: Identifier {:}.

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

Constructor for sort expression FBag(S)

Parameters:

  • s A sort expression

Returns: Sort expression fbag(s)

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

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

Parameters:

  • s A sort expression.

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

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

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

Parameters:

  • s A sort expression

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

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

Give all system defined mappings and constructors for fbag.

Parameters:

  • s A sort expression

Returns: All system defined mappings for fbag

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

Give all system defined constructors for fbag.

Parameters:

  • s A sort expression.

Returns: All system defined constructors for fbag.

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

Give all system defined equations for fbag.

Parameters:

  • s A sort expression

Returns: All system defined equations for sort fbag

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

Give all system defined mappings for fbag.

Parameters:

  • s A sort expression

Returns: All system defined mappings for fbag

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

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

Parameters:

  • s A sort expression.

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

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

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

Parameters:

  • s A sort expression

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

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

Constructor for function symbol @fset2fbag.

Parameters:

  • s A sort expression.

Returns: Function symbol fset2fbag.

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

Application of function symbol @fset2fbag.

Parameters:

  • s A sort expression.
  • arg0 A data expression.

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

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

Generate identifier @fset2fbag.

Returns: Identifier @fset2fbag.

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

Constructor for function symbol in.

Parameters:

  • s A sort expression.

Returns: Function symbol in.

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

Application of function symbol in.

Parameters:

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

Returns: Application of in to a number of arguments.

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

Generate identifier in.

Returns: Identifier in.

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

Constructor for function symbol @fbag_insert.

Parameters:

  • s A sort expression.

Returns: Function symbol insert.

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

Application of function symbol @fbag_insert.

Parameters:

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

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

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

Generate identifier @fbag_insert.

Returns: Identifier @fbag_insert.

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

Constructor for function symbol *.

Parameters:

  • s A sort expression.

Returns: Function symbol intersection.

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

Application of function symbol *.

Parameters:

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

Returns: Application of * to a number of arguments.

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

Generate identifier *.

Returns: Identifier *.

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

Recogniser for application of @fbag_cinsert.

Parameters:

  • e A data expression.

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

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

Recogniser for function @fbag_cinsert.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag_cinsert.

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

Recogniser for application of @fbag_cons.

Parameters:

  • e A data expression.

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

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

Recogniser for function @fbag_cons.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag_cons.

bool mcrl2::data::sort_fbag::is_count_all_application(const atermpp::aterm_appl &e)

Recogniser for application of #.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol count_all to a number of arguments.

bool mcrl2::data::sort_fbag::is_count_all_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function #.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching #.

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

Recogniser for application of count.

Parameters:

  • e A data expression.

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

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

Recogniser for function count.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching count.

bool mcrl2::data::sort_fbag::is_difference_application(const atermpp::aterm_appl &e)

Recogniser for application of -.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol difference to a number of arguments.

bool mcrl2::data::sort_fbag::is_difference_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function -.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching -.

bool mcrl2::data::sort_fbag::is_empty_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function {:}.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching {:}.

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

Recogniser for sort expression FBag(s)

Parameters:

  • e A sort expression

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

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

Recogniser for application of @fset2fbag.

Parameters:

  • e A data expression.

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

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

Recogniser for function @fset2fbag.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fset2fbag.

bool mcrl2::data::sort_fbag::is_in_application(const atermpp::aterm_appl &e)

Recogniser for application of in.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol in to a number of arguments.

bool mcrl2::data::sort_fbag::is_in_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function in.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching in.

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

Recogniser for application of @fbag_insert.

Parameters:

  • e A data expression.

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

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

Recogniser for function @fbag_insert.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching @fbag_insert.

bool mcrl2::data::sort_fbag::is_intersection_application(const atermpp::aterm_appl &e)

Recogniser for application of *.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol intersection to a number of arguments.

bool mcrl2::data::sort_fbag::is_intersection_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function *.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching *.

bool mcrl2::data::sort_fbag::is_union_application(const atermpp::aterm_appl &e)

Recogniser for application of +.

Parameters:

  • e A data expression.

Returns: true iff e is an application of function symbol union_ to a number of arguments.

bool mcrl2::data::sort_fbag::is_union_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function +.

Parameters:

  • e A data expression.

Returns: true iff e is the function symbol matching +.

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

Function for projecting out argument. left from an application.

Parameters:

  • e A data expression.

Pre: left is defined for e.

Returns: The argument of e that corresponds to left.

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

Make an application of function symbol @fbag_cinsert.

Parameters:

  • result The data expression where the @fbag_cinsert expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::sort_fbag::make_cons_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Make an application of function symbol @fbag_cons.

Parameters:

  • result The data expression where the @fbag_cons expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::sort_fbag::make_count(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol count.

Parameters:

  • result The data expression where the count expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_fbag::make_count_all(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol #.

Parameters:

  • result The data expression where the # expression is put.
  • s A sort expression.
  • arg0 A data expression.
void mcrl2::data::sort_fbag::make_difference(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol -.

Parameters:

  • result The data expression where the - expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_fbag::make_fset2fbag(data_expression &result, const sort_expression &s, const data_expression &arg0)

Make an application of function symbol @fset2fbag.

Parameters:

  • result The data expression where the @fset2fbag expression is put.
  • s A sort expression.
  • arg0 A data expression.
void mcrl2::data::sort_fbag::make_in(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol in.

Parameters:

  • result The data expression where the in expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_fbag::make_insert(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Make an application of function symbol @fbag_insert.

Parameters:

  • result The data expression where the @fbag_insert expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::sort_fbag::make_intersection(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol *.

Parameters:

  • result The data expression where the * expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_fbag::make_union_(data_expression &result, const sort_expression &s, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol +.

Parameters:

  • result The data expression where the + expression is put.
  • s A sort expression.
  • arg0 A data expression.
  • arg1 A data expression.
const data_expression &mcrl2::data::sort_fbag::right(const data_expression &e)

Function for projecting out argument. right from an application.

Parameters:

  • e A data expression.

Pre: right is defined for e.

Returns: The argument of e that corresponds to right.

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

Constructor for function symbol +.

Parameters:

  • s A sort expression.

Returns: Function symbol union_.

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

Application of function symbol +.

Parameters:

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

Returns: Application of + to a number of arguments.

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

Generate identifier +.

Returns: Identifier +.