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