pres_expression.h File Reference

The class pres_expression. More...

Go to the source code of this file.

Classes
class	mcrl2::pres_system::pres_expression
	\brief A pres expression More...
class	mcrl2::pres_system::propositional_variable_instantiation
	\brief A propositional variable instantiation More...
class	mcrl2::pres_system::minus
	\brief The not operator for pres expressions More...
class	mcrl2::pres_system::and_
	\brief The and operator for pres expressions More...
class	mcrl2::pres_system::or_
	\brief The or operator for pres expressions More...
class	mcrl2::pres_system::imp
	\brief The implication operator for pres expressions More...
class	mcrl2::pres_system::plus
	\brief The addition operator for pres expressions More...
class	mcrl2::pres_system::const_multiply
	\brief The multiplication with a positive constant with the constant at the left. More...
class	mcrl2::pres_system::const_multiply_alt
	\brief The multiplication with a positive constant with the constant at the right. More...
class	mcrl2::pres_system::infimum
	\brief The infimum over a data type for pres expressions More...
class	mcrl2::pres_system::supremum
	\brief The supremeum over a data type for pres expressions More...
class	mcrl2::pres_system::sum
	\brief The generic sum operator for pres expressions More...
class	mcrl2::pres_system::eqinf
	\brief The indicator whether the argument is infinite More...
class	mcrl2::pres_system::eqninf
	\brief The indicator whether the argument is -infinite More...
class	mcrl2::pres_system::condsm
	\brief Conditional operator with condition smaller than 0 More...
class	mcrl2::pres_system::condeq
	\brief Conditional operator with condition smaller than or equal to 0 More...
struct	mcrl2::core::term_traits< pres_system::pres_expression >
	Contains type information for pres expressions. More...
struct	std::hash< mcrl2::pres_system::pres_expression >
struct	std::hash< mcrl2::pres_system::propositional_variable_instantiation >

Namespaces
namespace	mcrl2
	A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
namespace	mcrl2::pres_system
	The main namespace for the PRES library.
namespace	mcrl2::pres_system::accessors
	The namespace for accessor functions on pres expressions.
namespace	mcrl2::core
namespace	std
	STL namespace.

Typedefs
typedef pbes_system::propositional_variable	mcrl2::pres_system::propositional_variable
	The propositional variable is taken from a pbes_system.
typedef atermpp::term_list< pres_expression >	mcrl2::pres_system::pres_expression_list
	\brief list of pres_expressions
typedef std::vector< pres_expression >	mcrl2::pres_system::pres_expression_vector
	\brief vector of pres_expressions
typedef atermpp::term_list< propositional_variable_instantiation >	mcrl2::pres_system::propositional_variable_instantiation_list
	\brief list of propositional_variable_instantiations
typedef std::vector< propositional_variable_instantiation >	mcrl2::pres_system::propositional_variable_instantiation_vector
	\brief vector of propositional_variable_instantiations
typedef atermpp::term_list< pbes_system::propositional_variable >	mcrl2::pres_system::propositional_variable_list
	\brief list of propositional_variables
typedef std::vector< pbes_system::propositional_variable >	mcrl2::pres_system::propositional_variable_vector
	\brief vector of propositional_variables

Functions
bool	mcrl2::pres_system::is_propositional_variable_instantiation (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_minus (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_and (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_or (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_imp (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_plus (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_const_multiply (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_const_multiply_alt (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_infimum (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_supremum (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_sum (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_eqinf (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_eqninf (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_condsm (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_condeq (const atermpp::aterm &x)
bool	mcrl2::pres_system::is_pres_expression (const atermpp::aterm &x)
std::string	mcrl2::pres_system::pp (const pres_expression &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const pres_expression &x)
void	mcrl2::pres_system::swap (pres_expression &t1, pres_expression &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_propositional_variable_instantiation (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const propositional_variable_instantiation &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const propositional_variable_instantiation &x)
void	mcrl2::pres_system::swap (propositional_variable_instantiation &t1, propositional_variable_instantiation &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_minus (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const minus &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const minus &x)
void	mcrl2::pres_system::swap (minus &t1, minus &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_and_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const and_ &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const and_ &x)
void	mcrl2::pres_system::swap (and_ &t1, and_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_or_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const or_ &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const or_ &x)
void	mcrl2::pres_system::swap (or_ &t1, or_ &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const imp &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const imp &x)
void	mcrl2::pres_system::swap (imp &t1, imp &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_plus (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const plus &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const plus &x)
void	mcrl2::pres_system::swap (plus &t1, plus &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_const_multiply (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const const_multiply &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const const_multiply &x)
void	mcrl2::pres_system::swap (const_multiply &t1, const_multiply &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_const_multiply_alt (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const const_multiply_alt &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const const_multiply_alt &x)
void	mcrl2::pres_system::swap (const_multiply_alt &t1, const_multiply_alt &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_infimum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const infimum &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const infimum &x)
void	mcrl2::pres_system::swap (infimum &t1, infimum &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_supremum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const supremum &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const supremum &x)
void	mcrl2::pres_system::swap (supremum &t1, supremum &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_sum (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const sum &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const sum &x)
void	mcrl2::pres_system::swap (sum &t1, sum &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_eqinf (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const eqinf &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const eqinf &x)
void	mcrl2::pres_system::swap (eqinf &t1, eqinf &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_eqninf (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const eqninf &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const eqninf &x)
void	mcrl2::pres_system::swap (eqninf &t1, eqninf &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_condsm (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const condsm &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const condsm &x)
void	mcrl2::pres_system::swap (condsm &t1, condsm &t2)
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_condeq (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pres_system::pp (const condeq &x)
std::ostream &	mcrl2::pres_system::operator<< (std::ostream &out, const condeq &x)
void	mcrl2::pres_system::swap (condeq &t1, condeq &t2)
	\brief swap overload
std::string	mcrl2::pres_system::pp (const pres_expression_list &x)
std::string	mcrl2::pres_system::pp (const pres_expression_vector &x)
std::string	mcrl2::pres_system::pp (const propositional_variable_instantiation_list &x)
std::string	mcrl2::pres_system::pp (const propositional_variable_instantiation_vector &x)
std::set< pres_system::propositional_variable_instantiation >	mcrl2::pres_system::find_propositional_variable_instantiations (const pres_system::pres_expression &x)
std::set< core::identifier_string >	mcrl2::pres_system::find_identifiers (const pres_system::pres_expression &x)
std::set< data::variable >	mcrl2::pres_system::find_free_variables (const pres_system::pres_expression &x)
bool	mcrl2::pres_system::search_variable (const pres_system::pres_expression &x, const data::variable &v)
pres_system::pres_expression	mcrl2::pres_system::normalize_sorts (const pres_system::pres_expression &x, const data::sort_specification &sortspec)
pres_system::pres_expression	mcrl2::pres_system::translate_user_notation (const pres_system::pres_expression &x)
const pres_expression &	mcrl2::pres_system::true_ ()
const pres_expression &	mcrl2::pres_system::false_ ()
bool	mcrl2::pres_system::is_true (const pres_expression &t)
	Test for the value true.
bool	mcrl2::pres_system::is_false (const pres_expression &t)
	Test for the value false.
bool	mcrl2::pres_system::is_pres_minus (const pres_expression &t)
	Returns true if the term t is a minus expression.
bool	mcrl2::pres_system::is_pres_and (const pres_expression &t)
	Returns true if the term t is an and expression.
bool	mcrl2::pres_system::is_pres_or (const pres_expression &t)
	Returns true if the term t is an or expression.
bool	mcrl2::pres_system::is_pres_imp (const pres_expression &t)
	Returns true if the term t is an imp expression.
bool	mcrl2::pres_system::is_pres_infimum (const pres_expression &t)
	Returns true if the term t is a generalized minus expression.
bool	mcrl2::pres_system::is_pres_supremum (const pres_expression &t)
	Returns true if the term t is a generalized maximum expression.
bool	mcrl2::pres_system::is_universal_and (const pres_expression &t)
	Test for a conjunction.
bool	mcrl2::pres_system::is_universal_or (const pres_expression &t)
	Test for a disjunction.
bool	mcrl2::pres_system::is_data (const pres_expression &t)
	Returns true if the term t is a data expression.
const pres_expression &	mcrl2::pres_system::accessors::arg (const pres_expression &t)
	Returns the pres expression argument of expressions of type not, exists and forall.
pres_expression	mcrl2::pres_system::accessors::data_arg (const pres_expression &t)
	Returns the pres expression argument of expressions of type not, exists and forall.
const pres_expression &	mcrl2::pres_system::accessors::left (const pres_expression &t)
	Returns the left hand side of an expression of type and, or or imp.
pres_expression	mcrl2::pres_system::accessors::data_left (const pres_expression &x)
	Returns the left hand side of an expression of type and, or or imp.
const pres_expression &	mcrl2::pres_system::accessors::right (const pres_expression &t)
	Returns the right hand side of an expression of type and, or or imp.
pres_expression	mcrl2::pres_system::accessors::data_right (const pres_expression &x)
	Returns the left hand side of an expression of type and, or or imp.
const data::variable_list &	mcrl2::pres_system::accessors::var (const pres_expression &t)
	Returns the variables of a quantification expression.
const core::identifier_string &	mcrl2::pres_system::accessors::name (const pres_expression &t)
	Returns the name of a propositional variable expression.
const data::data_expression_list &	mcrl2::pres_system::accessors::param (const pres_expression &t)
	Returns the parameters of a propositional variable instantiation.
pres_expression	mcrl2::pres_system::make_infimum (const data::variable_list &l, const pres_expression &p)
	Make a generalized minimum. It checks for an empty variable list, which is not allowed.
pres_expression	mcrl2::pres_system::make_supremum (const data::variable_list &l, const pres_expression &p)
	Make an generalized maximum. It checks for an empty variable list, which is not allowed.
void	mcrl2::pres_system::optimized_minus (pres_expression &result, const pres_expression &p)
	Make a negation.
void	mcrl2::pres_system::optimized_and (pres_expression &result, const pres_expression &p, const pres_expression &q)
	Make a conjunction.
void	mcrl2::pres_system::optimized_or (pres_expression &result, const pres_expression &p, const pres_expression &q)
	Make a disjunction.
void	mcrl2::pres_system::optimized_plus (pres_expression &result, const pres_expression &p, const pres_expression &q)
	Make a disjunction.
void	mcrl2::pres_system::optimized_infimum (pres_expression &result, const data::variable_list &l, const pres_expression &p)
	Make an implication.
void	mcrl2::pres_system::optimized_supremum (pres_expression &result, const data::variable_list &l, const pres_expression &p)
	Make a supremum. If l is empty, p is returned.
void	mcrl2::pres_system::optimized_sum (pres_expression &result, const data::variable_list &l, const pres_expression &p, const data::data_specification &data_specification, const data::rewriter &rewr)
	Make an sum quantification. If l is empty, p is returned.
void	mcrl2::pres_system::optimized_condsm (pres_expression &result, const pres_expression &p1, const pres_expression &p2, const pres_expression &p3)
	Make an optimized condsm expression.
void	mcrl2::pres_system::optimized_condeq (pres_expression &result, const pres_expression &p1, const pres_expression &p2, const pres_expression &p3)
	Make an optimized condsm expression.
void	mcrl2::pres_system::optimized_eqinf (pres_expression &result, const pres_expression &p)
	Make an optimized eqinf expression.
void	mcrl2::pres_system::optimized_eqninf (pres_expression &result, const pres_expression &p)
	Make an optimized eqinf expression.
void	mcrl2::pres_system::optimized_const_multiply (pres_expression &result, const data::data_expression &d, const pres_expression &p)
	Make an optimized const_multiply expression.
void	mcrl2::pres_system::optimized_const_multiply_alt (pres_expression &result, const data::data_expression &d, const pres_expression &p)
	Make an optimized const_multiply_alt expression.
bool	mcrl2::pres_system::is_constant (const pres_expression &x)
data::variable_list	mcrl2::pres_system::free_variables (const pres_expression &x)
template<class... ARGUMENTS>
void	mcrl2::pres_system::make_propositional_variable (atermpp::aterm &t, const ARGUMENTS &... args)

Detailed Description

The class pres_expression.

Definition in file pres_expression.h.