1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
|
/********************* */
/*! \file cardinality.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Representation of cardinality
**
** Simple class to represent a cardinality; used by the CVC4 type system
** give the cardinality of sorts.
**/
#include "cvc4_public.h"
#ifndef __CVC4__CARDINALITY_H
#define __CVC4__CARDINALITY_H
#include <iostream>
#include <utility>
#include "util/integer.h"
#include "util/Assert.h"
namespace CVC4 {
/**
* A simple representation of a cardinality. We store an
* arbitrary-precision integer for finite cardinalities, and we
* distinguish infinite cardinalities represented as Beth numbers.
*/
class CVC4_PUBLIC Cardinality {
/** Cardinality of the integers */
static const Integer s_intCard;
/** Cardinality of the reals */
static const Integer s_realCard;
/**
* In the case of finite cardinality, this is >= 0, and is equal to
* the cardinality. If infinite, it is < 0, and is Beth[|card|-1].
* That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
*/
Integer d_card;
public:
/** The cardinality of the set of integers. */
static const Cardinality INTEGERS;
/** The cardinality of the set of real numbers. */
static const Cardinality REALS;
/**
* Representation for a Beth number, used only to construct
* Cardinality objects.
*/
class Beth {
Integer d_index;
public:
Beth(const Integer& beth) : d_index(beth) {
CheckArgument(beth >= 0, beth,
"Beth index must be a nonnegative integer, not %s.",
beth.toString().c_str());
}
const Integer& getNumber() const throw() {
return d_index;
}
};/* class Cardinality::Beth */
/**
* Construct a finite cardinality equal to the integer argument.
* The argument must be nonnegative. If we change this to an
* "unsigned" argument to enforce the restriction, we mask some
* errors that automatically convert, like "Cardinality(-1)".
*/
Cardinality(long card) : d_card(card) {
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %ld.", card);
Assert(isFinite());
}
/**
* Construct a finite cardinality equal to the integer argument.
* The argument must be nonnegative.
*/
Cardinality(const Integer& card) : d_card(card) {
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %s.",
card.toString().c_str());
Assert(isFinite());
}
/**
* Construct an infinite cardinality equal to the given Beth number.
*/
Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) {
Assert(!isFinite());
}
/** Returns true iff this cardinality is finite. */
bool isFinite() const throw() {
return d_card >= 0;
}
/**
* Returns true iff this cardinality is finite or countably
* infinite.
*/
bool isCountable() const throw() {
return d_card >= s_intCard;
}
/**
* In the case that this cardinality is finite, return its
* cardinality. (If this cardinality is infinite, this function
* throws an IllegalArgumentException.)
*/
const Integer& getFiniteCardinality() const throw(IllegalArgumentException) {
CheckArgument(isFinite(), *this, "This cardinality is not finite.");
return d_card;
}
/**
* In the case that this cardinality is infinite, return its Beth
* number. (If this cardinality is finite, this function throws an
* IllegalArgumentException.)
*/
Integer getBethNumber() const throw(IllegalArgumentException) {
CheckArgument(!isFinite(), *this, "This cardinality is not infinite.");
return -d_card - 1;
}
/** Assigning addition of this cardinality with another. */
Cardinality& operator+=(const Cardinality& c) throw();
/** Assigning multiplication of this cardinality with another. */
Cardinality& operator*=(const Cardinality& c) throw();
/** Assigning exponentiation of this cardinality with another. */
Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException);
/** Add two cardinalities. */
Cardinality operator+(const Cardinality& c) const throw() {
Cardinality card(*this);
card += c;
return card;
}
/** Multiply two cardinalities. */
Cardinality operator*(const Cardinality& c) const throw() {
Cardinality card(*this);
card *= c;
return card;
}
/**
* Exponentiation of two cardinalities. Throws an exception if both
* are finite and the exponent is too large.
*/
Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) {
Cardinality card(*this);
card ^= c;
return card;
}
/** Test for equality between cardinalities. */
bool operator==(const Cardinality& c) const throw() {
return d_card == c.d_card;
}
/** Test for disequality between cardinalities. */
bool operator!=(const Cardinality& c) const throw() {
return !(*this == c);
}
/** Test whether this cardinality is less than another. */
bool operator<(const Cardinality& c) const throw() {
return
( isFinite() && !c.isFinite() ) ||
( isFinite() && c.isFinite() && d_card < c.d_card ) ||
( !isFinite() && !c.isFinite() && d_card > c.d_card );
}
/**
* Test whether this cardinality is less than or equal to
* another.
*/
bool operator<=(const Cardinality& c) const throw() {
return *this < c || *this == c;
}
/** Test whether this cardinality is greater than another. */
bool operator>(const Cardinality& c) const throw() {
return !(*this <= c);
}
/**
* Test whether this cardinality is greater than or equal to
* another.
*/
bool operator>=(const Cardinality& c) const throw() {
return !(*this < c);
}
/**
* Return a string representation of this cardinality.
*/
std::string toString() const throw();
};/* class Cardinality */
/** Print an element of the InfiniteCardinality enumeration. */
std::ostream& operator<<(std::ostream& out, Cardinality::Beth b)
throw() CVC4_PUBLIC;
/** Print a cardinality in a human-readable fashion. */
std::ostream& operator<<(std::ostream& out, const Cardinality& c)
throw() CVC4_PUBLIC;
}/* CVC4 namespace */
#endif /* __CVC4__CARDINALITY_H */
|
