mCRL2
Loading...
Searching...
No Matches
mcrl2::data::sort_bool Namespace Reference

Namespace for system defined sort bool_. More...

Typedefs

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

Functions

const core::identifier_stringbool_name ()
 
const basic_sortbool_ ()
 Constructor for sort expression Bool.
 
bool is_bool (const sort_expression &e)
 Recogniser for sort expression Bool.
 
const core::identifier_stringtrue_name ()
 Generate identifier true.
 
const function_symboltrue_ ()
 Constructor for function symbol true.
 
bool is_true_function_symbol (const atermpp::aterm &e)
 Recogniser for function true.
 
const core::identifier_stringfalse_name ()
 Generate identifier false.
 
const function_symbolfalse_ ()
 Constructor for function symbol false.
 
bool is_false_function_symbol (const atermpp::aterm &e)
 Recogniser for function false.
 
function_symbol_vector bool_generate_constructors_code ()
 Give all system defined constructors for bool_.
 
function_symbol_vector bool_mCRL2_usable_constructors ()
 Give all defined constructors which can be used in mCRL2 specs for bool_.
 
implementation_map bool_cpp_implementable_constructors ()
 Give all system defined constructors which have an implementation in C++ and not in rewrite rules for bool_.
 
const core::identifier_stringnot_name ()
 Generate identifier !.
 
const function_symbolnot_ ()
 Constructor for function symbol !.
 
bool is_not_function_symbol (const atermpp::aterm &e)
 Recogniser for function !.
 
application not_ (const data_expression &arg0)
 Application of function symbol !.
 
void make_not_ (data_expression &result, const data_expression &arg0)
 Make an application of function symbol !.
 
bool is_not_application (const atermpp::aterm &e)
 Recogniser for application of !.
 
const core::identifier_stringand_name ()
 Generate identifier &&.
 
const function_symboland_ ()
 Constructor for function symbol &&.
 
bool is_and_function_symbol (const atermpp::aterm &e)
 Recogniser for function &&.
 
application and_ (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol &&.
 
void make_and_ (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol &&.
 
bool is_and_application (const atermpp::aterm &e)
 Recogniser for application of &&.
 
const core::identifier_stringor_name ()
 Generate identifier ||.
 
const function_symbolor_ ()
 Constructor for function symbol ||.
 
bool is_or_function_symbol (const atermpp::aterm &e)
 Recogniser for function ||.
 
application or_ (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol ||.
 
void make_or_ (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol ||.
 
bool is_or_application (const atermpp::aterm &e)
 Recogniser for application of ||.
 
const core::identifier_stringimplies_name ()
 Generate identifier =>.
 
const function_symbolimplies ()
 Constructor for function symbol =>.
 
bool is_implies_function_symbol (const atermpp::aterm &e)
 Recogniser for function =>.
 
application implies (const data_expression &arg0, const data_expression &arg1)
 Application of function symbol =>.
 
void make_implies (data_expression &result, const data_expression &arg0, const data_expression &arg1)
 Make an application of function symbol =>.
 
bool is_implies_application (const atermpp::aterm &e)
 Recogniser for application of =>.
 
function_symbol_vector bool_generate_functions_code ()
 Give all system defined mappings for bool_.
 
function_symbol_vector bool_generate_constructors_and_functions_code ()
 Give all system defined mappings and constructors for bool_.
 
function_symbol_vector bool_mCRL2_usable_mappings ()
 Give all system defined mappings that can be used in mCRL2 specs for bool_.
 
implementation_map bool_cpp_implementable_mappings ()
 Give all system defined mappings that are to be implemented in C++ code for bool_.
 
const data_expressionarg (const data_expression &e)
 Function for projecting out argument. arg from an application.
 
const data_expressionleft (const data_expression &e)
 Function for projecting out argument. left from an application.
 
const data_expressionright (const data_expression &e)
 Function for projecting out argument. right from an application.
 
data_equation_vector bool_generate_equations_code ()
 Give all system defined equations for bool_.
 
data_expression bool_ (bool b)
 Constructs expression of type Bool from an integral type.
 
bool is_boolean_constant (data_expression const &b)
 Determines whether b is a Boolean constant.
 

Detailed Description

Namespace for system defined sort bool_.

Typedef Documentation

◆ implementation_map

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

Definition at line 150 of file bool.h.

Function Documentation

◆ and_() [1/2]

const function_symbol & mcrl2::data::sort_bool::and_ ( )
inline

Constructor for function symbol &&.

Returns
Function symbol and_.

Definition at line 235 of file bool.h.

◆ and_() [2/2]

application mcrl2::data::sort_bool::and_ ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol &&.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of && to a number of arguments.

Definition at line 260 of file bool.h.

◆ and_name()

const core::identifier_string & mcrl2::data::sort_bool::and_name ( )
inline

Generate identifier &&.

Returns
Identifier &&.

Definition at line 225 of file bool.h.

◆ arg()

const data_expression & mcrl2::data::sort_bool::arg ( const data_expression e)
inline

Function for projecting out argument. arg from an application.

Parameters
eA data expression.
Precondition
arg is defined for e.
Returns
The argument of e that corresponds to arg.

Definition at line 469 of file bool.h.

◆ bool_() [1/2]

const basic_sort & mcrl2::data::sort_bool::bool_ ( )
inline

Constructor for sort expression Bool.

Returns
Sort expression Bool.

Definition at line 44 of file bool.h.

◆ bool_() [2/2]

data_expression mcrl2::data::sort_bool::bool_ ( bool  b)
inline

Constructs expression of type Bool from an integral type.

Parameters
bA Boolean

Definition at line 30 of file standard_utility.h.

◆ bool_cpp_implementable_constructors()

implementation_map mcrl2::data::sort_bool::bool_cpp_implementable_constructors ( )
inline

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

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

Definition at line 154 of file bool.h.

◆ bool_cpp_implementable_mappings()

implementation_map mcrl2::data::sort_bool::bool_cpp_implementable_mappings ( )
inline

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

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

Definition at line 458 of file bool.h.

◆ bool_generate_constructors_and_functions_code()

function_symbol_vector mcrl2::data::sort_bool::bool_generate_constructors_and_functions_code ( )
inline

Give all system defined mappings and constructors for bool_.

Returns
All system defined mappings for bool_

Definition at line 429 of file bool.h.

◆ bool_generate_constructors_code()

function_symbol_vector mcrl2::data::sort_bool::bool_generate_constructors_code ( )
inline

Give all system defined constructors for bool_.

Returns
All system defined constructors for bool_.

Definition at line 130 of file bool.h.

◆ bool_generate_equations_code()

data_equation_vector mcrl2::data::sort_bool::bool_generate_equations_code ( )
inline

Give all system defined equations for bool_.

Returns
All system defined equations for sort bool_

Definition at line 502 of file bool.h.

◆ bool_generate_functions_code()

function_symbol_vector mcrl2::data::sort_bool::bool_generate_functions_code ( )
inline

Give all system defined mappings for bool_.

Returns
All system defined mappings for bool_

Definition at line 416 of file bool.h.

◆ bool_mCRL2_usable_constructors()

function_symbol_vector mcrl2::data::sort_bool::bool_mCRL2_usable_constructors ( )
inline

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

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

Definition at line 141 of file bool.h.

◆ bool_mCRL2_usable_mappings()

function_symbol_vector mcrl2::data::sort_bool::bool_mCRL2_usable_mappings ( )
inline

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

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

Definition at line 442 of file bool.h.

◆ bool_name()

const core::identifier_string & mcrl2::data::sort_bool::bool_name ( )
inline

Definition at line 35 of file bool.h.

◆ false_()

const function_symbol & mcrl2::data::sort_bool::false_ ( )
inline

Constructor for function symbol false.

Returns
Function symbol false_.

Definition at line 109 of file bool.h.

◆ false_name()

const core::identifier_string & mcrl2::data::sort_bool::false_name ( )
inline

Generate identifier false.

Returns
Identifier false.

Definition at line 99 of file bool.h.

◆ implies() [1/2]

const function_symbol & mcrl2::data::sort_bool::implies ( )
inline

Constructor for function symbol =>.

Returns
Function symbol implies.

Definition at line 363 of file bool.h.

◆ implies() [2/2]

application mcrl2::data::sort_bool::implies ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol =>.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of => to a number of arguments.

Definition at line 388 of file bool.h.

◆ implies_name()

const core::identifier_string & mcrl2::data::sort_bool::implies_name ( )
inline

Generate identifier =>.

Returns
Identifier =>.

Definition at line 353 of file bool.h.

◆ is_and_application()

bool mcrl2::data::sort_bool::is_and_application ( const atermpp::aterm e)
inline

Recogniser for application of &&.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol and_ to a number of arguments.

Definition at line 281 of file bool.h.

◆ is_and_function_symbol()

bool mcrl2::data::sort_bool::is_and_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function &&.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching &&.

Definition at line 245 of file bool.h.

◆ is_bool()

bool mcrl2::data::sort_bool::is_bool ( const sort_expression e)
inline

Recogniser for sort expression Bool.

Parameters
eA sort expression
Returns
true iff e == bool_()

Definition at line 54 of file bool.h.

◆ is_boolean_constant()

bool mcrl2::data::sort_bool::is_boolean_constant ( data_expression const &  b)
inline

Determines whether b is a Boolean constant.

Parameters
bA data expression

Definition at line 37 of file standard_utility.h.

◆ is_false_function_symbol()

bool mcrl2::data::sort_bool::is_false_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function false.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching false.

Definition at line 119 of file bool.h.

◆ is_implies_application()

bool mcrl2::data::sort_bool::is_implies_application ( const atermpp::aterm e)
inline

Recogniser for application of =>.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol implies to a number of arguments.

Definition at line 409 of file bool.h.

◆ is_implies_function_symbol()

bool mcrl2::data::sort_bool::is_implies_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function =>.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching =>.

Definition at line 373 of file bool.h.

◆ is_not_application()

bool mcrl2::data::sort_bool::is_not_application ( const atermpp::aterm e)
inline

Recogniser for application of !.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol not_ to a number of arguments.

Definition at line 217 of file bool.h.

◆ is_not_function_symbol()

bool mcrl2::data::sort_bool::is_not_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function !.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching !.

Definition at line 183 of file bool.h.

◆ is_or_application()

bool mcrl2::data::sort_bool::is_or_application ( const atermpp::aterm e)
inline

Recogniser for application of ||.

Parameters
eA data expression.
Returns
true iff e is an application of function symbol or_ to a number of arguments.

Definition at line 345 of file bool.h.

◆ is_or_function_symbol()

bool mcrl2::data::sort_bool::is_or_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function ||.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching ||.

Definition at line 309 of file bool.h.

◆ is_true_function_symbol()

bool mcrl2::data::sort_bool::is_true_function_symbol ( const atermpp::aterm e)
inline

Recogniser for function true.

Parameters
eA data expression.
Returns
true iff e is the function symbol matching true.

Definition at line 87 of file bool.h.

◆ left()

const data_expression & mcrl2::data::sort_bool::left ( const data_expression e)
inline

Function for projecting out argument. left from an application.

Parameters
eA data expression.
Precondition
left is defined for e.
Returns
The argument of e that corresponds to left.

Definition at line 481 of file bool.h.

◆ make_and_()

void mcrl2::data::sort_bool::make_and_ ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol &&.

Parameters
resultThe data expression where the && expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 271 of file bool.h.

◆ make_implies()

void mcrl2::data::sort_bool::make_implies ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol =>.

Parameters
resultThe data expression where the => expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 399 of file bool.h.

◆ make_not_()

void mcrl2::data::sort_bool::make_not_ ( data_expression result,
const data_expression arg0 
)
inline

Make an application of function symbol !.

Parameters
resultThe data expression where the ! expression is put.
arg0A data expression.

Definition at line 207 of file bool.h.

◆ make_or_()

void mcrl2::data::sort_bool::make_or_ ( data_expression result,
const data_expression arg0,
const data_expression arg1 
)
inline

Make an application of function symbol ||.

Parameters
resultThe data expression where the || expression is put.
arg0A data expression.
arg1A data expression.

Definition at line 335 of file bool.h.

◆ not_() [1/2]

const function_symbol & mcrl2::data::sort_bool::not_ ( )
inline

Constructor for function symbol !.

Returns
Function symbol not_.

Definition at line 173 of file bool.h.

◆ not_() [2/2]

application mcrl2::data::sort_bool::not_ ( const data_expression arg0)
inline

Application of function symbol !.

Parameters
arg0A data expression.
Returns
Application of ! to a number of arguments.

Definition at line 197 of file bool.h.

◆ not_name()

const core::identifier_string & mcrl2::data::sort_bool::not_name ( )
inline

Generate identifier !.

Returns
Identifier !.

Definition at line 163 of file bool.h.

◆ or_() [1/2]

const function_symbol & mcrl2::data::sort_bool::or_ ( )
inline

Constructor for function symbol ||.

Returns
Function symbol or_.

Definition at line 299 of file bool.h.

◆ or_() [2/2]

application mcrl2::data::sort_bool::or_ ( const data_expression arg0,
const data_expression arg1 
)
inline

Application of function symbol ||.

Parameters
arg0A data expression.
arg1A data expression.
Returns
Application of || to a number of arguments.

Definition at line 324 of file bool.h.

◆ or_name()

const core::identifier_string & mcrl2::data::sort_bool::or_name ( )
inline

Generate identifier ||.

Returns
Identifier ||.

Definition at line 289 of file bool.h.

◆ right()

const data_expression & mcrl2::data::sort_bool::right ( const data_expression e)
inline

Function for projecting out argument. right from an application.

Parameters
eA data expression.
Precondition
right is defined for e.
Returns
The argument of e that corresponds to right.

Definition at line 493 of file bool.h.

◆ true_()

const function_symbol & mcrl2::data::sort_bool::true_ ( )
inline

Constructor for function symbol true.

Returns
Function symbol true_.

Definition at line 77 of file bool.h.

◆ true_name()

const core::identifier_string & mcrl2::data::sort_bool::true_name ( )
inline

Generate identifier true.

Returns
Identifier true.

Definition at line 67 of file bool.h.