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.

Typedefs¶

type mcrl2::data::sort_real::implementation_map¶: typedef for std::map< function_symbol, std::pair< std::function< data_expression(const data_expression &)>, std::string > >

Functions¶

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.

function_symbol mcrl2::data::sort_real::abs(const sort_expression &s0)¶

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

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

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

Generate identifier ceil.

Returns: Identifier ceil.

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

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

Generate identifier @cReal.

Returns: Identifier @cReal.

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.

function_symbol mcrl2::data::sort_real::divides(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::divides_name()¶

Generate identifier /.

Returns: Identifier /.

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.

function_symbol mcrl2::data::sort_real::exp(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::exp_name()¶

Generate identifier exp.

Returns: Identifier exp.

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

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

Generate identifier floor.

Returns: Identifier floor.

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

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

void mcrl2::data::sort_real::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_real::make_ceil(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol ceil.

Parameters:

result The data expression where the ceil expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::make_creal(data_expression &result, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol @cReal.

Parameters:

result The data expression where the @cReal expression is put.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_real::make_divides(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_real::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_real::make_floor(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol floor.

Parameters:

result The data expression where the floor expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::make_int2real(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol Int2Real.

Parameters:

result The data expression where the Int2Real expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::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_real::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_real::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_real::make_nat2real(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol Nat2Real.

Parameters:

result The data expression where the Nat2Real expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::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_real::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_real::make_pos2real(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol Pos2Real.

Parameters:

result The data expression where the Pos2Real expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::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_real::make_real2int(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol Real2Int.

Parameters:

result The data expression where the Real2Int expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::make_real2nat(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol Real2Nat.

Parameters:

result The data expression where the Real2Nat expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::make_real2pos(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol Real2Pos.

Parameters:

result The data expression where the Real2Pos expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::make_reduce_fraction(data_expression &result, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol @redfrac.

Parameters:

result The data expression where the @redfrac expression is put.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_real::make_reduce_fraction_helper(data_expression &result, const data_expression &arg0, const data_expression &arg1)¶

Make an application of function symbol @redfrachlp.

Parameters:

result The data expression where the @redfrachlp expression is put.
arg0 A data expression.
arg1 A data expression.

void mcrl2::data::sort_real::make_reduce_fraction_where(data_expression &result, const data_expression &arg0, const data_expression &arg1, const data_expression &arg2)¶

Make an application of function symbol @redfracwhr.

Parameters:

result The data expression where the @redfracwhr expression is put.
arg0 A data expression.
arg1 A data expression.
arg2 A data expression.

void mcrl2::data::sort_real::make_round(data_expression &result, const data_expression &arg0)¶

Make an application of function symbol round.

Parameters:

result The data expression where the round expression is put.
arg0 A data expression.

void mcrl2::data::sort_real::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_real::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_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.

function_symbol mcrl2::data::sort_real::maximum(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::maximum_name()¶

Generate identifier max.

Returns: Identifier max.

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.

function_symbol mcrl2::data::sort_real::minimum(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::minimum_name()¶

Generate identifier min.

Returns: Identifier min.

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.

function_symbol mcrl2::data::sort_real::minus(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::minus_name()¶

Generate identifier -.

Returns: Identifier -.

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

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

Generate identifier Nat2Real.

Returns: Identifier Nat2Real.

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.

function_symbol mcrl2::data::sort_real::negate(const sort_expression &s0)¶

const core::identifier_string &mcrl2::data::sort_real::negate_name()¶

Generate identifier -.

Returns: Identifier -.

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.

function_symbol mcrl2::data::sort_real::plus(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::plus_name()¶

Generate identifier +.

Returns: Identifier +.

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

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

Generate identifier Pos2Real.

Returns: Identifier Pos2Real.

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.

function_symbol mcrl2::data::sort_real::pred(const sort_expression &s0)¶

const core::identifier_string &mcrl2::data::sort_real::pred_name()¶

Generate identifier pred.

Returns: Identifier pred.

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

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

Generate identifier Real2Int.

Returns: Identifier Real2Int.

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

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

Generate identifier Real2Nat.

Returns: Identifier Real2Nat.

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

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

Generate identifier Real2Pos.

Returns: Identifier Real2Pos.

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

Constructor for sort expression Real.

Returns: Sort expression Real.

implementation_map mcrl2::data::sort_real::real_cpp_implementable_constructors()¶

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

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

implementation_map mcrl2::data::sort_real::real_cpp_implementable_mappings()¶

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

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

function_symbol_vector mcrl2::data::sort_real::real_generate_constructors_and_functions_code()¶

Give all system defined mappings and constructors for real_.

Returns: All system defined mappings for 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_

function_symbol_vector mcrl2::data::sort_real::real_mCRL2_usable_constructors()¶

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

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

function_symbol_vector mcrl2::data::sort_real::real_mCRL2_usable_mappings()¶

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

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

const core::identifier_string &mcrl2::data::sort_real::real_name()¶

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

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

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

Generate identifier @redfrachlp.

Returns: Identifier @redfrachlp.

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

Generate identifier @redfrac.

Returns: Identifier @redfrac.

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

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

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

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

Generate identifier round.

Returns: Identifier round.

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.

function_symbol mcrl2::data::sort_real::succ(const sort_expression &s0)¶

const core::identifier_string &mcrl2::data::sort_real::succ_name()¶

Generate identifier succ.

Returns: Identifier succ.

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.

function_symbol mcrl2::data::sort_real::times(const sort_expression &s0, const sort_expression &s1)¶

const core::identifier_string &mcrl2::data::sort_real::times_name()¶

Generate identifier *.

Returns: Identifier *.

mcrl2/data/real.h¶

Typedefs¶

Functions¶

Table of Contents

Previous topic

Next topic

This page