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 |
111689 |
Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ |
28 |
223378 |
Node ret; |
29 |
111689 |
if( i<d_terms[tn].size() ){ |
30 |
98023 |
ret = d_terms[tn][i]; |
31 |
|
}else{ |
32 |
13666 |
Debug("dt-enum-debug") << "get term enum " << tn << " " << i << std::endl; |
33 |
13666 |
std::map< TypeNode, unsigned >::iterator it = d_te_index.find( tn ); |
34 |
|
unsigned tei; |
35 |
13666 |
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 |
74 |
DatatypesEnumerator * dte = new DatatypesEnumerator( tn, true, d_tep ); |
42 |
74 |
d_children.push_back( TypeEnumerator( dte ) ); |
43 |
|
}else{ |
44 |
3927 |
d_children.push_back( TypeEnumerator( tn, d_tep ) ); |
45 |
|
} |
46 |
4001 |
d_terms[tn].push_back( *d_children[tei] ); |
47 |
|
}else{ |
48 |
9665 |
tei = it->second; |
49 |
|
} |
50 |
|
//enumerate terms until index is reached |
51 |
29628 |
while( i>=d_terms[tn].size() ){ |
52 |
9665 |
++d_children[tei]; |
53 |
9665 |
if( d_children[tei].isFinished() ){ |
54 |
1684 |
Debug("dt-enum-debug") << "...fail term enum " << tn << " " << i << std::endl; |
55 |
1684 |
return Node::null(); |
56 |
|
} |
57 |
7981 |
d_terms[tn].push_back( *d_children[tei] ); |
58 |
|
} |
59 |
11982 |
Debug("dt-enum-debug") << "...return term enum " << tn << " " << i << " : " << d_terms[tn][i] << std::endl; |
60 |
11982 |
ret = d_terms[tn][i]; |
61 |
|
} |
62 |
110005 |
return ret; |
63 |
|
} |
64 |
|
|
65 |
38311 |
bool DatatypesEnumerator::increment( unsigned index ){ |
66 |
38311 |
Debug("dt-enum") << "Incrementing " << d_type << " " << d_ctor << " at size " << d_sel_sum[index] << "/" << d_size_limit << std::endl; |
67 |
38311 |
if( d_sel_sum[index]==-1 ){ |
68 |
|
//first time |
69 |
21556 |
d_sel_sum[index] = 0; |
70 |
|
//special case: no children to iterate |
71 |
21556 |
if( index>=d_has_debruijn && d_sel_types[index].empty() ){ |
72 |
8685 |
Debug("dt-enum") << "...success (nc) = " << (d_size_limit==0) << std::endl; |
73 |
8685 |
return d_size_limit==0; |
74 |
|
}else{ |
75 |
12871 |
Debug("dt-enum") << "...success" << std::endl; |
76 |
12871 |
return true; |
77 |
|
} |
78 |
|
}else{ |
79 |
16755 |
unsigned i = 0; |
80 |
28105 |
while( i < d_sel_index[index].size() ){ |
81 |
|
//increment if the sum of iterations on arguments is less than the limit |
82 |
9457 |
if( d_sel_sum[index]<(int)d_size_limit ){ |
83 |
|
//also check if child enumerator has enough terms |
84 |
4777 |
if( !getTermEnum( d_sel_types[index][i], d_sel_index[index][i]+1 ).isNull() ){ |
85 |
3782 |
Debug("dt-enum") << "...success increment child " << i << std::endl; |
86 |
3782 |
d_sel_index[index][i]++; |
87 |
3782 |
d_sel_sum[index]++; |
88 |
3782 |
return true; |
89 |
|
} |
90 |
|
} |
91 |
5675 |
Debug("dt-enum") << "......failed increment child " << i << std::endl; |
92 |
|
//reset child, iterate next |
93 |
5675 |
d_sel_sum[index] -= d_sel_index[index][i]; |
94 |
5675 |
d_sel_index[index][i] = 0; |
95 |
5675 |
i++; |
96 |
|
} |
97 |
12973 |
Debug("dt-enum") << "...failure." << std::endl; |
98 |
12973 |
return false; |
99 |
|
} |
100 |
|
} |
101 |
|
|
102 |
63428 |
Node DatatypesEnumerator::getCurrentTerm(unsigned index) |
103 |
|
{ |
104 |
126856 |
Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type |
105 |
63428 |
<< std::endl; |
106 |
126856 |
Node ret; |
107 |
63428 |
if (index < d_has_debruijn) |
108 |
|
{ |
109 |
2319 |
if (d_child_enum) |
110 |
|
{ |
111 |
3600 |
ret = NodeManager::currentNM()->mkConst( |
112 |
3600 |
UninterpretedConstant(d_type, d_size_limit)); |
113 |
|
} |
114 |
|
else |
115 |
|
{ |
116 |
|
// no top-level variables |
117 |
519 |
return Node::null(); |
118 |
|
} |
119 |
|
} |
120 |
|
else |
121 |
|
{ |
122 |
122218 |
Debug("dt-enum-debug") |
123 |
61109 |
<< "Look at constructor " << (index - d_has_debruijn) << std::endl; |
124 |
61109 |
const DTypeConstructor& ctor = d_datatype[index - d_has_debruijn]; |
125 |
61109 |
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 |
121529 |
Node lc; |
129 |
61109 |
if (ctor.getNumArgs() > 0) |
130 |
|
{ |
131 |
56724 |
Assert(index < d_sel_types.size()); |
132 |
56724 |
Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size()); |
133 |
56724 |
lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1], |
134 |
56724 |
d_size_limit - d_sel_sum[index]); |
135 |
56724 |
if (lc.isNull()) |
136 |
|
{ |
137 |
689 |
Debug("dt-enum-debug") << "Current infeasible." << std::endl; |
138 |
689 |
return Node::null(); |
139 |
|
} |
140 |
|
} |
141 |
60420 |
Debug("dt-enum-debug") << "Get constructor..." << std::endl; |
142 |
120840 |
NodeBuilder b(kind::APPLY_CONSTRUCTOR); |
143 |
60420 |
if (d_datatype.isParametric()) |
144 |
|
{ |
145 |
260 |
NodeManager* nm = NodeManager::currentNM(); |
146 |
520 |
TypeNode typ = ctor.getSpecializedConstructorType(d_type); |
147 |
1300 |
b << nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, |
148 |
520 |
nm->mkConst(AscriptionType(typ)), |
149 |
1040 |
ctor.getConstructor()); |
150 |
|
} |
151 |
|
else |
152 |
|
{ |
153 |
60160 |
b << ctor.getConstructor(); |
154 |
|
} |
155 |
60420 |
Debug("dt-enum-debug") << "Get arguments..." << std::endl; |
156 |
60420 |
if (ctor.getNumArgs() > 0) |
157 |
|
{ |
158 |
56035 |
Assert(index < d_sel_types.size()); |
159 |
56035 |
Assert(index < d_sel_index.size()); |
160 |
56035 |
Assert(d_sel_types[index].size() == ctor.getNumArgs()); |
161 |
56035 |
Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1); |
162 |
106223 |
for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++) |
163 |
|
{ |
164 |
100376 |
Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]); |
165 |
50188 |
Assert(!c.isNull()); |
166 |
50188 |
b << c; |
167 |
|
} |
168 |
56035 |
b << lc; |
169 |
|
} |
170 |
120840 |
Node nnn = Node(b); |
171 |
60420 |
Debug("dt-enum-debug") << "Return... " << nnn << std::endl; |
172 |
60420 |
ret = nnn; |
173 |
|
} |
174 |
|
|
175 |
62220 |
if (!d_child_enum && d_has_debruijn) |
176 |
|
{ |
177 |
1095 |
Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret); |
178 |
765 |
if (nret != ret) |
179 |
|
{ |
180 |
435 |
if (nret.isNull()) |
181 |
|
{ |
182 |
353 |
Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl; |
183 |
|
} |
184 |
|
else |
185 |
|
{ |
186 |
82 |
Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl; |
187 |
82 |
Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl; |
188 |
|
} |
189 |
435 |
return Node::null(); |
190 |
|
} |
191 |
|
} |
192 |
|
|
193 |
61785 |
return ret; |
194 |
|
} |
195 |
|
|
196 |
85095 |
void DatatypesEnumerator::init() |
197 |
|
{ |
198 |
170190 |
Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() |
199 |
85095 |
<< std::endl; |
200 |
85095 |
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl; |
201 |
85095 |
Debug("dt-enum") << "datatype is " << d_type << std::endl; |
202 |
170190 |
Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " |
203 |
85095 |
<< d_datatype.isRecursiveSingleton(d_type); |
204 |
170190 |
Debug("dt-enum") << " " << d_datatype.getCardinalityClass(d_type) |
205 |
85095 |
<< 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 |
85095 |
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 |
85095 |
d_zeroTermActive = !d_zeroTerm.isNull(); |
220 |
85095 |
if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype)) |
221 |
|
{ |
222 |
|
// start with uninterpreted constant |
223 |
153 |
d_has_debruijn = 1; |
224 |
153 |
d_sel_types.push_back(std::vector<TypeNode>()); |
225 |
153 |
d_sel_index.push_back(std::vector<unsigned>()); |
226 |
153 |
d_sel_sum.push_back(-1); |
227 |
|
} |
228 |
|
else |
229 |
|
{ |
230 |
|
// find the "zero" term via mkGroundTerm |
231 |
84942 |
Debug("dt-enum-debug") << "make ground term..." << std::endl; |
232 |
84942 |
Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl; |
233 |
84942 |
Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR); |
234 |
84942 |
d_has_debruijn = 0; |
235 |
|
} |
236 |
85095 |
Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl; |
237 |
85095 |
d_ctor = 0; |
238 |
598523 |
for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i) |
239 |
|
{ |
240 |
513428 |
d_sel_types.push_back(std::vector<TypeNode>()); |
241 |
513428 |
d_sel_index.push_back(std::vector<unsigned>()); |
242 |
513428 |
d_sel_sum.push_back(-1); |
243 |
513428 |
const DTypeConstructor& ctor = d_datatype[i]; |
244 |
1026856 |
TypeNode typ; |
245 |
513428 |
if (d_datatype.isParametric()) |
246 |
|
{ |
247 |
148 |
typ = ctor.getSpecializedConstructorType(d_type); |
248 |
|
} |
249 |
1121138 |
for (unsigned a = 0; a < ctor.getNumArgs(); ++a) |
250 |
|
{ |
251 |
1215420 |
TypeNode tn; |
252 |
607710 |
if (d_datatype.isParametric()) |
253 |
|
{ |
254 |
177 |
tn = typ[a]; |
255 |
|
} |
256 |
|
else |
257 |
|
{ |
258 |
607533 |
tn = ctor[a].getSelector().getType()[1]; |
259 |
|
} |
260 |
607710 |
d_sel_types.back().push_back(tn); |
261 |
607710 |
d_sel_index.back().push_back(0); |
262 |
|
} |
263 |
513428 |
if (!d_sel_index.back().empty()) |
264 |
|
{ |
265 |
298400 |
d_sel_index.back().pop_back(); |
266 |
|
} |
267 |
|
} |
268 |
85095 |
d_size_limit = 0; |
269 |
85095 |
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 |
85095 |
AlwaysAssert(!isFinished()); |
279 |
85095 |
} |
280 |
|
|
281 |
16256 |
DatatypesEnumerator& DatatypesEnumerator::operator++() |
282 |
|
{ |
283 |
16256 |
Debug("dt-enum-debug") << ": increment " << this << std::endl; |
284 |
16256 |
if (d_zeroTermActive) |
285 |
|
{ |
286 |
2685 |
d_zeroTermActive = false; |
287 |
|
} |
288 |
16256 |
unsigned prevSize = d_size_limit; |
289 |
55120 |
while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) |
290 |
|
{ |
291 |
|
// increment at index |
292 |
41909 |
while (increment(d_ctor)) |
293 |
|
{ |
294 |
22477 |
Node n = getCurrentTerm(d_ctor); |
295 |
18879 |
if (!n.isNull()) |
296 |
|
{ |
297 |
17236 |
if (n == d_zeroTerm) |
298 |
|
{ |
299 |
1955 |
d_zeroTerm = Node::null(); |
300 |
|
} |
301 |
|
else |
302 |
|
{ |
303 |
15281 |
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 |
19432 |
d_ctor = d_ctor + 1; |
311 |
19432 |
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 |
16316 |
if (prevSize == d_size_limit |
316 |
999 |
|| (d_size_limit == 0 && d_datatype.isCodatatype()) |
317 |
17315 |
|| d_datatype.getCardinalityClass(d_type) |
318 |
|
== CardinalityClass::INFINITE) |
319 |
|
{ |
320 |
7591 |
d_size_limit++; |
321 |
7591 |
d_ctor = 0; |
322 |
25111 |
for (unsigned i = 0; i < d_sel_sum.size(); i++) |
323 |
|
{ |
324 |
17520 |
d_sel_sum[i] = -1; |
325 |
|
} |
326 |
|
} |
327 |
|
} |
328 |
|
} |
329 |
975 |
return *this; |
330 |
29286 |
} |