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