mCRL2
Loading...
Searching...
No Matches
mcrl2::data::detail::lhs_t Class Reference

#include <linear_inequalities.h>

Inheritance diagram for mcrl2::data::detail::lhs_t:
atermpp::term_list< variable_with_a_rational_factor > atermpp::aterm atermpp::aterm_core atermpp::unprotected_aterm_core

Public Member Functions

 lhs_t ()
 Constructor.
 
 lhs_t (const aterm &t)
 Constructor from an aterm.
 
template<class ITERATOR >
 lhs_t (const ITERATOR begin, const ITERATOR end)
 Constructor.
 
template<class ITERATOR , class TRANSFORMER >
 lhs_t (const ITERATOR begin, const ITERATOR end, TRANSFORMER f)
 Constructor.
 
lhs_t::const_iterator find (const variable &v) const
 Give an iterator of the factor/variable pair for v, or end() if v does not occur.
 
lhs_t erase (const variable &v) const
 Erase a variable and its factor.
 
const data_expressionoperator[] (const variable &v) const
 Give the factor of variable v.
 
std::size_t count (const variable &v) const
 Give the factor of variable v.
 
template<typename SubstitutionFunction >
data_expression evaluate (const SubstitutionFunction &beta, const rewriter &r) const
 Evaluate the variables in this lhs_t according to the subsitution function.
 
data_expression transform_to_data_expression () const
 
- Public Member Functions inherited from atermpp::term_list< variable_with_a_rational_factor >
 term_list () noexcept
 Default constructor. Creates an empty list.
 
 term_list (const aterm &t) noexcept
 Constructor from an aterm.
 
 term_list (const term_list< variable_with_a_rational_factor > &t) noexcept
 Copy constructor.
 
 term_list (term_list< variable_with_a_rational_factor > &&t) noexcept
 Move constructor.
 
 term_list (Iter first, Iter last, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
 Creates a term_list with the elements from first to last.
 
 term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=0)
 Creates a term_list with the elements from first to last converting the elements before inserting.
 
 term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter, typename std::enable_if< std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=0)
 Creates a term_list with the elements from first to last, converting and filtering the list.
 
 term_list (Iter first, Iter last, typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
 Creates a term_list from the elements from first to last.
 
 term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, typename std::enable_if< !std::is_base_of< std::bidirectional_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
 Creates a term_list from the elements from first to last converting the elements before inserting.
 
 term_list (Iter first, Iter last, const ATermConverter &convert_to_aterm, const ATermFilter &aterm_filter, typename std::enable_if< !std::is_base_of< std::random_access_iterator_tag, typename std::iterator_traits< Iter >::iterator_category >::value >::type *=nullptr)
 Creates a term_list from the elements from first to last converting and filtering the elements before inserting.
 
 term_list (std::initializer_list< variable_with_a_rational_factor > init)
 A constructor based on an initializer list.
 
term_listoperator= (const term_list &other) noexcept=default
 This class has user-declared copy constructor so declare copy and move assignment.
 
term_listoperator= (term_list &&other) noexcept=default
 
const term_list< variable_with_a_rational_factor > & tail () const
 Returns the tail of the list.
 
void pop_front ()
 Removes the first element of the list.
 
const variable_with_a_rational_factor & front () const
 Returns the first element of the list.
 
void push_front (const variable_with_a_rational_factor &el)
 Inserts a new element at the beginning of the current list.
 
void emplace_front (Args &&... arguments)
 Construct and insert a new element at the beginning of the current list.
 
size_type size () const
 Returns the size of the term_list.
 
bool empty () const
 Returns true if the list's size is 0.
 
const_iterator begin () const
 Returns a const_iterator pointing to the beginning of the term_list.
 
const_iterator end () const
 Returns a const_iterator pointing to the end of the term_list.
 
const_reverse_iterator rbegin () const
 Returns a const_reverse_iterator pointing to the end of the term_list.
 
const_reverse_iterator rend () const
 Returns a const_iterator pointing to the end of the term_list.
 
size_type max_size () const
 Returns the largest possible size of the term_list.
 
- 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.
 

Additional Inherited Members

- Public Types inherited from atermpp::term_list< variable_with_a_rational_factor >
typedef variable_with_a_rational_factor value_type
 The type of object, T stored in the term_list.
 
typedef variable_with_a_rational_factor * pointer
 Pointer to T.
 
typedef variable_with_a_rational_factor & reference
 Reference to T.
 
typedef const variable_with_a_rational_factor & const_reference
 Const reference to T.
 
typedef std::size_t size_type
 An unsigned integral type.
 
typedef ptrdiff_t difference_type
 A signed integral type.
 
typedef term_list_iterator< variable_with_a_rational_factor > iterator
 Iterator used to iterate through an term_list.
 
typedef term_list_iterator< variable_with_a_rational_factor > const_iterator
 Const iterator used to iterate through an term_list.
 
typedef reverse_term_list_iterator< variable_with_a_rational_factor > const_reverse_iterator
 Const iterator used to iterate through an term_list.
 
- 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::term_list< variable_with_a_rational_factor >
 term_list (detail::_aterm_appl<> *t) noexcept
 Constructor for term lists from internally constructed terms delivered as reference.
 
- Protected Member Functions inherited from atermpp::aterm
 aterm (detail::_term_appl *t)
 Constructor.
 
- Protected Attributes inherited from atermpp::unprotected_aterm_core
const detail::_atermm_term
 

Detailed Description

Definition at line 174 of file linear_inequalities.h.

Constructor & Destructor Documentation

◆ lhs_t() [1/4]

mcrl2::data::detail::lhs_t::lhs_t ( )
inline

Constructor.

Definition at line 178 of file linear_inequalities.h.

◆ lhs_t() [2/4]

mcrl2::data::detail::lhs_t::lhs_t ( const aterm t)
inlineexplicit

Constructor from an aterm.

Definition at line 183 of file linear_inequalities.h.

◆ lhs_t() [3/4]

template<class ITERATOR >
mcrl2::data::detail::lhs_t::lhs_t ( const ITERATOR  begin,
const ITERATOR  end 
)
inline

Constructor.

Definition at line 189 of file linear_inequalities.h.

◆ lhs_t() [4/4]

template<class ITERATOR , class TRANSFORMER >
mcrl2::data::detail::lhs_t::lhs_t ( const ITERATOR  begin,
const ITERATOR  end,
TRANSFORMER  f 
)
inline

Constructor.

Definition at line 195 of file linear_inequalities.h.

Member Function Documentation

◆ count()

std::size_t mcrl2::data::detail::lhs_t::count ( const variable v) const
inline

Give the factor of variable v.

Definition at line 234 of file linear_inequalities.h.

◆ erase()

lhs_t mcrl2::data::detail::lhs_t::erase ( const variable v) const
inline

Erase a variable and its factor.

Definition at line 209 of file linear_inequalities.h.

◆ evaluate()

template<typename SubstitutionFunction >
data_expression mcrl2::data::detail::lhs_t::evaluate ( const SubstitutionFunction &  beta,
const rewriter r 
) const
inline

Evaluate the variables in this lhs_t according to the subsitution function.

Definition at line 246 of file linear_inequalities.h.

◆ find()

lhs_t::const_iterator mcrl2::data::detail::lhs_t::find ( const variable v) const
inline

Give an iterator of the factor/variable pair for v, or end() if v does not occur.

Definition at line 200 of file linear_inequalities.h.

◆ operator[]()

const data_expression & mcrl2::data::detail::lhs_t::operator[] ( const variable v) const
inline

Give the factor of variable v.

Definition at line 223 of file linear_inequalities.h.

◆ transform_to_data_expression()

data_expression mcrl2::data::detail::lhs_t::transform_to_data_expression ( ) const
inline

Definition at line 267 of file linear_inequalities.h.


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