pbes_expression.h File Reference

The class pbes_expression. More...

Go to the source code of this file.

Classes
class	mcrl2::pbes_system::pbes_expression
	\brief A pbes expression More...
class	mcrl2::pbes_system::propositional_variable_instantiation
	\brief A propositional variable instantiation More...
class	mcrl2::pbes_system::not_
	\brief The not operator for pbes expressions More...
class	mcrl2::pbes_system::and_
	\brief The and operator for pbes expressions More...
class	mcrl2::pbes_system::or_
	\brief The or operator for pbes expressions More...
class	mcrl2::pbes_system::imp
	\brief The implication operator for pbes expressions More...
class	mcrl2::pbes_system::forall
	\brief The universal quantification operator for pbes expressions More...
class	mcrl2::pbes_system::exists
	\brief The existential quantification operator for pbes expressions More...
struct	mcrl2::core::term_traits< pbes_system::pbes_expression >
	Contains type information for pbes expressions. More...
struct	std::hash< mcrl2::pbes_system::pbes_expression >
struct	std::hash< mcrl2::pbes_system::propositional_variable_instantiation >

Namespaces
namespace	mcrl2
namespace	mcrl2::pbes_system
	The main namespace for the PBES library.
namespace	mcrl2::pbes_system::accessors
	The namespace for accessor functions on pbes expressions.
namespace	mcrl2::core
namespace	std
	STL namespace.

Typedefs
using	mcrl2::pbes_system::pbes_expression_list = atermpp::term_list< pbes_expression >
	\brief list of pbes_expressions
using	mcrl2::pbes_system::pbes_expression_vector = std::vector< pbes_expression >
	\brief vector of pbes_expressions
using	mcrl2::pbes_system::propositional_variable_instantiation_list = atermpp::term_list< propositional_variable_instantiation >
	\brief list of propositional_variable_instantiations
using	mcrl2::pbes_system::propositional_variable_instantiation_vector = std::vector< propositional_variable_instantiation >
	\brief vector of propositional_variable_instantiations

Functions
bool	mcrl2::pbes_system::is_propositional_variable_instantiation (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_not (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_and (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_or (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_imp (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_forall (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_exists (const atermpp::aterm &x)
bool	mcrl2::pbes_system::is_pbes_expression (const atermpp::aterm &x)
std::string	mcrl2::pbes_system::pp (const pbes_system::pbes_expression &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const pbes_expression &x)
void	mcrl2::pbes_system::swap (pbes_expression &t1, pbes_expression &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_propositional_variable_instantiation (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::propositional_variable_instantiation &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const propositional_variable_instantiation &x)
void	mcrl2::pbes_system::swap (propositional_variable_instantiation &t1, propositional_variable_instantiation &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_not_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::not_ &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const not_ &x)
void	mcrl2::pbes_system::swap (not_ &t1, not_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_and_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::and_ &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const and_ &x)
void	mcrl2::pbes_system::swap (and_ &t1, and_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_or_ (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::or_ &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const or_ &x)
void	mcrl2::pbes_system::swap (or_ &t1, or_ &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_imp (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::imp &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const imp &x)
void	mcrl2::pbes_system::swap (imp &t1, imp &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_forall (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::forall &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const forall &x)
void	mcrl2::pbes_system::swap (forall &t1, forall &t2) noexcept
	\brief swap overload
template<class... ARGUMENTS>
void	mcrl2::pbes_system::make_exists (atermpp::aterm &t, const ARGUMENTS &... args)
std::string	mcrl2::pbes_system::pp (const pbes_system::exists &x, bool arg0)
std::ostream &	mcrl2::pbes_system::operator<< (std::ostream &out, const exists &x)
void	mcrl2::pbes_system::swap (exists &t1, exists &t2) noexcept
	\brief swap overload
std::string	mcrl2::pbes_system::pp (const pbes_system::pbes_expression_list &x, bool arg0)
std::string	mcrl2::pbes_system::pp (const pbes_system::pbes_expression_vector &x, bool arg0)
std::string	mcrl2::pbes_system::pp (const pbes_system::propositional_variable_instantiation_list &x, bool arg0)
std::string	mcrl2::pbes_system::pp (const pbes_system::propositional_variable_instantiation_vector &x, bool arg0)
std::set< pbes_system::propositional_variable_instantiation >	mcrl2::pbes_system::find_propositional_variable_instantiations (const pbes_system::pbes_expression &x)
std::set< core::identifier_string >	mcrl2::pbes_system::find_identifiers (const pbes_system::pbes_expression &x)
std::set< data::variable >	mcrl2::pbes_system::find_free_variables (const pbes_system::pbes_expression &x)
bool	mcrl2::pbes_system::search_variable (const pbes_system::pbes_expression &x, const data::variable &v)
pbes_system::pbes_expression	mcrl2::pbes_system::normalize_sorts (const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
pbes_system::pbes_expression	mcrl2::pbes_system::translate_user_notation (const pbes_system::pbes_expression &x)
const pbes_expression &	mcrl2::pbes_system::true_ ()
const pbes_expression &	mcrl2::pbes_system::false_ ()
bool	mcrl2::pbes_system::is_true (const pbes_expression &t)
	Test for the value true.
bool	mcrl2::pbes_system::is_false (const pbes_expression &t)
	Test for the value false.
bool	mcrl2::pbes_system::is_pbes_not (const pbes_expression &t)
	Returns true if the term t is a not expression.
bool	mcrl2::pbes_system::is_pbes_and (const pbes_expression &t)
	Returns true if the term t is an and expression.
bool	mcrl2::pbes_system::is_pbes_or (const pbes_expression &t)
	Returns true if the term t is an or expression.
bool	mcrl2::pbes_system::is_pbes_imp (const pbes_expression &t)
	Returns true if the term t is an imp expression.
bool	mcrl2::pbes_system::is_pbes_forall (const pbes_expression &t)
	Returns true if the term t is a universal quantification.
bool	mcrl2::pbes_system::is_pbes_exists (const pbes_expression &t)
	Returns true if the term t is an existential quantification.
bool	mcrl2::pbes_system::is_universal_not (const pbes_expression &t)
	Test for a conjunction.
bool	mcrl2::pbes_system::is_universal_and (const pbes_expression &t)
	Test for a conjunction.
bool	mcrl2::pbes_system::is_universal_or (const pbes_expression &t)
	Test for a disjunction.
bool	mcrl2::pbes_system::is_data (const pbes_expression &t)
	Returns true if the term t is a data expression.
const pbes_expression &	mcrl2::pbes_system::accessors::arg (const pbes_expression &t)
	Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression &	mcrl2::pbes_system::accessors::data_arg (const pbes_expression &t)
	Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression &	mcrl2::pbes_system::accessors::left (const pbes_expression &t)
	Returns the left hand side of an expression of type and, or or imp.
const pbes_expression &	mcrl2::pbes_system::accessors::data_left (const pbes_expression &x)
	Returns the left hand side of an expression of type and, or or imp.
const pbes_expression &	mcrl2::pbes_system::accessors::right (const pbes_expression &t)
	Returns the right hand side of an expression of type and, or or imp.
const pbes_expression &	mcrl2::pbes_system::accessors::data_right (const pbes_expression &x)
	Returns the left hand side of an expression of type and, or or imp.
const data::variable_list &	mcrl2::pbes_system::accessors::var (const pbes_expression &t)
	Returns the variables of a quantification expression.
const core::identifier_string &	mcrl2::pbes_system::accessors::name (const pbes_expression &t)
	Returns the name of a propositional variable expression.
const data::data_expression_list &	mcrl2::pbes_system::accessors::param (const pbes_expression &t)
	Returns the parameters of a propositional variable instantiation.
pbes_expression	mcrl2::pbes_system::make_forall_ (const data::variable_list &l, const pbes_expression &p)
	Make a universal quantification. It checks for an empty variable list, which is not allowed.
pbes_expression	mcrl2::pbes_system::make_exists_ (const data::variable_list &l, const pbes_expression &p)
	Make an existential quantification. It checks for an empty variable list, which is not allowed.
void	mcrl2::pbes_system::optimized_not (pbes_expression &result, const pbes_expression &p)
	Make a negation.
void	mcrl2::pbes_system::optimized_and (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a conjunction.
void	mcrl2::pbes_system::optimized_or (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make a disjunction.
void	mcrl2::pbes_system::optimized_imp (pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
	Make an implication.
void	mcrl2::pbes_system::optimized_forall (pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
	Make a universal quantification If l is empty, p is returned.
void	mcrl2::pbes_system::optimized_exists (pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
	Make an existential quantification If l is empty, p is returned.
bool	mcrl2::pbes_system::is_constant (const pbes_expression &x)
const data::variable_list &	mcrl2::pbes_system::quantifier_variables (const pbes_expression &x)
data::variable_list	mcrl2::pbes_system::free_variables (const pbes_expression &x)

Detailed Description

The class pbes_expression.

Definition in file pbes_expression.h.