.. _enumerator.h: mcrl2/data/enumerator.h =============================================================================== Include file: .. code-block:: c++ #include "mcrl2/data/enumerator.h" The class enumerator. Classes ------- * :cpp:class:`mcrl2::data::enumerator_algorithm::always_false` * :cpp:class:`mcrl2::data::enumerator_algorithm` * :cpp:class:`mcrl2::data::enumerator_error` * :cpp:class:`mcrl2::data::enumerator_list_element` * :cpp:class:`mcrl2::data::enumerator_list_element_with_substitution` * :cpp:class:`mcrl2::data::enumerator_queue` Functions ------------------------------------------------------------------------------- .. cpp:function:: data_expression_vector mcrl2::data::enumerate_expressions(const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr) Returns a vector with all expressions of sort s. **Parameters:** * **s** A sort expression. * **dataspec** The data specification defining the terms of sort s. * **rewr** A rewriter to be used to simplify terms and conditions. It is assumed that the sort s has only a finite number of elements. .. cpp:function:: data_expression_vector mcrl2::data::enumerate_expressions(const sort_expression &s, const data_specification &dataspec, const Rewriter &rewr, enumerator_identifier_generator &id_generator) Returns a vector with all expressions of sort s. **Parameters:** * **s** A sort expression. * **dataspec** The data specification defining the terms of sort s. * **rewr** A rewriter to be used to simplify terms and conditions. * **id_generator** An identifier generator used to generate new names for variables. It is assumed that the sort s has only a finite number of elements. .. cpp:function:: static bool mcrl2::data::is_enumerable(const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort) .. cpp:function:: std::ostream& mcrl2::data::operator<<(std::ostream &out, const enumerator_list_element< Expression > &p) .. cpp:function:: std::ostream& mcrl2::data::operator<<(std::ostream &out, const enumerator_list_element_with_substitution< Expression > &p) Functions ------------------------------------------------------------------------------- .. cpp:function:: bool mcrl2::data::detail::compute_finite_function_sorts(const function_sort &sort, enumerator_identifier_generator &id_generator, const data::data_specification &dataspec, Rewriter datar, data_expression_vector &result, variable_list &function_parameter_list) Computes the elements of a finite function sort, and puts them in result. If there are too many elements, false is returned. .. cpp:function:: bool mcrl2::data::detail::compute_finite_set_elements(const container_sort &sort, const data_specification &dataspec, Rewriter datar, MutableSubstitution &sigma, data_expression_vector &result, enumerator_identifier_generator &id_generator) Computes the elements of a finite set sort, and puts them in result. If there are too many elements, false is returned. .. cpp:function:: bool mcrl2::data::detail::is_enumerable(const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort, std::list< sort_expression > &parents) .. cpp:function:: data_expression mcrl2::data::detail::make_if_expression_(std::size_t &function_index, const std::size_t argument_index, const std::vector< data_expression_vector > &data_domain_expressions, const data_expression_vector &codomain_expressions, const variable_vector ¶meters) .. cpp:function:: data_expression mcrl2::data::detail::make_set_(std::size_t function_index, const sort_expression &element_sort, const data_expression_vector &set_elements)