1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Morgan Deters, Andres Noetzli |
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 |
|
* Enumerators for datatypes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "expr/dtype_cons.h" |
17 |
|
#include "theory/datatypes/type_enumerator.h" |
18 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
19 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
20 |
|
|
21 |
|
using namespace cvc5; |
22 |
|
using namespace theory; |
23 |
|
using namespace datatypes; |
24 |
|
|
25 |
220342 |
Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ |
26 |
440684 |
Node ret; |
27 |
220342 |
if( i<d_terms[tn].size() ){ |
28 |
202643 |
ret = d_terms[tn][i]; |
29 |
|
}else{ |
30 |
17699 |
Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl; |
31 |
17699 |
std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn ); |
32 |
|
unsigned tei; |
33 |
17699 |
if( it==d_te_index.end() ){ |
34 |
|
//initialize child enumerator for type |
35 |
6163 |
tei = d_children.size(); |
36 |
6163 |
d_te_index[tn] = tei; |
37 |
6163 |
if( tn.isDatatype() && d_has_debruijn ){ |
38 |
|
//must indicate that this is a child enumerator (do not normalize constants for it) |
39 |
74 |
DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep ); |
40 |
74 |
d_children.push_back( TypeEnumerator( dte ) ); |
41 |
|
}else{ |
42 |
6089 |
d_children.push_back( TypeEnumerator( tn, d_tep ) ); |
43 |
|
} |
44 |
6163 |
d_terms[tn].push_back( *d_children[tei] ); |
45 |
|
}else{ |
46 |
11536 |
tei = it->second; |
47 |
|
} |
48 |
|
//enumerate terms until index is reached |
49 |
37419 |
while( i>=d_terms[tn].size() ){ |
50 |
11536 |
++d_children[tei]; |
51 |
11536 |
if( d_children[tei].isFinished() ){ |
52 |
1676 |
Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl; |
53 |
1676 |
return Node::null(); |
54 |
|
} |
55 |
9860 |
d_terms[tn].push_back( *d_children[tei] ); |
56 |
|
} |
57 |
16023 |
Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl; |
58 |
16023 |
ret = d_terms[tn][i]; |
59 |
|
} |
60 |
218666 |
return ret; |
61 |
|
} |
62 |
|
|
63 |
52699 |
bool DatatypesEnumerator::increment( unsigned index ){ |
64 |
52699 |
Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl; |
65 |
52699 |
if( d_sel_sum[index]==-1 ){ |
66 |
|
//first time |
67 |
26649 |
d_sel_sum[index] = 0; |
68 |
|
//special case: no children to iterate |
69 |
26649 |
if( index>=d_has_debruijn && d_sel_types[index].empty() ){ |
70 |
9353 |
Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl; |
71 |
9353 |
return d_size_limit==0; |
72 |
|
}else{ |
73 |
17296 |
Debug("dt-enum") << "...success" << std::endl; |
74 |
17296 |
return true; |
75 |
|
} |
76 |
|
}else{ |
77 |
26050 |
unsigned i = 0; |
78 |
49288 |
while( i < d_sel_index[index].size() ){ |
79 |
|
//increment if the sum of iterations on arguments is less than the limit |
80 |
20890 |
if( d_sel_sum[index]<(int)d_size_limit ){ |
81 |
|
//also check if child enumerator has enough terms |
82 |
10266 |
if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){ |
83 |
9271 |
Debug("dt-enum") << "...success increment child " << i << std::endl; |
84 |
9271 |
d_sel_index[index][i]++; |
85 |
9271 |
d_sel_sum[index]++; |
86 |
9271 |
return true; |
87 |
|
} |
88 |
|
} |
89 |
11619 |
Debug("dt-enum") << "......failed increment child " << i << std::endl; |
90 |
|
//reset child, iterate next |
91 |
11619 |
d_sel_sum[index] -= d_sel_index[index][i]; |
92 |
11619 |
d_sel_index[index][i] = 0; |
93 |
11619 |
i++; |
94 |
|
} |
95 |
16779 |
Debug("dt-enum") << "...failure." << std::endl; |
96 |
16779 |
return false; |
97 |
|
} |
98 |
|
} |
99 |
|
|
100 |
102622 |
Node DatatypesEnumerator::getCurrentTerm(unsigned index) |
101 |
|
{ |
102 |
205244 |
Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type |
103 |
102622 |
<< std::endl; |
104 |
205244 |
Node ret; |
105 |
102622 |
if (index < d_has_debruijn) |
106 |
|
{ |
107 |
2319 |
if (d_child_enum) |
108 |
|
{ |
109 |
3600 |
ret = NodeManager::currentNM()->mkConst( |
110 |
3600 |
UninterpretedConstant(d_type, d_size_limit)); |
111 |
|
} |
112 |
|
else |
113 |
|
{ |
114 |
|
// no top-level variables |
115 |
519 |
return Node::null(); |
116 |
|
} |
117 |
|
} |
118 |
|
else |
119 |
|
{ |
120 |
200606 |
Debug("dt-enum-debug") |
121 |
100303 |
<< "Look at constructor " << (index - d_has_debruijn) << std::endl; |
122 |
100303 |
const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn]; |
123 |
100303 |
Debug("dt-enum-debug") << "Check last term..." << std::endl; |
124 |
|
// we first check if the last argument (which is forced to make sum of |
125 |
|
// iterated arguments equal to d_size_limit) is defined |
126 |
199925 |
Node lc; |
127 |
100303 |
if (ctor.getNumArgs() > 0) |
128 |
|
{ |
129 |
95610 |
Assert(index < d_sel_types.size()); |
130 |
95610 |
Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size()); |
131 |
95610 |
lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1], |
132 |
95610 |
d_size_limit - d_sel_sum[index]); |
133 |
95610 |
if (lc.isNull()) |
134 |
|
{ |
135 |
681 |
Debug("dt-enum-debug") << "Current infeasible." << std::endl; |
136 |
681 |
return Node::null(); |
137 |
|
} |
138 |
|
} |
139 |
99622 |
Debug("dt-enum-debug") << "Get constructor..." << std::endl; |
140 |
199244 |
NodeBuilder b(kind::APPLY_CONSTRUCTOR); |
141 |
99622 |
if (d_datatype.isParametric()) |
142 |
|
{ |
143 |
282 |
NodeManager* nm = NodeManager::currentNM(); |
144 |
564 |
TypeNode typ = ctor.getSpecializedConstructorType(d_type); |
145 |
1410 |
b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, |
146 |
564 |
nm->mkConst(AscriptionType(typ)), |
147 |
1128 |
ctor.getConstructor()); |
148 |
|
} |
149 |
|
else |
150 |
|
{ |
151 |
99340 |
b << ctor.getConstructor(); |
152 |
|
} |
153 |
99622 |
Debug("dt-enum-debug") << "Get arguments..." << std::endl; |
154 |
99622 |
if (ctor.getNumArgs() > 0) |
155 |
|
{ |
156 |
94929 |
Assert(index < d_sel_types.size()); |
157 |
94929 |
Assert(index < d_sel_index.size()); |
158 |
94929 |
Assert(d_sel_types[index].size() == ctor.getNumArgs()); |
159 |
94929 |
Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1); |
160 |
209395 |
for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++) |
161 |
|
{ |
162 |
228932 |
Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]); |
163 |
114466 |
Assert(!c.isNull()); |
164 |
114466 |
b << c; |
165 |
|
} |
166 |
94929 |
b << lc; |
167 |
|
} |
168 |
199244 |
Node nnn = Node(b); |
169 |
99622 |
Debug("dt-enum-debug") << "Return... " << nnn << std::endl; |
170 |
99622 |
ret = nnn; |
171 |
|
} |
172 |
|
|
173 |
101422 |
if (!d_child_enum && d_has_debruijn) |
174 |
|
{ |
175 |
1095 |
Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret); |
176 |
765 |
if (nret != ret) |
177 |
|
{ |
178 |
435 |
if (nret.isNull()) |
179 |
|
{ |
180 |
353 |
Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl; |
181 |
|
} |
182 |
|
else |
183 |
|
{ |
184 |
82 |
Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl; |
185 |
82 |
Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl; |
186 |
|
} |
187 |
435 |
return Node::null(); |
188 |
|
} |
189 |
|
} |
190 |
|
|
191 |
100987 |
return ret; |
192 |
|
} |
193 |
|
|
194 |
95643 |
void DatatypesEnumerator::init() |
195 |
|
{ |
196 |
191286 |
Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() |
197 |
95643 |
<< std::endl; |
198 |
95643 |
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; |
199 |
95643 |
Debug("dt-enum") << "datatype is " << d_type << std::endl; |
200 |
191286 |
Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " |
201 |
95643 |
<< d_datatype.isRecursiveSingleton(d_type); |
202 |
191286 |
Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type) |
203 |
95643 |
<< std::endl; |
204 |
|
// Start with the ground term constructed via mkGroundValue, which does |
205 |
|
// a traversal over the structure of the datatype to find a finite term. |
206 |
|
// Notice that mkGroundValue may be dependent upon extracting the first |
207 |
|
// value of type enumerators for *other non-datatype* subfield types of |
208 |
|
// this datatype. Since datatypes can not be embedded in non-datatype |
209 |
|
// types (e.g. (Array D D) cannot be a subfield type of datatype D), this |
210 |
|
// call is guaranteed to avoid infinite recursion. It is important that we |
211 |
|
// start with this term, since it has the same shape as the one returned by |
212 |
|
// TypeNode::mkGroundTerm for d_type, which avoids debug check model |
213 |
|
// failures. |
214 |
95643 |
d_zeroTerm = d_datatype.mkGroundValue(d_type); |
215 |
|
// Only use the zero term if it was successfully constructed. This may |
216 |
|
// fail for codatatype types whose only values are infinite. |
217 |
95643 |
d_zeroTermActive = !d_zeroTerm.isNull(); |
218 |
95643 |
if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype)) |
219 |
|
{ |
220 |
|
// start with uninterpreted constant |
221 |
154 |
d_has_debruijn = 1; |
222 |
154 |
d_sel_types.push_back(std::vector<TypeNode>()); |
223 |
154 |
d_sel_index.push_back(std::vector<unsigned>()); |
224 |
154 |
d_sel_sum.push_back(-1); |
225 |
|
} |
226 |
|
else |
227 |
|
{ |
228 |
|
// find the "zero" term via mkGroundTerm |
229 |
95489 |
Debug("dt-enum-debug") << "make ground term..." << std::endl; |
230 |
95489 |
Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl; |
231 |
95489 |
Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR); |
232 |
95489 |
d_has_debruijn = 0; |
233 |
|
} |
234 |
95643 |
Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl; |
235 |
95643 |
d_ctor = 0; |
236 |
686118 |
for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i) |
237 |
|
{ |
238 |
590475 |
d_sel_types.push_back(std::vector<TypeNode>()); |
239 |
590475 |
d_sel_index.push_back(std::vector<unsigned>()); |
240 |
590475 |
d_sel_sum.push_back(-1); |
241 |
590475 |
const DTypeConstructor& ctor = d_datatype[i]; |
242 |
1180950 |
TypeNode typ; |
243 |
590475 |
if (d_datatype.isParametric()) |
244 |
|
{ |
245 |
164 |
typ = ctor.getSpecializedConstructorType(d_type); |
246 |
|
} |
247 |
1321642 |
for (unsigned a = 0; a < ctor.getNumArgs(); ++a) |
248 |
|
{ |
249 |
1462334 |
TypeNode tn; |
250 |
731167 |
if (d_datatype.isParametric()) |
251 |
|
{ |
252 |
197 |
tn = typ[a]; |
253 |
|
} |
254 |
|
else |
255 |
|
{ |
256 |
730970 |
tn = ctor[a].getSelector().getType()[1]; |
257 |
|
} |
258 |
731167 |
d_sel_types.back().push_back(tn); |
259 |
731167 |
d_sel_index.back().push_back(0); |
260 |
|
} |
261 |
590475 |
if (!d_sel_index.back().empty()) |
262 |
|
{ |
263 |
361242 |
d_sel_index.back().pop_back(); |
264 |
|
} |
265 |
|
} |
266 |
95643 |
d_size_limit = 0; |
267 |
95643 |
if (!d_zeroTermActive) |
268 |
|
{ |
269 |
|
// Set up initial conditions (should always succeed). Here, we are calling |
270 |
|
// the increment function of this class, which ensures a term is ready to |
271 |
|
// read via a dereference of this class. We use the same method for |
272 |
|
// setting up the first term, if it is not already set up |
273 |
|
// (d_zeroTermActive) using the increment function, for uniformity. |
274 |
6 |
++*this; |
275 |
|
} |
276 |
95643 |
AlwaysAssert(!isFinished()); |
277 |
95643 |
} |
278 |
|
|
279 |
26074 |
DatatypesEnumerator& DatatypesEnumerator::operator++() |
280 |
|
{ |
281 |
26074 |
Debug("dt-enum-debug") << ": increment " << this << std::endl; |
282 |
26074 |
if (d_zeroTermActive) |
283 |
|
{ |
284 |
3586 |
d_zeroTermActive = false; |
285 |
|
} |
286 |
26074 |
unsigned prevSize = d_size_limit; |
287 |
73258 |
while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) |
288 |
|
{ |
289 |
|
// increment at index |
290 |
56675 |
while (increment(d_ctor)) |
291 |
|
{ |
292 |
33083 |
Node n = getCurrentTerm(d_ctor); |
293 |
29107 |
if (!n.isNull()) |
294 |
|
{ |
295 |
27472 |
if (n == d_zeroTerm) |
296 |
|
{ |
297 |
2341 |
d_zeroTerm = Node::null(); |
298 |
|
} |
299 |
|
else |
300 |
|
{ |
301 |
25131 |
return *this; |
302 |
|
} |
303 |
|
} |
304 |
|
} |
305 |
|
// Here, we need to step from the current constructor to the next one |
306 |
|
|
307 |
|
// Go to the next constructor |
308 |
23592 |
d_ctor = d_ctor + 1; |
309 |
23592 |
if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors()) |
310 |
|
{ |
311 |
|
// try next size limit as long as new terms were generated at last size, |
312 |
|
// or other cases |
313 |
17692 |
if (prevSize == d_size_limit |
314 |
967 |
|| (d_size_limit == 0 && d_datatype.isCodatatype()) |
315 |
18659 |
|| d_datatype.getCardinalityClass(d_type) |
316 |
|
== CardinalityClass::INFINITE) |
317 |
|
{ |
318 |
8311 |
d_size_limit++; |
319 |
8311 |
d_ctor = 0; |
320 |
29239 |
for (unsigned i = 0; i < d_sel_sum.size(); i++) |
321 |
|
{ |
322 |
20928 |
d_sel_sum[i] = -1; |
323 |
|
} |
324 |
|
} |
325 |
|
} |
326 |
|
} |
327 |
943 |
return *this; |
328 |
27735 |
} |