GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/cardinality.cpp Lines: 114 144 79.2 %
Date: 2021-03-22 Branches: 223 462 48.3 %

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