12#ifndef MCRL2_DATA_CARDINALIY_H
13#define MCRL2_DATA_CARDINALIY_H
32 const std::vector<data_expression> already_found_elements,
33 bool& determined)
const
77 std::vector<data_expression> unique_found_elements;
84 unique_found_elements.push_back(t);
92 return unique_found_elements.size();
bool is_a_new_unique_element(const data_expression &t, const std::vector< data_expression > already_found_elements, bool &determined) const
std::size_t operator()(const sort_expression &s) const
Counts the number of elements in a sort.
const rewriter & m_rewriter
cardinality_calculator(const data_specification &specification, const rewriter &r)
const data_specification & m_specification
Rewriter that operates on data expressions.
const basic_sort & bool_()
Constructor for sort expression Bool.
const function_symbol & false_()
Constructor for function symbol false.
const function_symbol & true_()
Constructor for function symbol true.
data_expression_vector 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.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...