mcrl2/data/pos.h

Include file:

#include "mcrl2/data/pos.h"

The standard sort pos.

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

Typedefs

type mcrl2::data::sort_pos::implementation_map

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

Functions

const function_symbol &mcrl2::data::sort_pos::add_with_carry()

Constructor for function symbol @addc.

Returns: Function symbol add_with_carry.

application mcrl2::data::sort_pos::add_with_carry(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Application of function symbol @addc.

Parameters:

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

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

const core::identifier_string &mcrl2::data::sort_pos::add_with_carry_name()

Generate identifier @addc.

Returns: Identifier @addc.

const data_expression &mcrl2::data::sort_pos::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_pos::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_pos::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_pos::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.

const function_symbol &mcrl2::data::sort_pos::c1()

Constructor for function symbol @c1.

Returns: Function symbol c1.

const core::identifier_string &mcrl2::data::sort_pos::c1_name()

Generate identifier @c1.

Returns: Identifier @c1.

const function_symbol &mcrl2::data::sort_pos::cdub()

Constructor for function symbol @cDub.

Returns: Function symbol cdub.

application mcrl2::data::sort_pos::cdub(const data_expression &arg0, const data_expression &arg1)

Application of function symbol @cDub.

Parameters:

  • arg0 A data expression.
  • arg1 A data expression.

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

const core::identifier_string &mcrl2::data::sort_pos::cdub_name()

Generate identifier @cDub.

Returns: Identifier @cDub.

bool mcrl2::data::sort_pos::is_add_with_carry_application(const atermpp::aterm_appl &e)

Recogniser for application of @addc.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_add_with_carry_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @addc.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_c1_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @c1.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_cdub_application(const atermpp::aterm_appl &e)

Recogniser for application of @cDub.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_cdub_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cDub.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_maximum_application(const atermpp::aterm_appl &e)

Recogniser for application of max.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_maximum_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function max.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_minimum_application(const atermpp::aterm_appl &e)

Recogniser for application of min.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_minimum_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function min.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_plus_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 plus to a number of arguments.

bool mcrl2::data::sort_pos::is_plus_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_pos::is_pos(const sort_expression &e)

Recogniser for sort expression Pos.

Parameters:

  • e A sort expression

Returns: true iff e == pos()

bool mcrl2::data::sort_pos::is_pos_predecessor_application(const atermpp::aterm_appl &e)

Recogniser for application of @pospred.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_pos_predecessor_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @pospred.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_powerlog2_pos_application(const atermpp::aterm_appl &e)

Recogniser for application of @powerlog2.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_powerlog2_pos_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @powerlog2.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_succ_application(const atermpp::aterm_appl &e)

Recogniser for application of succ.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_succ_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function succ.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_pos::is_times_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 times to a number of arguments.

bool mcrl2::data::sort_pos::is_times_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_pos::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_pos::make_add_with_carry(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Make an application of function symbol @addc.

Parameters:

  • result The data expression where the @addc expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
  • arg2 A data expression.
void mcrl2::data::sort_pos::make_cdub(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol @cDub.

Parameters:

  • result The data expression where the @cDub expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_pos::make_maximum(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol max.

Parameters:

  • result The data expression where the max expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_pos::make_minimum(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol min.

Parameters:

  • result The data expression where the min expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_pos::make_plus(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol +.

Parameters:

  • result The data expression where the + expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_pos::make_pos_predecessor(data_expression &result, const data_expression &arg0)

Make an application of function symbol @pospred.

Parameters:

  • result The data expression where the @pospred expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_pos::make_powerlog2_pos(data_expression &result, const data_expression &arg0)

Make an application of function symbol @powerlog2.

Parameters:

  • result The data expression where the @powerlog2 expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_pos::make_succ(data_expression &result, const data_expression &arg0)

Make an application of function symbol succ.

Parameters:

  • result The data expression where the succ expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_pos::make_times(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol *.

Parameters:

  • result The data expression where the * expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
const function_symbol &mcrl2::data::sort_pos::maximum()

Constructor for function symbol max.

Returns: Function symbol maximum.

application mcrl2::data::sort_pos::maximum(const data_expression &arg0, const data_expression &arg1)

Application of function symbol max.

Parameters:

  • arg0 A data expression.
  • arg1 A data expression.

Returns: Application of max to a number of arguments.

const core::identifier_string &mcrl2::data::sort_pos::maximum_name()

Generate identifier max.

Returns: Identifier max.

const function_symbol &mcrl2::data::sort_pos::minimum()

Constructor for function symbol min.

Returns: Function symbol minimum.

application mcrl2::data::sort_pos::minimum(const data_expression &arg0, const data_expression &arg1)

Application of function symbol min.

Parameters:

  • arg0 A data expression.
  • arg1 A data expression.

Returns: Application of min to a number of arguments.

const core::identifier_string &mcrl2::data::sort_pos::minimum_name()

Generate identifier min.

Returns: Identifier min.

const function_symbol &mcrl2::data::sort_pos::plus()

Constructor for function symbol +.

Returns: Function symbol plus.

application mcrl2::data::sort_pos::plus(const data_expression &arg0, const data_expression &arg1)

Application of function symbol +.

Parameters:

  • arg0 A data expression.
  • arg1 A data expression.

Returns: Application of + to a number of arguments.

const core::identifier_string &mcrl2::data::sort_pos::plus_name()

Generate identifier +.

Returns: Identifier +.

const basic_sort &mcrl2::data::sort_pos::pos()

Constructor for sort expression Pos.

Returns: Sort expression Pos.

implementation_map mcrl2::data::sort_pos::pos_cpp_implementable_constructors()

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

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

implementation_map mcrl2::data::sort_pos::pos_cpp_implementable_mappings()

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

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

function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_and_functions_code()

Give all system defined mappings and constructors for pos.

Returns: All system defined mappings for pos

function_symbol_vector mcrl2::data::sort_pos::pos_generate_constructors_code()

Give all system defined constructors for pos.

Returns: All system defined constructors for pos.

data_equation_vector mcrl2::data::sort_pos::pos_generate_equations_code()

Give all system defined equations for pos.

Returns: All system defined equations for sort pos

function_symbol_vector mcrl2::data::sort_pos::pos_generate_functions_code()

Give all system defined mappings for pos.

Returns: All system defined mappings for pos

function_symbol_vector mcrl2::data::sort_pos::pos_mCRL2_usable_constructors()

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

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

function_symbol_vector mcrl2::data::sort_pos::pos_mCRL2_usable_mappings()

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

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

const core::identifier_string &mcrl2::data::sort_pos::pos_name()
const function_symbol &mcrl2::data::sort_pos::pos_predecessor()

Constructor for function symbol @pospred.

Returns: Function symbol pos_predecessor.

application mcrl2::data::sort_pos::pos_predecessor(const data_expression &arg0)

Application of function symbol @pospred.

Parameters:

  • arg0 A data expression.

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

const core::identifier_string &mcrl2::data::sort_pos::pos_predecessor_name()

Generate identifier @pospred.

Returns: Identifier @pospred.

const function_symbol &mcrl2::data::sort_pos::powerlog2_pos()

Constructor for function symbol @powerlog2.

Returns: Function symbol powerlog2_pos.

application mcrl2::data::sort_pos::powerlog2_pos(const data_expression &arg0)

Application of function symbol @powerlog2.

Parameters:

  • arg0 A data expression.

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

const core::identifier_string &mcrl2::data::sort_pos::powerlog2_pos_name()

Generate identifier @powerlog2.

Returns: Identifier @powerlog2.

const data_expression &mcrl2::data::sort_pos::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.

const function_symbol &mcrl2::data::sort_pos::succ()

Constructor for function symbol succ.

Returns: Function symbol succ.

application mcrl2::data::sort_pos::succ(const data_expression &arg0)

Application of function symbol succ.

Parameters:

  • arg0 A data expression.

Returns: Application of succ to a number of arguments.

const core::identifier_string &mcrl2::data::sort_pos::succ_name()

Generate identifier succ.

Returns: Identifier succ.

const function_symbol &mcrl2::data::sort_pos::times()

Constructor for function symbol *.

Returns: Function symbol times.

application mcrl2::data::sort_pos::times(const data_expression &arg0, const data_expression &arg1)

Application of function symbol *.

Parameters:

  • arg0 A data expression.
  • arg1 A data expression.

Returns: Application of * to a number of arguments.

const core::identifier_string &mcrl2::data::sort_pos::times_name()

Generate identifier *.

Returns: Identifier *.