GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_manager.cpp Lines: 483 584 82.7 %
Date: 2021-03-23 Branches: 647 1840 35.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_manager.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 Expression manager implementation.
13
 **
14
 ** Expression manager implementation.
15
 **
16
 ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
17
 **/
18
#include "expr/node_manager.h"
19
20
#include <algorithm>
21
#include <sstream>
22
#include <stack>
23
#include <utility>
24
25
#include "base/check.h"
26
#include "base/listener.h"
27
#include "expr/attribute.h"
28
#include "expr/bound_var_manager.h"
29
#include "expr/dtype.h"
30
#include "expr/dtype_cons.h"
31
#include "expr/metakind.h"
32
#include "expr/node_manager_attributes.h"
33
#include "expr/skolem_manager.h"
34
#include "expr/type_checker.h"
35
#include "util/resource_manager.h"
36
37
using namespace std;
38
using namespace CVC4::expr;
39
40
namespace CVC4 {
41
42
thread_local NodeManager* NodeManager::s_current = NULL;
43
44
namespace {
45
46
/**
47
 * This class sets it reference argument to true and ensures that it gets set
48
 * to false on destruction. This can be used to make sure a flag gets toggled
49
 * in a function even on exceptional exit (e.g., see reclaimZombies()).
50
 */
51
struct ScopedBool {
52
  bool& d_value;
53
54
183655
  ScopedBool(bool& value) :
55
183655
    d_value(value) {
56
57
183655
    Debug("gc") << ">> setting ScopedBool\n";
58
183655
    d_value = true;
59
183655
  }
60
61
367310
  ~ScopedBool() {
62
183655
    Debug("gc") << "<< clearing ScopedBool\n";
63
183655
    d_value = false;
64
183655
  }
65
};
66
67
/**
68
 * Similarly, ensure d_nodeUnderDeletion gets set to NULL even on
69
 * exceptional exit from NodeManager::reclaimZombies().
70
 */
71
struct NVReclaim {
72
  NodeValue*& d_deletionField;
73
74
29459522
  NVReclaim(NodeValue*& deletionField) :
75
29459522
    d_deletionField(deletionField) {
76
77
29459522
    Debug("gc") << ">> setting NVRECLAIM field\n";
78
29459522
  }
79
80
58919044
  ~NVReclaim() {
81
29459522
    Debug("gc") << "<< clearing NVRECLAIM field\n";
82
29459522
    d_deletionField = NULL;
83
29459522
  }
84
};
85
86
} // namespace
87
88
namespace attr {
89
  struct LambdaBoundVarListTag { };
90
}/* CVC4::attr namespace */
91
92
// attribute that stores the canonical bound variable list for function types
93
typedef expr::Attribute<attr::LambdaBoundVarListTag, Node> LambdaBoundVarListAttr;
94
95
7167
NodeManager::NodeManager()
96
7167
    : d_skManager(new SkolemManager),
97
7167
      d_bvManager(new BoundVarManager),
98
      next_id(0),
99
7167
      d_attrManager(new expr::attr::AttributeManager()),
100
      d_nodeUnderDeletion(nullptr),
101
      d_inReclaimZombies(false),
102
      d_abstractValueCount(0),
103
28668
      d_skolemCounter(0)
104
{
105
7167
  init();
106
7167
}
107
108
220447
bool NodeManager::isNAryKind(Kind k)
109
{
110
220447
  return kind::metakind::getMaxArityForKind(k) == expr::NodeValue::MAX_CHILDREN;
111
}
112
113
19560859
TypeNode NodeManager::booleanType()
114
{
115
19560859
  return mkTypeConst<TypeConstant>(BOOLEAN_TYPE);
116
}
117
118
4143963
TypeNode NodeManager::integerType()
119
{
120
4143963
  return mkTypeConst<TypeConstant>(INTEGER_TYPE);
121
}
122
123
4465334
TypeNode NodeManager::realType()
124
{
125
4465334
  return mkTypeConst<TypeConstant>(REAL_TYPE);
126
}
127
128
111592
TypeNode NodeManager::stringType()
129
{
130
111592
  return mkTypeConst<TypeConstant>(STRING_TYPE);
131
}
132
133
31826
TypeNode NodeManager::regExpType()
134
{
135
31826
  return mkTypeConst<TypeConstant>(REGEXP_TYPE);
136
}
137
138
7998
TypeNode NodeManager::roundingModeType()
139
{
140
7998
  return mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE);
141
}
142
143
201726
TypeNode NodeManager::boundVarListType()
144
{
145
201726
  return mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE);
146
}
147
148
8638
TypeNode NodeManager::instPatternType()
149
{
150
8638
  return mkTypeConst<TypeConstant>(INST_PATTERN_TYPE);
151
}
152
153
20036
TypeNode NodeManager::instPatternListType()
154
{
155
20036
  return mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE);
156
}
157
158
6622
TypeNode NodeManager::builtinOperatorType()
159
{
160
6622
  return mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE);
161
}
162
163
536807
TypeNode NodeManager::mkBitVectorType(unsigned size)
164
{
165
536807
  return mkTypeConst<BitVectorSize>(BitVectorSize(size));
166
}
167
168
5612
TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig)
169
{
170
5612
  return mkTypeConst<FloatingPointSize>(FloatingPointSize(exp, sig));
171
}
172
173
4303
TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs)
174
{
175
4303
  return mkTypeConst<FloatingPointSize>(fs);
176
}
177
178
7167
void NodeManager::init() {
179
  // `mkConst()` indirectly needs the correct NodeManager in scope because we
180
  // call `NodeValue::inc()` which uses `NodeManager::curentNM()`
181
14334
  NodeManagerScope nms(this);
182
183
7167
  poolInsert( &expr::NodeValue::null() );
184
185
2322108
  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
186
2314941
    Kind k = Kind(i);
187
188
2314941
    if(hasOperator(k)) {
189
1913589
      d_operators[i] = mkConst(Kind(k));
190
    }
191
  }
192
7167
}
193
194
14292
NodeManager::~NodeManager() {
195
  // have to ensure "this" is the current NodeManager during
196
  // destruction of operators, because they get GCed.
197
198
14292
  NodeManagerScope nms(this);
199
200
  // Destroy skolem and bound var manager before cleaning up attributes and
201
  // zombies
202
7146
  d_skManager = nullptr;
203
7146
  d_bvManager = nullptr;
204
205
  {
206
14292
    ScopedBool dontGC(d_inReclaimZombies);
207
    // hopefully by this point all SmtEngines have been deleted
208
    // already, along with all their attributes
209
7146
    d_attrManager->deleteAllAttributes();
210
  }
211
212
2315304
  for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
213
2308158
    d_operators[i] = Node::null();
214
  }
215
216
7146
  d_unique_vars.clear();
217
218
14292
  TypeNode dummy;
219
7146
  d_tt_cache.d_children.clear();
220
7146
  d_tt_cache.d_data = dummy;
221
7146
  d_rt_cache.d_children.clear();
222
7146
  d_rt_cache.d_data = dummy;
223
224
  // clear the datatypes
225
7146
  d_dtypes.clear();
226
227
7146
  Assert(!d_attrManager->inGarbageCollection());
228
229
14292
  std::vector<NodeValue*> order = TopologicalSort(d_maxedOut);
230
7146
  d_maxedOut.clear();
231
232
354940
  while (!d_zombies.empty() || !order.empty()) {
233
173897
    if (d_zombies.empty()) {
234
      // Delete the maxed out nodes in toplogical order once we know
235
      // there are no additional zombies, or other nodes to worry about.
236
7
      Assert(!order.empty());
237
      // We process these in reverse to reverse the topological order.
238
7
      NodeValue* greatest_maxed_out = order.back();
239
7
      order.pop_back();
240
7
      Assert(greatest_maxed_out->HasMaximizedReferenceCount());
241
7
      Debug("gc") << "Force zombify " << greatest_maxed_out << std::endl;
242
7
      greatest_maxed_out->d_rc = 0;
243
7
      markForDeletion(greatest_maxed_out);
244
    } else {
245
173890
      reclaimZombies();
246
    }
247
  }
248
249
7146
  poolRemove( &expr::NodeValue::null() );
250
251
7146
  if(Debug.isOn("gc:leaks")) {
252
    Debug("gc:leaks") << "still in pool:" << endl;
253
    for(NodeValuePool::const_iterator i = d_nodeValuePool.begin(),
254
          iend = d_nodeValuePool.end();
255
        i != iend;
256
        ++i) {
257
      Debug("gc:leaks") << "  " << *i
258
                        << " id=" << (*i)->d_id
259
                        << " rc=" << (*i)->d_rc
260
                        << " " << **i << endl;
261
    }
262
    Debug("gc:leaks") << ":end:" << endl;
263
  }
264
265
  // defensive coding, in case destruction-order issues pop up (they often do)
266
7146
  delete d_attrManager;
267
7146
  d_attrManager = NULL;
268
7146
}
269
270
5914380
const DType& NodeManager::getDTypeForIndex(size_t index) const
271
{
272
  // if this assertion fails, it is likely due to not managing datatypes
273
  // properly w.r.t. multiple NodeManagers.
274
5914380
  Assert(index < d_dtypes.size());
275
5914380
  return *d_dtypes[index];
276
}
277
278
176509
void NodeManager::reclaimZombies() {
279
  // FIXME multithreading
280
176509
  Assert(!d_attrManager->inGarbageCollection());
281
282
176509
  Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
283
284
  // during reclamation, reclaimZombies() is never supposed to be called
285
176509
  Assert(!d_inReclaimZombies)
286
      << "NodeManager::reclaimZombies() not re-entrant!";
287
288
  // whether exit is normal or exceptional, the Reclaim dtor is called
289
  // and ensures that d_inReclaimZombies is set back to false.
290
353018
  ScopedBool r(d_inReclaimZombies);
291
292
  // We copy the set away and clear the NodeManager's set of zombies.
293
  // This is because reclaimZombie() decrements the RC of the
294
  // NodeValue's children, which may (recursively) reclaim them.
295
  //
296
  // Let's say we're reclaiming zombie NodeValue "A" and its child "B"
297
  // then becomes a zombie (NodeManager::markForDeletion(B) is called).
298
  //
299
  // One way to handle B's zombification would be simply to put it
300
  // into d_zombies.  This is what we do.  However, if we were to
301
  // concurrently process d_zombies in the loop below, such addition
302
  // may be invisible to us (B is leaked) or even invalidate our
303
  // iterator, causing a crash.  So we need to copy the set away.
304
305
353018
  vector<NodeValue*> zombies;
306
176509
  zombies.reserve(d_zombies.size());
307
176509
  remove_copy_if(d_zombies.begin(),
308
                 d_zombies.end(),
309
                 back_inserter(zombies),
310
176509
                 NodeValueReferenceCountNonZero());
311
176509
  d_zombies.clear();
312
313
#ifdef _LIBCPP_VERSION
314
  NodeValue* last = NULL;
315
#endif
316
29636031
  for(vector<NodeValue*>::iterator i = zombies.begin();
317
29636031
      i != zombies.end();
318
      ++i) {
319
29459522
    NodeValue* nv = *i;
320
#ifdef _LIBCPP_VERSION
321
    // Work around an apparent bug in libc++'s hash_set<> which can
322
    // (very occasionally) have an element repeated.
323
    if(nv == last) {
324
      continue;
325
    }
326
    last = nv;
327
#endif
328
329
    // collect ONLY IF still zero
330
29459522
    if(nv->d_rc == 0) {
331
29459522
      if(Debug.isOn("gc")) {
332
        Debug("gc") << "deleting node value " << nv
333
                    << " [" << nv->d_id << "]: ";
334
        nv->printAst(Debug("gc"));
335
        Debug("gc") << endl;
336
      }
337
338
      // remove from the pool
339
29459522
      kind::MetaKind mk = nv->getMetaKind();
340
29459522
      if(mk != kind::metakind::VARIABLE && mk != kind::metakind::NULLARY_OPERATOR) {
341
28503914
        poolRemove(nv);
342
      }
343
344
      // whether exit is normal or exceptional, the NVReclaim dtor is
345
      // called and ensures that d_nodeUnderDeletion is set back to
346
      // NULL.
347
58919044
      NVReclaim rc(d_nodeUnderDeletion);
348
29459522
      d_nodeUnderDeletion = nv;
349
350
      // remove attributes
351
      { // notify listeners of deleted node
352
58919044
        TNode n;
353
29459522
        n.d_nv = nv;
354
29459522
        nv->d_rc = 1; // so that TNode doesn't assert-fail
355
55411268
        for (NodeManagerListener* listener : d_listeners)
356
        {
357
25951746
          listener->nmNotifyDeleteNode(n);
358
        }
359
        // this would mean that one of the listeners stowed away
360
        // a reference to this node!
361
29459522
        Assert(nv->d_rc == 1);
362
      }
363
29459522
      nv->d_rc = 0;
364
29459522
      d_attrManager->deleteAllAttributes(nv);
365
366
      // decr ref counts of children
367
29459522
      nv->decrRefCounts();
368
29459522
      if(mk == kind::metakind::CONSTANT) {
369
        // Destroy (call the destructor for) the C++ type representing
370
        // the constant in this NodeValue.  This is needed for
371
        // e.g. CVC4::Rational, since it has a gmp internal
372
        // representation that mallocs memory and should be cleaned
373
        // up.  (This won't delete a pointer value if used as a
374
        // constant, but then, you should probably use a smart-pointer
375
        // type for a constant payload.)
376
2434556
        kind::metakind::deleteNodeValueConstant(nv);
377
      }
378
29459522
      free(nv);
379
    }
380
  }
381
176509
}/* NodeManager::reclaimZombies() */
382
383
7150
std::vector<NodeValue*> NodeManager::TopologicalSort(
384
    const std::vector<NodeValue*>& roots) {
385
7150
  std::vector<NodeValue*> order;
386
  // The stack of nodes to visit. The Boolean value is false when visiting the
387
  // node in preorder and true when visiting it in postorder.
388
14300
  std::vector<std::pair<bool, NodeValue*> > stack;
389
  // Nodes that have been visited in both pre- and postorder
390
14300
  NodeValueIDSet visited;
391
14300
  const NodeValueIDSet root_set(roots.begin(), roots.end());
392
393
7163
  for (size_t index = 0; index < roots.size(); index++) {
394
13
    NodeValue* root = roots[index];
395
13
    if (visited.find(root) == visited.end()) {
396
42
      stack.push_back(std::make_pair(false, root));
397
    }
398
117
    while (!stack.empty()) {
399
52
      NodeValue* current = stack.back().second;
400
52
      const bool visited_children = stack.back().first;
401
104
      Debug("gc") << "Topological sort " << current << " " << visited_children
402
52
                  << std::endl;
403
52
      if (visited_children) {
404
21
        if (root_set.find(current) != root_set.end()) {
405
13
          order.push_back(current);
406
        }
407
21
        stack.pop_back();
408
      }
409
31
      else if (visited.find(current) == visited.end())
410
      {
411
21
        stack.back().first = true;
412
21
        visited.insert(current);
413
41
        for (unsigned i = 0; i < current->getNumChildren(); ++i) {
414
20
          expr::NodeValue* child = current->getChild(i);
415
20
          stack.push_back(std::make_pair(false, child));
416
        }
417
      }
418
      else
419
      {
420
10
        stack.pop_back();
421
      }
422
    }
423
  }
424
7150
  Assert(order.size() == roots.size());
425
14300
  return order;
426
} /* NodeManager::TopologicalSort() */
427
428
709621115
TypeNode NodeManager::getType(TNode n, bool check)
429
{
430
  // Many theories' type checkers call Node::getType() directly.  This
431
  // is incorrect, since "this" might not be the caller's current node
432
  // manager.  Rather than force the individual typecheckers not to do
433
  // this (by policy, which would be imperfect and lead to
434
  // hard-to-find bugs, which it has in the past), we just set this
435
  // node manager to be current for the duration of this check.
436
  //
437
1419242230
  NodeManagerScope nms(this);
438
439
709621115
  TypeNode typeNode;
440
709621115
  bool hasType = getAttribute(n, TypeAttr(), typeNode);
441
709621115
  bool needsCheck = check && !getAttribute(n, TypeCheckedAttr());
442
443
444
709621115
  Debug("getType") << this << " getting type for " << &n << " " << n << ", check=" << check << ", needsCheck = " << needsCheck << ", hasType = " << hasType << endl;
445
446
#ifdef CVC4_DEBUG
447
  // already did type check eagerly upon creation in node builder
448
709621115
  bool doTypeCheck = false;
449
#else
450
  bool doTypeCheck = true;
451
#endif
452
709621115
  if (needsCheck && doTypeCheck)
453
  {
454
    /* Iterate and compute the children bottom up. This avoids stack
455
       overflows in computeType() when the Node graph is really deep,
456
       which should only affect us when we're type checking lazily. */
457
    stack<TNode> worklist;
458
    worklist.push(n);
459
460
    while( !worklist.empty() ) {
461
      TNode m = worklist.top();
462
463
      bool readyToCompute = true;
464
465
      for( TNode::iterator it = m.begin(), end = m.end();
466
           it != end;
467
           ++it ) {
468
        if( !hasAttribute(*it, TypeAttr())
469
            || (check && !getAttribute(*it, TypeCheckedAttr())) ) {
470
          readyToCompute = false;
471
          worklist.push(*it);
472
        }
473
      }
474
475
      if( readyToCompute ) {
476
        Assert(check || m.getMetaKind() != kind::metakind::NULLARY_OPERATOR);
477
        /* All the children have types, time to compute */
478
        typeNode = TypeChecker::computeType(this, m, check);
479
        worklist.pop();
480
      }
481
    } // end while
482
483
    /* Last type computed in loop should be the type of n */
484
    Assert(typeNode == getAttribute(n, TypeAttr()));
485
709621115
  } else if( !hasType || needsCheck ) {
486
    /* We can compute the type top-down, without worrying about
487
       deep recursion. */
488
26402693
    Assert(check || n.getMetaKind() != kind::metakind::NULLARY_OPERATOR);
489
26402693
    typeNode = TypeChecker::computeType(this, n, check);
490
  }
491
492
  /* The type should be have been computed and stored. */
493
709620661
  Assert(hasAttribute(n, TypeAttr()));
494
  /* The check should have happened, if we asked for it. */
495
709620661
  Assert(!check || getAttribute(n, TypeCheckedAttr()));
496
497
709620661
  Debug("getType") << "type of " << &n << " " <<  n << " is " << typeNode << endl;
498
1419241322
  return typeNode;
499
}
500
501
164125
Node NodeManager::mkSkolem(const std::string& prefix, const TypeNode& type, const std::string& comment, int flags) {
502
164125
  Node n = NodeBuilder<0>(this, kind::SKOLEM);
503
164125
  setAttribute(n, TypeAttr(), type);
504
164125
  setAttribute(n, TypeCheckedAttr(), true);
505
164125
  if((flags & SKOLEM_EXACT_NAME) == 0) {
506
161662
    stringstream name;
507
80831
    name << prefix << '_' << ++d_skolemCounter;
508
80831
    setAttribute(n, expr::VarNameAttr(), name.str());
509
  } else {
510
83294
    setAttribute(n, expr::VarNameAttr(), prefix);
511
  }
512
164125
  if((flags & SKOLEM_NO_NOTIFY) == 0) {
513
263069
    for(vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
514
179846
      (*i)->nmNotifyNewSkolem(n, comment, (flags & SKOLEM_IS_GLOBAL) == SKOLEM_IS_GLOBAL);
515
    }
516
  }
517
164125
  return n;
518
}
519
520
407
TypeNode NodeManager::mkBagType(TypeNode elementType)
521
{
522
407
  CheckArgument(
523
407
      !elementType.isNull(), elementType, "unexpected NULL element type");
524
407
  CheckArgument(elementType.isFirstClass(),
525
                elementType,
526
                "cannot store types that are not first-class in bags. Try "
527
                "option --uf-ho.");
528
407
  Debug("bags") << "making bags type " << elementType << std::endl;
529
407
  return mkTypeNode(kind::BAG_TYPE, elementType);
530
}
531
532
722
TypeNode NodeManager::mkSequenceType(TypeNode elementType)
533
{
534
722
  CheckArgument(
535
722
      !elementType.isNull(), elementType, "unexpected NULL element type");
536
722
  CheckArgument(elementType.isFirstClass(),
537
                elementType,
538
                "cannot store types that are not first-class in sequences. Try "
539
                "option --uf-ho.");
540
722
  return mkTypeNode(kind::SEQUENCE_TYPE, elementType);
541
}
542
543
1953
TypeNode NodeManager::mkDatatypeType(DType& datatype, uint32_t flags)
544
{
545
  // Not worth a special implementation; this doesn't need to be fast
546
  // code anyway.
547
3906
  std::vector<DType> datatypes;
548
1953
  datatypes.push_back(datatype);
549
3906
  std::vector<TypeNode> result = mkMutualDatatypeTypes(datatypes, flags);
550
1953
  Assert(result.size() == 1);
551
3906
  return result.front();
552
}
553
554
1953
std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
555
    const std::vector<DType>& datatypes, uint32_t flags)
556
{
557
3906
  std::set<TypeNode> unresolvedTypes;
558
3906
  return mkMutualDatatypeTypes(datatypes, unresolvedTypes, flags);
559
}
560
561
4082
std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
562
    const std::vector<DType>& datatypes,
563
    const std::set<TypeNode>& unresolvedTypes,
564
    uint32_t flags)
565
{
566
8164
  NodeManagerScope nms(this);
567
8164
  std::map<std::string, TypeNode> nameResolutions;
568
4082
  std::vector<TypeNode> dtts;
569
570
  // First do some sanity checks, set up the final Type to be used for
571
  // each datatype, and set up the "named resolutions" used to handle
572
  // simple self- and mutual-recursion, for example in the definition
573
  // "nat = succ(pred:nat) | zero", a named resolution can handle the
574
  // pred selector.
575
9878
  for (const DType& dt : datatypes)
576
  {
577
5796
    uint32_t index = d_dtypes.size();
578
5796
    d_dtypes.push_back(std::unique_ptr<DType>(new DType(dt)));
579
5796
    DType* dtp = d_dtypes.back().get();
580
11592
    TypeNode typeNode;
581
5796
    if (dtp->getNumParameters() == 0)
582
    {
583
5725
      typeNode = mkTypeConst(DatatypeIndexConstant(index));
584
    }
585
    else
586
    {
587
142
      TypeNode cons = mkTypeConst(DatatypeIndexConstant(index));
588
142
      std::vector<TypeNode> params;
589
71
      params.push_back(cons);
590
165
      for (uint32_t ip = 0; ip < dtp->getNumParameters(); ++ip)
591
      {
592
94
        params.push_back(dtp->getParameter(ip));
593
      }
594
595
71
      typeNode = mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
596
    }
597
5796
    AlwaysAssert(nameResolutions.find(dtp->getName()) == nameResolutions.end())
598
        << "cannot construct two datatypes at the same time "
599
           "with the same name";
600
5796
    nameResolutions.insert(std::make_pair(dtp->getName(), typeNode));
601
5796
    dtts.push_back(typeNode);
602
  }
603
604
  // Second, set up the type substitution map for complex type
605
  // resolution (e.g. if "list" is the type we're defining, and it has
606
  // a selector of type "ARRAY INT OF list", this can't be taken care
607
  // of using the named resolutions that we set up above.  A
608
  // preliminary array type was set up, and now needs to have "list"
609
  // substituted in it for the correct type.
610
  //
611
  // @TODO get rid of named resolutions altogether and handle
612
  // everything with these resolutions?
613
8164
  std::vector<TypeNode> paramTypes;
614
8164
  std::vector<TypeNode> paramReplacements;
615
8164
  std::vector<TypeNode> placeholders;  // to hold the "unresolved placeholders"
616
8164
  std::vector<TypeNode> replacements;  // to hold our final, resolved types
617
7888
  for (const TypeNode& ut : unresolvedTypes)
618
  {
619
7612
    std::string name = ut.getAttribute(expr::VarNameAttr());
620
    std::map<std::string, TypeNode>::const_iterator resolver =
621
3806
        nameResolutions.find(name);
622
7612
    AlwaysAssert(resolver != nameResolutions.end())
623
3806
        << "cannot resolve type " + name
624
3806
               + "; it's not among the datatypes being defined";
625
    // We will instruct the Datatype to substitute "ut" (the
626
    // unresolved SortType used as a placeholder in complex types)
627
    // with "(*resolver).second" (the TypeNode we created in the
628
    // first step, above).
629
3806
    if (ut.isSort())
630
    {
631
3753
      placeholders.push_back(ut);
632
3753
      replacements.push_back((*resolver).second);
633
    }
634
    else
635
    {
636
53
      Assert(ut.isSortConstructor());
637
53
      paramTypes.push_back(ut);
638
53
      paramReplacements.push_back((*resolver).second);
639
    }
640
  }
641
642
  // Lastly, perform the final resolutions and checks.
643
9878
  for (const TypeNode& ut : dtts)
644
  {
645
5796
    const DType& dt = ut.getDType();
646
5796
    if (!dt.isResolved())
647
    {
648
5796
      const_cast<DType&>(dt).resolve(nameResolutions,
649
                                     placeholders,
650
                                     replacements,
651
                                     paramTypes,
652
                                     paramReplacements);
653
    }
654
    // Check the datatype has been resolved properly.
655
25094
    for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
656
    {
657
19298
      const DTypeConstructor& c = dt[i];
658
38596
      TypeNode testerType CVC4_UNUSED = c.getTester().getType();
659
19298
      Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut)
660
          << "malformed tester in datatype post-resolution";
661
38596
      TypeNode ctorType CVC4_UNUSED = c.getConstructor().getType();
662
19298
      Assert(ctorType.isConstructor()
663
            && ctorType.getNumChildren() == c.getNumArgs() + 1
664
            && ctorType.getRangeType() == ut)
665
          << "malformed constructor in datatype post-resolution";
666
      // for all selectors...
667
39327
      for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
668
      {
669
20029
        const DTypeSelector& a = c[j];
670
40058
        TypeNode selectorType = a.getType();
671
20029
        Assert(a.isResolved() && selectorType.isSelector()
672
              && selectorType[0] == ut)
673
            << "malformed selector in datatype post-resolution";
674
        // This next one's a "hard" check, performed in non-debug builds
675
        // as well; the other ones should all be guaranteed by the
676
        // CVC4::DType class, but this actually needs to be checked.
677
20029
        AlwaysAssert(!selectorType.getRangeType().isFunctionLike())
678
            << "cannot put function-like things in datatypes";
679
      }
680
    }
681
  }
682
683
9964
  for (NodeManagerListener* nml : d_listeners)
684
  {
685
5882
    nml->nmNotifyNewDatatypes(dtts, flags);
686
  }
687
688
8164
  return dtts;
689
}
690
691
19298
TypeNode NodeManager::mkConstructorType(const std::vector<TypeNode>& args,
692
                                        TypeNode range)
693
{
694
38596
  std::vector<TypeNode> sorts = args;
695
19298
  sorts.push_back(range);
696
38596
  return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
697
}
698
699
29397
TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
700
29397
  if( index==types.size() ){
701
10710
    if( d_data.isNull() ){
702
3638
      std::stringstream sst;
703
1819
      sst << "__cvc4_tuple";
704
2818
      for (unsigned i = 0; i < types.size(); ++ i) {
705
999
        sst << "_" << types[i];
706
      }
707
3638
      DType dt(sst.str());
708
1819
      dt.setTuple();
709
3638
      std::stringstream ssc;
710
1819
      ssc << sst.str() << "_ctor";
711
      std::shared_ptr<DTypeConstructor> c =
712
3638
          std::make_shared<DTypeConstructor>(ssc.str());
713
2818
      for (unsigned i = 0; i < types.size(); ++ i) {
714
1998
        std::stringstream ss;
715
999
        ss << sst.str() << "_stor_" << i;
716
999
        c->addArg(ss.str().c_str(), types[i]);
717
      }
718
1819
      dt.addConstructor(c);
719
1819
      d_data = nm->mkDatatypeType(dt);
720
1819
      Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
721
    }
722
10710
    return d_data;
723
  }else{
724
18687
    return d_children[types[index]].getTupleType( nm, types, index+1 );
725
  }
726
}
727
728
262
TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Record& rec, unsigned index ) {
729
262
  if (index == rec.size())
730
  {
731
99
    if( d_data.isNull() ){
732
100
      std::stringstream sst;
733
50
      sst << "__cvc4_record";
734
137
      for (const std::pair<std::string, TypeNode>& i : rec)
735
      {
736
87
        sst << "_" << i.first << "_" << i.second;
737
      }
738
100
      DType dt(sst.str());
739
50
      dt.setRecord();
740
100
      std::stringstream ssc;
741
50
      ssc << sst.str() << "_ctor";
742
      std::shared_ptr<DTypeConstructor> c =
743
100
          std::make_shared<DTypeConstructor>(ssc.str());
744
137
      for (const std::pair<std::string, TypeNode>& i : rec)
745
      {
746
87
        c->addArg(i.first, i.second);
747
      }
748
50
      dt.addConstructor(c);
749
50
      d_data = nm->mkDatatypeType(dt);
750
50
      Debug("tuprec-debug") << "Return type : " << d_data << std::endl;
751
    }
752
99
    return d_data;
753
  }
754
163
  return d_children[rec[index].second][rec[index].first].getRecordType(
755
163
      nm, rec, index + 1);
756
}
757
758
54549
TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts,
759
                                     bool reqFlat)
760
{
761
54549
  Assert(sorts.size() >= 2);
762
54549
  CheckArgument(!reqFlat || !sorts[sorts.size() - 1].isFunction(),
763
54549
                sorts[sorts.size() - 1],
764
                "must flatten function types");
765
54549
  return mkTypeNode(kind::FUNCTION_TYPE, sorts);
766
}
767
768
50
TypeNode NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts,
769
                                      bool reqFlat)
770
{
771
50
  Assert(sorts.size() >= 1);
772
100
  std::vector<TypeNode> sortNodes;
773
50
  sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end());
774
50
  sortNodes.push_back(booleanType());
775
100
  return mkFunctionType(sortNodes, reqFlat);
776
}
777
778
1198
TypeNode NodeManager::mkFunctionType(const TypeNode& domain,
779
                                     const TypeNode& range,
780
                                     bool reqFlat)
781
{
782
2396
  std::vector<TypeNode> sorts;
783
1198
  sorts.push_back(domain);
784
1198
  sorts.push_back(range);
785
2396
  return mkFunctionType(sorts, reqFlat);
786
}
787
788
45413
TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes,
789
                                     const TypeNode& range,
790
                                     bool reqFlat)
791
{
792
45413
  Assert(argTypes.size() >= 1);
793
90826
  std::vector<TypeNode> sorts(argTypes);
794
45413
  sorts.push_back(range);
795
90826
  return mkFunctionType(sorts, reqFlat);
796
}
797
798
10710
TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
799
21420
  std::vector< TypeNode > ts;
800
10710
  Debug("tuprec-debug") << "Make tuple type : ";
801
29397
  for (unsigned i = 0; i < types.size(); ++ i) {
802
18687
    CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples");
803
18687
    ts.push_back( types[i] );
804
18687
    Debug("tuprec-debug") << types[i] << " ";
805
  }
806
10710
  Debug("tuprec-debug") << std::endl;
807
21420
  return d_tt_cache.getTupleType( this, ts );
808
}
809
810
99
TypeNode NodeManager::mkRecordType(const Record& rec) {
811
99
  return d_rt_cache.getRecordType( this, rec );
812
}
813
814
void NodeManager::reclaimAllZombies(){
815
  reclaimZombiesUntil(0u);
816
}
817
818
/** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
819
void NodeManager::reclaimZombiesUntil(uint32_t k){
820
  if(safeToReclaimZombies()){
821
    while(poolSize() >= k && !d_zombies.empty()){
822
      reclaimZombies();
823
    }
824
  }
825
}
826
827
1
size_t NodeManager::poolSize() const{
828
1
  return d_nodeValuePool.size();
829
}
830
831
14
TypeNode NodeManager::mkSort(uint32_t flags) {
832
28
  NodeBuilder<1> nb(this, kind::SORT_TYPE);
833
28
  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
834
14
  nb << sortTag;
835
14
  TypeNode tn = nb.constructTypeNode();
836
16
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
837
2
    (*i)->nmNotifyNewSort(tn, flags);
838
  }
839
28
  return tn;
840
}
841
842
8489
TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) {
843
16978
  NodeBuilder<1> nb(this, kind::SORT_TYPE);
844
16978
  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
845
8489
  nb << sortTag;
846
8489
  TypeNode tn = nb.constructTypeNode();
847
8489
  setAttribute(tn, expr::VarNameAttr(), name);
848
21089
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
849
12600
    (*i)->nmNotifyNewSort(tn, flags);
850
  }
851
16978
  return tn;
852
}
853
854
483
TypeNode NodeManager::mkSort(TypeNode constructor,
855
                                    const std::vector<TypeNode>& children,
856
                                    uint32_t flags) {
857
483
  Assert(constructor.getKind() == kind::SORT_TYPE
858
         && constructor.getNumChildren() == 0)
859
      << "expected a sort constructor";
860
483
  Assert(children.size() > 0) << "expected non-zero # of children";
861
483
  Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr())
862
         && hasAttribute(constructor.d_nv, expr::VarNameAttr()))
863
      << "expected a sort constructor";
864
966
  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
865
483
  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr())
866
         == children.size())
867
      << "arity mismatch in application of sort constructor";
868
966
  NodeBuilder<> nb(this, kind::SORT_TYPE);
869
966
  Node sortTag = Node(constructor.d_nv->d_children[0]);
870
483
  nb << sortTag;
871
483
  nb.append(children);
872
483
  TypeNode type = nb.constructTypeNode();
873
483
  setAttribute(type, expr::VarNameAttr(), name);
874
1110
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
875
627
    (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
876
  }
877
966
  return type;
878
}
879
880
94
TypeNode NodeManager::mkSortConstructor(const std::string& name,
881
                                        size_t arity,
882
                                        uint32_t flags)
883
{
884
94
  Assert(arity > 0);
885
188
  NodeBuilder<> nb(this, kind::SORT_TYPE);
886
188
  Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
887
94
  nb << sortTag;
888
94
  TypeNode type = nb.constructTypeNode();
889
94
  setAttribute(type, expr::VarNameAttr(), name);
890
94
  setAttribute(type, expr::SortArityAttr(), arity);
891
194
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
892
100
    (*i)->nmNotifyNewSortConstructor(type, flags);
893
  }
894
188
  return type;
895
}
896
897
172080
Node NodeManager::mkVar(const std::string& name, const TypeNode& type)
898
{
899
172080
  Node n = NodeBuilder<0>(this, kind::VARIABLE);
900
172080
  setAttribute(n, TypeAttr(), type);
901
172080
  setAttribute(n, TypeCheckedAttr(), true);
902
172080
  setAttribute(n, expr::VarNameAttr(), name);
903
366671
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
904
194591
    (*i)->nmNotifyNewVar(n);
905
  }
906
172080
  return n;
907
}
908
909
Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type)
910
{
911
  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
912
  setAttribute(*n, TypeAttr(), type);
913
  setAttribute(*n, TypeCheckedAttr(), true);
914
  setAttribute(*n, expr::VarNameAttr(), name);
915
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
916
    (*i)->nmNotifyNewVar(*n);
917
  }
918
  return n;
919
}
920
921
530965
Node NodeManager::mkBoundVar(const std::string& name, const TypeNode& type) {
922
530965
  Node n = mkBoundVar(type);
923
530965
  setAttribute(n, expr::VarNameAttr(), name);
924
530965
  return n;
925
}
926
927
Node* NodeManager::mkBoundVarPtr(const std::string& name,
928
                                 const TypeNode& type) {
929
  Node* n = mkBoundVarPtr(type);
930
  setAttribute(*n, expr::VarNameAttr(), name);
931
  return n;
932
}
933
934
3553
Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) {
935
3553
  Assert(tn.isFunction());
936
3553
  Node bvl = tn.getAttribute(LambdaBoundVarListAttr());
937
3553
  if( bvl.isNull() ){
938
448
    std::vector< Node > vars;
939
543
    for( unsigned i=0; i<tn.getNumChildren()-1; i++ ){
940
319
      vars.push_back(mkBoundVar(tn[i]));
941
    }
942
224
    bvl = mkNode(kind::BOUND_VAR_LIST, vars);
943
224
    Trace("functions") << "Make standard bound var list " << bvl << " for " << tn << std::endl;
944
224
    tn.setAttribute(LambdaBoundVarListAttr(),bvl);
945
  }
946
3553
  return bvl;
947
}
948
949
1000444
Node NodeManager::mkAssociative(Kind kind, const std::vector<Node>& children)
950
{
951
1000444
  AlwaysAssert(kind::isAssociative(kind)) << "Illegal kind in mkAssociative";
952
953
1000444
  const unsigned int max = kind::metakind::getMaxArityForKind(kind);
954
1000444
  size_t numChildren = children.size();
955
956
  /* If the number of children is within bounds, then there's nothing to do. */
957
1000444
  if (numChildren <= max)
958
  {
959
1000444
    return mkNode(kind, children);
960
  }
961
  const unsigned int min = kind::metakind::getMinArityForKind(kind);
962
963
  std::vector<Node>::const_iterator it = children.begin();
964
  std::vector<Node>::const_iterator end = children.end();
965
966
  /* The new top-level children and the children of each sub node */
967
  std::vector<Node> newChildren;
968
  std::vector<Node> subChildren;
969
970
  while (it != end && numChildren > max)
971
  {
972
    /* Grab the next max children and make a node for them. */
973
    for (std::vector<Node>::const_iterator next = it + max; it != next;
974
         ++it, --numChildren)
975
    {
976
      subChildren.push_back(*it);
977
    }
978
    Node subNode = mkNode(kind, subChildren);
979
    newChildren.push_back(subNode);
980
981
    subChildren.clear();
982
  }
983
984
  // add the leftover children
985
  if (numChildren > 0)
986
  {
987
    for (; it != end; ++it)
988
    {
989
      newChildren.push_back(*it);
990
    }
991
  }
992
993
  /* It would be really weird if this happened (it would require
994
   * min > 2, for one thing), but let's make sure. */
995
  AlwaysAssert(newChildren.size() >= min)
996
      << "Too few new children in mkAssociative";
997
998
  // recurse
999
  return mkAssociative(kind, newChildren);
1000
}
1001
1002
724
Node NodeManager::mkLeftAssociative(Kind kind,
1003
                                    const std::vector<Node>& children)
1004
{
1005
724
  Node n = children[0];
1006
4609
  for (size_t i = 1, size = children.size(); i < size; i++)
1007
  {
1008
3885
    n = mkNode(kind, n, children[i]);
1009
  }
1010
724
  return n;
1011
}
1012
1013
Node NodeManager::mkRightAssociative(Kind kind,
1014
                                     const std::vector<Node>& children)
1015
{
1016
  Node n = children[children.size() - 1];
1017
  for (size_t i = children.size() - 1; i > 0;)
1018
  {
1019
    n = mkNode(kind, children[--i], n);
1020
  }
1021
  return n;
1022
}
1023
1024
721
Node NodeManager::mkChain(Kind kind, const std::vector<Node>& children)
1025
{
1026
721
  if (children.size() == 2)
1027
  {
1028
    // if this is the case exactly 1 pair will be generated so the
1029
    // AND is not required
1030
    return mkNode(kind, children[0], children[1]);
1031
  }
1032
1442
  std::vector<Node> cchildren;
1033
3615
  for (size_t i = 0, nargsmo = children.size() - 1; i < nargsmo; i++)
1034
  {
1035
2894
    cchildren.push_back(mkNode(kind, children[i], children[i + 1]));
1036
  }
1037
721
  return mkNode(kind::AND, cchildren);
1038
}
1039
1040
85
Node NodeManager::mkVar(const TypeNode& type)
1041
{
1042
85
  Node n = NodeBuilder<0>(this, kind::VARIABLE);
1043
85
  setAttribute(n, TypeAttr(), type);
1044
85
  setAttribute(n, TypeCheckedAttr(), true);
1045
168
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
1046
83
    (*i)->nmNotifyNewVar(n);
1047
  }
1048
85
  return n;
1049
}
1050
1051
Node* NodeManager::mkVarPtr(const TypeNode& type)
1052
{
1053
  Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
1054
  setAttribute(*n, TypeAttr(), type);
1055
  setAttribute(*n, TypeCheckedAttr(), true);
1056
  for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
1057
    (*i)->nmNotifyNewVar(*n);
1058
  }
1059
  return n;
1060
}
1061
1062
551321
Node NodeManager::mkBoundVar(const TypeNode& type) {
1063
551321
  Node n = NodeBuilder<0>(this, kind::BOUND_VARIABLE);
1064
551321
  setAttribute(n, TypeAttr(), type);
1065
551321
  setAttribute(n, TypeCheckedAttr(), true);
1066
551321
  return n;
1067
}
1068
1069
Node* NodeManager::mkBoundVarPtr(const TypeNode& type) {
1070
  Node* n = NodeBuilder<0>(this, kind::BOUND_VARIABLE).constructNodePtr();
1071
  setAttribute(*n, TypeAttr(), type);
1072
  setAttribute(*n, TypeCheckedAttr(), true);
1073
  return n;
1074
}
1075
1076
54565
Node NodeManager::mkInstConstant(const TypeNode& type) {
1077
54565
  Node n = NodeBuilder<0>(this, kind::INST_CONSTANT);
1078
54565
  n.setAttribute(TypeAttr(), type);
1079
54565
  n.setAttribute(TypeCheckedAttr(), true);
1080
54565
  return n;
1081
}
1082
1083
706
Node NodeManager::mkBooleanTermVariable() {
1084
706
  Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE);
1085
706
  n.setAttribute(TypeAttr(), booleanType());
1086
706
  n.setAttribute(TypeCheckedAttr(), true);
1087
706
  return n;
1088
}
1089
1090
6898
Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) {
1091
6898
  std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
1092
6898
  if( it==d_unique_vars[k].end() ){
1093
8656
    Node n = NodeBuilder<0>(this, k).constructNode();
1094
4328
    setAttribute(n, TypeAttr(), type);
1095
    //setAttribute(n, TypeCheckedAttr(), true);
1096
4328
    d_unique_vars[k][type] = n;
1097
4328
    Assert(n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
1098
4328
    return n;
1099
  }else{
1100
2570
    return it->second;
1101
  }
1102
}
1103
1104
12234
Node NodeManager::mkSingleton(const TypeNode& t, const TNode n)
1105
{
1106
24468
  Assert(n.getType().isSubtypeOf(t))
1107
12234
      << "Invalid operands for mkSingleton. The type '" << n.getType()
1108
12234
      << "' of node '" << n << "' is not a subtype of '" << t << "'."
1109
      << std::endl;
1110
24468
  Node op = mkConst(SingletonOp(t));
1111
12234
  Node singleton = mkNode(kind::SINGLETON, op, n);
1112
24468
  return singleton;
1113
}
1114
1115
328
Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m)
1116
{
1117
656
  Assert(n.getType().isSubtypeOf(t))
1118
328
      << "Invalid operands for mkBag. The type '" << n.getType()
1119
328
      << "' of node '" << n << "' is not a subtype of '" << t << "'."
1120
      << std::endl;
1121
656
  Node op = mkConst(MakeBagOp(t));
1122
328
  Node bag = mkNode(kind::MK_BAG, op, n, m);
1123
656
  return bag;
1124
}
1125
1126
8
Node NodeManager::mkAbstractValue(const TypeNode& type) {
1127
8
  Node n = mkConst(AbstractValue(++d_abstractValueCount));
1128
8
  n.setAttribute(TypeAttr(), type);
1129
8
  n.setAttribute(TypeCheckedAttr(), true);
1130
8
  return n;
1131
}
1132
1133
47506187
bool NodeManager::safeToReclaimZombies() const{
1134
  // FIXME multithreading
1135
47506187
  return !d_inReclaimZombies && !d_attrManager->inGarbageCollection();
1136
}
1137
1138
void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){
1139
  d_attrManager->deleteAttributes(ids);
1140
}
1141
1142
void NodeManager::debugHook(int debugFlag){
1143
  // For debugging purposes only, DO NOT CHECK IN ANY CODE!
1144
}
1145
1146
156
Kind NodeManager::getKindForFunction(TNode fun)
1147
{
1148
312
  TypeNode tn = fun.getType();
1149
156
  if (tn.isFunction())
1150
  {
1151
22
    return kind::APPLY_UF;
1152
  }
1153
134
  else if (tn.isConstructor())
1154
  {
1155
35
    return kind::APPLY_CONSTRUCTOR;
1156
  }
1157
99
  else if (tn.isSelector())
1158
  {
1159
59
    return kind::APPLY_SELECTOR;
1160
  }
1161
40
  else if (tn.isTester())
1162
  {
1163
40
    return kind::APPLY_TESTER;
1164
  }
1165
  return kind::UNDEFINED_KIND;
1166
}
1167
1168
26685
}/* CVC4 namespace */