cvc4-1.4
cardinality.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__CARDINALITY_H
21 #define __CVC4__CARDINALITY_H
22 
23 #include <iostream>
24 #include <utility>
25 
26 #include "util/integer.h"
27 #include "util/exception.h"
28 
29 namespace CVC4 {
30 
36  Integer d_index;
37 
38 public:
39  CardinalityBeth(const Integer& beth) : d_index(beth) {
40  CheckArgument(beth >= 0, beth,
41  "Beth index must be a nonnegative integer, not %s.",
42  beth.toString().c_str());
43  }
44 
45  const Integer& getNumber() const throw() {
46  return d_index;
47  }
48 
49 };/* class CardinalityBeth */
50 
55 public:
56  CardinalityUnknown() throw() {}
57  ~CardinalityUnknown() throw() {}
58 };/* class CardinalityUnknown */
59 
67  static const Integer s_intCard;
68 
70  static const Integer s_realCard;
71 
73  static const Integer s_unknownCard;
74 
76  static const Integer s_largeFiniteCard;
77 
88  Integer d_card;
89 
90 public:
91 
93  static const Cardinality INTEGERS;
94 
96  static const Cardinality REALS;
97 
99  static const Cardinality UNKNOWN_CARD;
100 
107  };/* enum CardinalityComparison */
108 
115  Cardinality(long card) : d_card(card) {
116  CheckArgument(card >= 0, card,
117  "Cardinality must be a nonnegative integer, not %ld.", card);
118  d_card += 1;
119  }
120 
125  Cardinality(const Integer& card) : d_card(card) {
126  CheckArgument(card >= 0, card,
127  "Cardinality must be a nonnegative integer, not %s.",
128  card.toString().c_str());
129  d_card += 1;
130  }
131 
135  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
136  }
137 
142  }
143 
151  bool isUnknown() const throw() {
152  return d_card == 0;
153  }
154 
156  bool isFinite() const throw() {
157  return d_card > 0;
158  }
159 
164  bool isLargeFinite() const throw() {
165  return d_card >= s_largeFiniteCard;
166  }
167 
169  bool isInfinite() const throw() {
170  return d_card < 0;
171  }
172 
177  bool isCountable() const throw() {
178  return isFinite() || d_card == s_intCard;
179  }
180 
187  CheckArgument(isFinite(), *this, "This cardinality is not finite.");
188  CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
189  return d_card - 1;
190  }
191 
198  CheckArgument(!isFinite() && !isUnknown(), *this,
199  "This cardinality is not infinite (or is unknown).");
200  return -d_card - 1;
201  }
202 
204  Cardinality& operator+=(const Cardinality& c) throw();
205 
207  Cardinality& operator*=(const Cardinality& c) throw();
208 
210  Cardinality& operator^=(const Cardinality& c) throw();
211 
213  Cardinality operator+(const Cardinality& c) const throw() {
214  Cardinality card(*this);
215  card += c;
216  return card;
217  }
218 
220  Cardinality operator*(const Cardinality& c) const throw() {
221  Cardinality card(*this);
222  card *= c;
223  return card;
224  }
225 
229  Cardinality operator^(const Cardinality& c) const throw() {
230  Cardinality card(*this);
231  card ^= c;
232  return card;
233  }
234 
242 
246  std::string toString() const throw();
247 
252  bool knownLessThanOrEqual(const Cardinality& c) const throw();
253 };/* class Cardinality */
254 
255 
257 std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
258  throw() CVC4_PUBLIC;
259 
260 
262 std::ostream& operator<<(std::ostream& out, const Cardinality& c)
263  throw() CVC4_PUBLIC;
264 
265 }/* CVC4 namespace */
266 
267 #endif /* __CVC4__CARDINALITY_H */
static const Cardinality INTEGERS
The cardinality of the set of integers.
Definition: cardinality.h:93
std::string toString(int base=10) const
bool isCountable() const
Returns true iff this cardinality is finite or countably infinite.
Definition: cardinality.h:177
Integer getFiniteCardinality() const
In the case that this cardinality is finite, return its cardinality.
Definition: cardinality.h:186
Cardinality operator^(const Cardinality &c) const
Exponentiation of two cardinalities.
Definition: cardinality.h:229
CardinalityBeth(const Integer &beth)
Definition: cardinality.h:39
int compare(const Expr &e1, const Expr &e2)
Cardinality(const Integer &card)
Construct a finite cardinality equal to the integer argument.
Definition: cardinality.h:125
static const Cardinality UNKNOWN_CARD
The unknown cardinality.
Definition: cardinality.h:99
A simple representation of a cardinality.
Definition: cardinality.h:65
bool isLargeFinite() const
Returns true iff this cardinality is finite and large (i.e., at the ceiling of representable finite c...
Definition: cardinality.h:164
std::ostream & operator<<(std::ostream &out, const Predicate &p)
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
CVC4&#39;s exception base class and some associated utilities.
Cardinality(long card)
Construct a finite cardinality equal to the integer argument.
Definition: cardinality.h:115
bool isInfinite() const
Returns true iff this cardinality is infinite.
Definition: cardinality.h:169
Representation for a Beth number, used only to construct Cardinality objects.
Definition: cardinality.h:35
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Representation for an unknown cardinality.
Definition: cardinality.h:54
bool isFinite() const
Returns true iff this cardinality is finite.
Definition: cardinality.h:156
Macros that should be defined everywhere during the building of the libraries and driver binary...
Cardinality operator*(const Cardinality &c) const
Multiply two cardinalities.
Definition: cardinality.h:220
bool isUnknown() const
Returns true iff this cardinality is unknown.
Definition: cardinality.h:151
Cardinality operator+(const Cardinality &c) const
Add two cardinalities.
Definition: cardinality.h:213
static const Cardinality REALS
The cardinality of the set of real numbers.
Definition: cardinality.h:96
Cardinality(CardinalityUnknown)
Construct an unknown cardinality.
Definition: cardinality.h:141
struct CVC4::options::out__option_t out
Cardinality(CardinalityBeth beth)
Construct an infinite cardinality equal to the given Beth number.
Definition: cardinality.h:135
CardinalityComparison
Used as a result code for Cardinality::compare().
Definition: cardinality.h:102
Integer getBethNumber() const
In the case that this cardinality is infinite, return its Beth number.
Definition: cardinality.h:197
const Integer & getNumber() const
Definition: cardinality.h:45