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

This file contains some functions that are present in all libraries except the data library. In the data library they have different names, or are located in different namespaces. Note that this file can not be used everywhere, in particular not when people expose the sort_bool namespace. More...

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.
 

Functions

bool mcrl2::data::is_true (const data_expression &x)
 Test if x is true.
 
bool mcrl2::data::is_false (const data_expression &x)
 Test if x is false.
 
bool mcrl2::data::is_not (const data_expression &x)
 Test if x is a negation.
 
bool mcrl2::data::is_or (const data_expression &x)
 Test if x is a disjunction.
 
bool mcrl2::data::is_and (const data_expression &x)
 Test if x is a conjunction.
 
bool mcrl2::data::is_imp (const data_expression &x)
 Test if x is an implication.
 
bool mcrl2::data::is_equal_to (const data_expression &x)
 Test if x is an equality.
 
bool mcrl2::data::is_not_equal_to (const data_expression &x)
 Test if x is an inequality.
 
const data_expressionmcrl2::data::true_ ()
 
const data_expressionmcrl2::data::false_ ()
 
data_expression mcrl2::data::not_ (const data_expression &x)
 
data_expression mcrl2::data::or_ (const data_expression &x, const data_expression &y)
 
data_expression mcrl2::data::and_ (const data_expression &x, const data_expression &y)
 
data_expression mcrl2::data::imp (const data_expression &x, const data_expression &y)
 
bool mcrl2::data::is_bool (const sort_expression &x)
 
sort_expression mcrl2::data::bool_ ()
 
data_expression mcrl2::data::make_forall_ (const data::variable_list &v, const data_expression &x)
 Make a universal quantification. It checks for an empty variable list, which is not allowed.
 
data_expression mcrl2::data::make_exists_ (const data::variable_list &v, const data_expression &x)
 Make an existential quantification. It checks for an empty variable list, which is not allowed.
 

Detailed Description

This file contains some functions that are present in all libraries except the data library. In the data library they have different names, or are located in different namespaces. Note that this file can not be used everywhere, in particular not when people expose the sort_bool namespace.

Definition in file consistency.h.