GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/cardinality.h Lines: 25 25 100.0 %
Date: 2021-03-23 Branches: 12 22 54.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cardinality.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief Representation of cardinality
13
 **
14
 ** Simple class to represent a cardinality; used by the CVC4 type system
15
 ** give the cardinality of sorts.
16
 **/
17
18
#include "cvc4_public.h"
19
20
#ifndef CVC4__CARDINALITY_H
21
#define CVC4__CARDINALITY_H
22
23
#include <iosfwd>
24
25
#include "util/integer.h"
26
27
namespace CVC4 {
28
29
/**
30
 * Representation for a Beth number, used only to construct
31
 * Cardinality objects.
32
 */
33
17791
class CardinalityBeth
34
{
35
  Integer d_index;
36
37
 public:
38
  CardinalityBeth(const Integer& beth);
39
40
17791
  const Integer& getNumber() const { return d_index; }
41
42
}; /* class CardinalityBeth */
43
44
/**
45
 * Representation for an unknown cardinality.
46
 */
47
class CardinalityUnknown
48
{
49
 public:
50
14701
  CardinalityUnknown() {}
51
14701
  ~CardinalityUnknown() {}
52
}; /* class CardinalityUnknown */
53
54
/**
55
 * A simple representation of a cardinality.  We store an
56
 * arbitrary-precision integer for finite cardinalities, and we
57
 * distinguish infinite cardinalities represented as Beth numbers.
58
 */
59
168188
class Cardinality
60
{
61
  /** Cardinality of the integers */
62
  static const Integer s_intCard;
63
64
  /** Cardinality of the reals */
65
  static const Integer s_realCard;
66
67
  /** A representation for unknown cardinality */
68
  static const Integer s_unknownCard;
69
70
  /** A representation for large, finite cardinality */
71
  static const Integer s_largeFiniteCard;
72
73
  /**
74
   * In the case of finite cardinality, this is > 0, and is equal to
75
   * the cardinality+1.  If infinite, it is < 0, and is Beth[|card|-1].
76
   * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
77
   * If this field is 0, the cardinality is unknown.
78
   *
79
   * We impose a ceiling on finite cardinalities of 2^64.  If this field
80
   * is >= 2^64 + 1, we consider it at "ceiling" cardinality, and
81
   * comparisons between all such cardinalities result in "unknown."
82
   */
83
  Integer d_card;
84
85
 public:
86
  /** The cardinality of the set of integers. */
87
  static const Cardinality INTEGERS;
88
89
  /** The cardinality of the set of real numbers. */
90
  static const Cardinality REALS;
91
92
  /** The unknown cardinality */
93
  static const Cardinality UNKNOWN_CARD;
94
95
  /** Used as a result code for Cardinality::compare(). */
96
  enum CardinalityComparison
97
  {
98
    LESS,
99
    EQUAL,
100
    GREATER,
101
    UNKNOWN
102
  }; /* enum CardinalityComparison */
103
104
  /**
105
   * Construct a finite cardinality equal to the integer argument.
106
   * The argument must be nonnegative.  If we change this to an
107
   * "unsigned" argument to enforce the restriction, we mask some
108
   * errors that automatically convert, like "Cardinality(-1)".
109
   */
110
  Cardinality(long card);
111
112
  /**
113
   * Construct a finite cardinality equal to the integer argument.
114
   * The argument must be nonnegative.
115
   */
116
  Cardinality(const Integer& card);
117
118
  /**
119
   * Construct an infinite cardinality equal to the given Beth number.
120
   */
121
17790
  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {}
122
123
  /**
124
   * Construct an unknown cardinality.
125
   */
126
14701
  Cardinality(CardinalityUnknown) : d_card(0) {}
127
128
  /**
129
   * Returns true iff this cardinality is unknown.  "Unknown" in this
130
   * sense means that the cardinality is completely unknown; it might
131
   * be finite, or infinite---anything.  Large, finite cardinalities
132
   * at the "ceiling" return "false" for isUnknown() and true for
133
   * isFinite() and isLargeFinite().
134
   */
135
76810
  bool isUnknown() const { return d_card == 0; }
136
137
  /** Returns true iff this cardinality is finite. */
138
114113
  bool isFinite() const { return d_card > 0; }
139
  /** Returns true iff this cardinality is one */
140
178
  bool isOne() const { return d_card == 2; }
141
  /**
142
   * Returns true iff this cardinality is finite and large (i.e.,
143
   * at the ceiling of representable finite cardinalities).
144
   */
145
104088
  bool isLargeFinite() const { return d_card >= s_largeFiniteCard; }
146
147
  /** Returns true iff this cardinality is infinite. */
148
45120
  bool isInfinite() const { return d_card < 0; }
149
150
  /**
151
   * Returns true iff this cardinality is finite or countably
152
   * infinite.
153
   */
154
6
  bool isCountable() const { return isFinite() || d_card == s_intCard; }
155
156
  /**
157
   * In the case that this cardinality is finite, return its
158
   * cardinality.  (If this cardinality is infinite, this function
159
   * throws an IllegalArgumentException.)
160
   */
161
  Integer getFiniteCardinality() const;
162
163
  /**
164
   * In the case that this cardinality is infinite, return its Beth
165
   * number.  (If this cardinality is finite, this function throws an
166
   * IllegalArgumentException.)
167
   */
168
  Integer getBethNumber() const;
169
170
  /** Assigning addition of this cardinality with another. */
171
  Cardinality& operator+=(const Cardinality& c);
172
173
  /** Assigning multiplication of this cardinality with another. */
174
  Cardinality& operator*=(const Cardinality& c);
175
176
  /** Assigning exponentiation of this cardinality with another. */
177
  Cardinality& operator^=(const Cardinality& c);
178
179
  /** Add two cardinalities. */
180
8
  Cardinality operator+(const Cardinality& c) const {
181
8
    Cardinality card(*this);
182
8
    card += c;
183
8
    return card;
184
  }
185
186
  /** Multiply two cardinalities. */
187
8
  Cardinality operator*(const Cardinality& c) const {
188
8
    Cardinality card(*this);
189
8
    card *= c;
190
8
    return card;
191
  }
192
193
  /**
194
   * Exponentiation of two cardinalities.
195
   */
196
683
  Cardinality operator^(const Cardinality& c) const {
197
683
    Cardinality card(*this);
198
683
    card ^= c;
199
683
    return card;
200
  }
201
202
  /**
203
   * Compare two cardinalities.  This can return UNKNOWN if two
204
   * finite cardinalities are at the ceiling (and thus not precisely
205
   * represented), or if one or the other is the special "unknown"
206
   * cardinality.
207
   */
208
  Cardinality::CardinalityComparison compare(const Cardinality& c) const;
209
210
  /**
211
   * Return a string representation of this cardinality.
212
   */
213
  std::string toString() const;
214
215
  /**
216
   * Compare two cardinalities and if it is known that the current
217
   * cardinality is smaller or equal to c, it returns true.
218
   */
219
  bool knownLessThanOrEqual(const Cardinality& c) const;
220
}; /* class Cardinality */
221
222
/** Print an element of the InfiniteCardinality enumeration. */
223
std::ostream& operator<<(std::ostream& out, CardinalityBeth b);
224
225
/** Print a cardinality in a human-readable fashion. */
226
std::ostream& operator<<(std::ostream& out, const Cardinality& c);
227
228
} /* CVC4 namespace */
229
230
#endif /* CVC4__CARDINALITY_H */