mCRL2
Loading...
Searching...
No Matches
real1.h File Reference

Go to the source code of this file.

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::data
 Namespace for all data library functionality.
 
namespace  mcrl2::data::sort_real
 Namespace for system defined sort real_.
 

Typedefs

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

Functions

const core::identifier_stringmcrl2::data::sort_real::real_name ()
 
const basic_sortmcrl2::data::sort_real::real_ ()
 Constructor for sort expression Real.
 
bool mcrl2::data::sort_real::is_real (const sort_expression &e)
 Recogniser for sort expression Real.
 
function_symbol_vector mcrl2::data::sort_real::real_generate_constructors_code ()
 Give all system defined constructors 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_.
 
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_.
 
const core::identifier_stringmcrl2::data::sort_real::creal_name ()
 Generate identifier @cReal.
 
const function_symbolmcrl2::data::sort_real::creal ()
 Constructor for function symbol @cReal.
 
bool mcrl2::data::sort_real::is_creal_function_symbol (const atermpp::aterm &e)
 Recogniser for function @cReal.
 
application mcrl2::data::sort_real::creal (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @cReal.
 
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.
 
bool mcrl2::data::sort_real::is_creal_application (const atermpp::aterm &e)
 Recogniser for application of @cReal.
 
const core::identifier_stringmcrl2::data::sort_real::pos2real_name ()
 Generate identifier Pos2Real.
 
const function_symbolmcrl2::data::sort_real::pos2real ()
 Constructor for function symbol Pos2Real.
 
bool mcrl2::data::sort_real::is_pos2real_function_symbol (const atermpp::aterm &e)
 Recogniser for function Pos2Real.
 
application mcrl2::data::sort_real::pos2real (const data_expression &arg0)
 Application of function symbol Pos2Real.
 
void mcrl2::data::sort_real::make_pos2real (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Pos2Real.
 
bool mcrl2::data::sort_real::is_pos2real_application (const atermpp::aterm &e)
 Recogniser for application of Pos2Real.
 
const core::identifier_stringmcrl2::data::sort_real::nat2real_name ()
 Generate identifier Nat2Real.
 
const function_symbolmcrl2::data::sort_real::nat2real ()
 Constructor for function symbol Nat2Real.
 
bool mcrl2::data::sort_real::is_nat2real_function_symbol (const atermpp::aterm &e)
 Recogniser for function Nat2Real.
 
application mcrl2::data::sort_real::nat2real (const data_expression &arg0)
 Application of function symbol Nat2Real.
 
void mcrl2::data::sort_real::make_nat2real (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Nat2Real.
 
bool mcrl2::data::sort_real::is_nat2real_application (const atermpp::aterm &e)
 Recogniser for application of Nat2Real.
 
const core::identifier_stringmcrl2::data::sort_real::int2real_name ()
 Generate identifier Int2Real.
 
const function_symbolmcrl2::data::sort_real::int2real ()
 Constructor for function symbol Int2Real.
 
bool mcrl2::data::sort_real::is_int2real_function_symbol (const atermpp::aterm &e)
 Recogniser for function Int2Real.
 
application mcrl2::data::sort_real::int2real (const data_expression &arg0)
 Application of function symbol Int2Real.
 
void mcrl2::data::sort_real::make_int2real (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Int2Real.
 
bool mcrl2::data::sort_real::is_int2real_application (const atermpp::aterm &e)
 Recogniser for application of Int2Real.
 
const core::identifier_stringmcrl2::data::sort_real::real2pos_name ()
 Generate identifier Real2Pos.
 
const function_symbolmcrl2::data::sort_real::real2pos ()
 Constructor for function symbol Real2Pos.
 
bool mcrl2::data::sort_real::is_real2pos_function_symbol (const atermpp::aterm &e)
 Recogniser for function Real2Pos.
 
application mcrl2::data::sort_real::real2pos (const data_expression &arg0)
 Application of function symbol Real2Pos.
 
void mcrl2::data::sort_real::make_real2pos (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Real2Pos.
 
bool mcrl2::data::sort_real::is_real2pos_application (const atermpp::aterm &e)
 Recogniser for application of Real2Pos.
 
const core::identifier_stringmcrl2::data::sort_real::real2nat_name ()
 Generate identifier Real2Nat.
 
const function_symbolmcrl2::data::sort_real::real2nat ()
 Constructor for function symbol Real2Nat.
 
bool mcrl2::data::sort_real::is_real2nat_function_symbol (const atermpp::aterm &e)
 Recogniser for function Real2Nat.
 
application mcrl2::data::sort_real::real2nat (const data_expression &arg0)
 Application of function symbol Real2Nat.
 
void mcrl2::data::sort_real::make_real2nat (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Real2Nat.
 
bool mcrl2::data::sort_real::is_real2nat_application (const atermpp::aterm &e)
 Recogniser for application of Real2Nat.
 
const core::identifier_stringmcrl2::data::sort_real::real2int_name ()
 Generate identifier Real2Int.
 
const function_symbolmcrl2::data::sort_real::real2int ()
 Constructor for function symbol Real2Int.
 
bool mcrl2::data::sort_real::is_real2int_function_symbol (const atermpp::aterm &e)
 Recogniser for function Real2Int.
 
application mcrl2::data::sort_real::real2int (const data_expression &arg0)
 Application of function symbol Real2Int.
 
void mcrl2::data::sort_real::make_real2int (data_expression &result, const data_expression &arg0)
 Make an application of function symbol Real2Int.
 
bool mcrl2::data::sort_real::is_real2int_application (const atermpp::aterm &e)
 Recogniser for application of Real2Int.
 
const core::identifier_stringmcrl2::data::sort_real::maximum_name ()
 Generate identifier max.
 
function_symbol mcrl2::data::sort_real::maximum (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_maximum_function_symbol (const atermpp::aterm &e)
 Recogniser for function max.
 
application mcrl2::data::sort_real::maximum (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol max.
 
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.
 
bool mcrl2::data::sort_real::is_maximum_application (const atermpp::aterm &e)
 Recogniser for application of max.
 
const core::identifier_stringmcrl2::data::sort_real::minimum_name ()
 Generate identifier min.
 
function_symbol mcrl2::data::sort_real::minimum (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_minimum_function_symbol (const atermpp::aterm &e)
 Recogniser for function min.
 
application mcrl2::data::sort_real::minimum (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol min.
 
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.
 
bool mcrl2::data::sort_real::is_minimum_application (const atermpp::aterm &e)
 Recogniser for application of min.
 
const core::identifier_stringmcrl2::data::sort_real::abs_name ()
 Generate identifier abs.
 
function_symbol mcrl2::data::sort_real::abs (const sort_expression &s0)
 
bool mcrl2::data::sort_real::is_abs_function_symbol (const atermpp::aterm &e)
 Recogniser for function abs.
 
application mcrl2::data::sort_real::abs (const data_expression &arg0)
 Application of function symbol abs.
 
void mcrl2::data::sort_real::make_abs (data_expression &result, const data_expression &arg0)
 Make an application of function symbol abs.
 
bool mcrl2::data::sort_real::is_abs_application (const atermpp::aterm &e)
 Recogniser for application of abs.
 
const core::identifier_stringmcrl2::data::sort_real::negate_name ()
 Generate identifier -.
 
function_symbol mcrl2::data::sort_real::negate (const sort_expression &s0)
 
bool mcrl2::data::sort_real::is_negate_function_symbol (const atermpp::aterm &e)
 Recogniser for function -.
 
application mcrl2::data::sort_real::negate (const data_expression &arg0)
 Application of function symbol -.
 
void mcrl2::data::sort_real::make_negate (data_expression &result, const data_expression &arg0)
 Make an application of function symbol -.
 
bool mcrl2::data::sort_real::is_negate_application (const atermpp::aterm &e)
 Recogniser for application of -.
 
const core::identifier_stringmcrl2::data::sort_real::succ_name ()
 Generate identifier succ.
 
function_symbol mcrl2::data::sort_real::succ (const sort_expression &s0)
 
bool mcrl2::data::sort_real::is_succ_function_symbol (const atermpp::aterm &e)
 Recogniser for function succ.
 
application mcrl2::data::sort_real::succ (const data_expression &arg0)
 Application of function symbol succ.
 
void mcrl2::data::sort_real::make_succ (data_expression &result, const data_expression &arg0)
 Make an application of function symbol succ.
 
bool mcrl2::data::sort_real::is_succ_application (const atermpp::aterm &e)
 Recogniser for application of succ.
 
const core::identifier_stringmcrl2::data::sort_real::pred_name ()
 Generate identifier pred.
 
function_symbol mcrl2::data::sort_real::pred (const sort_expression &s0)
 
bool mcrl2::data::sort_real::is_pred_function_symbol (const atermpp::aterm &e)
 Recogniser for function pred.
 
application mcrl2::data::sort_real::pred (const data_expression &arg0)
 Application of function symbol pred.
 
void mcrl2::data::sort_real::make_pred (data_expression &result, const data_expression &arg0)
 Make an application of function symbol pred.
 
bool mcrl2::data::sort_real::is_pred_application (const atermpp::aterm &e)
 Recogniser for application of pred.
 
const core::identifier_stringmcrl2::data::sort_real::plus_name ()
 Generate identifier +.
 
function_symbol mcrl2::data::sort_real::plus (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_plus_function_symbol (const atermpp::aterm &e)
 Recogniser for function +.
 
application mcrl2::data::sort_real::plus (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol +.
 
void mcrl2::data::sort_real::make_plus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol +.
 
bool mcrl2::data::sort_real::is_plus_application (const atermpp::aterm &e)
 Recogniser for application of +.
 
const core::identifier_stringmcrl2::data::sort_real::minus_name ()
 Generate identifier -.
 
function_symbol mcrl2::data::sort_real::minus (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_minus_function_symbol (const atermpp::aterm &e)
 Recogniser for function -.
 
application mcrl2::data::sort_real::minus (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol -.
 
void mcrl2::data::sort_real::make_minus (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol -.
 
bool mcrl2::data::sort_real::is_minus_application (const atermpp::aterm &e)
 Recogniser for application of -.
 
const core::identifier_stringmcrl2::data::sort_real::times_name ()
 Generate identifier *.
 
function_symbol mcrl2::data::sort_real::times (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_times_function_symbol (const atermpp::aterm &e)
 Recogniser for function *.
 
application mcrl2::data::sort_real::times (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol *.
 
void mcrl2::data::sort_real::make_times (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol *.
 
bool mcrl2::data::sort_real::is_times_application (const atermpp::aterm &e)
 Recogniser for application of *.
 
const core::identifier_stringmcrl2::data::sort_real::exp_name ()
 Generate identifier exp.
 
function_symbol mcrl2::data::sort_real::exp (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_exp_function_symbol (const atermpp::aterm &e)
 Recogniser for function exp.
 
application mcrl2::data::sort_real::exp (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol exp.
 
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.
 
bool mcrl2::data::sort_real::is_exp_application (const atermpp::aterm &e)
 Recogniser for application of exp.
 
const core::identifier_stringmcrl2::data::sort_real::divides_name ()
 Generate identifier /.
 
function_symbol mcrl2::data::sort_real::divides (const sort_expression &s0, const sort_expression &s1)
 
bool mcrl2::data::sort_real::is_divides_function_symbol (const atermpp::aterm &e)
 Recogniser for function /.
 
application mcrl2::data::sort_real::divides (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol /.
 
void mcrl2::data::sort_real::make_divides (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol /.
 
bool mcrl2::data::sort_real::is_divides_application (const atermpp::aterm &e)
 Recogniser for application of /.
 
const core::identifier_stringmcrl2::data::sort_real::floor_name ()
 Generate identifier floor.
 
const function_symbolmcrl2::data::sort_real::floor ()
 Constructor for function symbol floor.
 
bool mcrl2::data::sort_real::is_floor_function_symbol (const atermpp::aterm &e)
 Recogniser for function floor.
 
application mcrl2::data::sort_real::floor (const data_expression &arg0)
 Application of function symbol floor.
 
void mcrl2::data::sort_real::make_floor (data_expression &result, const data_expression &arg0)
 Make an application of function symbol floor.
 
bool mcrl2::data::sort_real::is_floor_application (const atermpp::aterm &e)
 Recogniser for application of floor.
 
const core::identifier_stringmcrl2::data::sort_real::ceil_name ()
 Generate identifier ceil.
 
const function_symbolmcrl2::data::sort_real::ceil ()
 Constructor for function symbol ceil.
 
bool mcrl2::data::sort_real::is_ceil_function_symbol (const atermpp::aterm &e)
 Recogniser for function ceil.
 
application mcrl2::data::sort_real::ceil (const data_expression &arg0)
 Application of function symbol ceil.
 
void mcrl2::data::sort_real::make_ceil (data_expression &result, const data_expression &arg0)
 Make an application of function symbol ceil.
 
bool mcrl2::data::sort_real::is_ceil_application (const atermpp::aterm &e)
 Recogniser for application of ceil.
 
const core::identifier_stringmcrl2::data::sort_real::round_name ()
 Generate identifier round.
 
const function_symbolmcrl2::data::sort_real::round ()
 Constructor for function symbol round.
 
bool mcrl2::data::sort_real::is_round_function_symbol (const atermpp::aterm &e)
 Recogniser for function round.
 
application mcrl2::data::sort_real::round (const data_expression &arg0)
 Application of function symbol round.
 
void mcrl2::data::sort_real::make_round (data_expression &result, const data_expression &arg0)
 Make an application of function symbol round.
 
bool mcrl2::data::sort_real::is_round_application (const atermpp::aterm &e)
 Recogniser for application of round.
 
const core::identifier_stringmcrl2::data::sort_real::reduce_fraction_name ()
 Generate identifier @redfrac.
 
const function_symbolmcrl2::data::sort_real::reduce_fraction ()
 Constructor for function symbol @redfrac.
 
bool mcrl2::data::sort_real::is_reduce_fraction_function_symbol (const atermpp::aterm &e)
 Recogniser for function @redfrac.
 
application mcrl2::data::sort_real::reduce_fraction (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @redfrac.
 
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.
 
bool mcrl2::data::sort_real::is_reduce_fraction_application (const atermpp::aterm &e)
 Recogniser for application of @redfrac.
 
const core::identifier_stringmcrl2::data::sort_real::reduce_fraction_where_name ()
 Generate identifier @redfracwhr.
 
const function_symbolmcrl2::data::sort_real::reduce_fraction_where ()
 Constructor for function symbol @redfracwhr.
 
bool mcrl2::data::sort_real::is_reduce_fraction_where_function_symbol (const atermpp::aterm &e)
 Recogniser for function @redfracwhr.
 
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.
 
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.
 
bool mcrl2::data::sort_real::is_reduce_fraction_where_application (const atermpp::aterm &e)
 Recogniser for application of @redfracwhr.
 
const core::identifier_stringmcrl2::data::sort_real::reduce_fraction_helper_name ()
 Generate identifier @redfrachlp.
 
const function_symbolmcrl2::data::sort_real::reduce_fraction_helper ()
 Constructor for function symbol @redfrachlp.
 
bool mcrl2::data::sort_real::is_reduce_fraction_helper_function_symbol (const atermpp::aterm &e)
 Recogniser for function @redfrachlp.
 
application mcrl2::data::sort_real::reduce_fraction_helper (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol @redfrachlp.
 
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.
 
bool mcrl2::data::sort_real::is_reduce_fraction_helper_application (const atermpp::aterm &e)
 Recogniser for application of @redfrachlp.
 
function_symbol_vector mcrl2::data::sort_real::real_generate_functions_code ()
 Give all system defined mappings for real_.
 
function_symbol_vector mcrl2::data::sort_real::real_generate_constructors_and_functions_code ()
 Give all system defined mappings and constructors 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_.
 
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_.
 
const data_expressionmcrl2::data::sort_real::left (const data_expression &e)
 Function for projecting out argument. left from an application.
 
const data_expressionmcrl2::data::sort_real::right (const data_expression &e)
 Function for projecting out argument. right from an application.
 
const data_expressionmcrl2::data::sort_real::arg (const data_expression &e)
 Function for projecting out argument. arg from an application.
 
const data_expressionmcrl2::data::sort_real::arg1 (const data_expression &e)
 Function for projecting out argument. arg1 from an application.
 
const data_expressionmcrl2::data::sort_real::arg2 (const data_expression &e)
 Function for projecting out argument. arg2 from an application.
 
const data_expressionmcrl2::data::sort_real::arg3 (const data_expression &e)
 Function for projecting out argument. arg3 from an application.
 
data_equation_vector mcrl2::data::sort_real::real_generate_equations_code ()
 Give all system defined equations for real_.