mCRL2
Searching...
No Matches
cardinality.h
Go to the documentation of this file.
1// Author: Jan Friso Groote
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
6// (See accompanying file LICENSE_1_0.txt or copy at
8//
11
12#ifndef MCRL2_DATA_CARDINALIY_H
13#define MCRL2_DATA_CARDINALIY_H
14
16
17namespace mcrl2
18{
19namespace data
20{
21
23{
24 protected:
25
28
29 // Determine whether f is a new unique element of sort s. If this cannot be determined,
30 // the boolean determined is set to false, and the function yields false.
33 bool& determined) const
34 {
35 data_expression result;
37 {
38 result=m_rewriter(equal_to(t,u));
39 if (result==sort_bool::true_())
40 {
41 determined=true;
42 return false;
43 }
44 else if (result!=sort_bool::false_())
45 {
46 determined=false;
47 return false;
48 }
49 // else result==false and the element can still be unique.
50 }
51 determined=true;
52 return true;
53 }
54
55 public:
56
57 cardinality_calculator(const data_specification& specification, const rewriter& r)
58 : m_specification(specification),
59 m_rewriter(r)
60 {}
61
66 std::size_t operator()(const sort_expression& s) const
67 {
68 if (s==sort_bool::bool_()) // Special case that occurs often.
69 {
70 return 2;
71 }
72 /* if (!m_specification.is_certainly_finite(s))
73 {
74 return 0;
75 } */
76 std::vector<data_expression> found_elements(enumerate_expressions(s, m_specification, m_rewriter));
77 std::vector<data_expression> unique_found_elements;
78
79 for(const data_expression& t: found_elements)
80 {
81 bool determined;
82 if (is_a_new_unique_element(t, unique_found_elements, determined))
83 {
84 unique_found_elements.push_back(t);
85 }
86 else if (!determined)
87 {
88 // It is not possible to determine whether the found element is equal to any earlier element.
89 return 0;
90 }
91 }
92 return unique_found_elements.size();
93 }
94};
95
96} // namespace data
97} // namespace mcrl2
98
99#endif // MCRL2_DATA_CARDINALITY_H
bool is_a_new_unique_element(const data_expression &t, const std::vector< data_expression > already_found_elements, bool &determined) const
Definition cardinality.h:31
std::size_t operator()(const sort_expression &s) const
Counts the number of elements in a sort.
Definition cardinality.h:66
cardinality_calculator(const data_specification &specification, const rewriter &r)
Definition cardinality.h:57
const data_specification & m_specification
Definition cardinality.h:26
Rewriter that operates on data expressions.
Definition rewriter.h:81
\brief A sort expression
The class enumerator.
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
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 ==.
Definition standard.h:126
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72