cvc4-1.3
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
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
CVC4's exception base class and some associated utilities.
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
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
struct CVC4::options::out__option_t out
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
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