1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Clark Barrett, Morgan Deters |
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 |
|
#include "theory/arrays/type_enumerator.h" |
16 |
|
|
17 |
|
#include "expr/array_store_all.h" |
18 |
|
#include "expr/kind.h" |
19 |
|
#include "expr/type_node.h" |
20 |
|
#include "theory/rewriter.h" |
21 |
|
#include "theory/type_enumerator.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace arrays { |
26 |
|
|
27 |
101 |
ArrayEnumerator::ArrayEnumerator(TypeNode type, TypeEnumeratorProperties* tep) |
28 |
|
: TypeEnumeratorBase<ArrayEnumerator>(type), |
29 |
|
d_tep(tep), |
30 |
202 |
d_index(type.getArrayIndexType(), tep), |
31 |
|
d_constituentType(type.getArrayConstituentType()), |
32 |
101 |
d_nm(NodeManager::currentNM()), |
33 |
|
d_indexVec(), |
34 |
|
d_constituentVec(), |
35 |
|
d_finished(false), |
36 |
404 |
d_arrayConst() |
37 |
|
{ |
38 |
101 |
d_indexVec.push_back(*d_index); |
39 |
101 |
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); |
40 |
101 |
d_arrayConst = |
41 |
202 |
d_nm->mkConst(ArrayStoreAll(type, (*(*d_constituentVec.back())))); |
42 |
101 |
Trace("array-type-enum") << "Array const : " << d_arrayConst << std::endl; |
43 |
101 |
} |
44 |
|
|
45 |
2042 |
ArrayEnumerator::ArrayEnumerator(const ArrayEnumerator& ae) |
46 |
|
: TypeEnumeratorBase<ArrayEnumerator>( |
47 |
4084 |
ae.d_nm->mkArrayType(ae.d_index.getType(), ae.d_constituentType)), |
48 |
2042 |
d_tep(ae.d_tep), |
49 |
|
d_index(ae.d_index), |
50 |
|
d_constituentType(ae.d_constituentType), |
51 |
2042 |
d_nm(ae.d_nm), |
52 |
|
d_indexVec(ae.d_indexVec), |
53 |
|
d_constituentVec(), // copied below |
54 |
2042 |
d_finished(ae.d_finished), |
55 |
12252 |
d_arrayConst(ae.d_arrayConst) |
56 |
|
{ |
57 |
2042 |
for (std::vector<TypeEnumerator*>::const_iterator |
58 |
2042 |
i = ae.d_constituentVec.begin(), |
59 |
2042 |
i_end = ae.d_constituentVec.end(); |
60 |
4084 |
i != i_end; |
61 |
|
++i) |
62 |
|
{ |
63 |
2042 |
d_constituentVec.push_back(new TypeEnumerator(**i)); |
64 |
|
} |
65 |
2042 |
} |
66 |
|
|
67 |
6429 |
ArrayEnumerator::~ArrayEnumerator() |
68 |
|
{ |
69 |
6463 |
while (!d_constituentVec.empty()) |
70 |
|
{ |
71 |
2160 |
delete d_constituentVec.back(); |
72 |
2160 |
d_constituentVec.pop_back(); |
73 |
|
} |
74 |
4286 |
} |
75 |
|
|
76 |
10862 |
Node ArrayEnumerator::operator*() |
77 |
|
{ |
78 |
10862 |
if (d_finished) |
79 |
|
{ |
80 |
|
throw NoMoreValuesException(getType()); |
81 |
|
} |
82 |
10862 |
Node n = d_arrayConst; |
83 |
21950 |
for (size_t i = 0, size = d_indexVec.size(); i < size; ++i) |
84 |
|
{ |
85 |
33264 |
n = d_nm->mkNode(kind::STORE, |
86 |
|
n, |
87 |
11088 |
d_indexVec[d_indexVec.size() - 1 - i], |
88 |
22176 |
*(*(d_constituentVec[i]))); |
89 |
|
} |
90 |
10862 |
Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl; |
91 |
10862 |
n = Rewriter::rewrite(n); |
92 |
10862 |
Trace("array-type-enum") << "operator * returning: " << n << std::endl; |
93 |
10862 |
return n; |
94 |
|
} |
95 |
|
|
96 |
2145 |
ArrayEnumerator& ArrayEnumerator::operator++() |
97 |
|
{ |
98 |
4290 |
Trace("array-type-enum") << "operator++ called, **this = " << **this |
99 |
2145 |
<< std::endl; |
100 |
|
|
101 |
2145 |
if (d_finished) |
102 |
|
{ |
103 |
|
Trace("array-type-enum") << "operator++ finished!" << std::endl; |
104 |
|
return *this; |
105 |
|
} |
106 |
2207 |
while (!d_constituentVec.empty()) |
107 |
|
{ |
108 |
2155 |
++(*d_constituentVec.back()); |
109 |
2155 |
if (d_constituentVec.back()->isFinished()) |
110 |
|
{ |
111 |
31 |
delete d_constituentVec.back(); |
112 |
31 |
d_constituentVec.pop_back(); |
113 |
|
} |
114 |
|
else |
115 |
|
{ |
116 |
2124 |
break; |
117 |
|
} |
118 |
|
} |
119 |
|
|
120 |
2145 |
if (d_constituentVec.empty()) |
121 |
|
{ |
122 |
21 |
++d_index; |
123 |
21 |
if (d_index.isFinished()) |
124 |
|
{ |
125 |
1 |
Trace("array-type-enum") << "operator++ finished!" << std::endl; |
126 |
1 |
d_finished = true; |
127 |
1 |
return *this; |
128 |
|
} |
129 |
20 |
d_indexVec.push_back(*d_index); |
130 |
20 |
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); |
131 |
20 |
++(*d_constituentVec.back()); |
132 |
20 |
if (d_constituentVec.back()->isFinished()) |
133 |
|
{ |
134 |
|
Trace("array-type-enum") << "operator++ finished!" << std::endl; |
135 |
|
d_finished = true; |
136 |
|
return *this; |
137 |
|
} |
138 |
|
} |
139 |
|
|
140 |
2200 |
while (d_constituentVec.size() < d_indexVec.size()) |
141 |
|
{ |
142 |
28 |
d_constituentVec.push_back(new TypeEnumerator(d_constituentType, d_tep)); |
143 |
|
} |
144 |
|
|
145 |
4288 |
Trace("array-type-enum") << "operator++ returning, **this = " << **this |
146 |
2144 |
<< std::endl; |
147 |
2144 |
return *this; |
148 |
|
} |
149 |
|
|
150 |
8718 |
bool ArrayEnumerator::isFinished() |
151 |
|
{ |
152 |
17436 |
Trace("array-type-enum") << "isFinished returning: " << d_finished |
153 |
8718 |
<< std::endl; |
154 |
8718 |
return d_finished; |
155 |
|
} |
156 |
|
|
157 |
|
} // namespace arrays |
158 |
|
} // namespace theory |
159 |
22746 |
} // namespace cvc5 |