mcrl2/data/real.h

Include file:

#include "mcrl2/data/real.h"

The standard sort real_.

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

Functions

function_symbol const &mcrl2::data::sort_real::abs(const sort_expression &s0)
application mcrl2::data::sort_real::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_real::abs_name()

Generate identifier abs.

Returns: Identifier abs

const data_expression &mcrl2::data::sort_real::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_real::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_real::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_real::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 const &mcrl2::data::sort_real::ceil()

Constructor for function symbol ceil.

Returns: Function symbol ceil

application mcrl2::data::sort_real::ceil(const data_expression &arg0)

Application of function symbol ceil.

Parameters:

  • arg0 A data expression

Returns: Application of ceil to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::ceil_name()

Generate identifier ceil.

Returns: Identifier ceil

function_symbol const &mcrl2::data::sort_real::creal()

Constructor for function symbol @cReal.

Returns: Function symbol creal

application mcrl2::data::sort_real::creal(const data_expression &arg0, const data_expression &arg1)

Application of function symbol @cReal.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @cReal to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::creal_name()

Generate identifier @cReal.

Returns: Identifier @cReal

function_symbol const &mcrl2::data::sort_real::divides(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_real::divides(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_real::divides_name()

Generate identifier /.

Returns: Identifier /

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

Generate identifier exp.

Returns: Identifier exp

function_symbol const &mcrl2::data::sort_real::floor()

Constructor for function symbol floor.

Returns: Function symbol floor

application mcrl2::data::sort_real::floor(const data_expression &arg0)

Application of function symbol floor.

Parameters:

  • arg0 A data expression

Returns: Application of floor to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::floor_name()

Generate identifier floor.

Returns: Identifier floor

function_symbol const &mcrl2::data::sort_real::int2real()

Constructor for function symbol Int2Real.

Returns: Function symbol int2real

application mcrl2::data::sort_real::int2real(const data_expression &arg0)

Application of function symbol Int2Real.

Parameters:

  • arg0 A data expression

Returns: Application of Int2Real to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::int2real_name()

Generate identifier Int2Real.

Returns: Identifier Int2Real

bool mcrl2::data::sort_real::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_real::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_real::is_ceil_application(const atermpp::aterm_appl &e)

Recogniser for application of ceil.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_ceil_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function ceil.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching ceil

bool mcrl2::data::sort_real::is_creal_application(const atermpp::aterm_appl &e)

Recogniser for application of @cReal.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_creal_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @cReal.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @cReal

bool mcrl2::data::sort_real::is_divides_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 divides to a number of arguments

bool mcrl2::data::sort_real::is_divides_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_real::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_real::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_real::is_floor_application(const atermpp::aterm_appl &e)

Recogniser for application of floor.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_floor_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function floor.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching floor

bool mcrl2::data::sort_real::is_int2real_application(const atermpp::aterm_appl &e)

Recogniser for application of Int2Real.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_int2real_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Int2Real.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Int2Real

bool mcrl2::data::sort_real::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_real::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_real::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_real::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_real::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_real::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_real::is_nat2real_application(const atermpp::aterm_appl &e)

Recogniser for application of Nat2Real.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_nat2real_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Nat2Real.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Nat2Real

bool mcrl2::data::sort_real::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_real::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_real::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_real::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_real::is_pos2real_application(const atermpp::aterm_appl &e)

Recogniser for application of Pos2Real.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_pos2real_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Pos2Real.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Pos2Real

bool mcrl2::data::sort_real::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_real::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_real::is_real(const sort_expression &e)

Recogniser for sort expression Real.

Parameters:

  • e A sort expression

Returns: true iff e == real_()

bool mcrl2::data::sort_real::is_real2int_application(const atermpp::aterm_appl &e)

Recogniser for application of Real2Int.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_real2int_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Real2Int.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Real2Int

bool mcrl2::data::sort_real::is_real2nat_application(const atermpp::aterm_appl &e)

Recogniser for application of Real2Nat.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_real2nat_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Real2Nat.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Real2Nat

bool mcrl2::data::sort_real::is_real2pos_application(const atermpp::aterm_appl &e)

Recogniser for application of Real2Pos.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_real2pos_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function Real2Pos.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching Real2Pos

bool mcrl2::data::sort_real::is_reduce_fraction_application(const atermpp::aterm_appl &e)

Recogniser for application of @redfrac.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_reduce_fraction_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @redfrac.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @redfrac

bool mcrl2::data::sort_real::is_reduce_fraction_helper_application(const atermpp::aterm_appl &e)

Recogniser for application of @redfrachlp.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_reduce_fraction_helper_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @redfrachlp.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @redfrachlp

bool mcrl2::data::sort_real::is_reduce_fraction_where_application(const atermpp::aterm_appl &e)

Recogniser for application of @redfracwhr.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_reduce_fraction_where_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function @redfracwhr.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching @redfracwhr

bool mcrl2::data::sort_real::is_round_application(const atermpp::aterm_appl &e)

Recogniser for application of round.

Parameters:

  • e A data expression

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

bool mcrl2::data::sort_real::is_round_function_symbol(const atermpp::aterm_appl &e)

Recogniser for function round.

Parameters:

  • e A data expression

Returns: true iff e is the function symbol matching round

bool mcrl2::data::sort_real::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_real::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_real::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_real::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_real::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_real::maximum(const sort_expression &s0, const sort_expression &s1)
application mcrl2::data::sort_real::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_real::maximum_name()

Generate identifier max.

Returns: Identifier max

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

Generate identifier min.

Returns: Identifier min

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

Generate identifier -.

Returns: Identifier -

function_symbol const &mcrl2::data::sort_real::nat2real()

Constructor for function symbol Nat2Real.

Returns: Function symbol nat2real

application mcrl2::data::sort_real::nat2real(const data_expression &arg0)

Application of function symbol Nat2Real.

Parameters:

  • arg0 A data expression

Returns: Application of Nat2Real to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::nat2real_name()

Generate identifier Nat2Real.

Returns: Identifier Nat2Real

function_symbol const &mcrl2::data::sort_real::negate(const sort_expression &s0)
application mcrl2::data::sort_real::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_real::negate_name()

Generate identifier -.

Returns: Identifier -

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

Generate identifier +.

Returns: Identifier +

function_symbol const &mcrl2::data::sort_real::pos2real()

Constructor for function symbol Pos2Real.

Returns: Function symbol pos2real

application mcrl2::data::sort_real::pos2real(const data_expression &arg0)

Application of function symbol Pos2Real.

Parameters:

  • arg0 A data expression

Returns: Application of Pos2Real to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::pos2real_name()

Generate identifier Pos2Real.

Returns: Identifier Pos2Real

function_symbol const &mcrl2::data::sort_real::pred(const sort_expression &s0)
application mcrl2::data::sort_real::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_real::pred_name()

Generate identifier pred.

Returns: Identifier pred

function_symbol const &mcrl2::data::sort_real::real2int()

Constructor for function symbol Real2Int.

Returns: Function symbol real2int

application mcrl2::data::sort_real::real2int(const data_expression &arg0)

Application of function symbol Real2Int.

Parameters:

  • arg0 A data expression

Returns: Application of Real2Int to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::real2int_name()

Generate identifier Real2Int.

Returns: Identifier Real2Int

function_symbol const &mcrl2::data::sort_real::real2nat()

Constructor for function symbol Real2Nat.

Returns: Function symbol real2nat

application mcrl2::data::sort_real::real2nat(const data_expression &arg0)

Application of function symbol Real2Nat.

Parameters:

  • arg0 A data expression

Returns: Application of Real2Nat to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::real2nat_name()

Generate identifier Real2Nat.

Returns: Identifier Real2Nat

function_symbol const &mcrl2::data::sort_real::real2pos()

Constructor for function symbol Real2Pos.

Returns: Function symbol real2pos

application mcrl2::data::sort_real::real2pos(const data_expression &arg0)

Application of function symbol Real2Pos.

Parameters:

  • arg0 A data expression

Returns: Application of Real2Pos to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::real2pos_name()

Generate identifier Real2Pos.

Returns: Identifier Real2Pos

basic_sort const &mcrl2::data::sort_real::real_()

Constructor for sort expression Real.

Returns: Sort expression Real

function_symbol_vector mcrl2::data::sort_real::real_generate_constructors_code()

Give all system defined constructors for real_.

Returns: All system defined constructors for real_

data_equation_vector mcrl2::data::sort_real::real_generate_equations_code()

Give all system defined equations for real_.

Returns: All system defined equations for sort real_

function_symbol_vector mcrl2::data::sort_real::real_generate_functions_code()

Give all system defined mappings for real_.

Returns: All system defined mappings for real_

core::identifier_string const &mcrl2::data::sort_real::real_name()
function_symbol const &mcrl2::data::sort_real::reduce_fraction()

Constructor for function symbol @redfrac.

Returns: Function symbol reduce_fraction

application mcrl2::data::sort_real::reduce_fraction(const data_expression &arg0, const data_expression &arg1)

Application of function symbol @redfrac.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @redfrac to a number of arguments

function_symbol const &mcrl2::data::sort_real::reduce_fraction_helper()

Constructor for function symbol @redfrachlp.

Returns: Function symbol reduce_fraction_helper

application mcrl2::data::sort_real::reduce_fraction_helper(const data_expression &arg0, const data_expression &arg1)

Application of function symbol @redfrachlp.

Parameters:

  • arg0 A data expression
  • arg1 A data expression

Returns: Application of @redfrachlp to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::reduce_fraction_helper_name()

Generate identifier @redfrachlp.

Returns: Identifier @redfrachlp

core::identifier_string const &mcrl2::data::sort_real::reduce_fraction_name()

Generate identifier @redfrac.

Returns: Identifier @redfrac

function_symbol const &mcrl2::data::sort_real::reduce_fraction_where()

Constructor for function symbol @redfracwhr.

Returns: Function symbol reduce_fraction_where

application mcrl2::data::sort_real::reduce_fraction_where(const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)

Application of function symbol @redfracwhr.

Parameters:

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

Returns: Application of @redfracwhr to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::reduce_fraction_where_name()

Generate identifier @redfracwhr.

Returns: Identifier @redfracwhr

const data_expression &mcrl2::data::sort_real::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_real::round()

Constructor for function symbol round.

Returns: Function symbol round

application mcrl2::data::sort_real::round(const data_expression &arg0)

Application of function symbol round.

Parameters:

  • arg0 A data expression

Returns: Application of round to a number of arguments

core::identifier_string const &mcrl2::data::sort_real::round_name()

Generate identifier round.

Returns: Identifier round

function_symbol const &mcrl2::data::sort_real::succ(const sort_expression &s0)
application mcrl2::data::sort_real::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_real::succ_name()

Generate identifier succ.

Returns: Identifier succ

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

Generate identifier *.

Returns: Identifier *