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 precedence(const data_expression &x)
int mcrl2::data::precedence(const application &x)
constexpr int mcrl2::data::precedence(const forall&)
constexpr int mcrl2::data::precedence(const exists&)
constexpr int mcrl2::data::precedence(const lambda&)
constexpr int mcrl2::data::precedence(const set_comprehension&)
constexpr int mcrl2::data::precedence(const bag_comprehension&)
constexpr int mcrl2::data::precedence(const where_clause&)

Functions

function_symbol const &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

core::identifier_string const &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

function_symbol const &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

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

Generate identifier @cInt.

Returns: Identifier @cInt

function_symbol const &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

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

Generate identifier @cNeg.

Returns: Identifier @cNeg

function_symbol const &mcrl2::data::sort_int::div(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier div.

Returns: Identifier div

function_symbol const &mcrl2::data::sort_int::exp(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier exp.

Returns: Identifier exp

function_symbol const &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

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

Generate identifier Int2Nat.

Returns: Identifier Int2Nat

function_symbol const &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

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

Generate identifier Int2Pos.

Returns: Identifier Int2Pos

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

Constructor for sort expression Int.

Returns: Sort expression 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_

core::identifier_string const &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

function_symbol const &mcrl2::data::sort_int::maximum(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier max.

Returns: Identifier max

function_symbol const &mcrl2::data::sort_int::minimum(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier min.

Returns: Identifier min

function_symbol const &mcrl2::data::sort_int::minus(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier -.

Returns: Identifier -

function_symbol const &mcrl2::data::sort_int::mod(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier mod.

Returns: Identifier mod

function_symbol const &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

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

Generate identifier Nat2Int.

Returns: Identifier Nat2Int

function_symbol const &mcrl2::data::sort_int::negate(const sort_expression &s0)
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

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

Generate identifier -.

Returns: Identifier -

function_symbol const &mcrl2::data::sort_int::plus(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier +.

Returns: Identifier +

function_symbol const &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

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

Generate identifier Pos2Int.

Returns: Identifier Pos2Int

function_symbol const &mcrl2::data::sort_int::pred(const sort_expression &s0)
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

core::identifier_string const &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

function_symbol const &mcrl2::data::sort_int::succ(const sort_expression &s0)
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

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

Generate identifier succ.

Returns: Identifier succ

function_symbol const &mcrl2::data::sort_int::times(const sort_expression &s0, const sort_expression &s1)
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

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

Generate identifier *.

Returns: Identifier *