GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/type_cardinality_black.cpp Lines: 210 210 100.0 %
Date: 2021-03-23 Branches: 532 1498 35.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_cardinality_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Morgan Deters
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 Public box testing of Type::getCardinality() for various Types
13
 **
14
 ** Public box testing of Type::getCardinality() for various Types.
15
 **/
16
17
#include <string>
18
19
#include "expr/kind.h"
20
#include "expr/node_manager.h"
21
#include "test_node.h"
22
#include "util/cardinality.h"
23
24
namespace CVC4 {
25
26
using namespace kind;
27
28
namespace test {
29
30
28
class TestNodeBlackTypeCardinality : public TestNode
31
{
32
};
33
34
16
TEST_F(TestNodeBlackTypeCardinality, basics)
35
{
36
2
  ASSERT_EQ(d_nodeManager->booleanType().getCardinality().compare(2),
37
2
            Cardinality::EQUAL);
38
2
  ASSERT_EQ(d_nodeManager->integerType().getCardinality().compare(
39
                Cardinality::INTEGERS),
40
2
            Cardinality::EQUAL);
41
2
  ASSERT_EQ(
42
      d_nodeManager->realType().getCardinality().compare(Cardinality::REALS),
43
2
      Cardinality::EQUAL);
44
}
45
46
16
TEST_F(TestNodeBlackTypeCardinality, arrays)
47
{
48
4
  TypeNode intToInt = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
49
8
                                                 d_nodeManager->integerType());
50
4
  TypeNode realToReal = d_nodeManager->mkArrayType(d_nodeManager->realType(),
51
8
                                                   d_nodeManager->realType());
52
4
  TypeNode realToInt = d_nodeManager->mkArrayType(d_nodeManager->realType(),
53
8
                                                  d_nodeManager->integerType());
54
4
  TypeNode intToReal = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
55
8
                                                  d_nodeManager->realType());
56
4
  TypeNode intToBool = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
57
8
                                                  d_nodeManager->booleanType());
58
  TypeNode realToBool = d_nodeManager->mkArrayType(
59
4
      d_nodeManager->realType(), d_nodeManager->booleanType());
60
4
  TypeNode boolToReal = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
61
8
                                                   d_nodeManager->realType());
62
4
  TypeNode boolToInt = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
63
8
                                                  d_nodeManager->integerType());
64
  TypeNode boolToBool = d_nodeManager->mkArrayType(
65
4
      d_nodeManager->booleanType(), d_nodeManager->booleanType());
66
67
2
  ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
68
2
            Cardinality::EQUAL);
69
2
  ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS),
70
2
            Cardinality::GREATER);
71
2
  ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS),
72
2
            Cardinality::GREATER);
73
2
  ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS),
74
2
            Cardinality::EQUAL);
75
2
  ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS),
76
2
            Cardinality::EQUAL);
77
2
  ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS),
78
2
            Cardinality::GREATER);
79
2
  ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS),
80
2
            Cardinality::EQUAL);
81
2
  ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS),
82
2
            Cardinality::EQUAL);
83
2
  ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL);
84
}
85
86
16
TEST_F(TestNodeBlackTypeCardinality, unary_functions)
87
{
88
  TypeNode intToInt = d_nodeManager->mkFunctionType(
89
4
      d_nodeManager->integerType(), d_nodeManager->integerType());
90
  TypeNode realToReal = d_nodeManager->mkFunctionType(
91
4
      d_nodeManager->realType(), d_nodeManager->realType());
92
  TypeNode realToInt = d_nodeManager->mkFunctionType(
93
4
      d_nodeManager->realType(), d_nodeManager->integerType());
94
  TypeNode intToReal = d_nodeManager->mkFunctionType(
95
4
      d_nodeManager->integerType(), d_nodeManager->realType());
96
  TypeNode intToBool = d_nodeManager->mkFunctionType(
97
4
      d_nodeManager->integerType(), d_nodeManager->booleanType());
98
  TypeNode realToBool = d_nodeManager->mkFunctionType(
99
4
      d_nodeManager->realType(), d_nodeManager->booleanType());
100
  TypeNode boolToReal = d_nodeManager->mkFunctionType(
101
4
      d_nodeManager->booleanType(), d_nodeManager->realType());
102
  TypeNode boolToInt = d_nodeManager->mkFunctionType(
103
4
      d_nodeManager->booleanType(), d_nodeManager->integerType());
104
  TypeNode boolToBool = d_nodeManager->mkFunctionType(
105
4
      d_nodeManager->booleanType(), d_nodeManager->booleanType());
106
107
2
  ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
108
2
            Cardinality::EQUAL);
109
2
  ASSERT_EQ(realToReal.getCardinality().compare(Cardinality::REALS),
110
2
            Cardinality::GREATER);
111
2
  ASSERT_EQ(realToInt.getCardinality().compare(Cardinality::REALS),
112
2
            Cardinality::GREATER);
113
2
  ASSERT_EQ(intToReal.getCardinality().compare(Cardinality::REALS),
114
2
            Cardinality::EQUAL);
115
2
  ASSERT_EQ(intToBool.getCardinality().compare(Cardinality::REALS),
116
2
            Cardinality::EQUAL);
117
2
  ASSERT_EQ(realToBool.getCardinality().compare(Cardinality::REALS),
118
2
            Cardinality::GREATER);
119
2
  ASSERT_EQ(boolToReal.getCardinality().compare(Cardinality::REALS),
120
2
            Cardinality::EQUAL);
121
2
  ASSERT_EQ(boolToInt.getCardinality().compare(Cardinality::INTEGERS),
122
2
            Cardinality::EQUAL);
123
2
  ASSERT_EQ(boolToBool.getCardinality().compare(4), Cardinality::EQUAL);
124
}
125
126
16
TEST_F(TestNodeBlackTypeCardinality, binary_functions)
127
{
128
4
  std::vector<TypeNode> boolbool;
129
2
  boolbool.push_back(d_nodeManager->booleanType());
130
2
  boolbool.push_back(d_nodeManager->booleanType());
131
4
  std::vector<TypeNode> boolint;
132
2
  boolint.push_back(d_nodeManager->booleanType());
133
2
  boolint.push_back(d_nodeManager->integerType());
134
4
  std::vector<TypeNode> intbool;
135
2
  intbool.push_back(d_nodeManager->integerType());
136
2
  intbool.push_back(d_nodeManager->booleanType());
137
4
  std::vector<TypeNode> intint;
138
2
  intint.push_back(d_nodeManager->integerType());
139
2
  intint.push_back(d_nodeManager->integerType());
140
4
  std::vector<TypeNode> intreal;
141
2
  intreal.push_back(d_nodeManager->integerType());
142
2
  intreal.push_back(d_nodeManager->realType());
143
4
  std::vector<TypeNode> realint;
144
2
  realint.push_back(d_nodeManager->realType());
145
2
  realint.push_back(d_nodeManager->integerType());
146
4
  std::vector<TypeNode> realreal;
147
2
  realreal.push_back(d_nodeManager->realType());
148
2
  realreal.push_back(d_nodeManager->realType());
149
4
  std::vector<TypeNode> realbool;
150
2
  realbool.push_back(d_nodeManager->realType());
151
2
  realbool.push_back(d_nodeManager->booleanType());
152
4
  std::vector<TypeNode> boolreal;
153
2
  boolreal.push_back(d_nodeManager->booleanType());
154
2
  boolreal.push_back(d_nodeManager->realType());
155
156
  TypeNode boolboolToBool =
157
4
      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->booleanType());
158
  TypeNode boolboolToInt =
159
4
      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->integerType());
160
  TypeNode boolboolToReal =
161
4
      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->realType());
162
163
  TypeNode boolintToBool =
164
4
      d_nodeManager->mkFunctionType(boolint, d_nodeManager->booleanType());
165
  TypeNode boolintToInt =
166
4
      d_nodeManager->mkFunctionType(boolint, d_nodeManager->integerType());
167
  TypeNode boolintToReal =
168
4
      d_nodeManager->mkFunctionType(boolint, d_nodeManager->realType());
169
170
  TypeNode intboolToBool =
171
4
      d_nodeManager->mkFunctionType(intbool, d_nodeManager->booleanType());
172
  TypeNode intboolToInt =
173
4
      d_nodeManager->mkFunctionType(intbool, d_nodeManager->integerType());
174
  TypeNode intboolToReal =
175
4
      d_nodeManager->mkFunctionType(intbool, d_nodeManager->realType());
176
177
  TypeNode intintToBool =
178
4
      d_nodeManager->mkFunctionType(intint, d_nodeManager->booleanType());
179
  TypeNode intintToInt =
180
4
      d_nodeManager->mkFunctionType(intint, d_nodeManager->integerType());
181
  TypeNode intintToReal =
182
4
      d_nodeManager->mkFunctionType(intint, d_nodeManager->realType());
183
184
  TypeNode intrealToBool =
185
4
      d_nodeManager->mkFunctionType(intreal, d_nodeManager->booleanType());
186
  TypeNode intrealToInt =
187
4
      d_nodeManager->mkFunctionType(intreal, d_nodeManager->integerType());
188
  TypeNode intrealToReal =
189
4
      d_nodeManager->mkFunctionType(intreal, d_nodeManager->realType());
190
191
  TypeNode realintToBool =
192
4
      d_nodeManager->mkFunctionType(realint, d_nodeManager->booleanType());
193
  TypeNode realintToInt =
194
4
      d_nodeManager->mkFunctionType(realint, d_nodeManager->integerType());
195
  TypeNode realintToReal =
196
4
      d_nodeManager->mkFunctionType(realint, d_nodeManager->realType());
197
198
  TypeNode realrealToBool =
199
4
      d_nodeManager->mkFunctionType(realreal, d_nodeManager->booleanType());
200
  TypeNode realrealToInt =
201
4
      d_nodeManager->mkFunctionType(realreal, d_nodeManager->integerType());
202
  TypeNode realrealToReal =
203
4
      d_nodeManager->mkFunctionType(realreal, d_nodeManager->realType());
204
205
  TypeNode realboolToBool =
206
4
      d_nodeManager->mkFunctionType(realbool, d_nodeManager->booleanType());
207
  TypeNode realboolToInt =
208
4
      d_nodeManager->mkFunctionType(realbool, d_nodeManager->integerType());
209
  TypeNode realboolToReal =
210
4
      d_nodeManager->mkFunctionType(realbool, d_nodeManager->realType());
211
212
  TypeNode boolrealToBool =
213
4
      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->booleanType());
214
  TypeNode boolrealToInt =
215
4
      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->integerType());
216
  TypeNode boolrealToReal =
217
4
      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->realType());
218
219
2
  ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL);
220
2
  ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS),
221
2
            Cardinality::EQUAL);
222
2
  ASSERT_EQ(boolboolToReal.getCardinality().compare(Cardinality::REALS),
223
2
            Cardinality::EQUAL);
224
225
2
  ASSERT_EQ(boolintToBool.getCardinality().compare(Cardinality::REALS),
226
2
            Cardinality::EQUAL);
227
2
  ASSERT_EQ(boolintToInt.getCardinality().compare(Cardinality::REALS),
228
2
            Cardinality::EQUAL);
229
2
  ASSERT_EQ(boolintToReal.getCardinality().compare(Cardinality::REALS),
230
2
            Cardinality::EQUAL);
231
232
2
  ASSERT_EQ(intboolToBool.getCardinality().compare(Cardinality::REALS),
233
2
            Cardinality::EQUAL);
234
2
  ASSERT_EQ(intboolToInt.getCardinality().compare(Cardinality::REALS),
235
2
            Cardinality::EQUAL);
236
2
  ASSERT_EQ(intboolToReal.getCardinality().compare(Cardinality::REALS),
237
2
            Cardinality::EQUAL);
238
239
2
  ASSERT_EQ(intintToBool.getCardinality().compare(Cardinality::REALS),
240
2
            Cardinality::EQUAL);
241
2
  ASSERT_EQ(intintToInt.getCardinality().compare(Cardinality::REALS),
242
2
            Cardinality::EQUAL);
243
2
  ASSERT_EQ(intintToReal.getCardinality().compare(Cardinality::REALS),
244
2
            Cardinality::EQUAL);
245
246
2
  ASSERT_EQ(intrealToBool.getCardinality().compare(Cardinality::REALS),
247
2
            Cardinality::GREATER);
248
2
  ASSERT_EQ(intrealToInt.getCardinality().compare(Cardinality::REALS),
249
2
            Cardinality::GREATER);
250
2
  ASSERT_EQ(intrealToReal.getCardinality().compare(Cardinality::REALS),
251
2
            Cardinality::GREATER);
252
253
2
  ASSERT_EQ(realintToBool.getCardinality().compare(Cardinality::REALS),
254
2
            Cardinality::GREATER);
255
2
  ASSERT_EQ(realintToInt.getCardinality().compare(Cardinality::REALS),
256
2
            Cardinality::GREATER);
257
2
  ASSERT_EQ(realintToReal.getCardinality().compare(Cardinality::REALS),
258
2
            Cardinality::GREATER);
259
260
2
  ASSERT_EQ(realrealToBool.getCardinality().compare(Cardinality::REALS),
261
2
            Cardinality::GREATER);
262
2
  ASSERT_EQ(realrealToInt.getCardinality().compare(Cardinality::REALS),
263
2
            Cardinality::GREATER);
264
2
  ASSERT_EQ(realrealToReal.getCardinality().compare(Cardinality::REALS),
265
2
            Cardinality::GREATER);
266
267
2
  ASSERT_EQ(realboolToBool.getCardinality().compare(Cardinality::REALS),
268
2
            Cardinality::GREATER);
269
2
  ASSERT_EQ(realboolToInt.getCardinality().compare(Cardinality::REALS),
270
2
            Cardinality::GREATER);
271
2
  ASSERT_EQ(realboolToReal.getCardinality().compare(Cardinality::REALS),
272
2
            Cardinality::GREATER);
273
274
2
  ASSERT_EQ(boolrealToBool.getCardinality().compare(Cardinality::REALS),
275
2
            Cardinality::GREATER);
276
2
  ASSERT_EQ(boolrealToInt.getCardinality().compare(Cardinality::REALS),
277
2
            Cardinality::GREATER);
278
2
  ASSERT_EQ(boolrealToReal.getCardinality().compare(Cardinality::REALS),
279
2
            Cardinality::GREATER);
280
}
281
282
16
TEST_F(TestNodeBlackTypeCardinality, ternary_functions)
283
{
284
4
  std::vector<TypeNode> boolbool;
285
2
  boolbool.push_back(d_nodeManager->booleanType());
286
2
  boolbool.push_back(d_nodeManager->booleanType());
287
4
  std::vector<TypeNode> boolboolbool = boolbool;
288
2
  boolboolbool.push_back(d_nodeManager->booleanType());
289
290
4
  TypeNode boolboolTuple = d_nodeManager->mkTupleType(boolbool);
291
4
  TypeNode boolboolboolTuple = d_nodeManager->mkTupleType(boolboolbool);
292
293
  TypeNode boolboolboolToBool =
294
4
      d_nodeManager->mkFunctionType(boolboolbool, d_nodeManager->booleanType());
295
  TypeNode boolboolToBoolbool =
296
4
      d_nodeManager->mkFunctionType(boolbool, boolboolTuple);
297
  TypeNode boolToBoolboolbool = d_nodeManager->mkFunctionType(
298
4
      d_nodeManager->booleanType(), boolboolboolTuple);
299
300
2
  ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8),
301
2
            Cardinality::EQUAL);
302
2
  ASSERT_EQ(
303
      boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4),
304
2
      Cardinality::EQUAL);
305
2
  ASSERT_EQ(boolToBoolboolbool.getCardinality().compare(/* 8 ^ 2 */ 8 * 8),
306
2
            Cardinality::EQUAL);
307
}
308
309
16
TEST_F(TestNodeBlackTypeCardinality, undefined_sorts)
310
{
311
4
  TypeNode foo = d_nodeManager->mkSort("foo", NodeManager::SORT_FLAG_NONE);
312
  // We've currently assigned them a specific Beth number, which
313
  // isn't really correct, but...
314
2
  ASSERT_FALSE(foo.getCardinality().isFinite());
315
}
316
317
16
TEST_F(TestNodeBlackTypeCardinality, bitvectors)
318
{
319
2
  ASSERT_EQ(d_nodeManager->mkBitVectorType(0).getCardinality().compare(0),
320
2
            Cardinality::EQUAL);
321
4
  Cardinality lastCard = 0;
322
132
  for (unsigned i = 1; i <= 65; ++i)
323
  {
324
260
    Cardinality card = Cardinality(2) ^ i;
325
260
    Cardinality typeCard = d_nodeManager->mkBitVectorType(i).getCardinality();
326
130
    ASSERT_TRUE(typeCard.compare(lastCard) == Cardinality::GREATER
327
130
                || (typeCard.isLargeFinite() && lastCard.isLargeFinite()));
328
130
    ASSERT_TRUE(typeCard.compare(card) == Cardinality::EQUAL
329
130
                || typeCard.isLargeFinite());
330
130
    lastCard = typeCard;
331
  }
332
}
333
334
}  // namespace test
335
66440
}  // namespace CVC4