GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/dtype.cpp Lines: 423 484 87.4 %
Date: 2021-03-23 Branches: 732 2066 35.4 %

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