Represents an edge of the dependency graph. The assignments are stored implicitly using the 'right' parameter. The condition determines under what circumstances the influence of the edge is propagated to its target vertex. More...

#include <constelm.h>

Inheritance diagram for mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge:

Public Member Functions
	edge ()=default
	Constructor.

	edge (const propositional_variable &src, const qvar_list &qvars, const propositional_variable_instantiation &tgt, const std::set< data::variable > &conj_context, const std::set< data::variable > &disj_context, data::data_expression c=data::sort_bool::true_())
	Constructor.

std::string	to_string () const
	Returns a string representation of the edge.

const propositional_variable &	source () const
	The propositional variable at the source of the edge.

const qvar_list &	quantified_variables () const

const propositional_variable_instantiation &	target () const
	The propositional variable instantiation that determines the target of the edge.

const data::data_expression &	condition () const
	The condition of the edge.

qvar_list	quantifier_inside_approximation (const qvar_list &Q) const
	Try to guess which quantifiers of Q can end up directly before target, when the quantifier inside rewriter is applied.

Public Member Functions inherited from mcrl2::data::data_expression
	data_expression ()
	\brief Default constructor X3.

	data_expression (const atermpp::aterm &term)

	data_expression (const data_expression &) noexcept=default
	Move semantics.

	data_expression (data_expression &&) noexcept=default

data_expression &	operator= (const data_expression &) noexcept=default

data_expression &	operator= (data_expression &&) noexcept=default

bool	is_default_data_expression () const
	A function to efficiently determine whether a data expression is made by the default constructor.

application	operator() (const data_expression &e) const
	Apply a data expression to a data expression.

application	operator() (const data_expression &e1, const data_expression &e2) const
	Apply a data expression to two data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3) const
	Apply a data expression to three data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4) const
	Apply a data expression to four data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5) const
	Apply a data expression to five data expressions.

application	operator() (const data_expression &e1, const data_expression &e2, const data_expression &e3, const data_expression &e4, const data_expression &e5, const data_expression &e6) const
	Apply a data expression to six data expressions.

sort_expression	sort () const
	Returns the sort of the data expression.

Public Member Functions inherited from atermpp::aterm
	aterm ()
	Default constructor.

	aterm (const aterm &other) noexcept=default
	This class has user-declared copy constructor so declare default copy and move operators.

aterm &	operator= (const aterm &other) noexcept=default

	aterm (aterm &&other) noexcept=default

aterm &	operator= (aterm &&other) noexcept=default

template<class ForwardIterator , typename std::enable_if< mcrl2::utilities::is_iterator< ForwardIterator >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr, typename std::enable_if<!std::is_same< typename ForwardIterator::iterator_category, std::output_iterator_tag >::value >::type * = nullptr>
	aterm (const function_symbol &sym, ForwardIterator begin, ForwardIterator end)
	Constructor that provides an aterm based on a function symbol and forward iterator providing the arguments.

template<class InputIterator , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr, typename std::enable_if< std::is_same< typename InputIterator::iterator_category, std::input_iterator_tag >::value >::type * = nullptr>
	aterm (const function_symbol &sym, InputIterator begin, InputIterator end)
	Constructor that provides an aterm based on a function symbol and an input iterator providing the arguments.

template<class InputIterator , class TermConverter , typename std::enable_if< mcrl2::utilities::is_iterator< InputIterator >::value >::type * = nullptr>
	aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter)

	aterm (const function_symbol &sym)
	Constructor.

template<typename ... Terms>
	aterm (const function_symbol &symbol, const Terms &...arguments)
	Constructor for n-arity function application.

const function_symbol &	function () const
	Returns the function symbol belonging to an aterm.

size_type	size () const
	Returns the number of arguments of this term.

bool	empty () const
	Returns true if the term has no arguments.

const_iterator	begin () const
	Returns an iterator pointing to the first argument.

const_iterator	end () const
	Returns a const_iterator pointing past the last argument.

constexpr size_type	max_size () const
	Returns the largest possible number of arguments.

const aterm &	operator[] (const size_type i) const
	Returns the i-th argument.

Public Member Functions inherited from atermpp::aterm_core
	aterm_core () noexcept
	Default constructor.

	~aterm_core () noexcept
	Standard destructor.

	aterm_core (const detail::_aterm *t) noexcept
	Constructor based on an internal term data structure. This is not for public use.

	aterm_core (const aterm_core &other) noexcept
	Copy constructor.

	aterm_core (aterm_core &&other) noexcept
	Move constructor.

aterm_core &	operator= (const aterm_core &other) noexcept
	Assignment operator.

aterm_core &	assign (const aterm_core &other, detail::thread_aterm_pool &pool) noexcept
	Assignment operator, to be used if busy and forbidden flags are explicitly available.

template<bool CHECK_BUSY_FLAG = true>
aterm_core &	unprotected_assign (const aterm_core &other) noexcept
	Assignment operator, to be used when the busy flags do not need to be set.

aterm_core &	operator= (aterm_core &&other) noexcept
	Move assignment operator.

Public Member Functions inherited from atermpp::unprotected_aterm_core
	unprotected_aterm_core () noexcept
	Default constuctor.

	unprotected_aterm_core (const detail::_aterm *term) noexcept
	Constructor.

bool	type_is_appl () const noexcept
	Dynamic check whether the term is an aterm.

bool	type_is_int () const noexcept
	Dynamic check whether the term is an aterm_int.

bool	type_is_list () const noexcept
	Dynamic check whether the term is an aterm_list.

bool	operator== (const unprotected_aterm_core &t) const
	Comparison operator.

bool	operator!= (const unprotected_aterm_core &t) const
	Inequality operator on two unprotected aterms.

bool	operator< (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	operator> (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	operator<= (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	operator>= (const unprotected_aterm_core &t) const
	Comparison operator for two unprotected aterms.

bool	defined () const
	Returns true if this term is not equal to the term assigned by the default constructor of aterms, aterm_appls and aterm_int.

void	swap (unprotected_aterm_core &t) noexcept
	Swaps this term with its argument.

const function_symbol &	function () const
	Yields the function symbol in an aterm.

Protected Attributes
const propositional_variable	m_source
	The propositional variable at the source of the edge.

const qvar_list	m_qvars
	The quantifiers in whose direct context the target PVI occurs.

const propositional_variable_instantiation	m_target
	The propositional variable instantiation that determines the target of the edge.

const std::set< data::variable >	m_conj_context

const std::set< data::variable >	m_disj_context

Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_aterm *	m_term

Additional Inherited Members
Public Types inherited from atermpp::aterm
typedef std::size_t	size_type
	An unsigned integral type.

typedef ptrdiff_t	difference_type
	A signed integral type.

typedef term_appl_iterator< aterm >	iterator
	Iterator used to iterate through an term_appl.

typedef term_appl_iterator< aterm >	const_iterator
	Const iterator used to iterate through an term_appl.

Protected Member Functions inherited from atermpp::aterm
	aterm (detail::_term_appl *t)
	Constructor.

Detailed Description

template<typename DataRewriter, typename PresRewriter>
class mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge

Represents an edge of the dependency graph. The assignments are stored implicitly using the 'right' parameter. The condition determines under what circumstances the influence of the edge is propagated to its target vertex.

Definition at line 428 of file constelm.h.

Constructor & Destructor Documentation

◆ edge() [1/2]

template<typename DataRewriter , typename PresRewriter >

mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::edge ( )

default

Constructor.

◆ edge() [2/2]

template<typename DataRewriter , typename PresRewriter >

mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::edge	(	const propositional_variable &	src,
		const qvar_list &	qvars,
		const propositional_variable_instantiation &	tgt,
		const std::set< data::variable > &	conj_context,
		const std::set< data::variable > &	disj_context,
		data::data_expression	c = `data::sort_bool::true_()`
	)

inline

Constructor.

Parameters

src	A propositional variable declaration
tgt	A propositional variable
c	A term

Definition at line 451 of file constelm.h.

Member Function Documentation

◆ condition()

template<typename DataRewriter , typename PresRewriter >

const data::data_expression & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::condition ( ) const

inline

The condition of the edge.

Definition at line 499 of file constelm.h.

◆ quantified_variables()

template<typename DataRewriter , typename PresRewriter >

const qvar_list & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::quantified_variables ( ) const

inline

Definition at line 487 of file constelm.h.

◆ quantifier_inside_approximation()

template<typename DataRewriter , typename PresRewriter >

qvar_list mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::quantifier_inside_approximation ( const qvar_list & Q ) const

inline

Try to guess which quantifiers of Q can end up directly before target, when the quantifier inside rewriter is applied.

Definition at line 506 of file constelm.h.

◆ source()

template<typename DataRewriter , typename PresRewriter >

const propositional_variable & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::source ( ) const

inline

The propositional variable at the source of the edge.

Definition at line 482 of file constelm.h.

◆ target()

template<typename DataRewriter , typename PresRewriter >

const propositional_variable_instantiation & mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::target ( ) const

inline

The propositional variable instantiation that determines the target of the edge.

Definition at line 493 of file constelm.h.

◆ to_string()

template<typename DataRewriter , typename PresRewriter >

std::string mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::to_string ( ) const

inline

Returns a string representation of the edge.

Returns: A string representation of the edge.

Definition at line 469 of file constelm.h.

Member Data Documentation

◆ m_conj_context

template<typename DataRewriter , typename PresRewriter >

const std::set<data::variable> mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::m_conj_context

protected

Definition at line 440 of file constelm.h.

◆ m_disj_context

template<typename DataRewriter , typename PresRewriter >

const std::set<data::variable> mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::m_disj_context

protected

Definition at line 441 of file constelm.h.

◆ m_qvars

template<typename DataRewriter , typename PresRewriter >

const qvar_list mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::m_qvars

protected

The quantifiers in whose direct context the target PVI occurs.

Definition at line 435 of file constelm.h.

◆ m_source

template<typename DataRewriter , typename PresRewriter >

const propositional_variable mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::m_source

protected

The propositional variable at the source of the edge.

Definition at line 432 of file constelm.h.

◆ m_target

template<typename DataRewriter , typename PresRewriter >

const propositional_variable_instantiation mcrl2::pres_system::pres_constelm_algorithm< DataRewriter, PresRewriter >::edge::m_target

protected

The propositional variable instantiation that determines the target of the edge.

Definition at line 438 of file constelm.h.

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

pres/include/mcrl2/pres/constelm.h

Public Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ edge() [1/2]

◆ edge() [2/2]

Member Function Documentation

◆ condition()

◆ quantified_variables()

◆ quantifier_inside_approximation()

◆ source()

◆ target()

◆ to_string()

Member Data Documentation

◆ m_conj_context

◆ m_disj_context

◆ m_qvars

◆ m_source

◆ m_target