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