GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_type_enumerator.cpp Lines: 61 61 100.0 %
Date: 2021-03-23 Branches: 86 186 46.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_type_enumerator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mudathir Mohamed, Andres Noetzli
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 set enumerator implementation
13
 **
14
 ** set enumerator implementation
15
 **/
16
17
#include "theory/sets/theory_sets_type_enumerator.h"
18
19
namespace CVC4 {
20
namespace theory {
21
namespace sets {
22
23
41
SetEnumerator::SetEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
24
    : TypeEnumeratorBase<SetEnumerator>(type),
25
41
      d_nodeManager(NodeManager::currentNM()),
26
82
      d_elementEnumerator(type.getSetElementType(), tep),
27
      d_isFinished(false),
28
      d_currentSetIndex(0),
29
164
      d_currentSet()
30
{
31
41
  d_currentSet = d_nodeManager->mkConst(EmptySet(type));
32
41
}
33
34
10
SetEnumerator::SetEnumerator(const SetEnumerator& enumerator)
35
20
    : TypeEnumeratorBase<SetEnumerator>(enumerator.getType()),
36
10
      d_nodeManager(enumerator.d_nodeManager),
37
      d_elementEnumerator(enumerator.d_elementEnumerator),
38
10
      d_isFinished(enumerator.d_isFinished),
39
10
      d_currentSetIndex(enumerator.d_currentSetIndex),
40
60
      d_currentSet(enumerator.d_currentSet)
41
{
42
10
}
43
44
94
SetEnumerator::~SetEnumerator() {}
45
46
184
Node SetEnumerator::operator*()
47
{
48
184
  if (d_isFinished)
49
  {
50
18
    throw NoMoreValuesException(getType());
51
  }
52
53
332
  Trace("set-type-enum") << "SetEnumerator::operator* d_currentSet = "
54
166
                         << d_currentSet << std::endl;
55
56
166
  return d_currentSet;
57
}
58
59
102
SetEnumerator& SetEnumerator::operator++()
60
{
61
102
  if (d_isFinished)
62
  {
63
32
    Trace("set-type-enum") << "SetEnumerator::operator++ finished!"
64
16
                           << std::endl;
65
32
    Trace("set-type-enum") << "SetEnumerator::operator++ d_currentSet = "
66
16
                           << d_currentSet << std::endl;
67
16
    return *this;
68
  }
69
70
86
  d_currentSetIndex++;
71
72
  // if the index is a power of 2, get a new element from d_elementEnumerator
73
86
  if (d_currentSetIndex == static_cast<unsigned>(1 << d_elementsSoFar.size()))
74
  {
75
    // if there are no more values from d_elementEnumerator, set d_isFinished
76
    // to true
77
46
    if (d_elementEnumerator.isFinished())
78
    {
79
6
      d_isFinished = true;
80
81
12
      Trace("set-type-enum")
82
6
          << "SetEnumerator::operator++ finished!" << std::endl;
83
12
      Trace("set-type-enum")
84
6
          << "SetEnumerator::operator++ d_currentSet = " << d_currentSet
85
6
          << std::endl;
86
6
      return *this;
87
    }
88
89
    // get a new element and return it as a singleton set
90
80
    Node element = *d_elementEnumerator;
91
40
    d_elementsSoFar.push_back(element);
92
80
    TypeNode elementType = d_elementEnumerator.getType();
93
40
    d_currentSet = d_nodeManager->mkSingleton(elementType, element);
94
40
    d_elementEnumerator++;
95
  }
96
  else
97
  {
98
    // determine which elements are included in the set
99
80
    BitVector indices = BitVector(d_elementsSoFar.size(), d_currentSetIndex);
100
80
    std::vector<Node> elements;
101
166
    for (unsigned i = 0; i < d_elementsSoFar.size(); i++)
102
    {
103
      // add the element to the set if its corresponding bit is set
104
126
      if (indices.isBitSet(i))
105
      {
106
96
        elements.push_back(d_elementsSoFar[i]);
107
      }
108
    }
109
80
    d_currentSet = NormalForm::elementsToSet(
110
120
        std::set<TNode>(elements.begin(), elements.end()), getType());
111
  }
112
113
80
  Assert(d_currentSet.isConst());
114
80
  Assert(d_currentSet == Rewriter::rewrite(d_currentSet));
115
116
160
  Trace("set-type-enum") << "SetEnumerator::operator++ d_elementsSoFar = "
117
80
                         << d_elementsSoFar << std::endl;
118
160
  Trace("set-type-enum") << "SetEnumerator::operator++ d_currentSet = "
119
80
                         << d_currentSet << std::endl;
120
121
80
  return *this;
122
}
123
124
202
bool SetEnumerator::isFinished()
125
{
126
404
  Trace("set-type-enum") << "SetEnumerator::isFinished = " << d_isFinished
127
202
                         << std::endl;
128
202
  return d_isFinished;
129
}
130
131
}  // namespace sets
132
}  // namespace theory
133
26685
}  // namespace CVC4