mCRL2
Loading...
Searching...
No Matches
mcrl2::data::enumerator_list_element_with_substitution< Expression > Class Template Reference

An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi. More...

#include <enumerator.h>

Inheritance diagram for mcrl2::data::enumerator_list_element_with_substitution< Expression >:
mcrl2::data::enumerator_list_element< Expression >

Public Types

typedef Expression expression_type
 
- Public Types inherited from mcrl2::data::enumerator_list_element< Expression >
typedef Expression expression_type
 

Public Member Functions

 enumerator_list_element_with_substitution ()=default
 Default constructor.
 
 enumerator_list_element_with_substitution (const data::variable_list &v, const Expression &phi)
 Constructs the element (v, phi, [])
 
 enumerator_list_element_with_substitution (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem)
 Constructs the element (v, phi, e.sigma[v := x])
 
 enumerator_list_element_with_substitution (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem, const data::variable &d, const data::data_expression &e)
 Constructs the element (v, phi, e.sigma[v := x])
 
template<typename VariableList , typename MutableSubstitution , typename Rewriter >
void add_assignments (const VariableList &v, MutableSubstitution &result, const Rewriter &rewriter) const
 Adds the assignments that correspond with this element to the substitution result.
 
template<typename VariableList , typename MutableSubstitution >
void remove_assignments (const VariableList &v, MutableSubstitution &result) const
 Removes the assignments corresponding with this element from the substitution result.
 
template<typename VariableList , typename Rewriter >
data::data_expression_list assign_expressions (const VariableList &v, const Rewriter &rewriter) const
 Returns the right hand sides corresponding to the variables v.
 
data::enumerator_substitution sigma () const
 
void mark (std::stack< std::reference_wrapper< atermpp::detail::_aterm > > &todo) const
 The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.

 
void set (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem, const data::variable &d, const data::data_expression &e)
 Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
 
void set (const data::variable_list &v, const Expression &phi, const enumerator_list_element_with_substitution< Expression > &elem)
 Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
 
- Public Member Functions inherited from mcrl2::data::enumerator_list_element< Expression >
 enumerator_list_element ()=default
 Default constructor.
 
 enumerator_list_element (data::variable_list v_, const Expression &phi_)
 Constructs the element (v, phi)
 
 enumerator_list_element (data::variable_list v_, const Expression &phi_, const enumerator_list_element &)
 Constructs the element (v, phi)
 
 enumerator_list_element (data::variable_list v_, const Expression &phi_, const enumerator_list_element &, const data::variable &, const data::data_expression &)
 Constructs the element (v, phi)
 
const data::variable_listvariables () const
 
const Expression & expression () const
 
Expression & expression ()
 
bool is_solution () const
 
void invalidate ()
 Invalidates the element, by giving phi an undefined value.
 
bool is_valid () const
 Returns true if the element is valid. If it becomes false, this is used to signal that the enumeration has been aborted.
 
void mark (atermpp::term_mark_stack &todo) const
 The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.

 
void set (const data::variable_list &v_, const Expression &phi_)
 Set the variables and the condition explicitly.
 
void set (const data::variable_list &v_, const Expression &phi_, const enumerator_list_element &)
 Set the variables and the condition explicitly.
 
void set (const data::variable_list &v_, const Expression &phi_, const enumerator_list_element &, const data::variable &, const data::data_expression &)
 Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).
 

Protected Attributes

data::variable_list m_variables
 
data::data_expression_list m_expressions
 
- Protected Attributes inherited from mcrl2::data::enumerator_list_element< Expression >
data::variable_list v
 
Expression phi
 

Detailed Description

template<typename Expression = data::data_expression>
class mcrl2::data::enumerator_list_element_with_substitution< Expression >

An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi.

Definition at line 347 of file enumerator.h.

Member Typedef Documentation

◆ expression_type

template<typename Expression = data::data_expression>
typedef Expression mcrl2::data::enumerator_list_element_with_substitution< Expression >::expression_type

Definition at line 354 of file enumerator.h.

Constructor & Destructor Documentation

◆ enumerator_list_element_with_substitution() [1/4]

template<typename Expression = data::data_expression>
mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution ( )
default

Default constructor.

◆ enumerator_list_element_with_substitution() [2/4]

template<typename Expression = data::data_expression>
mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution ( const data::variable_list v,
const Expression &  phi 
)
inline

Constructs the element (v, phi, [])

Definition at line 360 of file enumerator.h.

◆ enumerator_list_element_with_substitution() [3/4]

template<typename Expression = data::data_expression>
mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution ( const data::variable_list v,
const Expression &  phi,
const enumerator_list_element_with_substitution< Expression > &  elem 
)
inline

Constructs the element (v, phi, e.sigma[v := x])

Definition at line 365 of file enumerator.h.

◆ enumerator_list_element_with_substitution() [4/4]

template<typename Expression = data::data_expression>
mcrl2::data::enumerator_list_element_with_substitution< Expression >::enumerator_list_element_with_substitution ( const data::variable_list v,
const Expression &  phi,
const enumerator_list_element_with_substitution< Expression > &  elem,
const data::variable d,
const data::data_expression e 
)
inline

Constructs the element (v, phi, e.sigma[v := x])

Definition at line 376 of file enumerator.h.

Member Function Documentation

◆ add_assignments()

template<typename Expression = data::data_expression>
template<typename VariableList , typename MutableSubstitution , typename Rewriter >
void mcrl2::data::enumerator_list_element_with_substitution< Expression >::add_assignments ( const VariableList &  v,
MutableSubstitution &  result,
const Rewriter &  rewriter 
) const
inline

Adds the assignments that correspond with this element to the substitution result.

Definition at line 393 of file enumerator.h.

◆ assign_expressions()

template<typename Expression = data::data_expression>
template<typename VariableList , typename Rewriter >
data::data_expression_list mcrl2::data::enumerator_list_element_with_substitution< Expression >::assign_expressions ( const VariableList &  v,
const Rewriter &  rewriter 
) const
inline

Returns the right hand sides corresponding to the variables v.

Precondition
variables in v must be contained in variables()

Definition at line 416 of file enumerator.h.

◆ mark()

template<typename Expression = data::data_expression>
void mcrl2::data::enumerator_list_element_with_substitution< Expression >::mark ( std::stack< std::reference_wrapper< atermpp::detail::_aterm > > &  todo) const
inline

The following function is needed to mark the aterms in this class, when elements of this class are used in an atermpp standard container. When garbage collection of aterms is taking place this function is called for all elements of this class in the atermpp container.

Definition at line 432 of file enumerator.h.

◆ remove_assignments()

template<typename Expression = data::data_expression>
template<typename VariableList , typename MutableSubstitution >
void mcrl2::data::enumerator_list_element_with_substitution< Expression >::remove_assignments ( const VariableList &  v,
MutableSubstitution &  result 
) const
inline

Removes the assignments corresponding with this element from the substitution result.

Definition at line 405 of file enumerator.h.

◆ set() [1/2]

template<typename Expression = data::data_expression>
void mcrl2::data::enumerator_list_element_with_substitution< Expression >::set ( const data::variable_list v,
const Expression &  phi,
const enumerator_list_element_with_substitution< Expression > &  elem 
)
inline

Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

Definition at line 456 of file enumerator.h.

◆ set() [2/2]

template<typename Expression = data::data_expression>
void mcrl2::data::enumerator_list_element_with_substitution< Expression >::set ( const data::variable_list v,
const Expression &  phi,
const enumerator_list_element_with_substitution< Expression > &  elem,
const data::variable d,
const data::data_expression e 
)
inline

Set the variable ands and the expression explicitly as the element (v, phi, e.sigma[v := x]).

Definition at line 441 of file enumerator.h.

◆ sigma()

template<typename Expression = data::data_expression>
data::enumerator_substitution mcrl2::data::enumerator_list_element_with_substitution< Expression >::sigma ( ) const
inline

Definition at line 423 of file enumerator.h.

Member Data Documentation

◆ m_expressions

template<typename Expression = data::data_expression>
data::data_expression_list mcrl2::data::enumerator_list_element_with_substitution< Expression >::m_expressions
protected

Definition at line 351 of file enumerator.h.

◆ m_variables

template<typename Expression = data::data_expression>
data::variable_list mcrl2::data::enumerator_list_element_with_substitution< Expression >::m_variables
protected

Definition at line 350 of file enumerator.h.


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