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 "expr/array_store_all.h" |
22 |
|
#include "expr/kind.h" |
23 |
|
#include "expr/type_node.h" |
24 |
|
#include "theory/rewriter.h" |
25 |
|
#include "theory/type_enumerator.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
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 |
108 |
ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr) |
44 |
108 |
: TypeEnumeratorBase<ArrayEnumerator>(type), |
45 |
|
d_tep(tep), |
46 |
216 |
d_index(type.getArrayIndexType(), tep), |
47 |
|
d_constituentType(type.getArrayConstituentType()), |
48 |
108 |
d_nm(NodeManager::currentNM()), |
49 |
|
d_indexVec(), |
50 |
|
d_constituentVec(), |
51 |
|
d_finished(false), |
52 |
432 |
d_arrayConst() |
53 |
|
{ |
54 |
108 |
d_indexVec.push_back(*d_index); |
55 |
108 |
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); |
56 |
108 |
d_arrayConst = |
57 |
216 |
d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back())))); |
58 |
108 |
Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl; |
59 |
108 |
} |
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 |
6450 |
~ArrayEnumerator() { |
85 |
6484 |
while (!d_constituentVec.empty()) { |
86 |
2167 |
delete d_constituentVec.back(); |
87 |
2167 |
d_constituentVec.pop_back(); |
88 |
|
} |
89 |
4300 |
} |
90 |
|
|
91 |
10922 |
Node operator*() override |
92 |
|
{ |
93 |
10922 |
if (d_finished) { |
94 |
|
throw NoMoreValuesException(getType()); |
95 |
|
} |
96 |
10922 |
Node n = d_arrayConst; |
97 |
22070 |
for (unsigned i = 0; i < d_indexVec.size(); ++i) { |
98 |
11148 |
n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i]))); |
99 |
|
} |
100 |
10922 |
Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl; |
101 |
10922 |
n = Rewriter::rewrite(n); |
102 |
10922 |
Trace("array-type-enum") << "operator * returning: " << n << std::endl; |
103 |
10922 |
return n; |
104 |
|
} |
105 |
|
|
106 |
2155 |
ArrayEnumerator& operator++() override |
107 |
|
{ |
108 |
2155 |
Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl; |
109 |
|
|
110 |
2155 |
if (d_finished) { |
111 |
|
Trace("array-type-enum") << "operator++ finished!" << std::endl; |
112 |
|
return *this; |
113 |
|
} |
114 |
2217 |
while (!d_constituentVec.empty()) { |
115 |
2165 |
++(*d_constituentVec.back()); |
116 |
2165 |
if (d_constituentVec.back()->isFinished()) { |
117 |
31 |
delete d_constituentVec.back(); |
118 |
31 |
d_constituentVec.pop_back(); |
119 |
|
} |
120 |
|
else { |
121 |
2134 |
break; |
122 |
|
} |
123 |
|
} |
124 |
|
|
125 |
2155 |
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 |
2210 |
while (d_constituentVec.size() < d_indexVec.size()) { |
143 |
28 |
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); |
144 |
|
} |
145 |
|
|
146 |
2154 |
Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl; |
147 |
2154 |
return *this; |
148 |
|
} |
149 |
|
|
150 |
8768 |
bool isFinished() override |
151 |
|
{ |
152 |
8768 |
Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl; |
153 |
8768 |
return d_finished; |
154 |
|
} |
155 |
|
|
156 |
|
};/* class ArrayEnumerator */ |
157 |
|
|
158 |
|
} // namespace arrays |
159 |
|
} // namespace theory |
160 |
|
} // namespace cvc5 |
161 |
|
|
162 |
|
#endif /* CVC5__THEORY__ARRAYS__TYPE_ENUMERATOR_H */ |