|
| | linear_inequality () |
| | Constructor yielding an inconsistent inequality.
|
| |
| | linear_inequality (const detail::lhs_t &lhs, const data_expression &r, detail::comparison_t t) |
| | Basic constructor.
|
| |
| | linear_inequality (const detail::lhs_t &lhs, const data_expression &rhs, detail::comparison_t comparison, const rewriter &r) |
| | constructor.
|
| |
| | linear_inequality (const data_expression &lhs, const data_expression &rhs, const detail::comparison_t comparison, const rewriter &r, const bool negate=false) |
| | constructor.
|
| |
| | linear_inequality (const data_expression &e, const rewriter &r) |
| | Constructor that constructs a linear inequality out of a data expression.
|
| |
| detail::lhs_t::const_iterator | lhs_begin () const |
| |
| detail::lhs_t::const_iterator | lhs_end () const |
| |
| const detail::lhs_t & | lhs () const |
| |
| const data_expression & | rhs () const |
| |
| data_expression | get_factor_for_a_variable (const variable &x) |
| |
| detail::comparison_t | comparison () const |
| |
| data_expression | transform_to_data_expression () const |
| |
| bool | is_false (const rewriter &r) const |
| |
| bool | is_true (const rewriter &r) const |
| |
| bool | typical_pair (data_expression &lhs_expression, data_expression &rhs_expression, detail::comparison_t &comparison_operator, const rewriter &r) const |
| | Return this inequality as a typical pair of terms of the form <x1+c2 x2+...+cn xn, d> where c2,...,cn, d are real constants.
|
| |
| linear_inequality | invert (const rewriter &r) |
| |
| void | add_variables (std::set< variable > &variable_set) const |
| |
| | 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 >
requires (mcrl2::utilities::is_iterator<ForwardIterator>::value && !std::is_same_v<typename ForwardIterator::iterator_category, std::input_iterator_tag> && !std::is_same_v<typename ForwardIterator::iterator_category, std::output_iterator_tag>) |
| | 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 >
requires mcrl2::utilities::is_iterator<InputIterator> |
| | 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 >
requires mcrl2::utilities::is_iterator<InputIterator> |
| | aterm (const function_symbol &sym, InputIterator begin, InputIterator end, TermConverter converter) |
| | 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.
|
| |
| | 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.
|
| |
| | 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.
|
| |
| std::weak_ordering | 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.
|
| |
Definition at line 558 of file linear_inequalities.h.
Public Member Functions inherited from atermpp::aterm