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