mCRL2
|
#include <linear_inequalities.h>
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_expression & | operator[] (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_list & | operator= (const term_list &other) noexcept=default |
This class has user-declared copy constructor so declare copy and move assignment. | |
term_list & | operator= (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. | |
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. | |
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< 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::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::_aterm * | m_term |
Definition at line 174 of file linear_inequalities.h.
|
inline |
Constructor.
Definition at line 178 of file linear_inequalities.h.
|
inlineexplicit |
Constructor from an aterm.
Definition at line 183 of file linear_inequalities.h.
|
inline |
Constructor.
Definition at line 189 of file linear_inequalities.h.
|
inline |
Constructor.
Definition at line 195 of file linear_inequalities.h.
|
inline |
Give the factor of variable v.
Definition at line 234 of file linear_inequalities.h.
Erase a variable and its factor.
Definition at line 209 of file linear_inequalities.h.
|
inline |
Evaluate the variables in this lhs_t according to the subsitution function.
Definition at line 246 of file linear_inequalities.h.
|
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.
|
inline |
Give the factor of variable v.
Definition at line 223 of file linear_inequalities.h.
|
inline |
Definition at line 267 of file linear_inequalities.h.