1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, 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 |
|
* A class representing a datatype definition. |
14 |
|
*/ |
15 |
|
#include "expr/dtype.h" |
16 |
|
|
17 |
|
#include <sstream> |
18 |
|
|
19 |
|
#include "expr/dtype_cons.h" |
20 |
|
#include "expr/node_algorithm.h" |
21 |
|
#include "expr/skolem_manager.h" |
22 |
|
#include "expr/type_matcher.h" |
23 |
|
|
24 |
|
using namespace cvc5::kind; |
25 |
|
|
26 |
|
namespace cvc5 { |
27 |
|
|
28 |
3895 |
DType::DType(std::string name, bool isCo) |
29 |
|
: d_name(name), |
30 |
|
d_params(), |
31 |
|
d_isCo(isCo), |
32 |
|
d_isTuple(false), |
33 |
|
d_isRecord(false), |
34 |
|
d_constructors(), |
35 |
|
d_resolved(false), |
36 |
|
d_self(), |
37 |
|
d_involvesExt(false), |
38 |
|
d_involvesUt(false), |
39 |
|
d_sygusAllowConst(false), |
40 |
|
d_sygusAllowAll(false), |
41 |
7790 |
d_card(CardinalityUnknown()), |
42 |
|
d_wellFounded(0), |
43 |
11685 |
d_nestedRecursion(0) |
44 |
|
{ |
45 |
3895 |
} |
46 |
|
|
47 |
1274 |
DType::DType(std::string name, const std::vector<TypeNode>& params, bool isCo) |
48 |
|
: d_name(name), |
49 |
|
d_params(params), |
50 |
|
d_isCo(isCo), |
51 |
|
d_isTuple(false), |
52 |
|
d_isRecord(false), |
53 |
|
d_constructors(), |
54 |
|
d_resolved(false), |
55 |
|
d_self(), |
56 |
|
d_involvesExt(false), |
57 |
|
d_involvesUt(false), |
58 |
|
d_sygusAllowConst(false), |
59 |
|
d_sygusAllowAll(false), |
60 |
2548 |
d_card(CardinalityUnknown()), |
61 |
|
d_wellFounded(0), |
62 |
3822 |
d_nestedRecursion(0) |
63 |
|
{ |
64 |
1274 |
} |
65 |
|
|
66 |
24653 |
DType::~DType() {} |
67 |
|
|
68 |
1256681 |
std::string DType::getName() const { return d_name; } |
69 |
9823570 |
size_t DType::getNumConstructors() const { return d_constructors.size(); } |
70 |
|
|
71 |
1591756 |
bool DType::isParametric() const { return d_params.size() > 0; } |
72 |
8243 |
size_t DType::getNumParameters() const { return d_params.size(); } |
73 |
3204 |
TypeNode DType::getParameter(size_t i) const |
74 |
|
{ |
75 |
3204 |
Assert(isParametric()); |
76 |
3204 |
Assert(i < d_params.size()); |
77 |
3204 |
return d_params[i]; |
78 |
|
} |
79 |
|
|
80 |
818 |
std::vector<TypeNode> DType::getParameters() const |
81 |
|
{ |
82 |
818 |
Assert(isParametric()); |
83 |
818 |
return d_params; |
84 |
|
} |
85 |
|
|
86 |
806164 |
bool DType::isCodatatype() const { return d_isCo; } |
87 |
|
|
88 |
2383765 |
bool DType::isSygus() const { return !d_sygusType.isNull(); } |
89 |
|
|
90 |
98259 |
bool DType::isTuple() const { return d_isTuple; } |
91 |
|
|
92 |
391 |
bool DType::isRecord() const { return d_isRecord; } |
93 |
|
|
94 |
888945 |
bool DType::isResolved() const { return d_resolved; } |
95 |
|
|
96 |
8019 |
const DType& DType::datatypeOf(Node item) |
97 |
|
{ |
98 |
16038 |
TypeNode t = item.getType(); |
99 |
8019 |
switch (t.getKind()) |
100 |
|
{ |
101 |
8019 |
case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType(); |
102 |
|
case SELECTOR_TYPE: |
103 |
|
case TESTER_TYPE: return t[0].getDType(); |
104 |
|
default: |
105 |
|
Unhandled() << "arg must be a datatype constructor, selector, or tester"; |
106 |
|
} |
107 |
|
} |
108 |
|
|
109 |
2781442 |
size_t DType::indexOf(Node item) |
110 |
|
{ |
111 |
2781442 |
Assert(item.getType().isConstructor() || item.getType().isTester() |
112 |
|
|| item.getType().isSelector() || item.getType().isUpdater()); |
113 |
2781442 |
return indexOfInternal(item); |
114 |
|
} |
115 |
|
|
116 |
2781442 |
size_t DType::indexOfInternal(Node item) |
117 |
|
{ |
118 |
2781442 |
if (item.getKind() == APPLY_TYPE_ASCRIPTION) |
119 |
|
{ |
120 |
5585 |
return indexOf(item[0]); |
121 |
|
} |
122 |
2775857 |
Assert(item.hasAttribute(DTypeIndexAttr())); |
123 |
2775857 |
return item.getAttribute(DTypeIndexAttr()); |
124 |
|
} |
125 |
|
|
126 |
3273 |
size_t DType::cindexOf(Node item) |
127 |
|
{ |
128 |
3273 |
Assert(item.getType().isSelector() || item.getType().isUpdater()); |
129 |
3273 |
return cindexOfInternal(item); |
130 |
|
} |
131 |
3273 |
size_t DType::cindexOfInternal(Node item) |
132 |
|
{ |
133 |
3273 |
if (item.getKind() == APPLY_TYPE_ASCRIPTION) |
134 |
|
{ |
135 |
|
return cindexOf(item[0]); |
136 |
|
} |
137 |
3273 |
Assert(item.hasAttribute(DTypeConsIndexAttr())); |
138 |
3273 |
return item.getAttribute(DTypeConsIndexAttr()); |
139 |
|
} |
140 |
|
|
141 |
5159 |
bool DType::resolve(const std::map<std::string, TypeNode>& resolutions, |
142 |
|
const std::vector<TypeNode>& placeholders, |
143 |
|
const std::vector<TypeNode>& replacements, |
144 |
|
const std::vector<TypeNode>& paramTypes, |
145 |
|
const std::vector<TypeNode>& paramReplacements) |
146 |
|
{ |
147 |
5159 |
Trace("datatypes-init") << "DType::resolve: " << std::endl; |
148 |
5159 |
Assert(!d_resolved); |
149 |
5159 |
Assert(resolutions.find(d_name) != resolutions.end()); |
150 |
5159 |
Assert(placeholders.size() == replacements.size()); |
151 |
5159 |
Assert(paramTypes.size() == paramReplacements.size()); |
152 |
5159 |
Assert(getNumConstructors() > 0); |
153 |
10318 |
TypeNode self = (*resolutions.find(d_name)).second; |
154 |
5159 |
Assert(&self.getDType() == this); |
155 |
5159 |
d_resolved = true; |
156 |
5159 |
size_t index = 0; |
157 |
20133 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
158 |
|
{ |
159 |
14974 |
Trace("datatypes-init") << "DType::resolve ctor " << std::endl; |
160 |
14974 |
if (!ctor->resolve(self, |
161 |
|
resolutions, |
162 |
|
placeholders, |
163 |
|
replacements, |
164 |
|
paramTypes, |
165 |
|
paramReplacements, |
166 |
|
index)) |
167 |
|
{ |
168 |
|
return false; |
169 |
|
} |
170 |
14974 |
ctor->d_constructor.setAttribute(DTypeIndexAttr(), index); |
171 |
14974 |
ctor->d_tester.setAttribute(DTypeIndexAttr(), index++); |
172 |
14974 |
Assert(ctor->isResolved()); |
173 |
14974 |
Trace("datatypes-init") << "DType::resolve ctor finished" << std::endl; |
174 |
|
} |
175 |
5159 |
d_self = self; |
176 |
|
|
177 |
5159 |
d_involvesExt = false; |
178 |
5159 |
d_involvesUt = false; |
179 |
20133 |
for (const std::shared_ptr<DTypeConstructor>& ctor : d_constructors) |
180 |
|
{ |
181 |
14974 |
if (ctor->involvesExternalType()) |
182 |
|
{ |
183 |
1434 |
d_involvesExt = true; |
184 |
|
} |
185 |
14974 |
if (ctor->involvesUninterpretedType()) |
186 |
|
{ |
187 |
7675 |
d_involvesUt = true; |
188 |
|
} |
189 |
|
} |
190 |
|
|
191 |
5159 |
if (isSygus()) |
192 |
|
{ |
193 |
|
// all datatype constructors should be sygus and have sygus operators whose |
194 |
|
// free variables are subsets of sygus bound var list. |
195 |
3572 |
std::unordered_set<Node> svs; |
196 |
4673 |
for (const Node& sv : d_sygusBvl) |
197 |
|
{ |
198 |
2887 |
svs.insert(sv); |
199 |
|
} |
200 |
12002 |
for (size_t i = 0, ncons = d_constructors.size(); i < ncons; i++) |
201 |
|
{ |
202 |
20432 |
Node sop = d_constructors[i]->getSygusOp(); |
203 |
10216 |
Assert(!sop.isNull()) |
204 |
|
<< "Sygus datatype contains a non-sygus constructor"; |
205 |
20432 |
std::unordered_set<Node> fvs; |
206 |
10216 |
expr::getFreeVariables(sop, fvs); |
207 |
11421 |
for (const Node& v : fvs) |
208 |
|
{ |
209 |
1205 |
if (svs.find(v) == svs.end()) |
210 |
|
{ |
211 |
|
// return false, indicating we should abort, since this datatype is |
212 |
|
// not well formed. |
213 |
|
return false; |
214 |
|
} |
215 |
|
} |
216 |
|
} |
217 |
|
} |
218 |
5159 |
Trace("datatypes-init") << "DType::resolve: finished" << std::endl; |
219 |
5159 |
return true; |
220 |
|
} |
221 |
|
|
222 |
14974 |
void DType::addConstructor(std::shared_ptr<DTypeConstructor> c) |
223 |
|
{ |
224 |
14974 |
Assert(!d_resolved); |
225 |
14974 |
d_constructors.push_back(c); |
226 |
14974 |
} |
227 |
|
|
228 |
10187 |
void DType::addSygusConstructor(Node op, |
229 |
|
const std::string& cname, |
230 |
|
const std::vector<TypeNode>& cargs, |
231 |
|
int weight) |
232 |
|
{ |
233 |
|
// avoid name clashes |
234 |
20374 |
std::stringstream ss; |
235 |
10187 |
ss << getName() << "_" << getNumConstructors() << "_" << cname; |
236 |
20374 |
std::string name = ss.str(); |
237 |
10187 |
unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1); |
238 |
|
std::shared_ptr<DTypeConstructor> c = |
239 |
20374 |
std::make_shared<DTypeConstructor>(name, cweight); |
240 |
10187 |
c->setSygus(op); |
241 |
21792 |
for (size_t j = 0, nargs = cargs.size(); j < nargs; j++) |
242 |
|
{ |
243 |
23210 |
std::stringstream sname; |
244 |
11605 |
sname << name << "_" << j; |
245 |
11605 |
c->addArg(sname.str(), cargs[j]); |
246 |
|
} |
247 |
10187 |
addConstructor(c); |
248 |
10187 |
} |
249 |
|
|
250 |
1786 |
void DType::setSygus(TypeNode st, Node bvl, bool allowConst, bool allowAll) |
251 |
|
{ |
252 |
1786 |
Assert(!d_resolved); |
253 |
|
// We can be in a case where the only rule specified was |
254 |
|
// (Constant T), in which case we have not yet added a constructor. We |
255 |
|
// ensure an arbitrary constant is added in this case. We additionally |
256 |
|
// add a constant if the grammar has only non-nullary constructors, since this |
257 |
|
// ensures the datatype is well-founded (see 3423). |
258 |
|
// Notice we only want to do this for sygus datatypes that are user-provided. |
259 |
|
// At the moment, the condition !allow_all implies the grammar is |
260 |
|
// user-provided and hence may require a default constant. |
261 |
|
// TODO (https://github.com/CVC4/cvc4-projects/issues/38): |
262 |
|
// In an API for SyGuS, it probably makes more sense for the user to |
263 |
|
// explicitly add the "any constant" constructor with a call instead of |
264 |
|
// passing a flag. This would make the block of code unnecessary. |
265 |
1786 |
if (allowConst && !allowAll) |
266 |
|
{ |
267 |
|
// if I don't already have a constant (0-ary constructor) |
268 |
35 |
bool hasConstant = false; |
269 |
59 |
for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++) |
270 |
|
{ |
271 |
30 |
if ((*this)[i].getNumArgs() == 0) |
272 |
|
{ |
273 |
6 |
hasConstant = true; |
274 |
6 |
break; |
275 |
|
} |
276 |
|
} |
277 |
35 |
if (!hasConstant) |
278 |
|
{ |
279 |
|
// add an arbitrary one |
280 |
58 |
Node op = st.mkGroundTerm(); |
281 |
|
// use same naming convention as SygusDatatype |
282 |
58 |
std::stringstream ss; |
283 |
29 |
ss << getName() << "_" << getNumConstructors() << "_" << op; |
284 |
|
// it has zero weight |
285 |
|
std::shared_ptr<DTypeConstructor> c = |
286 |
58 |
std::make_shared<DTypeConstructor>(ss.str(), 0); |
287 |
29 |
c->setSygus(op); |
288 |
29 |
addConstructor(c); |
289 |
|
} |
290 |
|
} |
291 |
|
|
292 |
1786 |
d_sygusType = st; |
293 |
1786 |
d_sygusBvl = bvl; |
294 |
1786 |
d_sygusAllowConst = allowConst || allowAll; |
295 |
1786 |
d_sygusAllowAll = allowAll; |
296 |
1786 |
} |
297 |
|
|
298 |
1930 |
void DType::setTuple() |
299 |
|
{ |
300 |
1930 |
Assert(!d_resolved); |
301 |
1930 |
d_isTuple = true; |
302 |
1930 |
} |
303 |
|
|
304 |
67 |
void DType::setRecord() |
305 |
|
{ |
306 |
67 |
Assert(!d_resolved); |
307 |
67 |
d_isRecord = true; |
308 |
67 |
} |
309 |
|
|
310 |
3144 |
Cardinality DType::getCardinality(TypeNode t) const |
311 |
|
{ |
312 |
3144 |
Trace("datatypes-init") << "DType::getCardinality " << std::endl; |
313 |
3144 |
Assert(isResolved()); |
314 |
3144 |
Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); |
315 |
6288 |
std::vector<TypeNode> processing; |
316 |
3144 |
computeCardinality(t, processing); |
317 |
6288 |
return d_card; |
318 |
|
} |
319 |
|
|
320 |
22 |
Cardinality DType::getCardinality() const |
321 |
|
{ |
322 |
22 |
Assert(!isParametric()); |
323 |
22 |
return getCardinality(d_self); |
324 |
|
} |
325 |
|
|
326 |
7614 |
Cardinality DType::computeCardinality(TypeNode t, |
327 |
|
std::vector<TypeNode>& processing) const |
328 |
|
{ |
329 |
7614 |
Trace("datatypes-init") << "DType::computeCardinality " << std::endl; |
330 |
7614 |
Assert(isResolved()); |
331 |
22842 |
if (std::find(processing.begin(), processing.end(), d_self) |
332 |
22842 |
!= processing.end()) |
333 |
|
{ |
334 |
263 |
d_card = Cardinality::INTEGERS; |
335 |
263 |
return d_card; |
336 |
|
} |
337 |
7351 |
processing.push_back(d_self); |
338 |
14702 |
Cardinality c = 0; |
339 |
21288 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
340 |
|
{ |
341 |
13937 |
c += ctor->computeCardinality(t, processing); |
342 |
|
} |
343 |
7351 |
d_card = c; |
344 |
7351 |
processing.pop_back(); |
345 |
7351 |
return d_card; |
346 |
|
} |
347 |
|
|
348 |
172472 |
bool DType::isRecursiveSingleton(TypeNode t) const |
349 |
|
{ |
350 |
172472 |
Trace("datatypes-init") << "DType::isRecursiveSingleton " << std::endl; |
351 |
172472 |
Assert(isResolved()); |
352 |
172472 |
Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); |
353 |
172472 |
if (d_cardRecSingleton.find(t) != d_cardRecSingleton.end()) |
354 |
|
{ |
355 |
171079 |
return d_cardRecSingleton[t] == 1; |
356 |
|
} |
357 |
1393 |
if (isCodatatype()) |
358 |
|
{ |
359 |
17 |
Assert(d_cardUAssume[t].empty()); |
360 |
34 |
std::vector<TypeNode> processing; |
361 |
17 |
if (computeCardinalityRecSingleton(t, processing, d_cardUAssume[t])) |
362 |
|
{ |
363 |
3 |
d_cardRecSingleton[t] = 1; |
364 |
3 |
if (Trace.isOn("dt-card")) |
365 |
|
{ |
366 |
|
Trace("dt-card") << "DType " << getName() |
367 |
|
<< " is recursive singleton, dependent upon " |
368 |
|
<< d_cardUAssume[t].size() |
369 |
|
<< " uninterpreted sorts: " << std::endl; |
370 |
|
for (size_t i = 0; i < d_cardUAssume[t].size(); i++) |
371 |
|
{ |
372 |
|
Trace("dt-card") << " " << d_cardUAssume[t][i] << std::endl; |
373 |
|
} |
374 |
|
Trace("dt-card") << std::endl; |
375 |
|
} |
376 |
|
} |
377 |
|
else |
378 |
|
{ |
379 |
14 |
d_cardRecSingleton[t] = -1; |
380 |
|
} |
381 |
|
} |
382 |
|
else |
383 |
|
{ |
384 |
1376 |
d_cardRecSingleton[t] = -1; |
385 |
|
} |
386 |
1393 |
return d_cardRecSingleton[t] == 1; |
387 |
|
} |
388 |
|
|
389 |
|
bool DType::isRecursiveSingleton() const |
390 |
|
{ |
391 |
|
Assert(!isParametric()); |
392 |
|
return isRecursiveSingleton(d_self); |
393 |
|
} |
394 |
|
|
395 |
4 |
unsigned DType::getNumRecursiveSingletonArgTypes(TypeNode t) const |
396 |
|
{ |
397 |
4 |
Assert(d_cardRecSingleton.find(t) != d_cardRecSingleton.end()); |
398 |
4 |
Assert(isRecursiveSingleton(t)); |
399 |
4 |
return d_cardUAssume[t].size(); |
400 |
|
} |
401 |
|
|
402 |
|
unsigned DType::getNumRecursiveSingletonArgTypes() const |
403 |
|
{ |
404 |
|
Assert(!isParametric()); |
405 |
|
return getNumRecursiveSingletonArgTypes(d_self); |
406 |
|
} |
407 |
|
|
408 |
|
TypeNode DType::getRecursiveSingletonArgType(TypeNode t, size_t i) const |
409 |
|
{ |
410 |
|
Assert(d_cardRecSingleton.find(t) != d_cardRecSingleton.end()); |
411 |
|
Assert(isRecursiveSingleton(t)); |
412 |
|
return d_cardUAssume[t][i]; |
413 |
|
} |
414 |
|
|
415 |
|
TypeNode DType::getRecursiveSingletonArgType(size_t i) const |
416 |
|
{ |
417 |
|
Assert(!isParametric()); |
418 |
|
return getRecursiveSingletonArgType(d_self, i); |
419 |
|
} |
420 |
|
|
421 |
22 |
bool DType::computeCardinalityRecSingleton( |
422 |
|
TypeNode t, |
423 |
|
std::vector<TypeNode>& processing, |
424 |
|
std::vector<TypeNode>& u_assume) const |
425 |
|
{ |
426 |
44 |
Trace("datatypes-init") << "DType::computeCardinalityRecSingleton " |
427 |
22 |
<< std::endl; |
428 |
66 |
if (std::find(processing.begin(), processing.end(), d_self) |
429 |
66 |
!= processing.end()) |
430 |
|
{ |
431 |
3 |
return true; |
432 |
|
} |
433 |
19 |
if (d_cardRecSingleton[t] == 0) |
434 |
|
{ |
435 |
|
// if not yet computed |
436 |
19 |
if (d_constructors.size() != 1) |
437 |
|
{ |
438 |
14 |
return false; |
439 |
|
} |
440 |
5 |
bool success = false; |
441 |
5 |
processing.push_back(d_self); |
442 |
8 |
for (size_t i = 0, nargs = d_constructors[0]->getNumArgs(); i < nargs; i++) |
443 |
|
{ |
444 |
8 |
TypeNode tc = d_constructors[0]->getArgType(i); |
445 |
|
// if it is an uninterpreted sort, then we depend on it having cardinality |
446 |
|
// one |
447 |
5 |
if (tc.isSort()) |
448 |
|
{ |
449 |
|
if (std::find(u_assume.begin(), u_assume.end(), tc) == u_assume.end()) |
450 |
|
{ |
451 |
|
u_assume.push_back(tc); |
452 |
|
} |
453 |
|
// if it is a datatype, recurse |
454 |
|
} |
455 |
5 |
else if (tc.isDatatype()) |
456 |
|
{ |
457 |
5 |
const DType& dt = tc.getDType(); |
458 |
5 |
if (!dt.computeCardinalityRecSingleton(t, processing, u_assume)) |
459 |
|
{ |
460 |
2 |
return false; |
461 |
|
} |
462 |
|
else |
463 |
|
{ |
464 |
3 |
success = true; |
465 |
|
} |
466 |
|
// if it is a builtin type, it must have cardinality one |
467 |
|
} |
468 |
|
else if (!tc.getCardinality().isOne()) |
469 |
|
{ |
470 |
|
return false; |
471 |
|
} |
472 |
|
} |
473 |
3 |
processing.pop_back(); |
474 |
3 |
return success; |
475 |
|
} |
476 |
|
else if (d_cardRecSingleton[t] == -1) |
477 |
|
{ |
478 |
|
return false; |
479 |
|
} |
480 |
|
for (size_t i = 0, csize = d_cardUAssume[t].size(); i < csize; i++) |
481 |
|
{ |
482 |
|
if (std::find(u_assume.begin(), u_assume.end(), d_cardUAssume[t][i]) |
483 |
|
== u_assume.end()) |
484 |
|
{ |
485 |
|
u_assume.push_back(d_cardUAssume[t][i]); |
486 |
|
} |
487 |
|
} |
488 |
|
return true; |
489 |
|
} |
490 |
|
|
491 |
135094 |
CardinalityClass DType::getCardinalityClass(TypeNode t) const |
492 |
|
{ |
493 |
135094 |
Trace("datatypes-init") << "DType::isFinite " << std::endl; |
494 |
135094 |
Assert(isResolved()); |
495 |
135094 |
Assert(t.isDatatype() && t.getDType().getTypeNode() == d_self); |
496 |
|
|
497 |
|
// is this already in the cache ? |
498 |
135094 |
std::map<TypeNode, CardinalityClass>::const_iterator it = d_cardClass.find(t); |
499 |
135094 |
if (it != d_cardClass.end()) |
500 |
|
{ |
501 |
132693 |
return it->second; |
502 |
|
} |
503 |
|
// it is the max cardinality class of a constructor, with base case ONE |
504 |
|
// if we have one constructor and FINITE otherwise. |
505 |
2401 |
CardinalityClass c = d_constructors.size() == 1 ? CardinalityClass::ONE |
506 |
2401 |
: CardinalityClass::FINITE; |
507 |
11377 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
508 |
|
{ |
509 |
8976 |
CardinalityClass cc = ctor->getCardinalityClass(t); |
510 |
8976 |
c = maxCardinalityClass(c, cc); |
511 |
|
} |
512 |
2401 |
d_cardClass[t] = c; |
513 |
2401 |
return c; |
514 |
|
} |
515 |
14 |
CardinalityClass DType::getCardinalityClass() const |
516 |
|
{ |
517 |
14 |
Assert(isResolved() && !isParametric()); |
518 |
14 |
return getCardinalityClass(d_self); |
519 |
|
} |
520 |
|
|
521 |
22 |
bool DType::isFinite(TypeNode t, bool fmfEnabled) const |
522 |
|
{ |
523 |
22 |
return isCardinalityClassFinite(getCardinalityClass(t), fmfEnabled); |
524 |
|
} |
525 |
|
|
526 |
22 |
bool DType::isFinite(bool fmfEnabled) const |
527 |
|
{ |
528 |
22 |
return isFinite(d_self, fmfEnabled); |
529 |
|
} |
530 |
|
|
531 |
53863 |
bool DType::isWellFounded() const |
532 |
|
{ |
533 |
53863 |
Assert(isResolved()); |
534 |
53863 |
if (d_wellFounded != 0) |
535 |
|
{ |
536 |
|
// already computed |
537 |
50863 |
return d_wellFounded == 1; |
538 |
|
} |
539 |
3000 |
Trace("datatypes-init") << "DType::isWellFounded " << getName() << std::endl; |
540 |
6000 |
std::vector<TypeNode> processing; |
541 |
3000 |
if (!computeWellFounded(processing)) |
542 |
|
{ |
543 |
|
// not well-founded since no ground term can be constructed |
544 |
4 |
Trace("datatypes-init") << "DType::isWellFounded: false for " << getName() |
545 |
2 |
<< " due to no ground terms." << std::endl; |
546 |
2 |
d_wellFounded = -1; |
547 |
2 |
return false; |
548 |
|
} |
549 |
5996 |
Trace("datatypes-init") << "DType::isWellFounded: true for " << getName() |
550 |
2998 |
<< std::endl; |
551 |
2998 |
d_wellFounded = 1; |
552 |
2998 |
return true; |
553 |
|
} |
554 |
|
|
555 |
6025 |
bool DType::computeWellFounded(std::vector<TypeNode>& processing) const |
556 |
|
{ |
557 |
6025 |
Trace("datatypes-init") << "DType::computeWellFounded " << std::endl; |
558 |
6025 |
Assert(isResolved()); |
559 |
18075 |
if (std::find(processing.begin(), processing.end(), d_self) |
560 |
18075 |
!= processing.end()) |
561 |
|
{ |
562 |
1053 |
return d_isCo; |
563 |
|
} |
564 |
4972 |
processing.push_back(d_self); |
565 |
6071 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
566 |
|
{ |
567 |
6005 |
if (ctor->computeWellFounded(processing)) |
568 |
|
{ |
569 |
4906 |
processing.pop_back(); |
570 |
4906 |
return true; |
571 |
|
} |
572 |
|
else |
573 |
|
{ |
574 |
2198 |
Trace("dt-wf") << "Constructor " << ctor->getName() |
575 |
1099 |
<< " is not well-founded." << std::endl; |
576 |
|
} |
577 |
|
} |
578 |
66 |
processing.pop_back(); |
579 |
132 |
Trace("dt-wf") << "DType " << getName() << " is not well-founded." |
580 |
66 |
<< std::endl; |
581 |
66 |
return false; |
582 |
|
} |
583 |
|
|
584 |
88694 |
Node DType::mkGroundTerm(TypeNode t) const |
585 |
|
{ |
586 |
88694 |
Trace("datatypes-init") << "DType::mkGroundTerm of type " << t << std::endl; |
587 |
88694 |
Assert(isResolved()); |
588 |
88694 |
return mkGroundTermInternal(t, false); |
589 |
|
} |
590 |
|
|
591 |
95643 |
Node DType::mkGroundValue(TypeNode t) const |
592 |
|
{ |
593 |
95643 |
Assert(isResolved()); |
594 |
95643 |
Trace("datatypes-init") << "DType::mkGroundValue of type " << t << std::endl; |
595 |
95643 |
Node v = mkGroundTermInternal(t, true); |
596 |
95643 |
return v; |
597 |
|
} |
598 |
|
|
599 |
184337 |
Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const |
600 |
|
{ |
601 |
368674 |
Trace("datatypes-init") << "DType::mkGroundTerm of type " << t |
602 |
184337 |
<< ", isValue = " << isValue << std::endl; |
603 |
|
// is this already in the cache ? |
604 |
184337 |
std::map<TypeNode, Node>& cache = isValue ? d_groundValue : d_groundTerm; |
605 |
184337 |
std::map<TypeNode, Node>::iterator it = cache.find(t); |
606 |
184337 |
if (it != cache.end()) |
607 |
|
{ |
608 |
366200 |
Trace("datatypes-init") |
609 |
183100 |
<< "\nin cache: " << d_self << " => " << it->second << std::endl; |
610 |
183100 |
return it->second; |
611 |
|
} |
612 |
2474 |
std::vector<TypeNode> processing; |
613 |
2474 |
Node groundTerm = computeGroundTerm(t, processing, isValue); |
614 |
1237 |
if (!groundTerm.isNull()) |
615 |
|
{ |
616 |
|
// we found a ground-term-constructing constructor! |
617 |
1227 |
cache[t] = groundTerm; |
618 |
2454 |
Trace("datatypes-init") |
619 |
1227 |
<< "constructed: " << getName() << " => " << groundTerm << std::endl; |
620 |
|
} |
621 |
|
// if ground term is null, we are not well-founded |
622 |
2474 |
Trace("datatypes-init") << "DType::mkGroundTerm for " << t |
623 |
1237 |
<< ", isValue=" << isValue << " returns " |
624 |
1237 |
<< groundTerm << std::endl; |
625 |
1237 |
return groundTerm; |
626 |
|
} |
627 |
|
|
628 |
11812 |
void DType::getAlienSubfieldTypes(std::unordered_set<TypeNode>& types, |
629 |
|
std::map<TypeNode, bool>& processed, |
630 |
|
bool isAlienPos) const |
631 |
|
{ |
632 |
11812 |
std::map<TypeNode, bool>::iterator it = processed.find(d_self); |
633 |
11812 |
if (it != processed.end()) |
634 |
|
{ |
635 |
8839 |
if (it->second || (!isAlienPos && !it->second)) |
636 |
|
{ |
637 |
|
// already processed as an alien subfield type, or already processed |
638 |
|
// as a non-alien subfield type and isAlienPos is false. |
639 |
8821 |
return; |
640 |
|
} |
641 |
|
} |
642 |
2991 |
processed[d_self] = isAlienPos; |
643 |
13782 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
644 |
|
{ |
645 |
22694 |
for (unsigned j = 0, nargs = ctor->getNumArgs(); j < nargs; ++j) |
646 |
|
{ |
647 |
23767 |
TypeNode tn = ctor->getArgType(j); |
648 |
11903 |
if (tn.isDatatype()) |
649 |
|
{ |
650 |
|
// special case for datatypes, we must recurse to collect subfield types |
651 |
9947 |
if (!isAlienPos) |
652 |
|
{ |
653 |
|
// since we aren't adding it to types below, we add its alien |
654 |
|
// subfield types here. |
655 |
9917 |
const DType& dt = tn.getDType(); |
656 |
9917 |
dt.getAlienSubfieldTypes(types, processed, false); |
657 |
|
} |
658 |
9947 |
if (tn.isParametricDatatype() && !isAlienPos) |
659 |
|
{ |
660 |
|
// (instantiated) parametric datatypes have an AST structure: |
661 |
|
// (PARAMETRIC_DATATYPE D T1 ... Tn) |
662 |
|
// where D is the uninstantiated datatype type. We should not view D |
663 |
|
// as an alien subfield type of tn. Thus, we need a special case here |
664 |
|
// which ignores the first child, when isAlienPos is false. |
665 |
80 |
for (unsigned i = 1, nchild = tn.getNumChildren(); i < nchild; i++) |
666 |
|
{ |
667 |
41 |
expr::getComponentTypes(tn[i], types); |
668 |
|
} |
669 |
39 |
continue; |
670 |
|
} |
671 |
|
} |
672 |
|
// we are in a case where tn is not a datatype, we add all (alien) |
673 |
|
// component types to types below. |
674 |
11864 |
bool hasTn = types.find(tn) != types.end(); |
675 |
23728 |
Trace("datatypes-init") |
676 |
11864 |
<< "Collect subfield types " << tn << ", hasTn=" << hasTn |
677 |
11864 |
<< ", isAlienPos=" << isAlienPos << std::endl; |
678 |
11864 |
expr::getComponentTypes(tn, types); |
679 |
11864 |
if (!isAlienPos && !hasTn) |
680 |
|
{ |
681 |
|
// the top-level type is added by getComponentTypes, so remove it if it |
682 |
|
// was not already listed in types |
683 |
11791 |
Assert(types.find(tn) != types.end()); |
684 |
11791 |
types.erase(tn); |
685 |
|
} |
686 |
|
} |
687 |
|
} |
688 |
|
// Now, go back and add all alien subfield types from datatypes if |
689 |
|
// not done so already. This is because getComponentTypes does not |
690 |
|
// recurse into subfield types of datatypes. |
691 |
3271 |
for (const TypeNode& sstn : types) |
692 |
|
{ |
693 |
280 |
if (sstn.isDatatype()) |
694 |
|
{ |
695 |
162 |
const DType& dt = sstn.getDType(); |
696 |
162 |
dt.getAlienSubfieldTypes(types, processed, true); |
697 |
|
} |
698 |
|
} |
699 |
|
} |
700 |
|
|
701 |
52384 |
bool DType::hasNestedRecursion() const |
702 |
|
{ |
703 |
52384 |
if (d_nestedRecursion != 0) |
704 |
|
{ |
705 |
50651 |
return d_nestedRecursion == 1; |
706 |
|
} |
707 |
3466 |
Trace("datatypes-init") << "Compute simply recursive for " << getName() |
708 |
1733 |
<< std::endl; |
709 |
|
// get the alien subfield types of this datatype |
710 |
3466 |
std::unordered_set<TypeNode> types; |
711 |
3466 |
std::map<TypeNode, bool> processed; |
712 |
1733 |
getAlienSubfieldTypes(types, processed, false); |
713 |
1733 |
if (Trace.isOn("datatypes-init")) |
714 |
|
{ |
715 |
|
Trace("datatypes-init") << "Alien subfield types: " << std::endl; |
716 |
|
for (const TypeNode& t : types) |
717 |
|
{ |
718 |
|
Trace("datatypes-init") << "- " << t << std::endl; |
719 |
|
} |
720 |
|
} |
721 |
|
// does types contain self? |
722 |
1733 |
if (types.find(d_self) != types.end()) |
723 |
|
{ |
724 |
26 |
Trace("datatypes-init") |
725 |
26 |
<< "DType::hasNestedRecursion: true for " << getName() |
726 |
13 |
<< " due to alien subfield type" << std::endl; |
727 |
|
// has nested recursion since it has itself as an alien subfield type. |
728 |
13 |
d_nestedRecursion = 1; |
729 |
13 |
return true; |
730 |
|
} |
731 |
|
// If it is parametric, this type may match with an alien subfield type (e.g. |
732 |
|
// we may have a field (T Int) for parametric datatype (T x) where x |
733 |
|
// is a type parameter). Thus, we check whether the self type matches any |
734 |
|
// alien subfield type using the TypeMatcher utility. |
735 |
1720 |
if (isParametric()) |
736 |
|
{ |
737 |
63 |
for (const TypeNode& t : types) |
738 |
|
{ |
739 |
62 |
TypeMatcher m(d_self); |
740 |
31 |
Trace("datatypes-init") << " " << t << std::endl; |
741 |
31 |
if (m.doMatching(d_self, t)) |
742 |
|
{ |
743 |
|
Trace("datatypes-init") |
744 |
|
<< "DType::hasNestedRecursion: true for " << getName() |
745 |
|
<< " due to parametric strict component type, " << d_self |
746 |
|
<< " matching " << t << std::endl; |
747 |
|
d_nestedRecursion = 1; |
748 |
|
return true; |
749 |
|
} |
750 |
|
} |
751 |
|
} |
752 |
3440 |
Trace("datatypes-init") << "DType::hasNestedRecursion: false for " |
753 |
1720 |
<< getName() << std::endl; |
754 |
1720 |
d_nestedRecursion = -1; |
755 |
1720 |
return false; |
756 |
|
} |
757 |
|
|
758 |
2800 |
Node getSubtermWithType(Node e, TypeNode t, bool isTop) |
759 |
|
{ |
760 |
2800 |
if (!isTop && e.getType() == t) |
761 |
|
{ |
762 |
2 |
return e; |
763 |
|
} |
764 |
3867 |
for (const Node& ei : e) |
765 |
|
{ |
766 |
2141 |
Node se = getSubtermWithType(ei, t, false); |
767 |
1072 |
if (!se.isNull()) |
768 |
|
{ |
769 |
3 |
return se; |
770 |
|
} |
771 |
|
} |
772 |
2795 |
return Node(); |
773 |
|
} |
774 |
|
|
775 |
1830 |
Node DType::computeGroundTerm(TypeNode t, |
776 |
|
std::vector<TypeNode>& processing, |
777 |
|
bool isValue) const |
778 |
|
{ |
779 |
1830 |
if (std::find(processing.begin(), processing.end(), t) != processing.end()) |
780 |
|
{ |
781 |
180 |
Trace("datatypes-init") |
782 |
90 |
<< "...already processing " << t << " " << d_self << std::endl; |
783 |
90 |
return Node(); |
784 |
|
} |
785 |
1740 |
processing.push_back(t); |
786 |
1740 |
std::map<TypeNode, Node>& gtCache = isValue ? d_groundValue : d_groundTerm; |
787 |
2133 |
for (unsigned r = 0; r < 2; r++) |
788 |
|
{ |
789 |
2213 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
790 |
|
{ |
791 |
|
// do nullary constructors first |
792 |
3042 |
if ((ctor->getNumArgs() == 0) != (r == 0)) |
793 |
|
{ |
794 |
1222 |
continue; |
795 |
|
} |
796 |
3640 |
Trace("datatypes-init") << "Try constructing for " << ctor->getName() |
797 |
3640 |
<< ", processing = " << processing.size() |
798 |
1820 |
<< ", isValue=" << isValue << std::endl; |
799 |
1912 |
Node e = ctor->computeGroundTerm(t, processing, gtCache, isValue); |
800 |
1820 |
if (!e.isNull()) |
801 |
|
{ |
802 |
|
// must check subterms for the same type to avoid infinite loops in |
803 |
|
// type enumeration |
804 |
3456 |
Node se = getSubtermWithType(e, t, true); |
805 |
1728 |
if (!se.isNull()) |
806 |
|
{ |
807 |
2 |
Trace("datatypes-init") << "Take subterm " << se << std::endl; |
808 |
2 |
e = se; |
809 |
|
} |
810 |
1728 |
processing.pop_back(); |
811 |
1728 |
return e; |
812 |
|
} |
813 |
|
else |
814 |
|
{ |
815 |
92 |
Trace("datatypes-init") << "...failed." << std::endl; |
816 |
|
} |
817 |
|
} |
818 |
|
} |
819 |
12 |
processing.pop_back(); |
820 |
12 |
return Node(); |
821 |
|
} |
822 |
|
|
823 |
312456 |
TypeNode DType::getTypeNode() const |
824 |
|
{ |
825 |
312456 |
Assert(isResolved()); |
826 |
312456 |
Assert(!d_self.isNull()); |
827 |
312456 |
return d_self; |
828 |
|
} |
829 |
|
|
830 |
8 |
TypeNode DType::getTypeNode(const std::vector<TypeNode>& params) const |
831 |
|
{ |
832 |
8 |
Assert(isResolved()); |
833 |
8 |
Assert(!d_self.isNull() && d_self.isParametricDatatype()); |
834 |
8 |
return d_self.instantiateParametricDatatype(params); |
835 |
|
} |
836 |
|
|
837 |
6245616 |
const DTypeConstructor& DType::operator[](size_t index) const |
838 |
|
{ |
839 |
6245616 |
Assert(index < getNumConstructors()); |
840 |
6245616 |
return *d_constructors[index]; |
841 |
|
} |
842 |
|
|
843 |
2663 |
Node DType::getSharedSelector(TypeNode dtt, TypeNode t, size_t index) const |
844 |
|
{ |
845 |
2663 |
Assert(isResolved()); |
846 |
|
std::map<TypeNode, std::map<TypeNode, std::map<unsigned, Node> > >::iterator |
847 |
2663 |
itd = d_sharedSel.find(dtt); |
848 |
2663 |
if (itd != d_sharedSel.end()) |
849 |
|
{ |
850 |
|
std::map<TypeNode, std::map<unsigned, Node> >::iterator its = |
851 |
1843 |
itd->second.find(t); |
852 |
1843 |
if (its != itd->second.end()) |
853 |
|
{ |
854 |
1323 |
std::map<unsigned, Node>::iterator it = its->second.find(index); |
855 |
1323 |
if (it != its->second.end()) |
856 |
|
{ |
857 |
802 |
return it->second; |
858 |
|
} |
859 |
|
} |
860 |
|
} |
861 |
|
// make the shared selector |
862 |
3722 |
Node s; |
863 |
1861 |
NodeManager* nm = NodeManager::currentNM(); |
864 |
3722 |
std::stringstream ss; |
865 |
1861 |
ss << "sel_" << index; |
866 |
1861 |
SkolemManager* sm = nm->getSkolemManager(); |
867 |
5583 |
s = sm->mkDummySkolem(ss.str(), |
868 |
3722 |
nm->mkSelectorType(dtt, t), |
869 |
|
"is a shared selector", |
870 |
|
NodeManager::SKOLEM_NO_NOTIFY); |
871 |
1861 |
d_sharedSel[dtt][t][index] = s; |
872 |
3722 |
Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t |
873 |
1861 |
<< std::endl; |
874 |
1861 |
return s; |
875 |
|
} |
876 |
|
|
877 |
823689 |
TypeNode DType::getSygusType() const { return d_sygusType; } |
878 |
|
|
879 |
157121 |
Node DType::getSygusVarList() const { return d_sygusBvl; } |
880 |
|
|
881 |
1300 |
bool DType::getSygusAllowConst() const { return d_sygusAllowConst; } |
882 |
|
|
883 |
1155 |
bool DType::getSygusAllowAll() const { return d_sygusAllowAll; } |
884 |
|
|
885 |
|
bool DType::involvesExternalType() const { return d_involvesExt; } |
886 |
|
|
887 |
21028 |
bool DType::involvesUninterpretedType() const { return d_involvesUt; } |
888 |
|
|
889 |
10 |
const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors() |
890 |
|
const |
891 |
|
{ |
892 |
10 |
return d_constructors; |
893 |
|
} |
894 |
|
|
895 |
20 |
std::ostream& operator<<(std::ostream& os, const DType& dt) |
896 |
|
{ |
897 |
|
// can only output datatypes in the cvc5 native language |
898 |
40 |
language::SetLanguage::Scope ls(os, language::output::LANG_CVC); |
899 |
20 |
dt.toStream(os); |
900 |
40 |
return os; |
901 |
|
} |
902 |
|
|
903 |
20 |
void DType::toStream(std::ostream& out) const |
904 |
|
{ |
905 |
20 |
out << "DATATYPE " << getName(); |
906 |
20 |
if (isParametric()) |
907 |
|
{ |
908 |
|
out << '['; |
909 |
|
for (size_t i = 0, nparams = getNumParameters(); i < nparams; ++i) |
910 |
|
{ |
911 |
|
if (i > 0) |
912 |
|
{ |
913 |
|
out << ','; |
914 |
|
} |
915 |
|
out << getParameter(i); |
916 |
|
} |
917 |
|
out << ']'; |
918 |
|
} |
919 |
20 |
out << " = " << std::endl; |
920 |
20 |
bool firstTime = true; |
921 |
58 |
for (std::shared_ptr<DTypeConstructor> ctor : d_constructors) |
922 |
|
{ |
923 |
38 |
if (!firstTime) |
924 |
|
{ |
925 |
20 |
out << " | "; |
926 |
|
} |
927 |
38 |
firstTime = false; |
928 |
38 |
out << *ctor; |
929 |
|
} |
930 |
20 |
out << " END;" << std::endl; |
931 |
20 |
} |
932 |
|
|
933 |
|
DTypeIndexConstant::DTypeIndexConstant(size_t index) : d_index(index) {} |
934 |
|
std::ostream& operator<<(std::ostream& out, const DTypeIndexConstant& dic) |
935 |
|
{ |
936 |
|
return out << "index_" << dic.getIndex(); |
937 |
|
} |
938 |
|
|
939 |
27735 |
} // namespace cvc5 |