GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/type_enumerator_white.cpp Lines: 201 201 100.0 %
Date: 2021-03-22 Branches: 962 2838 33.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, 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 White box testing of CVC4::theory::TypeEnumerator
13
 **
14
 ** White box testing of CVC4::theory::TypeEnumerator.  (These tests depends
15
 ** on the ordering that the TypeEnumerators use, so it's a white-box test.)
16
 **/
17
18
#include <unordered_set>
19
20
#include "expr/array_store_all.h"
21
#include "expr/dtype.h"
22
#include "expr/kind.h"
23
#include "expr/type_node.h"
24
#include "options/language.h"
25
#include "test_smt.h"
26
#include "theory/type_enumerator.h"
27
28
namespace CVC4 {
29
30
using namespace theory;
31
using namespace kind;
32
33
namespace test {
34
35
28
class TestTheoryWhiteTypeEnumerator : public TestSmt
36
{
37
};
38
39
16
TEST_F(TestTheoryWhiteTypeEnumerator, booleans)
40
{
41
4
  TypeEnumerator te(d_nodeManager->booleanType());
42
2
  ASSERT_FALSE(te.isFinished());
43
2
  ASSERT_EQ(*te, d_nodeManager->mkConst(false));
44
2
  ASSERT_FALSE(te.isFinished());
45
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(true));
46
2
  ASSERT_FALSE(te.isFinished());
47
4
  ASSERT_THROW(*++te, NoMoreValuesException);
48
2
  ASSERT_TRUE(te.isFinished());
49
4
  ASSERT_THROW(*++te, NoMoreValuesException);
50
2
  ASSERT_TRUE(te.isFinished());
51
4
  ASSERT_THROW(*++te, NoMoreValuesException);
52
2
  ASSERT_TRUE(te.isFinished());
53
}
54
55
16
TEST_F(TestTheoryWhiteTypeEnumerator, uf)
56
{
57
4
  TypeNode sort = d_nodeManager->mkSort("T");
58
4
  TypeNode sort2 = d_nodeManager->mkSort("U");
59
4
  TypeEnumerator te(sort);
60
2
  ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0)));
61
200
  for (size_t i = 1; i < 100; ++i)
62
  {
63
198
    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
64
198
    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i)));
65
198
    ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i)));
66
198
    ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2)));
67
  }
68
}
69
70
16
TEST_F(TestTheoryWhiteTypeEnumerator, arith)
71
{
72
4
  TypeEnumerator te(d_nodeManager->integerType());
73
2
  ASSERT_FALSE(te.isFinished());
74
2
  ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0)));
75
202
  for (int i = 1; i <= 100; ++i)
76
  {
77
200
    ASSERT_FALSE(te.isFinished());
78
200
    ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(i)));
79
200
    ASSERT_FALSE(te.isFinished());
80
200
    ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-i)));
81
  }
82
2
  ASSERT_FALSE(te.isFinished());
83
84
2
  te = TypeEnumerator(d_nodeManager->realType());
85
2
  ASSERT_FALSE(te.isFinished());
86
2
  ASSERT_EQ(*te, d_nodeManager->mkConst(Rational(0, 1)));
87
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 1)));
88
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 1)));
89
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 1)));
90
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 1)));
91
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 2)));
92
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 2)));
93
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 1)));
94
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 1)));
95
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 3)));
96
2
  ASSERT_FALSE(te.isFinished());
97
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 3)));
98
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 1)));
99
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 1)));
100
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 2)));
101
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 2)));
102
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 3)));
103
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 3)));
104
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 4)));
105
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 4)));
106
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 1)));
107
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 1)));
108
2
  ASSERT_FALSE(te.isFinished());
109
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 5)));
110
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 5)));
111
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(6, 1)));
112
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-6, 1)));
113
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 2)));
114
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 2)));
115
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(4, 3)));
116
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-4, 3)));
117
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 4)));
118
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 4)));
119
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(2, 5)));
120
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-2, 5)));
121
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 6)));
122
2
  ASSERT_FALSE(te.isFinished());
123
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 6)));
124
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(7, 1)));
125
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-7, 1)));
126
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(5, 3)));
127
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-5, 3)));
128
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(3, 5)));
129
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-3, 5)));
130
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(1, 7)));
131
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(Rational(-1, 7)));
132
2
  ASSERT_FALSE(te.isFinished());
133
}
134
135
16
TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_finite)
136
{
137
4
  DType dt("Colors");
138
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
139
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("orange"));
140
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
141
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
142
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
143
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("violet"));
144
4
  TypeNode datatype = d_nodeManager->mkDatatypeType(dt);
145
  const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
146
2
      datatype.getDType().getConstructors();
147
4
  TypeEnumerator te(datatype);
148
2
  ASSERT_EQ(
149
      *te,
150
2
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor()));
151
2
  ASSERT_EQ(
152
      *++te,
153
2
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor()));
154
2
  ASSERT_EQ(
155
      *++te,
156
2
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor()));
157
2
  ASSERT_EQ(
158
      *++te,
159
2
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[3]->getConstructor()));
160
2
  ASSERT_EQ(
161
      *++te,
162
2
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[4]->getConstructor()));
163
2
  ASSERT_EQ(
164
      *++te,
165
2
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[5]->getConstructor()));
166
4
  ASSERT_THROW(*++te, NoMoreValuesException);
167
4
  ASSERT_THROW(*++te, NoMoreValuesException);
168
4
  ASSERT_THROW(*++te, NoMoreValuesException);
169
}
170
171
16
TEST_F(TestTheoryWhiteTypeEnumerator, dtypes_infinite)
172
{
173
4
  DType colors("Colors");
174
2
  colors.addConstructor(std::make_shared<DTypeConstructor>("red"));
175
2
  colors.addConstructor(std::make_shared<DTypeConstructor>("orange"));
176
2
  colors.addConstructor(std::make_shared<DTypeConstructor>("yellow"));
177
2
  colors.addConstructor(std::make_shared<DTypeConstructor>("green"));
178
2
  colors.addConstructor(std::make_shared<DTypeConstructor>("blue"));
179
2
  colors.addConstructor(std::make_shared<DTypeConstructor>("violet"));
180
4
  TypeNode colorsType = d_nodeManager->mkDatatypeType(colors);
181
  const std::vector<std::shared_ptr<DTypeConstructor> >& ctCons =
182
2
      colorsType.getDType().getConstructors();
183
4
  DType listColors("ListColors");
184
  std::shared_ptr<DTypeConstructor> consC =
185
4
      std::make_shared<DTypeConstructor>("cons");
186
2
  consC->addArg("car", colorsType);
187
2
  consC->addArgSelf("cdr");
188
2
  listColors.addConstructor(consC);
189
2
  listColors.addConstructor(std::make_shared<DTypeConstructor>("nil"));
190
4
  TypeNode listColorsType = d_nodeManager->mkDatatypeType(listColors);
191
  const std::vector<std::shared_ptr<DTypeConstructor> >& lctCons =
192
2
      listColorsType.getDType().getConstructors();
193
194
4
  TypeEnumerator te(listColorsType);
195
2
  ASSERT_FALSE(te.isFinished());
196
4
  Node cons = lctCons[0]->getConstructor();
197
  Node nil =
198
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, lctCons[1]->getConstructor());
199
  Node red =
200
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[0]->getConstructor());
201
  Node orange =
202
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[1]->getConstructor());
203
  Node yellow =
204
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, ctCons[2]->getConstructor());
205
2
  ASSERT_EQ(*te, nil);
206
2
  ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
207
2
  ASSERT_FALSE(te.isFinished());
208
2
  ASSERT_EQ(*++te,
209
            d_nodeManager->mkNode(
210
                APPLY_CONSTRUCTOR,
211
                cons,
212
                red,
213
2
                d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
214
2
  ASSERT_FALSE(te.isFinished());
215
2
  ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil));
216
2
  ASSERT_FALSE(te.isFinished());
217
2
  ASSERT_EQ(*++te,
218
            d_nodeManager->mkNode(
219
                APPLY_CONSTRUCTOR,
220
                cons,
221
                red,
222
                d_nodeManager->mkNode(
223
                    APPLY_CONSTRUCTOR,
224
                    cons,
225
                    red,
226
2
                    d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
227
2
  ASSERT_FALSE(te.isFinished());
228
2
  ASSERT_EQ(*++te,
229
            d_nodeManager->mkNode(
230
                APPLY_CONSTRUCTOR,
231
                cons,
232
                orange,
233
2
                d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
234
2
  ASSERT_FALSE(te.isFinished());
235
2
  ASSERT_EQ(*++te, d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil));
236
2
  ASSERT_FALSE(te.isFinished());
237
2
  ASSERT_EQ(*++te,
238
            d_nodeManager->mkNode(
239
                APPLY_CONSTRUCTOR,
240
                cons,
241
                red,
242
2
                d_nodeManager->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)));
243
2
  ASSERT_FALSE(te.isFinished());
244
}
245
246
16
TEST_F(TestTheoryWhiteTypeEnumerator, arrays_infinite)
247
{
248
6
  TypeEnumerator te(d_nodeManager->mkArrayType(d_nodeManager->integerType(),
249
8
                                               d_nodeManager->integerType()));
250
4
  std::unordered_set<Node, NodeHashFunction> elts;
251
2002
  for (uint32_t i = 0; i < 1000; ++i)
252
  {
253
2000
    ASSERT_FALSE(te.isFinished());
254
4000
    Node elt = *te++;
255
    // ensure no duplicates
256
2000
    ASSERT_TRUE(elts.find(elt) == elts.end());
257
2000
    elts.insert(elt);
258
  }
259
2
  ASSERT_FALSE(te.isFinished());
260
261
  // ensure that certain items were found
262
4
  TypeNode arrayType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
263
8
                                                  d_nodeManager->integerType());
264
  Node zeroes = d_nodeManager->mkConst(
265
4
      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(0))));
266
  Node ones = d_nodeManager->mkConst(
267
4
      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(1))));
268
  Node twos = d_nodeManager->mkConst(
269
4
      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(2))));
270
  Node threes = d_nodeManager->mkConst(
271
4
      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(3))));
272
  Node fours = d_nodeManager->mkConst(
273
4
      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(4))));
274
  Node tens = d_nodeManager->mkConst(
275
4
      ArrayStoreAll(arrayType, d_nodeManager->mkConst(Rational(10))));
276
277
4
  Node zero = d_nodeManager->mkConst(Rational(0));
278
4
  Node one = d_nodeManager->mkConst(Rational(1));
279
4
  Node two = d_nodeManager->mkConst(Rational(2));
280
4
  Node three = d_nodeManager->mkConst(Rational(3));
281
4
  Node four = d_nodeManager->mkConst(Rational(4));
282
4
  Node five = d_nodeManager->mkConst(Rational(5));
283
4
  Node eleven = d_nodeManager->mkConst(Rational(11));
284
285
2
  ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, ones, zero, zero)),
286
2
            elts.end());
287
288
  // the arrays enumerator is currently not a fair enumerator -- when it is,
289
  // these should be flipped
290
2
  ASSERT_EQ(elts.find(d_nodeManager->mkNode(STORE, tens, four, five)),
291
2
            elts.end());
292
2
  ASSERT_EQ(elts.find(d_nodeManager->mkNode(
293
                STORE,
294
                d_nodeManager->mkNode(
295
                    STORE,
296
                    d_nodeManager->mkNode(STORE, fours, eleven, two),
297
                    two,
298
                    one),
299
                zero,
300
                two)),
301
2
            elts.end());
302
2
  ASSERT_EQ(elts.find(threes), elts.end());
303
2
  ASSERT_EQ(elts.find(d_nodeManager->mkNode(
304
                STORE,
305
                d_nodeManager->mkNode(
306
                    STORE,
307
                    d_nodeManager->mkNode(
308
                        STORE,
309
                        d_nodeManager->mkNode(STORE, twos, three, zero),
310
                        two,
311
                        zero),
312
                    one,
313
                    zero),
314
                zero,
315
                zero)),
316
2
            elts.end());
317
}
318
319
16
TEST_F(TestTheoryWhiteTypeEnumerator, bv)
320
{
321
4
  TypeEnumerator te(d_nodeManager->mkBitVectorType(3));
322
2
  ASSERT_EQ(*te, d_nodeManager->mkConst(BitVector(3u, 0u)));
323
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 1u)));
324
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 2u)));
325
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 3u)));
326
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 4u)));
327
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 5u)));
328
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 6u)));
329
2
  ASSERT_EQ(*++te, d_nodeManager->mkConst(BitVector(3u, 7u)));
330
4
  ASSERT_THROW(*++te, NoMoreValuesException);
331
4
  ASSERT_THROW(*++te, NoMoreValuesException);
332
4
  ASSERT_THROW(*++te, NoMoreValuesException);
333
}
334
}  // namespace test
335
1511026
}  // namespace CVC4