GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_sets_type_enumerator_white.cpp Lines: 80 80 100.0 %
Date: 2021-03-23 Branches: 259 752 34.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_type_enumerator_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds, Mudathir Mohamed
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::sets::SetsTypeEnumerator
13
 **
14
 ** White box testing of CVC4::theory::sets::SetsTypeEnumerator.  (These tests
15
 ** depends  on the ordering that the SetsTypeEnumerator use, so it's a
16
 *white-box
17
 ** test.)
18
 **/
19
20
#include "expr/dtype.h"
21
#include "test_smt.h"
22
#include "theory/sets/theory_sets_type_enumerator.h"
23
24
namespace CVC4 {
25
26
using namespace theory;
27
using namespace kind;
28
using namespace theory::sets;
29
30
namespace test {
31
32
16
class TestTheoryWhiteSetsTypeEnumerator : public TestSmt
33
{
34
 protected:
35
70
  void addAndCheckUnique(Node n, std::vector<Node>& elems)
36
  {
37
70
    ASSERT_TRUE(n.isConst());
38
70
    ASSERT_TRUE(std::find(elems.begin(), elems.end(), n) == elems.end());
39
70
    elems.push_back(n);
40
  }
41
};
42
43
13
TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans)
44
{
45
4
  TypeNode boolType = d_nodeManager->booleanType();
46
4
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(boolType));
47
2
  ASSERT_FALSE(setEnumerator.isFinished());
48
49
4
  std::vector<Node> elems;
50
51
4
  Node actual0 = *setEnumerator;
52
2
  addAndCheckUnique(actual0, elems);
53
2
  ASSERT_FALSE(setEnumerator.isFinished());
54
55
4
  Node actual1 = *++setEnumerator;
56
2
  addAndCheckUnique(actual1, elems);
57
2
  ASSERT_FALSE(setEnumerator.isFinished());
58
59
4
  Node actual2 = *++setEnumerator;
60
2
  addAndCheckUnique(actual2, elems);
61
2
  ASSERT_FALSE(setEnumerator.isFinished());
62
63
4
  Node actual3 = Rewriter::rewrite(*++setEnumerator);
64
2
  addAndCheckUnique(actual3, elems);
65
2
  ASSERT_FALSE(setEnumerator.isFinished());
66
67
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
68
2
  ASSERT_TRUE(setEnumerator.isFinished());
69
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
70
2
  ASSERT_TRUE(setEnumerator.isFinished());
71
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
72
2
  ASSERT_TRUE(setEnumerator.isFinished());
73
}
74
75
13
TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_UF)
76
{
77
4
  TypeNode sort = d_nodeManager->mkSort("Atom");
78
4
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(sort));
79
80
4
  Node actual0 = *setEnumerator;
81
  Node expected0 =
82
4
      d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(sort)));
83
2
  ASSERT_EQ(expected0, actual0);
84
2
  ASSERT_FALSE(setEnumerator.isFinished());
85
86
4
  std::vector<Node> elems;
87
16
  for (unsigned i = 0; i < 7; i++)
88
  {
89
28
    Node actual = *setEnumerator;
90
14
    addAndCheckUnique(actual, elems);
91
14
    ASSERT_FALSE(setEnumerator.isFinished());
92
14
    ++setEnumerator;
93
  }
94
}
95
96
13
TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_finite_dataype)
97
{
98
4
  DType dt("Colors");
99
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
100
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
101
2
  dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
102
4
  TypeNode datatype = d_nodeManager->mkDatatypeType(dt);
103
  const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
104
2
      datatype.getDType().getConstructors();
105
4
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(datatype));
106
107
  Node red =
108
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor());
109
110
  Node green =
111
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor());
112
113
  Node blue =
114
4
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
115
116
4
  std::vector<Node> elems;
117
18
  for (unsigned i = 0; i < 8; i++)
118
  {
119
32
    Node actual = *setEnumerator;
120
16
    addAndCheckUnique(actual, elems);
121
16
    ASSERT_FALSE(setEnumerator.isFinished());
122
16
    ++setEnumerator;
123
  }
124
125
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
126
2
  ASSERT_TRUE(setEnumerator.isFinished());
127
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
128
2
  ASSERT_TRUE(setEnumerator.isFinished());
129
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
130
2
  ASSERT_TRUE(setEnumerator.isFinished());
131
}
132
133
13
TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv)
134
{
135
4
  TypeNode bitVector2 = d_nodeManager->mkBitVectorType(2);
136
4
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(bitVector2));
137
138
4
  std::vector<Node> elems;
139
34
  for (unsigned i = 0; i < 16; i++)
140
  {
141
64
    Node actual = *setEnumerator;
142
32
    addAndCheckUnique(actual, elems);
143
32
    ASSERT_FALSE(setEnumerator.isFinished());
144
32
    ++setEnumerator;
145
  }
146
147
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
148
2
  ASSERT_TRUE(setEnumerator.isFinished());
149
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
150
2
  ASSERT_TRUE(setEnumerator.isFinished());
151
4
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
152
2
  ASSERT_TRUE(setEnumerator.isFinished());
153
}
154
}  // namespace test
155
75579
}  // namespace CVC4