1 /********************* */
2 /*! \file cardinality.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 ** Implementation of a simple class to represent a cardinality.
15 **/
16
17 #include "util/cardinality.h"
18
19 #include "base/cvc4_assert.h"
20
21 namespace CVC4 {
22
23 const Integer Cardinality::s_unknownCard(0);
24 const Integer Cardinality::s_intCard(-1);
25 const Integer Cardinality::s_realCard(-2);
26 const Integer Cardinality::s_largeFiniteCard(
27 Integer("18446744073709551617")); // 2^64 + 1
28
29 const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
30 const Cardinality Cardinality::REALS(CardinalityBeth(1));
31 const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
32
CardinalityBeth(const Integer & beth)33 CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) {
34 PrettyCheckArgument(beth >= 0, beth,
35 "Beth index must be a nonnegative integer, not %s.",
36 beth.toString().c_str());
37 }
38
Cardinality(long card)39 Cardinality::Cardinality(long card) : d_card(card) {
40 PrettyCheckArgument(card >= 0, card,
41 "Cardinality must be a nonnegative integer, not %ld.",
42 card);
43 d_card += 1;
44 }
45
Cardinality(const Integer & card)46 Cardinality::Cardinality(const Integer& card) : d_card(card) {
47 PrettyCheckArgument(card >= 0, card,
48 "Cardinality must be a nonnegative integer, not %s.",
49 card.toString().c_str());
50 d_card += 1;
51 }
52
getFiniteCardinality() const53 Integer Cardinality::getFiniteCardinality() const {
54 PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite.");
55 PrettyCheckArgument(
56 !isLargeFinite(), *this,
57 "This cardinality is finite, but too large to represent.");
58 return d_card - 1;
59 }
60
getBethNumber() const61 Integer Cardinality::getBethNumber() const {
62 PrettyCheckArgument(!isFinite() && !isUnknown(), *this,
63 "This cardinality is not infinite (or is unknown).");
64 return -d_card - 1;
65 }
66
operator +=(const Cardinality & c)67 Cardinality& Cardinality::operator+=(const Cardinality& c) {
68 if (isUnknown()) {
69 return *this;
70 } else if (c.isUnknown()) {
71 d_card = s_unknownCard;
72 return *this;
73 }
74
75 if (c.isFinite() && isLargeFinite()) {
76 return *this;
77 } else if (isFinite() && c.isLargeFinite()) {
78 d_card = s_largeFiniteCard;
79 return *this;
80 }
81
82 if (isFinite() && c.isFinite()) {
83 d_card += c.d_card - 1;
84 return *this;
85 }
86 if (compare(c) == LESS) {
87 return *this = c;
88 } else {
89 return *this;
90 }
91
92 Unreachable();
93 }
94
95 /** Assigning multiplication of this cardinality with another. */
operator *=(const Cardinality & c)96 Cardinality& Cardinality::operator*=(const Cardinality& c) {
97 if (isUnknown()) {
98 return *this;
99 } else if (c.isUnknown()) {
100 d_card = s_unknownCard;
101 return *this;
102 }
103
104 if (c.isFinite() && isLargeFinite()) {
105 return *this;
106 } else if (isFinite() && c.isLargeFinite()) {
107 d_card = s_largeFiniteCard;
108 return *this;
109 }
110
111 if (compare(0) == EQUAL || c.compare(0) == EQUAL) {
112 return *this = 0;
113 } else if (!isFinite() || !c.isFinite()) {
114 if (compare(c) == LESS) {
115 return *this = c;
116 } else {
117 return *this;
118 }
119 } else {
120 d_card -= 1;
121 d_card *= c.d_card - 1;
122 d_card += 1;
123 return *this;
124 }
125
126 Unreachable();
127 }
128
129 /** Assigning exponentiation of this cardinality with another. */
operator ^=(const Cardinality & c)130 Cardinality& Cardinality::operator^=(const Cardinality& c) {
131 if (isUnknown()) {
132 return *this;
133 } else if (c.isUnknown()) {
134 d_card = s_unknownCard;
135 return *this;
136 }
137
138 if (c.isFinite() && isLargeFinite()) {
139 return *this;
140 } else if (isFinite() && c.isLargeFinite()) {
141 d_card = s_largeFiniteCard;
142 return *this;
143 }
144
145 if (c.compare(0) == EQUAL) {
146 // (anything) ^ 0 == 1
147 d_card = 2; // remember, +1 for finite cardinalities
148 return *this;
149 } else if (compare(0) == EQUAL) {
150 // 0 ^ (>= 1) == 0
151 return *this;
152 } else if (compare(1) == EQUAL) {
153 // 1 ^ (>= 1) == 1
154 return *this;
155 } else if (c.compare(1) == EQUAL) {
156 // (anything) ^ 1 == (that thing)
157 return *this;
158 } else if (isFinite() && c.isFinite()) {
159 // finite ^ finite == finite
160 try {
161 // Note: can throw an assertion if c is too big for
162 // exponentiation
163 if (d_card - 1 >= 2 && c.d_card - 1 >= 64) {
164 // don't bother, it's too large anyways
165 d_card = s_largeFiniteCard;
166 } else {
167 d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
168 }
169 } catch (IllegalArgumentException&) {
170 d_card = s_largeFiniteCard;
171 }
172 return *this;
173 } else if (!isFinite() && c.isFinite()) {
174 // inf ^ finite == inf
175 return *this;
176 } else {
177 Assert(compare(2) != LESS && !c.isFinite(),
178 "fall-through case not as expected:\n%s\n%s",
179 this->toString().c_str(), c.toString().c_str());
180 // (>= 2) ^ beth_k == beth_(k+1)
181 // unless the base is already > the exponent
182 if (compare(c) == GREATER) {
183 return *this;
184 }
185 d_card = c.d_card - 1;
186 return *this;
187 }
188
189 Unreachable();
190 }
191
compare(const Cardinality & c) const192 Cardinality::CardinalityComparison Cardinality::compare(
193 const Cardinality& c) const {
194 if (isUnknown() || c.isUnknown()) {
195 return UNKNOWN;
196 } else if (isLargeFinite()) {
197 if (c.isLargeFinite()) {
198 return UNKNOWN;
199 } else if (c.isFinite()) {
200 return GREATER;
201 } else {
202 Assert(c.isInfinite());
203 return LESS;
204 }
205 } else if (c.isLargeFinite()) {
206 if (isLargeFinite()) {
207 return UNKNOWN;
208 } else if (isFinite()) {
209 return LESS;
210 } else {
211 Assert(isInfinite());
212 return GREATER;
213 }
214 } else if (isInfinite()) {
215 if (c.isFinite()) {
216 return GREATER;
217 } else {
218 return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS);
219 }
220 } else if (c.isInfinite()) {
221 Assert(isFinite());
222 return LESS;
223 } else {
224 Assert(isFinite() && !isLargeFinite());
225 Assert(c.isFinite() && !c.isLargeFinite());
226 return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER);
227 }
228
229 Unreachable();
230 }
231
knownLessThanOrEqual(const Cardinality & c) const232 bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const {
233 CardinalityComparison cmp = this->compare(c);
234 return cmp == LESS || cmp == EQUAL;
235 }
236
toString() const237 std::string Cardinality::toString() const {
238 std::stringstream ss;
239 ss << *this;
240 return ss.str();
241 }
242
operator <<(std::ostream & out,CardinalityBeth b)243 std::ostream& operator<<(std::ostream& out, CardinalityBeth b) {
244 out << "beth[" << b.getNumber() << ']';
245
246 return out;
247 }
248
operator <<(std::ostream & out,const Cardinality & c)249 std::ostream& operator<<(std::ostream& out, const Cardinality& c) {
250 if (c.isUnknown()) {
251 out << "Cardinality::UNKNOWN";
252 } else if (c.isFinite()) {
253 out << c.getFiniteCardinality();
254 } else {
255 out << CardinalityBeth(c.getBethNumber());
256 }
257
258 return out;
259 }
260
261 } /* CVC4 namespace */
262