mcrl2::pres_system::pres_equation Class Reference

pres equation. More...

#include <pres_equation.h>

Public Types
typedef pres_expression	term_type
	The expression type of the equation.
typedef propositional_variable	variable_type
	The variable type of the equation.
typedef fixpoint_symbol	symbol_type
	The symbol type of the equation.

Public Member Functions
	pres_equation ()=default
	Constructor.
	pres_equation (const fixpoint_symbol &symbol, const propositional_variable &variable, const pres_expression &expr)
	Constructor.
const fixpoint_symbol &	symbol () const
	Returns the fixpoint symbol of the equation.
fixpoint_symbol &	symbol ()
	Returns the fixpoint symbol of the equation.
const propositional_variable &	variable () const
	Returns the pres variable of the equation.
propositional_variable &	variable ()
	Returns the pres variable of the equation.
const pres_expression &	formula () const
	Returns the predicate formula on the right hand side of the equation.
pres_expression &	formula ()
	Returns the predicate formula on the right hand side of the equation.
bool	is_solved () const
	Returns true if the predicate formula on the right hand side contains no predicate variables.
void	swap (pres_equation &other)
	Swaps the contents.
void	mark (std::stack< std::reference_wrapper< atermpp::detail::_aterm > > &todo) const

Protected Attributes
fixpoint_symbol	m_symbol
	The fixpoint symbol of the equation.
propositional_variable	m_variable
	The variable on the left hand side of the equation.
pres_expression	m_formula
	The expression on the right hand side of the equation.

Detailed Description

pres equation.

Definition at line 33 of file pres_equation.h.

Member Typedef Documentation

symbol_type

typedef fixpoint_symbol mcrl2::pres_system::pres_equation::symbol_type

The symbol type of the equation.

Definition at line 53 of file pres_equation.h.

term_type

typedef pres_expression mcrl2::pres_system::pres_equation::term_type

The expression type of the equation.

Definition at line 47 of file pres_equation.h.

variable_type

typedef propositional_variable mcrl2::pres_system::pres_equation::variable_type

The variable type of the equation.

Definition at line 50 of file pres_equation.h.

Constructor & Destructor Documentation

pres_equation() [1/2]

mcrl2::pres_system::pres_equation::pres_equation ( )

default

Constructor.

pres_equation() [2/2]

mcrl2::pres_system::pres_equation::pres_equation ( const fixpoint_symbol &  symbol, const propositional_variable &  variable, const pres_expression &  expr  )

inline

Constructor.

Parameters

symbol	A fixpoint symbol
variable	A propositional variable declaration
expr	A PRES expression

Definition at line 62 of file pres_equation.h.

Member Function Documentation

formula() [1/2]

pres_expression & mcrl2::pres_system::pres_equation::formula ( )

inline

Returns the predicate formula on the right hand side of the equation.

Returns

The predicate formula on the right hand side of the equation.

Definition at line 107 of file pres_equation.h.

formula() [2/2]

const pres_expression & mcrl2::pres_system::pres_equation::formula ( ) const

inline

Returns the predicate formula on the right hand side of the equation.

Returns

The predicate formula on the right hand side of the equation.

Definition at line 100 of file pres_equation.h.

is_solved()

bool mcrl2::pres_system::pres_equation::is_solved

(

)

const

Returns true if the predicate formula on the right hand side contains no predicate variables.

Returns

True if the predicate formula on the right hand side contains no predicate variables.

Definition at line 106 of file pres.cpp.

mark()

void mcrl2::pres_system::pres_equation::mark ( std::stack< std::reference_wrapper< atermpp::detail::_aterm > > &  todo ) const

inline

Definition at line 126 of file pres_equation.h.

swap()

void mcrl2::pres_system::pres_equation::swap ( pres_equation &  other )

inline

Swaps the contents.

Definition at line 118 of file pres_equation.h.

symbol() [1/2]

fixpoint_symbol & mcrl2::pres_system::pres_equation::symbol ( )

inline

Returns the fixpoint symbol of the equation.

Returns

The fixpoint symbol of the equation.

Definition at line 79 of file pres_equation.h.

symbol() [2/2]

const fixpoint_symbol & mcrl2::pres_system::pres_equation::symbol ( ) const

inline

Returns the fixpoint symbol of the equation.

Returns

The fixpoint symbol of the equation.

Definition at line 72 of file pres_equation.h.

variable() [1/2]

propositional_variable & mcrl2::pres_system::pres_equation::variable ( )

inline

Returns the pres variable of the equation.

Returns

The pres variable of the equation.

Definition at line 93 of file pres_equation.h.

variable() [2/2]

const propositional_variable & mcrl2::pres_system::pres_equation::variable ( ) const

inline

Returns the pres variable of the equation.

Returns

The pres variable of the equation.

Definition at line 86 of file pres_equation.h.

Member Data Documentation

m_formula

pres_expression mcrl2::pres_system::pres_equation::m_formula

protected

The expression on the right hand side of the equation.

Definition at line 43 of file pres_equation.h.

m_symbol

fixpoint_symbol mcrl2::pres_system::pres_equation::m_symbol

protected

The fixpoint symbol of the equation.

Definition at line 37 of file pres_equation.h.

m_variable

propositional_variable mcrl2::pres_system::pres_equation::m_variable

protected

The variable on the left hand side of the equation.

Definition at line 40 of file pres_equation.h.

---

The documentation for this class was generated from the following files:

• pres/include/mcrl2/pres/pres_equation.h
• pres/source/pres.cpp