mCRL2
Loading...
Searching...
No Matches
enumerator.h File Reference

The class enumerator. More...

Go to the source code of this file.

Classes

struct  mcrl2::data::enumerator_error
 Enumerator exception. More...
 
class  mcrl2::data::enumerator_list_element< Expression >
 The default element for the todo list of the enumerator. More...
 
class  mcrl2::data::enumerator_list_element_with_substitution< Expression >
 An element for the todo list of the enumerator that collects the substitution corresponding to the expression phi. More...
 
class  mcrl2::data::enumerator_queue< EnumeratorListElement >
 Contains the enumerator queue. More...
 
class  mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >
 An enumerator algorithm that generates solutions of a condition. More...
 
struct  mcrl2::data::enumerator_algorithm< Rewriter, DataRewriter >::always_false< T >
 

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::data
 Namespace for all data library functionality.
 
namespace  mcrl2::data::detail
 

Functions

data_expression mcrl2::data::detail::make_set_ (std::size_t function_index, const sort_expression &element_sort, const data_expression_vector &set_elements)
 
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 &parameters)
 
template<class Rewriter , class MutableSubstitution >
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.
 
template<class Rewriter >
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.
 
template<typename Rewriter >
bool mcrl2::data::detail::is_enumerable (const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort, std::list< sort_expression > &parents)
 
template<typename Rewriter >
static bool mcrl2::data::is_enumerable (const data_specification &dataspec, const Rewriter &rewr, const sort_expression &sort)
 
template<typename Expression >
std::ostream & mcrl2::data::operator<< (std::ostream &out, const enumerator_list_element< Expression > &p)
 
template<typename Expression >
std::ostream & mcrl2::data::operator<< (std::ostream &out, const enumerator_list_element_with_substitution< Expression > &p)
 
template<class Rewriter >
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.
 
template<class Rewriter >
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.
 

Detailed Description

The class enumerator.

Definition in file enumerator.h.