1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Public-box testing of cvc5::Cardinality. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <sstream> |
17 |
|
#include <string> |
18 |
|
|
19 |
|
#include "base/exception.h" |
20 |
|
#include "test.h" |
21 |
|
#include "util/cardinality.h" |
22 |
|
#include "util/integer.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace test { |
26 |
|
|
27 |
4 |
class TestUtilBlackCardinality : public TestInternal |
28 |
|
{ |
29 |
|
protected: |
30 |
|
std::stringstream ss; |
31 |
|
}; |
32 |
|
|
33 |
10 |
TEST_F(TestUtilBlackCardinality, cardinalities) |
34 |
|
{ |
35 |
4 |
Cardinality zero(0); |
36 |
4 |
Cardinality one(1); |
37 |
4 |
Cardinality two(2); |
38 |
|
|
39 |
4 |
Cardinality invalid(0); |
40 |
2 |
ASSERT_THROW(invalid = Cardinality(-1), IllegalArgumentException); |
41 |
2 |
ASSERT_THROW(invalid = Cardinality(-2), IllegalArgumentException); |
42 |
2 |
ASSERT_THROW(invalid = Cardinality(Integer("-3983982192391747295721957")), |
43 |
2 |
IllegalArgumentException); |
44 |
2 |
invalid = one; // test assignment |
45 |
2 |
invalid = Cardinality(5); // test assignment to temporary |
46 |
|
|
47 |
4 |
Cardinality copy(one); // test copy |
48 |
4 |
Cardinality big(Integer("3983982192391747295721957")); |
49 |
4 |
Cardinality r(Cardinality::REALS); |
50 |
4 |
Cardinality i(Cardinality::INTEGERS); |
51 |
|
|
52 |
2 |
ASSERT_EQ(zero.compare(one), Cardinality::LESS); |
53 |
2 |
ASSERT_EQ(one.compare(two), Cardinality::LESS); |
54 |
2 |
ASSERT_EQ(two.compare(invalid), Cardinality::LESS); |
55 |
2 |
ASSERT_EQ(invalid.compare(big), Cardinality::LESS); |
56 |
2 |
ASSERT_EQ(big.compare(i), Cardinality::LESS); |
57 |
2 |
ASSERT_EQ(i.compare(r), Cardinality::LESS); |
58 |
|
|
59 |
2 |
ASSERT_NE(zero.compare(one), Cardinality::GREATER); |
60 |
2 |
ASSERT_NE(zero.compare(zero), Cardinality::GREATER); |
61 |
2 |
ASSERT_NE(one.compare(two), Cardinality::GREATER); |
62 |
2 |
ASSERT_NE(one.compare(one), Cardinality::GREATER); |
63 |
2 |
ASSERT_NE(two.compare(invalid), Cardinality::GREATER); |
64 |
2 |
ASSERT_NE(two.compare(two), Cardinality::GREATER); |
65 |
2 |
ASSERT_NE(invalid.compare(big), Cardinality::GREATER); |
66 |
2 |
ASSERT_NE(invalid.compare(invalid), Cardinality::GREATER); |
67 |
2 |
ASSERT_NE(big.compare(i), Cardinality::GREATER); |
68 |
2 |
ASSERT_NE(big.compare(big), Cardinality::GREATER); |
69 |
2 |
ASSERT_NE(i.compare(r), Cardinality::GREATER); |
70 |
2 |
ASSERT_NE(i.compare(i), Cardinality::GREATER); |
71 |
2 |
ASSERT_NE(r.compare(r), Cardinality::GREATER); |
72 |
|
|
73 |
2 |
ASSERT_EQ(zero.compare(zero), Cardinality::EQUAL); |
74 |
2 |
ASSERT_EQ(one.compare(one), Cardinality::EQUAL); |
75 |
2 |
ASSERT_EQ(two.compare(two), Cardinality::EQUAL); |
76 |
2 |
ASSERT_EQ(invalid.compare(invalid), Cardinality::EQUAL); |
77 |
2 |
ASSERT_EQ(copy.compare(copy), Cardinality::EQUAL); |
78 |
2 |
ASSERT_EQ(copy.compare(one), Cardinality::EQUAL); |
79 |
2 |
ASSERT_EQ(one.compare(copy), Cardinality::EQUAL); |
80 |
2 |
ASSERT_EQ(big.compare(big), Cardinality::UNKNOWN); |
81 |
2 |
ASSERT_EQ(i.compare(i), Cardinality::EQUAL); |
82 |
2 |
ASSERT_EQ(r.compare(r), Cardinality::EQUAL); |
83 |
|
|
84 |
2 |
ASSERT_NE(zero.compare(one), Cardinality::EQUAL); |
85 |
2 |
ASSERT_NE(one.compare(two), Cardinality::EQUAL); |
86 |
2 |
ASSERT_NE(two.compare(invalid), Cardinality::EQUAL); |
87 |
2 |
ASSERT_NE(copy.compare(r), Cardinality::EQUAL); |
88 |
2 |
ASSERT_NE(copy.compare(i), Cardinality::EQUAL); |
89 |
2 |
ASSERT_NE(big.compare(i), Cardinality::EQUAL); |
90 |
2 |
ASSERT_NE(i.compare(big), Cardinality::EQUAL); |
91 |
2 |
ASSERT_NE(big.compare(zero), Cardinality::EQUAL); |
92 |
2 |
ASSERT_NE(r.compare(i), Cardinality::EQUAL); |
93 |
2 |
ASSERT_NE(i.compare(r), Cardinality::EQUAL); |
94 |
|
|
95 |
2 |
ASSERT_EQ(r.compare(zero), Cardinality::GREATER); |
96 |
2 |
ASSERT_EQ(r.compare(one), Cardinality::GREATER); |
97 |
2 |
ASSERT_EQ(r.compare(two), Cardinality::GREATER); |
98 |
2 |
ASSERT_EQ(r.compare(copy), Cardinality::GREATER); |
99 |
2 |
ASSERT_EQ(r.compare(invalid), Cardinality::GREATER); |
100 |
2 |
ASSERT_EQ(r.compare(big), Cardinality::GREATER); |
101 |
2 |
ASSERT_EQ(r.compare(i), Cardinality::GREATER); |
102 |
2 |
ASSERT_NE(r.compare(r), Cardinality::GREATER); |
103 |
2 |
ASSERT_NE(r.compare(r), Cardinality::LESS); |
104 |
|
|
105 |
2 |
ASSERT_TRUE(zero.isFinite()); |
106 |
2 |
ASSERT_TRUE(one.isFinite()); |
107 |
2 |
ASSERT_TRUE(two.isFinite()); |
108 |
2 |
ASSERT_TRUE(copy.isFinite()); |
109 |
2 |
ASSERT_TRUE(invalid.isFinite()); |
110 |
2 |
ASSERT_TRUE(big.isFinite()); |
111 |
2 |
ASSERT_FALSE(i.isFinite()); |
112 |
2 |
ASSERT_FALSE(r.isFinite()); |
113 |
|
|
114 |
2 |
ASSERT_FALSE(zero.isLargeFinite()); |
115 |
2 |
ASSERT_FALSE(one.isLargeFinite()); |
116 |
2 |
ASSERT_FALSE(two.isLargeFinite()); |
117 |
2 |
ASSERT_FALSE(copy.isLargeFinite()); |
118 |
2 |
ASSERT_FALSE(invalid.isLargeFinite()); |
119 |
2 |
ASSERT_TRUE(big.isLargeFinite()); |
120 |
2 |
ASSERT_FALSE(i.isLargeFinite()); |
121 |
2 |
ASSERT_FALSE(r.isLargeFinite()); |
122 |
|
|
123 |
2 |
ASSERT_EQ(zero.getFiniteCardinality(), 0); |
124 |
2 |
ASSERT_EQ(one.getFiniteCardinality(), 1); |
125 |
2 |
ASSERT_EQ(two.getFiniteCardinality(), 2); |
126 |
2 |
ASSERT_EQ(copy.getFiniteCardinality(), 1); |
127 |
2 |
ASSERT_EQ(invalid.getFiniteCardinality(), 5); |
128 |
4 |
ASSERT_THROW(big.getFiniteCardinality(), IllegalArgumentException); |
129 |
4 |
ASSERT_THROW(i.getFiniteCardinality(), IllegalArgumentException); |
130 |
4 |
ASSERT_THROW(r.getFiniteCardinality(), IllegalArgumentException); |
131 |
|
|
132 |
4 |
ASSERT_THROW(zero.getBethNumber(), IllegalArgumentException); |
133 |
4 |
ASSERT_THROW(one.getBethNumber(), IllegalArgumentException); |
134 |
4 |
ASSERT_THROW(two.getBethNumber(), IllegalArgumentException); |
135 |
4 |
ASSERT_THROW(copy.getBethNumber(), IllegalArgumentException); |
136 |
4 |
ASSERT_THROW(invalid.getBethNumber(), IllegalArgumentException); |
137 |
4 |
ASSERT_THROW(big.getBethNumber(), IllegalArgumentException); |
138 |
2 |
ASSERT_TRUE(i.getBethNumber() == 0); |
139 |
2 |
ASSERT_TRUE(r.getBethNumber() == 1); |
140 |
|
|
141 |
2 |
ASSERT_NE(zero.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
142 |
2 |
ASSERT_NE(one.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
143 |
2 |
ASSERT_NE(two.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
144 |
2 |
ASSERT_NE(copy.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
145 |
2 |
ASSERT_NE(invalid.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
146 |
2 |
ASSERT_NE(big.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
147 |
2 |
ASSERT_NE(r.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
148 |
2 |
ASSERT_EQ(i.compare(Cardinality::INTEGERS), Cardinality::EQUAL); |
149 |
|
|
150 |
2 |
ASSERT_NE(zero.compare(Cardinality::REALS), Cardinality::EQUAL); |
151 |
2 |
ASSERT_NE(one.compare(Cardinality::REALS), Cardinality::EQUAL); |
152 |
2 |
ASSERT_NE(two.compare(Cardinality::REALS), Cardinality::EQUAL); |
153 |
2 |
ASSERT_NE(copy.compare(Cardinality::REALS), Cardinality::EQUAL); |
154 |
2 |
ASSERT_NE(invalid.compare(Cardinality::REALS), Cardinality::EQUAL); |
155 |
2 |
ASSERT_NE(big.compare(Cardinality::REALS), Cardinality::EQUAL); |
156 |
2 |
ASSERT_NE(i.compare(Cardinality::REALS), Cardinality::EQUAL); |
157 |
2 |
ASSERT_EQ(r.compare(Cardinality::REALS), Cardinality::EQUAL); |
158 |
|
|
159 |
|
// should work the other way too |
160 |
|
|
161 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(zero), Cardinality::EQUAL); |
162 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(one), Cardinality::EQUAL); |
163 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(two), Cardinality::EQUAL); |
164 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(copy), Cardinality::EQUAL); |
165 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(invalid), Cardinality::EQUAL); |
166 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(big), Cardinality::EQUAL); |
167 |
2 |
ASSERT_NE(Cardinality::INTEGERS.compare(r), Cardinality::EQUAL); |
168 |
2 |
ASSERT_EQ(Cardinality::INTEGERS.compare(i), Cardinality::EQUAL); |
169 |
|
|
170 |
2 |
ASSERT_NE(Cardinality::REALS.compare(zero), Cardinality::EQUAL); |
171 |
2 |
ASSERT_NE(Cardinality::REALS.compare(one), Cardinality::EQUAL); |
172 |
2 |
ASSERT_NE(Cardinality::REALS.compare(two), Cardinality::EQUAL); |
173 |
2 |
ASSERT_NE(Cardinality::REALS.compare(copy), Cardinality::EQUAL); |
174 |
2 |
ASSERT_NE(Cardinality::REALS.compare(invalid), Cardinality::EQUAL); |
175 |
2 |
ASSERT_NE(Cardinality::REALS.compare(big), Cardinality::EQUAL); |
176 |
2 |
ASSERT_NE(Cardinality::REALS.compare(i), Cardinality::EQUAL); |
177 |
2 |
ASSERT_EQ(Cardinality::REALS.compare(r), Cardinality::EQUAL); |
178 |
|
|
179 |
|
// finite cardinal arithmetic |
180 |
|
|
181 |
2 |
ASSERT_EQ((zero + zero).compare(zero), Cardinality::EQUAL); |
182 |
2 |
ASSERT_EQ((zero * zero).compare(zero), Cardinality::EQUAL); |
183 |
2 |
ASSERT_EQ((zero ^ zero).compare(one), Cardinality::EQUAL); |
184 |
2 |
ASSERT_EQ((zero + one).compare(one), Cardinality::EQUAL); |
185 |
2 |
ASSERT_EQ((zero * one).compare(zero), Cardinality::EQUAL); |
186 |
2 |
ASSERT_EQ((zero ^ one).compare(zero), Cardinality::EQUAL); |
187 |
2 |
ASSERT_EQ((one + zero).compare(one), Cardinality::EQUAL); |
188 |
2 |
ASSERT_EQ((one * zero).compare(zero), Cardinality::EQUAL); |
189 |
2 |
ASSERT_EQ((one ^ zero).compare(one), Cardinality::EQUAL); |
190 |
2 |
ASSERT_EQ((two + two).compare(4), Cardinality::EQUAL); |
191 |
2 |
ASSERT_EQ((two ^ two).compare(4), Cardinality::EQUAL); |
192 |
2 |
ASSERT_EQ((two * two).compare(4), Cardinality::EQUAL); |
193 |
2 |
ASSERT_EQ((two += two).compare(4), Cardinality::EQUAL); |
194 |
2 |
ASSERT_EQ(two.compare(4), Cardinality::EQUAL); |
195 |
2 |
ASSERT_EQ((two = 2).compare(2), Cardinality::EQUAL); |
196 |
2 |
ASSERT_EQ(two.compare(2), Cardinality::EQUAL); |
197 |
2 |
ASSERT_EQ((two *= 2).compare(4), Cardinality::EQUAL); |
198 |
2 |
ASSERT_EQ(two.compare(4), Cardinality::EQUAL); |
199 |
2 |
ASSERT_EQ(((two = 2) ^= 2).compare(4), Cardinality::EQUAL); |
200 |
2 |
ASSERT_EQ(two.compare(4), Cardinality::EQUAL); |
201 |
2 |
ASSERT_EQ((two = 2).compare(2), Cardinality::EQUAL); |
202 |
|
|
203 |
|
// infinite cardinal arithmetic |
204 |
|
|
205 |
4 |
Cardinality x = i, y = Cardinality(2) ^ x, z = Cardinality(2) ^ y; |
206 |
|
|
207 |
2 |
ASSERT_TRUE(x.compare(i) == Cardinality::EQUAL |
208 |
2 |
&& y.compare(r) == Cardinality::EQUAL); |
209 |
2 |
ASSERT_TRUE(x.compare(r) != Cardinality::EQUAL |
210 |
2 |
&& y.compare(i) != Cardinality::EQUAL); |
211 |
2 |
ASSERT_TRUE(x.compare(z) != Cardinality::EQUAL |
212 |
2 |
&& y.compare(z) != Cardinality::EQUAL); |
213 |
2 |
ASSERT_TRUE(x.isCountable() && !x.isFinite()); |
214 |
2 |
ASSERT_FALSE(y.isCountable() && !y.isFinite()); |
215 |
2 |
ASSERT_FALSE(z.isCountable() && !z.isFinite()); |
216 |
|
|
217 |
2 |
ASSERT_EQ(big.compare(x), Cardinality::LESS); |
218 |
2 |
ASSERT_EQ(x.compare(y), Cardinality::LESS); |
219 |
2 |
ASSERT_EQ(y.compare(z), Cardinality::LESS); |
220 |
|
|
221 |
4 |
ASSERT_THROW(big.getBethNumber(), IllegalArgumentException); |
222 |
2 |
ASSERT_EQ(x.getBethNumber(), 0); |
223 |
2 |
ASSERT_EQ(y.getBethNumber(), 1); |
224 |
2 |
ASSERT_EQ(z.getBethNumber(), 2); |
225 |
|
|
226 |
2 |
ASSERT_EQ((zero ^ x).compare(zero), Cardinality::EQUAL); |
227 |
2 |
ASSERT_EQ((one ^ x).compare(one), Cardinality::EQUAL); |
228 |
2 |
ASSERT_TRUE((two ^ x).compare(y) == Cardinality::EQUAL |
229 |
2 |
&& (two ^ x).compare(x) != Cardinality::EQUAL); |
230 |
2 |
ASSERT_TRUE((big ^ x).compare(y) == Cardinality::EQUAL |
231 |
2 |
&& (big ^ x).compare(x) != Cardinality::EQUAL); |
232 |
2 |
ASSERT_EQ((two ^ x).compare(big ^ x), Cardinality::EQUAL); |
233 |
|
|
234 |
2 |
ASSERT_EQ((x ^ zero).compare(one), Cardinality::EQUAL); |
235 |
2 |
ASSERT_EQ((x ^ one).compare(x), Cardinality::EQUAL); |
236 |
2 |
ASSERT_EQ((x ^ two).compare(x), Cardinality::EQUAL); |
237 |
2 |
ASSERT_EQ((x ^ big).compare(x), Cardinality::EQUAL); |
238 |
2 |
ASSERT_EQ((x ^ big).compare(x ^ two), Cardinality::EQUAL); |
239 |
|
|
240 |
2 |
ASSERT_EQ((zero ^ y).compare(zero), Cardinality::EQUAL); |
241 |
2 |
ASSERT_EQ((one ^ y).compare(one), Cardinality::EQUAL); |
242 |
2 |
ASSERT_TRUE((two ^ y).compare(x) != Cardinality::EQUAL |
243 |
2 |
&& (two ^ y).compare(y) != Cardinality::EQUAL); |
244 |
2 |
ASSERT_TRUE((big ^ y).compare(y) != Cardinality::EQUAL |
245 |
2 |
&& (big ^ y).compare(y) != Cardinality::EQUAL); |
246 |
2 |
ASSERT_EQ((big ^ y).getBethNumber(), 2); |
247 |
2 |
ASSERT_EQ((two ^ y).compare(big ^ y), Cardinality::EQUAL); |
248 |
|
|
249 |
2 |
ASSERT_EQ((y ^ zero).compare(one), Cardinality::EQUAL); |
250 |
2 |
ASSERT_EQ((y ^ one).compare(y), Cardinality::EQUAL); |
251 |
2 |
ASSERT_EQ((y ^ two).compare(y), Cardinality::EQUAL); |
252 |
2 |
ASSERT_EQ((y ^ big).compare(y), Cardinality::EQUAL); |
253 |
2 |
ASSERT_EQ((y ^ big).compare(y ^ two), Cardinality::EQUAL); |
254 |
|
|
255 |
2 |
ASSERT_EQ((x ^ x).compare(y), Cardinality::EQUAL); |
256 |
2 |
ASSERT_EQ((y ^ x).compare(y), Cardinality::EQUAL); |
257 |
2 |
ASSERT_EQ((x ^ y).compare(z), Cardinality::EQUAL); |
258 |
2 |
ASSERT_EQ((y ^ y).compare(z), Cardinality::EQUAL); |
259 |
2 |
ASSERT_EQ((z ^ x).compare(z), Cardinality::EQUAL); |
260 |
2 |
ASSERT_EQ((z ^ y).compare(z), Cardinality::EQUAL); |
261 |
2 |
ASSERT_EQ((zero ^ z).compare(0), Cardinality::EQUAL); |
262 |
2 |
ASSERT_EQ((z ^ zero).compare(1), Cardinality::EQUAL); |
263 |
2 |
ASSERT_EQ((z ^ 0).compare(1), Cardinality::EQUAL); |
264 |
2 |
ASSERT_EQ((two ^ z).compare(z), Cardinality::GREATER); |
265 |
2 |
ASSERT_EQ((big ^ z).compare(two ^ z), Cardinality::EQUAL); |
266 |
2 |
ASSERT_EQ((x ^ z).compare(two ^ z), Cardinality::EQUAL); |
267 |
2 |
ASSERT_EQ((y ^ z).compare(x ^ z), Cardinality::EQUAL); |
268 |
2 |
ASSERT_EQ((z ^ z).compare(x ^ z), Cardinality::EQUAL); |
269 |
2 |
ASSERT_EQ((z ^ z).getBethNumber(), 3); |
270 |
|
} |
271 |
|
} // namespace test |
272 |
6 |
} // namespace cvc5 |