GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/dtype_cons.cpp Lines: 311 338 92.0 %
Date: 2021-03-22 Branches: 493 1332 37.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dtype_cons.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_cons.h"
15
16
#include "expr/dtype.h"
17
#include "expr/node_manager.h"
18
#include "expr/type_matcher.h"
19
#include "options/datatypes_options.h"
20
21
using namespace CVC4::kind;
22
using namespace CVC4::theory;
23
24
namespace CVC4 {
25
26
19298
DTypeConstructor::DTypeConstructor(std::string name,
27
19298
                                   unsigned weight)
28
    :  // We don't want to introduce a new data member, because eventually
29
       // we're going to be a constant stuffed inside a node.  So we stow
30
       // the tester name away inside the constructor name until
31
       // resolution.
32
      d_name(name),
33
      d_tester(),
34
      d_args(),
35
19298
      d_weight(weight)
36
{
37
19298
  Assert(name != "");
38
19298
}
39
40
19965
void DTypeConstructor::addArg(std::string selectorName, TypeNode selectorType)
41
{
42
  // We don't want to introduce a new data member, because eventually
43
  // we're going to be a constant stuffed inside a node.  So we stow
44
  // the selector type away inside a var until resolution (when we can
45
  // create the proper selector type)
46
19965
  Assert(!isResolved());
47
19965
  Assert(!selectorType.isNull());
48
49
  Node type = NodeManager::currentNM()->mkSkolem(
50
39930
      "unresolved_" + selectorName,
51
      selectorType,
52
      "is an unresolved selector type placeholder",
53
79860
      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
54
19965
  Trace("datatypes") << "DTypeConstructor::addArg: " << type << std::endl;
55
  std::shared_ptr<DTypeSelector> a =
56
39930
      std::make_shared<DTypeSelector>(selectorName, type);
57
19965
  addArg(a);
58
19965
}
59
60
20029
void DTypeConstructor::addArg(std::shared_ptr<DTypeSelector> a)
61
{
62
20029
  d_args.push_back(a);
63
20029
}
64
65
64
void DTypeConstructor::addArgSelf(std::string selectorName)
66
{
67
64
  Trace("datatypes") << "DTypeConstructor::addArgSelf" << std::endl;
68
  std::shared_ptr<DTypeSelector> a =
69
128
      std::make_shared<DTypeSelector>(selectorName + '\0', Node::null());
70
64
  addArg(a);
71
64
}
72
73
44343
const std::string& DTypeConstructor::getName() const { return d_name; }
74
75
614999
Node DTypeConstructor::getConstructor() const
76
{
77
614999
  Assert(isResolved());
78
614999
  return d_constructor;
79
}
80
81
343968
Node DTypeConstructor::getTester() const
82
{
83
343968
  Assert(isResolved());
84
343968
  return d_tester;
85
}
86
87
14935
void DTypeConstructor::setSygus(Node op)
88
{
89
14935
  Assert(!isResolved());
90
14935
  d_sygusOp = op;
91
14935
}
92
93
2156860
Node DTypeConstructor::getSygusOp() const
94
{
95
2156860
  Assert(isResolved());
96
2156860
  return d_sygusOp;
97
}
98
99
1273
bool DTypeConstructor::isSygusIdFunc() const
100
{
101
1273
  Assert(isResolved());
102
3089
  return (d_sygusOp.getKind() == LAMBDA && d_sygusOp[0].getNumChildren() == 1
103
4003
          && d_sygusOp[0][0] == d_sygusOp[1]);
104
}
105
106
367035
unsigned DTypeConstructor::getWeight() const
107
{
108
367035
  Assert(isResolved());
109
367035
  return d_weight;
110
}
111
112
11022667
size_t DTypeConstructor::getNumArgs() const { return d_args.size(); }
113
114
691
TypeNode DTypeConstructor::getSpecializedConstructorType(
115
    TypeNode returnType) const
116
{
117
691
  Assert(isResolved());
118
691
  Assert(returnType.isDatatype())
119
      << "DTypeConstructor::getSpecializedConstructorType: expected datatype, "
120
         "got "
121
      << returnType;
122
691
  const DType& dt = DType::datatypeOf(d_constructor);
123
691
  Assert(dt.isParametric());
124
1382
  TypeNode dtt = dt.getTypeNode();
125
1382
  TypeMatcher m(dtt);
126
691
  m.doMatching(dtt, returnType);
127
1382
  std::vector<TypeNode> subst;
128
691
  m.getMatches(subst);
129
1382
  std::vector<TypeNode> params = dt.getParameters();
130
1382
  return d_constructor.getType().substitute(
131
1382
      params.begin(), params.end(), subst.begin(), subst.end());
132
}
133
134
3390
const std::vector<std::shared_ptr<DTypeSelector> >& DTypeConstructor::getArgs()
135
    const
136
{
137
3390
  return d_args;
138
}
139
140
Cardinality DTypeConstructor::getCardinality(TypeNode t) const
141
{
142
  Assert(isResolved());
143
144
  Cardinality c = 1;
145
146
  for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
147
  {
148
    c *= getArgType(i).getCardinality();
149
  }
150
151
  return c;
152
}
153
154
5002
bool DTypeConstructor::isFinite(TypeNode t) const
155
{
156
5002
  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
157
5002
  return cinfo.first == CardinalityType::FINITE;
158
}
159
160
176632
bool DTypeConstructor::isInterpretedFinite(TypeNode t) const
161
{
162
176632
  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
163
176632
  return cinfo.first != CardinalityType::INFINITE;
164
}
165
166
148162
bool DTypeConstructor::hasFiniteExternalArgType(TypeNode t) const
167
{
168
148162
  std::pair<CardinalityType, bool> cinfo = computeCardinalityInfo(t);
169
148162
  return cinfo.second;
170
}
171
172
std::pair<DTypeConstructor::CardinalityType, bool>
173
329796
DTypeConstructor::computeCardinalityInfo(TypeNode t) const
174
{
175
  std::map<TypeNode, std::pair<CardinalityType, bool> >::iterator it =
176
329796
      d_cardInfo.find(t);
177
329796
  if (it != d_cardInfo.end())
178
  {
179
322741
    return it->second;
180
  }
181
7055
  std::pair<CardinalityType, bool> ret(CardinalityType::FINITE, false);
182
14110
  std::vector<TypeNode> instTypes;
183
14110
  std::vector<TypeNode> paramTypes;
184
7055
  bool isParam = t.isParametricDatatype();
185
7055
  if (isParam)
186
  {
187
74
    paramTypes = t.getDType().getParameters();
188
74
    instTypes = t.getParamTypes();
189
  }
190
14325
  for (unsigned i = 0, nargs = getNumArgs(); i < nargs; i++)
191
  {
192
8128
    TypeNode tc = getArgType(i);
193
7270
    if (isParam)
194
    {
195
104
      tc = tc.substitute(paramTypes.begin(),
196
                         paramTypes.end(),
197
                         instTypes.begin(),
198
                         instTypes.end());
199
    }
200
7270
    if (tc.isFinite())
201
    {
202
      // do nothing
203
    }
204
12925
    else if (tc.isInterpretedFinite())
205
    {
206
101
      if (ret.first == CardinalityType::FINITE)
207
      {
208
        // not simply finite, it depends on uninterpreted sorts being finite
209
69
        ret.first = CardinalityType::INTERPRETED_FINITE;
210
      }
211
    }
212
    else
213
    {
214
      // infinite implies the constructor is infinite cardinality
215
6412
      ret.first = CardinalityType::INFINITE;
216
6412
      continue;
217
    }
218
    // if the argument is (interpreted) finite and external, set the flag
219
    // for indicating it has a finite external argument
220
858
    ret.second = ret.second || !tc.isDatatype();
221
  }
222
7055
  d_cardInfo[t] = ret;
223
7055
  return ret;
224
}
225
226
4542005
bool DTypeConstructor::isResolved() const { return !d_tester.isNull(); }
227
228
2215098
const DTypeSelector& DTypeConstructor::operator[](size_t index) const
229
{
230
2215098
  Assert(index < getNumArgs());
231
2215098
  return *d_args[index];
232
}
233
234
861005
TypeNode DTypeConstructor::getArgType(size_t index) const
235
{
236
861005
  Assert(index < getNumArgs());
237
861005
  return (*this)[index].getType().getSelectorRangeType();
238
}
239
240
514304
Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
241
                                           size_t index) const
242
{
243
514304
  Assert(isResolved());
244
514304
  Assert(index < getNumArgs());
245
514304
  if (options::dtSharedSelectors())
246
  {
247
514304
    computeSharedSelectors(domainType);
248
514304
    Assert(d_sharedSelectors[domainType].size() == getNumArgs());
249
514304
    return d_sharedSelectors[domainType][index];
250
  }
251
  else
252
  {
253
    return d_args[index]->getSelector();
254
  }
255
}
256
257
425021
int DTypeConstructor::getSelectorIndexInternal(Node sel) const
258
{
259
425021
  Assert(isResolved());
260
425021
  if (options::dtSharedSelectors())
261
  {
262
425021
    Assert(sel.getType().isSelector());
263
648307
    TypeNode domainType = sel.getType().getSelectorDomainType();
264
425021
    computeSharedSelectors(domainType);
265
    std::map<Node, unsigned>::iterator its =
266
425021
        d_sharedSelectorIndex[domainType].find(sel);
267
425021
    if (its != d_sharedSelectorIndex[domainType].end())
268
    {
269
201735
      return (int)its->second;
270
    }
271
  }
272
  else
273
  {
274
    unsigned sindex = DType::indexOf(sel);
275
    if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel)
276
    {
277
      return static_cast<int>(sindex);
278
    }
279
  }
280
223286
  return -1;
281
}
282
283
13
int DTypeConstructor::getSelectorIndexForName(const std::string& name) const
284
{
285
13
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
286
  {
287
13
    if (d_args[i]->getName() == name)
288
    {
289
13
      return i;
290
    }
291
  }
292
  return -1;
293
}
294
295
19296
bool DTypeConstructor::involvesExternalType() const
296
{
297
36786
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
298
  {
299
18888
    if (!getArgType(i).isDatatype())
300
    {
301
1398
      return true;
302
    }
303
  }
304
17898
  return false;
305
}
306
307
19296
bool DTypeConstructor::involvesUninterpretedType() const
308
{
309
19816
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
310
  {
311
10596
    if (!getArgType(i).isSort())
312
    {
313
10076
      return true;
314
    }
315
  }
316
9220
  return false;
317
}
318
319
13940
Cardinality DTypeConstructor::computeCardinality(
320
    TypeNode t, std::vector<TypeNode>& processing) const
321
{
322
13940
  Cardinality c = 1;
323
27880
  std::vector<TypeNode> instTypes;
324
27880
  std::vector<TypeNode> paramTypes;
325
13940
  bool isParam = t.isParametricDatatype();
326
13940
  if (isParam)
327
  {
328
    paramTypes = t.getDType().getParameters();
329
    instTypes = t.getParamTypes();
330
  }
331
19096
  for (size_t i = 0, nargs = d_args.size(); i < nargs; i++)
332
  {
333
10312
    TypeNode tc = getArgType(i);
334
5156
    if (isParam)
335
    {
336
      tc = tc.substitute(paramTypes.begin(),
337
                         paramTypes.end(),
338
                         instTypes.begin(),
339
                         instTypes.end());
340
    }
341
5156
    if (tc.isDatatype())
342
    {
343
4470
      const DType& dt = tc.getDType();
344
4470
      c *= dt.computeCardinality(t, processing);
345
    }
346
    else
347
    {
348
686
      c *= tc.getCardinality();
349
    }
350
  }
351
27880
  return c;
352
}
353
354
6047
bool DTypeConstructor::computeWellFounded(
355
    std::vector<TypeNode>& processing) const
356
{
357
11016
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
358
  {
359
10898
    TypeNode t = getArgType(i);
360
5929
    if (t.isDatatype())
361
    {
362
2917
      const DType& dt = t.getDType();
363
2917
      if (!dt.computeWellFounded(processing))
364
      {
365
960
        return false;
366
      }
367
    }
368
  }
369
5087
  return true;
370
}
371
372
2438
Node DTypeConstructor::computeGroundTerm(TypeNode t,
373
                                         std::vector<TypeNode>& processing,
374
                                         std::map<TypeNode, Node>& gt,
375
                                         bool isValue) const
376
{
377
2438
  NodeManager* nm = NodeManager::currentNM();
378
4876
  std::vector<Node> groundTerms;
379
2438
  groundTerms.push_back(getConstructor());
380
4876
  Trace("datatypes-init") << "cons " << d_constructor
381
2438
                          << " computeGroundTerm, isValue = " << isValue
382
2438
                          << std::endl;
383
384
  // for each selector, get a ground term
385
4876
  std::vector<TypeNode> instTypes;
386
4876
  std::vector<TypeNode> paramTypes;
387
2438
  bool isParam = t.isParametricDatatype();
388
2438
  if (isParam)
389
  {
390
28
    paramTypes = t.getDType().getParameters();
391
28
    instTypes = TypeNode(t).getParamTypes();
392
  }
393
3437
  for (size_t i = 0, nargs = getNumArgs(); i < nargs; i++)
394
  {
395
2105
    TypeNode selType = getArgType(i);
396
1106
    if (isParam)
397
    {
398
20
      selType = selType.substitute(paramTypes.begin(),
399
                                   paramTypes.end(),
400
                                   instTypes.begin(),
401
                                   instTypes.end());
402
    }
403
2105
    Node arg;
404
1106
    if (selType.isDatatype())
405
    {
406
800
      std::map<TypeNode, Node>::iterator itgt = gt.find(selType);
407
800
      if (itgt != gt.end())
408
      {
409
1
        arg = itgt->second;
410
      }
411
      else
412
      {
413
799
        const DType& dt = selType.getDType();
414
799
        arg = dt.computeGroundTerm(selType, processing, isValue);
415
      }
416
    }
417
    else
418
    {
419
      // call mkGroundValue or mkGroundTerm based on isValue
420
306
      arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm();
421
    }
422
1106
    if (arg.isNull())
423
    {
424
214
      Trace("datatypes-init") << "...unable to construct arg of "
425
107
                              << d_args[i]->getName() << std::endl;
426
107
      return Node();
427
    }
428
    else
429
    {
430
1998
      Trace("datatypes-init")
431
1998
          << "...constructed arg " << arg << " of type " << arg.getType()
432
999
          << ", isConst = " << arg.isConst() << std::endl;
433
1998
      Assert(!isValue || arg.isConst())
434
999
          << "Expected non-constant constructor argument : " << arg
435
999
          << " of type " << arg.getType();
436
999
      groundTerms.push_back(arg);
437
    }
438
  }
439
440
4662
  Node groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
441
2331
  if (isParam)
442
  {
443
27
    Assert(DType::datatypeOf(d_constructor).isParametric());
444
    // type is parametric, must apply type ascription
445
54
    Trace("datatypes-init") << "ambiguous type for " << groundTerm
446
27
                            << ", ascribe to " << t << std::endl;
447
81
    groundTerms[0] = nm->mkNode(
448
        APPLY_TYPE_ASCRIPTION,
449
54
        nm->mkConst(AscriptionType(getSpecializedConstructorType(t))),
450
27
        groundTerms[0]);
451
27
    groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms);
452
  }
453
2331
  Trace("datatypes-init") << "...return " << groundTerm << std::endl;
454
2331
  Assert(!isValue || groundTerm.isConst()) << "Non-constant term " << groundTerm
455
                                           << " returned for computeGroundTerm";
456
2331
  return groundTerm;
457
}
458
459
939325
void DTypeConstructor::computeSharedSelectors(TypeNode domainType) const
460
{
461
939325
  if (d_sharedSelectors[domainType].size() < getNumArgs())
462
  {
463
3718
    TypeNode ctype;
464
1859
    if (domainType.isParametricDatatype())
465
    {
466
43
      ctype = getSpecializedConstructorType(domainType);
467
    }
468
    else
469
    {
470
1816
      ctype = d_constructor.getType();
471
    }
472
1859
    Assert(ctype.isConstructor());
473
1859
    Assert(ctype.getNumChildren() - 1 == getNumArgs());
474
    // compute the shared selectors
475
1859
    const DType& dt = DType::datatypeOf(d_constructor);
476
3718
    std::map<TypeNode, unsigned> counter;
477
5452
    for (size_t j = 0, jend = ctype.getNumChildren() - 1; j < jend; j++)
478
    {
479
7186
      TypeNode t = ctype[j];
480
7186
      Node ss = dt.getSharedSelector(domainType, t, counter[t]);
481
3593
      d_sharedSelectors[domainType].push_back(ss);
482
3593
      Assert(d_sharedSelectorIndex[domainType].find(ss)
483
             == d_sharedSelectorIndex[domainType].end());
484
3593
      d_sharedSelectorIndex[domainType][ss] = j;
485
3593
      counter[t]++;
486
    }
487
  }
488
939325
}
489
490
19296
bool DTypeConstructor::resolve(
491
    TypeNode self,
492
    const std::map<std::string, TypeNode>& resolutions,
493
    const std::vector<TypeNode>& placeholders,
494
    const std::vector<TypeNode>& replacements,
495
    const std::vector<TypeNode>& paramTypes,
496
    const std::vector<TypeNode>& paramReplacements,
497
    size_t cindex)
498
{
499
19296
  if (isResolved())
500
  {
501
    // already resolved, fail
502
    return false;
503
  }
504
38592
  Trace("datatypes") << "DTypeConstructor::resolve, self type is " << self
505
19296
                     << std::endl;
506
507
19296
  NodeManager* nm = NodeManager::currentNM();
508
19296
  size_t index = 0;
509
38592
  std::vector<TypeNode> argTypes;
510
19296
  Trace("datatypes-init") << "Initialize constructor " << d_name << std::endl;
511
39325
  for (std::shared_ptr<DTypeSelector> arg : d_args)
512
  {
513
40058
    std::string argName = arg->d_name;
514
40058
    TypeNode range;
515
20029
    if (arg->d_selector.isNull())
516
    {
517
      // the unresolved type wasn't created here; do name resolution
518
128
      std::string typeName = argName.substr(argName.find('\0') + 1);
519
128
      Trace("datatypes-init")
520
64
          << "  - selector, typeName is " << typeName << std::endl;
521
64
      argName.resize(argName.find('\0'));
522
64
      if (typeName == "")
523
      {
524
64
        Trace("datatypes-init") << "  ...self selector" << std::endl;
525
64
        range = self;
526
256
        arg->d_selector = nm->mkSkolem(
527
            argName,
528
128
            nm->mkSelectorType(self, self),
529
            "is a selector",
530
64
            NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
531
      }
532
      else
533
      {
534
        std::map<std::string, TypeNode>::const_iterator j =
535
            resolutions.find(typeName);
536
        if (j == resolutions.end())
537
        {
538
          Trace("datatypes-init")
539
              << "  ...failed to resolve selector" << std::endl;
540
          // failed to resolve selector
541
          return false;
542
        }
543
        else
544
        {
545
          Trace("datatypes-init") << "  ...resolved selector" << std::endl;
546
          range = (*j).second;
547
          arg->d_selector = nm->mkSkolem(
548
              argName,
549
              nm->mkSelectorType(self, range),
550
              "is a selector",
551
              NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
552
        }
553
      }
554
    }
555
    else
556
    {
557
      // the type for the selector already exists; may need
558
      // complex-type substitution
559
19965
      range = arg->d_selector.getType();
560
39930
      Trace("datatypes-init")
561
19965
          << "  - null selector, range = " << range << std::endl;
562
19965
      if (!placeholders.empty())
563
      {
564
18689
        range = range.substitute(placeholders.begin(),
565
                                 placeholders.end(),
566
                                 replacements.begin(),
567
                                 replacements.end());
568
      }
569
39930
      Trace("datatypes-init")
570
19965
          << "  ...range after placeholder replacement " << range << std::endl;
571
19965
      if (!paramTypes.empty())
572
      {
573
105
        range = doParametricSubstitution(range, paramTypes, paramReplacements);
574
      }
575
39930
      Trace("datatypes-init")
576
19965
          << "  ...range after parametric substitution " << range << std::endl;
577
79860
      arg->d_selector = nm->mkSkolem(
578
          argName,
579
39930
          nm->mkSelectorType(self, range),
580
          "is a selector",
581
19965
          NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
582
    }
583
20029
    arg->d_selector.setAttribute(DTypeConsIndexAttr(), cindex);
584
20029
    arg->d_selector.setAttribute(DTypeIndexAttr(), index++);
585
20029
    arg->d_resolved = true;
586
20029
    argTypes.push_back(range);
587
    // We use \0 as a distinguished marker for unresolved selectors for doing
588
    // name resolutions. We now can remove \0 from name if necessary.
589
20029
    const size_t nul = arg->d_name.find('\0');
590
20029
    if (nul != std::string::npos)
591
    {
592
64
      arg->d_name.resize(nul);
593
    }
594
  }
595
596
19296
  Assert(index == getNumArgs());
597
598
  // Set constructor/tester last, since DTypeConstructor::isResolved()
599
  // returns true when d_tester is not the null Node.  If something
600
  // fails above, we want Constuctor::isResolved() to remain "false".
601
  // Further, mkConstructorType() iterates over the selectors, so
602
  // should get the results of any resolutions we did above.
603
  // The name of the tester variable does not matter, it is only used
604
  // internally.
605
38592
  std::string testerName("is_" + d_name);
606
77184
  d_tester = nm->mkSkolem(
607
      testerName,
608
38592
      nm->mkTesterType(self),
609
      "is a tester",
610
19296
      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
611
77184
  d_constructor = nm->mkSkolem(
612
      getName(),
613
38592
      nm->mkConstructorType(argTypes, self),
614
      "is a constructor",
615
19296
      NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY);
616
19296
  Assert(d_constructor.getType().isConstructor());
617
  // associate constructor with all selectors
618
39325
  for (std::shared_ptr<DTypeSelector> sel : d_args)
619
  {
620
20029
    sel->d_constructor = d_constructor;
621
  }
622
19296
  Assert(isResolved());
623
19296
  return true;
624
}
625
626
152
TypeNode DTypeConstructor::doParametricSubstitution(
627
    TypeNode range,
628
    const std::vector<TypeNode>& paramTypes,
629
    const std::vector<TypeNode>& paramReplacements)
630
{
631
152
  if (range.getNumChildren() == 0)
632
  {
633
109
    return range;
634
  }
635
86
  std::vector<TypeNode> origChildren;
636
86
  std::vector<TypeNode> children;
637
90
  for (TypeNode::const_iterator i = range.begin(), iend = range.end();
638
90
       i != iend;
639
       ++i)
640
  {
641
47
    origChildren.push_back((*i));
642
47
    children.push_back(
643
94
        doParametricSubstitution((*i), paramTypes, paramReplacements));
644
  }
645
53
  for (size_t i = 0, psize = paramTypes.size(); i < psize; ++i)
646
  {
647
51
    if (paramTypes[i].getSortConstructorArity() == origChildren.size())
648
    {
649
57
      TypeNode tn = paramTypes[i].instantiateSortConstructor(origChildren);
650
49
      if (range == tn)
651
      {
652
        TypeNode tret =
653
82
            paramReplacements[i].instantiateParametricDatatype(children);
654
41
        return tret;
655
      }
656
    }
657
  }
658
4
  NodeBuilder<> nb(range.getKind());
659
6
  for (size_t i = 0, csize = children.size(); i < csize; ++i)
660
  {
661
4
    nb << children[i];
662
  }
663
4
  TypeNode tn = nb.constructTypeNode();
664
2
  return tn;
665
}
666
667
38
void DTypeConstructor::toStream(std::ostream& out) const
668
{
669
38
  out << getName();
670
671
38
  unsigned nargs = getNumArgs();
672
38
  if (nargs == 0)
673
  {
674
18
    return;
675
  }
676
20
  out << "(";
677
54
  for (unsigned i = 0; i < nargs; i++)
678
  {
679
34
    out << *d_args[i];
680
34
    if (i + 1 < nargs)
681
    {
682
14
      out << ", ";
683
    }
684
  }
685
20
  out << ")";
686
}
687
688
38
std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
689
{
690
  // can only output datatypes in the CVC4 native language
691
76
  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
692
38
  ctor.toStream(os);
693
76
  return os;
694
}
695
696
26676
}  // namespace CVC4