mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge Class Reference

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::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge:
mcrl2::data::data_expression atermpp::aterm atermpp::aterm_core atermpp::unprotected_aterm_core

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_variablesource () const
 The propositional variable at the source of the edge.
 
const qvar_listquantified_variables () const
 
const propositional_variable_instantiationtarget () const
 The propositional variable instantiation that determines the target of the edge.
 
const data::data_expressioncondition () 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_expressionoperator= (const data_expression &) noexcept=default
 
data_expressionoperator= (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.
 
atermoperator= (const aterm &other) noexcept=default
 
 aterm (aterm &&other) noexcept=default
 
atermoperator= (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_symbolfunction () 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 atermoperator[] (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_coreoperator= (const aterm_core &other) noexcept
 Assignment operator.
 
aterm_coreassign (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_coreunprotected_assign (const aterm_core &other) noexcept
 Assignment operator, to be used when the busy flags do not need to be set.
 
aterm_coreoperator= (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_symbolfunction () 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::variablem_conj_context
 
const std::set< data::variablem_disj_context
 
- Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_atermm_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< atermiterator
 Iterator used to iterate through an term_appl.
 
typedef term_appl_iterator< atermconst_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 PbesRewriter>
class mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::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 416 of file constelm.h.

Constructor & Destructor Documentation

◆ edge() [1/2]

template<typename DataRewriter , typename PbesRewriter >
mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::edge ( )
default

Constructor.

◆ edge() [2/2]

template<typename DataRewriter , typename PbesRewriter >
mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::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
srcA propositional variable declaration
tgtA propositional variable
cA term

Definition at line 439 of file constelm.h.

Member Function Documentation

◆ condition()

template<typename DataRewriter , typename PbesRewriter >
const data::data_expression & mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::condition ( ) const
inline

The condition of the edge.

Definition at line 487 of file constelm.h.

◆ quantified_variables()

template<typename DataRewriter , typename PbesRewriter >
const qvar_list & mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::quantified_variables ( ) const
inline

Definition at line 475 of file constelm.h.

◆ quantifier_inside_approximation()

template<typename DataRewriter , typename PbesRewriter >
qvar_list mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::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 494 of file constelm.h.

◆ source()

template<typename DataRewriter , typename PbesRewriter >
const propositional_variable & mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::source ( ) const
inline

The propositional variable at the source of the edge.

Definition at line 470 of file constelm.h.

◆ target()

template<typename DataRewriter , typename PbesRewriter >
const propositional_variable_instantiation & mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::target ( ) const
inline

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

Definition at line 481 of file constelm.h.

◆ to_string()

template<typename DataRewriter , typename PbesRewriter >
std::string mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::to_string ( ) const
inline

Returns a string representation of the edge.

Returns
A string representation of the edge.

Definition at line 457 of file constelm.h.

Member Data Documentation

◆ m_conj_context

template<typename DataRewriter , typename PbesRewriter >
const std::set<data::variable> mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::m_conj_context
protected

Definition at line 428 of file constelm.h.

◆ m_disj_context

template<typename DataRewriter , typename PbesRewriter >
const std::set<data::variable> mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::m_disj_context
protected

Definition at line 429 of file constelm.h.

◆ m_qvars

template<typename DataRewriter , typename PbesRewriter >
const qvar_list mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::m_qvars
protected

The quantifiers in whose direct context the target PVI occurs.

Definition at line 423 of file constelm.h.

◆ m_source

template<typename DataRewriter , typename PbesRewriter >
const propositional_variable mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::m_source
protected

The propositional variable at the source of the edge.

Definition at line 420 of file constelm.h.

◆ m_target

template<typename DataRewriter , typename PbesRewriter >
const propositional_variable_instantiation mcrl2::pbes_system::pbes_constelm_algorithm< DataRewriter, PbesRewriter >::edge::m_target
protected

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

Definition at line 426 of file constelm.h.


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