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 "theory/datatypes/type_enumerator.h" |
17 |
|
|
18 |
|
#include "expr/ascription_type.h" |
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "theory/datatypes/datatypes_rewriter.h" |
21 |
|
#include "theory/datatypes/theory_datatypes_utils.h" |
22 |
|
|
23 |
|
using namespace cvc5; |
24 |
|
using namespace theory; |
25 |
|
using namespace datatypes; |
26 |
|
|
27 |
110631 |
Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ |
28 |
221262 |
Node ret; |
29 |
110631 |
if( i<d_terms[tn].size() ){ |
30 |
97388 |
ret = d_terms[tn][i]; |
31 |
|
}else{ |
32 |
13243 |
Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl; |
33 |
13243 |
std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn ); |
34 |
|
unsigned tei; |
35 |
13243 |
if( it==d_te_index.end() ){ |
36 |
|
//initialize child enumerator for type |
37 |
4001 |
tei = d_children.size(); |
38 |
4001 |
d_te_index[tn] = tei; |
39 |
4001 |
if( tn.isDatatype() && d_has_debruijn ){ |
40 |
|
//must indicate that this is a child enumerator (do not normalize constants for it) |
41 |
62 |
DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep ); |
42 |
62 |
d_children.push_back( TypeEnumerator( dte ) ); |
43 |
|
}else{ |
44 |
3939 |
d_children.push_back( TypeEnumerator( tn, d_tep ) ); |
45 |
|
} |
46 |
4001 |
d_terms[tn].push_back( *d_children[tei] ); |
47 |
|
}else{ |
48 |
9242 |
tei = it->second; |
49 |
|
} |
50 |
|
//enumerate terms until index is reached |
51 |
28791 |
while( i>=d_terms[tn].size() ){ |
52 |
9242 |
++d_children[tei]; |
53 |
9242 |
if( d_children[tei].isFinished() ){ |
54 |
1468 |
Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl; |
55 |
1468 |
return Node::null(); |
56 |
|
} |
57 |
7774 |
d_terms[tn].push_back( *d_children[tei] ); |
58 |
|
} |
59 |
11775 |
Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl; |
60 |
11775 |
ret = d_terms[tn][i]; |
61 |
|
} |
62 |
109163 |
return ret; |
63 |
|
} |
64 |
|
|
65 |
37223 |
bool DatatypesEnumerator::increment( unsigned index ){ |
66 |
37223 |
Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl; |
67 |
37223 |
if( d_sel_sum[index]==-1 ){ |
68 |
|
//first time |
69 |
20897 |
d_sel_sum[index] = 0; |
70 |
|
//special case: no children to iterate |
71 |
20897 |
if( index>=d_has_debruijn && d_sel_types[index].empty() ){ |
72 |
8464 |
Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl; |
73 |
8464 |
return d_size_limit==0; |
74 |
|
}else{ |
75 |
12433 |
Debug("dt-enum") << "...success" << std::endl; |
76 |
12433 |
return true; |
77 |
|
} |
78 |
|
}else{ |
79 |
16326 |
unsigned i = 0; |
80 |
27264 |
while( i < d_sel_index[index].size() ){ |
81 |
|
//increment if the sum of iterations on arguments is less than the limit |
82 |
9266 |
if( d_sel_sum[index]<(int)d_size_limit ){ |
83 |
|
//also check if child enumerator has enough terms |
84 |
4576 |
if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){ |
85 |
3797 |
Debug("dt-enum") << "...success increment child " << i << std::endl; |
86 |
3797 |
d_sel_index[index][i]++; |
87 |
3797 |
d_sel_sum[index]++; |
88 |
3797 |
return true; |
89 |
|
} |
90 |
|
} |
91 |
5469 |
Debug("dt-enum") << "......failed increment child " << i << std::endl; |
92 |
|
//reset child, iterate next |
93 |
5469 |
d_sel_sum[index] -= d_sel_index[index][i]; |
94 |
5469 |
d_sel_index[index][i] = 0; |
95 |
5469 |
i++; |
96 |
|
} |
97 |
12529 |
Debug("dt-enum") << "...failure." << std::endl; |
98 |
12529 |
return false; |
99 |
|
} |
100 |
|
} |
101 |
|
|
102 |
62434 |
Node DatatypesEnumerator::getCurrentTerm(unsigned index) |
103 |
|
{ |
104 |
124868 |
Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type |
105 |
62434 |
<< std::endl; |
106 |
124868 |
Node ret; |
107 |
62434 |
if (index < d_has_debruijn) |
108 |
|
{ |
109 |
1737 |
if (d_child_enum) |
110 |
|
{ |
111 |
2688 |
ret = NodeManager::currentNM()->mkConst( |
112 |
2688 |
UninterpretedConstant(d_type, d_size_limit)); |
113 |
|
} |
114 |
|
else |
115 |
|
{ |
116 |
|
// no top-level variables |
117 |
393 |
return Node::null(); |
118 |
|
} |
119 |
|
} |
120 |
|
else |
121 |
|
{ |
122 |
121394 |
Debug("dt-enum-debug") |
123 |
60697 |
<< "Look at constructor " << (index - d_has_debruijn) << std::endl; |
124 |
60697 |
const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn]; |
125 |
60697 |
Debug("dt-enum-debug") << "Check last term..." << std::endl; |
126 |
|
// we first check if the last argument (which is forced to make sum of |
127 |
|
// iterated arguments equal to d_size_limit) is defined |
128 |
120705 |
Node lc; |
129 |
60697 |
if (ctor.getNumArgs() > 0) |
130 |
|
{ |
131 |
56304 |
Assert(index < d_sel_types.size()); |
132 |
56304 |
Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size()); |
133 |
56304 |
lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1], |
134 |
56304 |
d_size_limit - d_sel_sum[index]); |
135 |
56304 |
if (lc.isNull()) |
136 |
|
{ |
137 |
689 |
Debug("dt-enum-debug") << "Current infeasible." << std::endl; |
138 |
689 |
return Node::null(); |
139 |
|
} |
140 |
|
} |
141 |
60008 |
Debug("dt-enum-debug") << "Get constructor..." << std::endl; |
142 |
120016 |
NodeBuilder b(kind::APPLY_CONSTRUCTOR); |
143 |
60008 |
if (d_datatype.isParametric()) |
144 |
|
{ |
145 |
267 |
NodeManager* nm = NodeManager::currentNM(); |
146 |
534 |
TypeNode typ = ctor.getSpecializedConstructorType(d_type); |
147 |
1335 |
b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, |
148 |
534 |
nm->mkConst(AscriptionType(typ)), |
149 |
1068 |
ctor.getConstructor()); |
150 |
|
} |
151 |
|
else |
152 |
|
{ |
153 |
59741 |
b << ctor.getConstructor(); |
154 |
|
} |
155 |
60008 |
Debug("dt-enum-debug") << "Get arguments..." << std::endl; |
156 |
60008 |
if (ctor.getNumArgs() > 0) |
157 |
|
{ |
158 |
55615 |
Assert(index < d_sel_types.size()); |
159 |
55615 |
Assert(index < d_sel_index.size()); |
160 |
55615 |
Assert(d_sel_types[index].size() == ctor.getNumArgs()); |
161 |
55615 |
Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1); |
162 |
105366 |
for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++) |
163 |
|
{ |
164 |
99502 |
Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]); |
165 |
49751 |
Assert(!c.isNull()); |
166 |
49751 |
b << c; |
167 |
|
} |
168 |
55615 |
b << lc; |
169 |
|
} |
170 |
120016 |
Node nnn = Node(b); |
171 |
60008 |
Debug("dt-enum-debug") << "Return... " << nnn << std::endl; |
172 |
60008 |
ret = nnn; |
173 |
|
} |
174 |
|
|
175 |
61352 |
if (!d_child_enum && d_has_debruijn) |
176 |
|
{ |
177 |
879 |
Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret); |
178 |
601 |
if (nret != ret) |
179 |
|
{ |
180 |
323 |
if (nret.isNull()) |
181 |
|
{ |
182 |
259 |
Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl; |
183 |
|
} |
184 |
|
else |
185 |
|
{ |
186 |
64 |
Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl; |
187 |
64 |
Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl; |
188 |
|
} |
189 |
323 |
return Node::null(); |
190 |
|
} |
191 |
|
} |
192 |
|
|
193 |
61029 |
return ret; |
194 |
|
} |
195 |
|
|
196 |
119883 |
void DatatypesEnumerator::init() |
197 |
|
{ |
198 |
239766 |
Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() |
199 |
119883 |
<< std::endl; |
200 |
119883 |
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; |
201 |
119883 |
Debug("dt-enum") << "datatype is " << d_type << std::endl; |
202 |
239766 |
Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " |
203 |
119883 |
<< d_datatype.isRecursiveSingleton(d_type); |
204 |
239766 |
Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type) |
205 |
119883 |
<< std::endl; |
206 |
|
// Start with the ground term constructed via mkGroundValue, which does |
207 |
|
// a traversal over the structure of the datatype to find a finite term. |
208 |
|
// Notice that mkGroundValue may be dependent upon extracting the first |
209 |
|
// value of type enumerators for *other non-datatype* subfield types of |
210 |
|
// this datatype. Since datatypes can not be embedded in non-datatype |
211 |
|
// types (e.g. (Array D D) cannot be a subfield type of datatype D), this |
212 |
|
// call is guaranteed to avoid infinite recursion. It is important that we |
213 |
|
// start with this term, since it has the same shape as the one returned by |
214 |
|
// TypeNode::mkGroundTerm for d_type, which avoids debug check model |
215 |
|
// failures. |
216 |
119883 |
d_zeroTerm = d_datatype.mkGroundValue(d_type); |
217 |
|
// Only use the zero term if it was successfully constructed. This may |
218 |
|
// fail for codatatype types whose only values are infinite. |
219 |
119883 |
d_zeroTermActive = !d_zeroTerm.isNull(); |
220 |
119883 |
if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype)) |
221 |
|
{ |
222 |
|
// start with uninterpreted constant |
223 |
136 |
d_has_debruijn = 1; |
224 |
136 |
d_sel_types.push_back(std::vector<TypeNode>()); |
225 |
136 |
d_sel_index.push_back(std::vector<unsigned>()); |
226 |
136 |
d_sel_sum.push_back(-1); |
227 |
|
} |
228 |
|
else |
229 |
|
{ |
230 |
|
// find the "zero" term via mkGroundTerm |
231 |
119747 |
Debug("dt-enum-debug") << "make ground term..." << std::endl; |
232 |
119747 |
Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl; |
233 |
119747 |
Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR); |
234 |
119747 |
d_has_debruijn = 0; |
235 |
|
} |
236 |
119883 |
Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl; |
237 |
119883 |
d_ctor = 0; |
238 |
864127 |
for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i) |
239 |
|
{ |
240 |
744244 |
d_sel_types.push_back(std::vector<TypeNode>()); |
241 |
744244 |
d_sel_index.push_back(std::vector<unsigned>()); |
242 |
744244 |
d_sel_sum.push_back(-1); |
243 |
744244 |
const DTypeConstructor& ctor = d_datatype[i]; |
244 |
1488488 |
TypeNode typ; |
245 |
744244 |
if (d_datatype.isParametric()) |
246 |
|
{ |
247 |
154 |
typ = ctor.getSpecializedConstructorType(d_type); |
248 |
|
} |
249 |
1650868 |
for (unsigned a = 0; a < ctor.getNumArgs(); ++a) |
250 |
|
{ |
251 |
1813248 |
TypeNode tn; |
252 |
906624 |
if (d_datatype.isParametric()) |
253 |
|
{ |
254 |
185 |
tn = typ[a]; |
255 |
|
} |
256 |
|
else |
257 |
|
{ |
258 |
906439 |
tn = ctor[a].getSelector().getType()[1]; |
259 |
|
} |
260 |
906624 |
d_sel_types.back().push_back(tn); |
261 |
906624 |
d_sel_index.back().push_back(0); |
262 |
|
} |
263 |
744244 |
if (!d_sel_index.back().empty()) |
264 |
|
{ |
265 |
438290 |
d_sel_index.back().pop_back(); |
266 |
|
} |
267 |
|
} |
268 |
119883 |
d_size_limit = 0; |
269 |
119883 |
if (!d_zeroTermActive) |
270 |
|
{ |
271 |
|
// Set up initial conditions (should always succeed). Here, we are calling |
272 |
|
// the increment function of this class, which ensures a term is ready to |
273 |
|
// read via a dereference of this class. We use the same method for |
274 |
|
// setting up the first term, if it is not already set up |
275 |
|
// (d_zeroTermActive) using the increment function, for uniformity. |
276 |
6 |
++*this; |
277 |
|
} |
278 |
119883 |
AlwaysAssert(!isFinished()); |
279 |
119883 |
} |
280 |
|
|
281 |
16068 |
DatatypesEnumerator& DatatypesEnumerator::operator++() |
282 |
|
{ |
283 |
16068 |
Debug("dt-enum-debug") << ": increment " << this << std::endl; |
284 |
16068 |
if (d_zeroTermActive) |
285 |
|
{ |
286 |
2686 |
d_zeroTermActive = false; |
287 |
|
} |
288 |
16068 |
unsigned prevSize = d_size_limit; |
289 |
53610 |
while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) |
290 |
|
{ |
291 |
|
// increment at index |
292 |
40582 |
while (increment(d_ctor)) |
293 |
|
{ |
294 |
21811 |
Node n = getCurrentTerm(d_ctor); |
295 |
18452 |
if (!n.isNull()) |
296 |
|
{ |
297 |
17047 |
if (n == d_zeroTerm) |
298 |
|
{ |
299 |
1954 |
d_zeroTerm = Node::null(); |
300 |
|
} |
301 |
|
else |
302 |
|
{ |
303 |
15093 |
return *this; |
304 |
|
} |
305 |
|
} |
306 |
|
} |
307 |
|
// Here, we need to step from the current constructor to the next one |
308 |
|
|
309 |
|
// Go to the next constructor |
310 |
18771 |
d_ctor = d_ctor + 1; |
311 |
18771 |
if (d_ctor >= d_has_debruijn + d_datatype.getNumConstructors()) |
312 |
|
{ |
313 |
|
// try next size limit as long as new terms were generated at last size, |
314 |
|
// or other cases |
315 |
15884 |
if (prevSize == d_size_limit |
316 |
886 |
|| (d_size_limit == 0 && d_datatype.isCodatatype()) |
317 |
16770 |
|| d_datatype.getCardinalityClass(d_type) |
318 |
|
== CardinalityClass::INFINITE) |
319 |
|
{ |
320 |
7376 |
d_size_limit++; |
321 |
7376 |
d_ctor = 0; |
322 |
24237 |
for (unsigned i = 0; i < d_sel_sum.size(); i++) |
323 |
|
{ |
324 |
16861 |
d_sel_sum[i] = -1; |
325 |
|
} |
326 |
|
} |
327 |
|
} |
328 |
|
} |
329 |
975 |
return *this; |
330 |
29511 |
} |