|
| | structured_sort () |
| | \brief Default constructor X3.
|
| |
| | structured_sort (const atermpp::aterm &term) |
| |
| | structured_sort (const structured_sort_constructor_list &constructors) |
| | \brief Constructor Z14.
|
| |
| template<typename Container > |
| | structured_sort (const Container &constructors, typename atermpp::enable_if_container< Container, structured_sort_constructor >::type *=nullptr) |
| | \brief Constructor Z2.
|
| |
| | structured_sort (const structured_sort &) noexcept=default |
| | Move semantics.
|
| |
| | structured_sort (structured_sort &&) noexcept=default |
| |
| structured_sort & | operator= (const structured_sort &) noexcept=default |
| |
| structured_sort & | operator= (structured_sort &&) noexcept=default |
| |
| const structured_sort_constructor_list & | constructors () const |
| |
| function_symbol_vector | constructor_functions () const |
| | Returns the constructor functions of this sort, such that the result can be used by the rewriter.
|
| |
| function_symbol_vector | comparison_functions () const |
| | Returns the additional functions of this sort, used to implement its comparison operators.
|
| |
| function_symbol_vector | projection_functions () const |
| | Returns the projection functions of this sort, such that the result can be used by the rewriter.
|
| |
| function_symbol_vector | recogniser_functions () const |
| | Returns the recogniser functions of this sort, such that the result can be used by the rewriter.
|
| |
| data_equation_vector | constructor_equations () const |
| | Returns the equations for ==, < and <= for this sort, such that the result can be used by the rewriter internally.
|
| |
| data_equation_vector | comparison_equations () const |
| | Returns the equations for the functions used to implement comparison operators on this sort. Needed to do proper rewriting.
|
| |
| data_equation_vector | projection_equations () const |
| | Generate equations for the projection functions of this sort.
|
| |
| data_equation_vector | recogniser_equations () const |
| | Generate equations for the recognisers of this sort, assuming that this sort is referred to with s.
|
| |
| | sort_expression () |
| | \brief Default constructor X3.
|
| |
| | sort_expression (const atermpp::aterm &term) |
| |
| | sort_expression (const sort_expression &) noexcept=default |
| | Move semantics.
|
| |
| | sort_expression (sort_expression &&) noexcept=default |
| |
| sort_expression & | operator= (const sort_expression &) noexcept=default |
| |
| sort_expression & | operator= (sort_expression &&) noexcept=default |
| |
| const sort_expression & | target_sort () const |
| | Returns the target sort of this expression.
|
| |
| | 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.
|
| |
| | 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.
|
| |
| 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.
|
| |
structured sort.
A structured sort is a sort with the following structure: struct c1(pr1,1:S1,1, ..., pr1,k1:S1,k1)?is_c1 | ... | cn(prn,1:Sn,1, ..., prn,kn:Sn,kn)?is_cn in this:
- c1, ..., cn are called constructors.
- pri,j are the projection functions (or constructor arguments).
- is_ci are the recognisers. \brief A structured sort
Definition at line 55 of file structured_sort.h.
Public Member Functions inherited from mcrl2::data::sort_expression