GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arrays/type_enumerator.h Lines: 63 69 91.3 %
Date: 2021-03-22 Branches: 99 202 49.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_enumerator.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Clark Barrett, Morgan Deters, Tim King
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 An enumerator for arrays
13
 **
14
 ** An enumerator for arrays.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
20
#define CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H
21
22
#include "theory/type_enumerator.h"
23
#include "expr/type_node.h"
24
#include "expr/kind.h"
25
#include "theory/rewriter.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace arrays {
30
31
class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
32
  /** type properties */
33
  TypeEnumeratorProperties * d_tep;
34
  TypeEnumerator d_index;
35
  TypeNode d_constituentType;
36
  NodeManager* d_nm;
37
  std::vector<Node> d_indexVec;
38
  std::vector<TypeEnumerator*> d_constituentVec;
39
  bool d_finished;
40
  Node d_arrayConst;
41
42
 public:
43
103
  ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr)
44
103
      : TypeEnumeratorBase<ArrayEnumerator>(type),
45
        d_tep(tep),
46
206
        d_index(type.getArrayIndexType(), tep),
47
        d_constituentType(type.getArrayConstituentType()),
48
103
        d_nm(NodeManager::currentNM()),
49
        d_indexVec(),
50
        d_constituentVec(),
51
        d_finished(false),
52
412
        d_arrayConst()
53
  {
54
103
    d_indexVec.push_back(*d_index);
55
103
    d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
56
103
    d_arrayConst =
57
206
        d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back()))));
58
103
    Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl;
59
103
  }
60
61
  // An array enumerator could be large, and generally you don't want to
62
  // go around copying these things; but a copy ctor is presently required
63
  // by the TypeEnumerator framework.
64
2042
  ArrayEnumerator(const ArrayEnumerator& ae)
65
2042
      : TypeEnumeratorBase<ArrayEnumerator>(
66
4084
            ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)),
67
2042
        d_tep(ae.d_tep),
68
        d_index(ae.d_index),
69
        d_constituentType(ae.d_constituentType),
70
2042
        d_nm(ae.d_nm),
71
        d_indexVec(ae.d_indexVec),
72
        d_constituentVec(),  // copied below
73
2042
        d_finished(ae.d_finished),
74
12252
        d_arrayConst(ae.d_arrayConst)
75
  {
76
2042
    for(std::vector<TypeEnumerator*>::const_iterator i =
77
2042
          ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
78
4084
        i != i_end;
79
        ++i) {
80
2042
      d_constituentVec.push_back(new TypeEnumerator(**i));
81
    }
82
2042
  }
83
84
6435
  ~ArrayEnumerator() {
85
6469
    while (!d_constituentVec.empty()) {
86
2162
      delete d_constituentVec.back();
87
2162
      d_constituentVec.pop_back();
88
    }
89
4290
  }
90
91
10878
  Node operator*() override
92
  {
93
10878
    if (d_finished) {
94
      throw NoMoreValuesException(getType());
95
    }
96
10878
    Node n = d_arrayConst;
97
21982
    for (unsigned i = 0; i < d_indexVec.size(); ++i) {
98
11104
      n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
99
    }
100
10878
    Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl;
101
10878
    n = Rewriter::rewrite(n);
102
10878
    Trace("array-type-enum") << "operator * returning: " << n << std::endl;
103
10878
    return n;
104
  }
105
106
2147
  ArrayEnumerator& operator++() override
107
  {
108
2147
    Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
109
110
2147
    if (d_finished) {
111
      Trace("array-type-enum") << "operator++ finished!" << std::endl;
112
      return *this;
113
    }
114
2209
    while (!d_constituentVec.empty()) {
115
2157
      ++(*d_constituentVec.back());
116
2157
      if (d_constituentVec.back()->isFinished()) {
117
31
        delete d_constituentVec.back();
118
31
        d_constituentVec.pop_back();
119
      }
120
      else {
121
2126
        break;
122
      }
123
    }
124
125
2147
    if (d_constituentVec.empty()) {
126
21
      ++d_index;
127
21
      if (d_index.isFinished()) {
128
1
        Trace("array-type-enum") << "operator++ finished!" << std::endl;
129
1
        d_finished = true;
130
1
        return *this;
131
      }
132
20
      d_indexVec.push_back(*d_index);
133
20
      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
134
20
      ++(*d_constituentVec.back());
135
20
      if (d_constituentVec.back()->isFinished()) {
136
        Trace("array-type-enum") << "operator++ finished!" << std::endl;
137
        d_finished = true;
138
        return *this;
139
      }
140
    }
141
142
2202
    while (d_constituentVec.size() < d_indexVec.size()) {
143
28
      d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep));
144
    }
145
146
2146
    Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl;
147
2146
    return *this;
148
  }
149
150
8732
  bool isFinished() override
151
  {
152
8732
    Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl;
153
8732
    return d_finished;
154
  }
155
156
};/* class ArrayEnumerator */
157
158
}/* CVC4::theory::arrays namespace */
159
}/* CVC4::theory namespace */
160
}/* CVC4 namespace */
161
162
#endif /* CVC4__THEORY__ARRAYS__TYPE_ENUMERATOR_H */