mcrl2/data/int.h

Include file:

#include "mcrl2/data/int.h"

The standard sort int_.

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

Functions

bool mcrl2::data::is_left_associative(const data_expression &x)
bool mcrl2::data::is_right_associative(const data_expression &x)
std::string mcrl2::data::pp(const T &x)

Returns a string representation of the object x.

int mcrl2::data::precedence(const application &x)
constexpr int mcrl2::data::precedence(const bag_comprehension&)
int precedence(const data_expression &x)
constexpr int mcrl2::data::precedence(const exists&)
constexpr int mcrl2::data::precedence(const forall&)
constexpr int mcrl2::data::precedence(const lambda&)
constexpr int mcrl2::data::precedence(const set_comprehension&)
constexpr int mcrl2::data::precedence(const where_clause&)

Typedefs

type mcrl2::data::sort_int::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_int::abs()

Constructor for function symbol abs.

Returns: Function symbol abs.

application mcrl2::data::sort_int::abs(const data_expression &arg0)

Application of function symbol abs.

Parameters:

  • arg0 A data expression.

Returns: Application of abs to a number of arguments.

const core::identifier_string &mcrl2::data::sort_int::abs_name()

Generate identifier abs.

Returns: Identifier abs.

const data_expression &mcrl2::data::sort_int::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 function_symbol &mcrl2::data::sort_int::cint()

Constructor for function symbol @cInt.

Returns: Function symbol cint.

application mcrl2::data::sort_int::cint(const data_expression &arg0)

Application of function symbol @cInt.

Parameters:

  • arg0 A data expression.

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

const core::identifier_string &mcrl2::data::sort_int::cint_name()

Generate identifier @cInt.

Returns: Identifier @cInt.

const function_symbol &mcrl2::data::sort_int::cneg()

Constructor for function symbol @cNeg.

Returns: Function symbol cneg.

application mcrl2::data::sort_int::cneg(const data_expression &arg0)

Application of function symbol @cNeg.

Parameters:

  • arg0 A data expression.

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

const core::identifier_string &mcrl2::data::sort_int::cneg_name()

Generate identifier @cNeg.

Returns: Identifier @cNeg.

application mcrl2::data::sort_int::div(const data_expression &arg0, const data_expression &arg1)

Application of function symbol div.

Parameters:

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

Returns: Application of div to a number of arguments.

function_symbol mcrl2::data::sort_int::div(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::div_name()

Generate identifier div.

Returns: Identifier div.

application mcrl2::data::sort_int::exp(const data_expression &arg0, const data_expression &arg1)

Application of function symbol exp.

Parameters:

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

Returns: Application of exp to a number of arguments.

function_symbol mcrl2::data::sort_int::exp(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::exp_name()

Generate identifier exp.

Returns: Identifier exp.

const function_symbol &mcrl2::data::sort_int::int2nat()

Constructor for function symbol Int2Nat.

Returns: Function symbol int2nat.

application mcrl2::data::sort_int::int2nat(const data_expression &arg0)

Application of function symbol Int2Nat.

Parameters:

  • arg0 A data expression.

Returns: Application of Int2Nat to a number of arguments.

const core::identifier_string &mcrl2::data::sort_int::int2nat_name()

Generate identifier Int2Nat.

Returns: Identifier Int2Nat.

const function_symbol &mcrl2::data::sort_int::int2pos()

Constructor for function symbol Int2Pos.

Returns: Function symbol int2pos.

application mcrl2::data::sort_int::int2pos(const data_expression &arg0)

Application of function symbol Int2Pos.

Parameters:

  • arg0 A data expression.

Returns: Application of Int2Pos to a number of arguments.

const core::identifier_string &mcrl2::data::sort_int::int2pos_name()

Generate identifier Int2Pos.

Returns: Identifier Int2Pos.

const basic_sort &mcrl2::data::sort_int::int_()

Constructor for sort expression Int.

Returns: Sort expression Int.

implementation_map mcrl2::data::sort_int::int_cpp_implementable_constructors()

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

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

implementation_map mcrl2::data::sort_int::int_cpp_implementable_mappings()

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

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

function_symbol_vector mcrl2::data::sort_int::int_generate_constructors_and_functions_code()

Give all system defined mappings and constructors for int_.

Returns: All system defined mappings for int_

function_symbol_vector mcrl2::data::sort_int::int_generate_constructors_code()

Give all system defined constructors for int_.

Returns: All system defined constructors for int_.

data_equation_vector mcrl2::data::sort_int::int_generate_equations_code()

Give all system defined equations for int_.

Returns: All system defined equations for sort int_

function_symbol_vector mcrl2::data::sort_int::int_generate_functions_code()

Give all system defined mappings for int_.

Returns: All system defined mappings for int_

function_symbol_vector mcrl2::data::sort_int::int_mCRL2_usable_constructors()

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

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

function_symbol_vector mcrl2::data::sort_int::int_mCRL2_usable_mappings()

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

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

const core::identifier_string &mcrl2::data::sort_int::int_name()
bool mcrl2::data::sort_int::is_abs_application(const atermpp::aterm_appl &e)

Recogniser for application of abs.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_abs_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function abs.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_cint_application(const atermpp::aterm_appl &e)

Recogniser for application of @cInt.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_cint_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cInt.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_cneg_application(const atermpp::aterm_appl &e)

Recogniser for application of @cNeg.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_cneg_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cNeg.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_div_application(const atermpp::aterm_appl &e)

Recogniser for application of div.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_div_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function div.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_exp_application(const atermpp::aterm_appl &e)

Recogniser for application of exp.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_exp_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function exp.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_int(const sort_expression &e)

Recogniser for sort expression Int.

Parameters:

  • e A sort expression

Returns: true iff e == int_()

bool mcrl2::data::sort_int::is_int2nat_application(const atermpp::aterm_appl &e)

Recogniser for application of Int2Nat.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_int2nat_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Int2Nat.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_int2pos_application(const atermpp::aterm_appl &e)

Recogniser for application of Int2Pos.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_int2pos_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Int2Pos.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::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_int::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_int::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_int::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_int::is_minus_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 minus to a number of arguments.

bool mcrl2::data::sort_int::is_minus_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_int::is_mod_application(const atermpp::aterm_appl &e)

Recogniser for application of mod.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_mod_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function mod.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_nat2int_application(const atermpp::aterm_appl &e)

Recogniser for application of Nat2Int.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_nat2int_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Nat2Int.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_negate_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 negate to a number of arguments.

bool mcrl2::data::sort_int::is_negate_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_int::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_int::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_int::is_pos2int_application(const atermpp::aterm_appl &e)

Recogniser for application of Pos2Int.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_pos2int_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Pos2Int.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_pred_application(const atermpp::aterm_appl &e)

Recogniser for application of pred.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::is_pred_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function pred.

Parameters:

  • e A data expression.

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

bool mcrl2::data::sort_int::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_int::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_int::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_int::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_int::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_int::make_abs(data_expression &result, const data_expression &arg0)

Make an application of function symbol abs.

Parameters:

  • result The data expression where the abs expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::make_cint(data_expression &result, const data_expression &arg0)

Make an application of function symbol @cInt.

Parameters:

  • result The data expression where the @cInt expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::make_cneg(data_expression &result, const data_expression &arg0)

Make an application of function symbol @cNeg.

Parameters:

  • result The data expression where the @cNeg expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::make_div(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol div.

Parameters:

  • result The data expression where the div expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_int::make_exp(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol exp.

Parameters:

  • result The data expression where the exp expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_int::make_int2nat(data_expression &result, const data_expression &arg0)

Make an application of function symbol Int2Nat.

Parameters:

  • result The data expression where the Int2Nat expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::make_int2pos(data_expression &result, const data_expression &arg0)

Make an application of function symbol Int2Pos.

Parameters:

  • result The data expression where the Int2Pos expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::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_int::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_int::make_minus(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_int::make_mod(data_expression &result, const data_expression &arg0, const data_expression &arg1)

Make an application of function symbol mod.

Parameters:

  • result The data expression where the mod expression is put.
  • arg0 A data expression.
  • arg1 A data expression.
void mcrl2::data::sort_int::make_nat2int(data_expression &result, const data_expression &arg0)

Make an application of function symbol Nat2Int.

Parameters:

  • result The data expression where the Nat2Int expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::make_negate(data_expression &result, const data_expression &arg0)

Make an application of function symbol -.

Parameters:

  • result The data expression where the - expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::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_int::make_pos2int(data_expression &result, const data_expression &arg0)

Make an application of function symbol Pos2Int.

Parameters:

  • result The data expression where the Pos2Int expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::make_pred(data_expression &result, const data_expression &arg0)

Make an application of function symbol pred.

Parameters:

  • result The data expression where the pred expression is put.
  • arg0 A data expression.
void mcrl2::data::sort_int::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_int::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.
application mcrl2::data::sort_int::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.

function_symbol mcrl2::data::sort_int::maximum(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::maximum_name()

Generate identifier max.

Returns: Identifier max.

application mcrl2::data::sort_int::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.

function_symbol mcrl2::data::sort_int::minimum(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::minimum_name()

Generate identifier min.

Returns: Identifier min.

application mcrl2::data::sort_int::minus(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.

function_symbol mcrl2::data::sort_int::minus(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::minus_name()

Generate identifier -.

Returns: Identifier -.

application mcrl2::data::sort_int::mod(const data_expression &arg0, const data_expression &arg1)

Application of function symbol mod.

Parameters:

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

Returns: Application of mod to a number of arguments.

function_symbol mcrl2::data::sort_int::mod(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::mod_name()

Generate identifier mod.

Returns: Identifier mod.

const function_symbol &mcrl2::data::sort_int::nat2int()

Constructor for function symbol Nat2Int.

Returns: Function symbol nat2int.

application mcrl2::data::sort_int::nat2int(const data_expression &arg0)

Application of function symbol Nat2Int.

Parameters:

  • arg0 A data expression.

Returns: Application of Nat2Int to a number of arguments.

const core::identifier_string &mcrl2::data::sort_int::nat2int_name()

Generate identifier Nat2Int.

Returns: Identifier Nat2Int.

application mcrl2::data::sort_int::negate(const data_expression &arg0)

Application of function symbol -.

Parameters:

  • arg0 A data expression.

Returns: Application of - to a number of arguments.

function_symbol mcrl2::data::sort_int::negate(const sort_expression &s0)
const core::identifier_string &mcrl2::data::sort_int::negate_name()

Generate identifier -.

Returns: Identifier -.

application mcrl2::data::sort_int::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.

function_symbol mcrl2::data::sort_int::plus(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::plus_name()

Generate identifier +.

Returns: Identifier +.

const function_symbol &mcrl2::data::sort_int::pos2int()

Constructor for function symbol Pos2Int.

Returns: Function symbol pos2int.

application mcrl2::data::sort_int::pos2int(const data_expression &arg0)

Application of function symbol Pos2Int.

Parameters:

  • arg0 A data expression.

Returns: Application of Pos2Int to a number of arguments.

const core::identifier_string &mcrl2::data::sort_int::pos2int_name()

Generate identifier Pos2Int.

Returns: Identifier Pos2Int.

application mcrl2::data::sort_int::pred(const data_expression &arg0)

Application of function symbol pred.

Parameters:

  • arg0 A data expression.

Returns: Application of pred to a number of arguments.

function_symbol mcrl2::data::sort_int::pred(const sort_expression &s0)
const core::identifier_string &mcrl2::data::sort_int::pred_name()

Generate identifier pred.

Returns: Identifier pred.

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

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

Application of function symbol succ.

Parameters:

  • arg0 A data expression.

Returns: Application of succ to a number of arguments.

function_symbol mcrl2::data::sort_int::succ(const sort_expression &s0)
const core::identifier_string &mcrl2::data::sort_int::succ_name()

Generate identifier succ.

Returns: Identifier succ.

application mcrl2::data::sort_int::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.

function_symbol mcrl2::data::sort_int::times(const sort_expression &s0, const sort_expression &s1)
const core::identifier_string &mcrl2::data::sort_int::times_name()

Generate identifier *.

Returns: Identifier *.