GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/node_manager.h Lines: 184 209 88.0 %
Date: 2021-03-22 Branches: 567 2154 26.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file node_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Andrew Reynolds, Christopher L. Conway
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 manager for Nodes
13
 **
14
 ** A manager for Nodes.
15
 **
16
 ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
17
 **/
18
19
#include "cvc4_private.h"
20
21
/* circular dependency; force node.h first */
22
//#include "expr/attribute.h"
23
#include "expr/node.h"
24
#include "expr/type_node.h"
25
26
#ifndef CVC4__NODE_MANAGER_H
27
#define CVC4__NODE_MANAGER_H
28
29
#include <vector>
30
#include <string>
31
#include <unordered_set>
32
33
#include "base/check.h"
34
#include "expr/kind.h"
35
#include "expr/metakind.h"
36
#include "expr/node_value.h"
37
38
namespace CVC4 {
39
40
namespace api {
41
class Solver;
42
}
43
44
class StatisticsRegistry;
45
class ResourceManager;
46
class SkolemManager;
47
class BoundVarManager;
48
49
class DType;
50
51
namespace expr {
52
  namespace attr {
53
    class AttributeUniqueId;
54
    class AttributeManager;
55
  }/* CVC4::expr::attr namespace */
56
57
  class TypeChecker;
58
}/* CVC4::expr namespace */
59
60
/**
61
 * An interface that an interested party can implement and then subscribe
62
 * to NodeManager events via NodeManager::subscribeEvents(this).
63
 */
64
18615
class NodeManagerListener {
65
 public:
66
18591
  virtual ~NodeManagerListener() {}
67
3526
  virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {}
68
6
  virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {}
69
627
  virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort,
70
627
                                                  uint32_t flags) {}
71
1537
  virtual void nmNotifyNewDatatypes(const std::vector<TypeNode>& datatypes,
72
                                    uint32_t flags)
73
  {
74
1537
  }
75
  virtual void nmNotifyNewVar(TNode n) {}
76
  virtual void nmNotifyNewSkolem(TNode n, const std::string& comment,
77
                                 uint32_t flags) {}
78
  /**
79
   * Notify a listener of a Node that's being GCed.  If this function stores a
80
   * reference
81
   * to the Node somewhere, very bad things will happen.
82
   */
83
11300937
  virtual void nmNotifyDeleteNode(TNode n) {}
84
}; /* class NodeManagerListener */
85
86
class NodeManager
87
{
88
  friend class api::Solver;
89
  friend class expr::NodeValue;
90
  friend class expr::TypeChecker;
91
92
  template <unsigned nchild_thresh>
93
  friend class NodeBuilder;
94
  friend class NodeManagerScope;
95
96
 public:
97
  /**
98
   * Return true if given kind is n-ary. The test is based on n-ary kinds
99
   * having their maximal arity as the maximal possible number of children
100
   * of a node.
101
   */
102
  static bool isNAryKind(Kind k);
103
104
 private:
105
  /** Predicate for use with STL algorithms */
106
  struct NodeValueReferenceCountNonZero {
107
30079118
    bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
108
  };
109
110
  typedef std::unordered_set<expr::NodeValue*,
111
                             expr::NodeValuePoolHashFunction,
112
                             expr::NodeValuePoolEq> NodeValuePool;
113
  typedef std::unordered_set<expr::NodeValue*,
114
                             expr::NodeValueIDHashFunction,
115
                             expr::NodeValueIDEquality> NodeValueIDSet;
116
117
  static thread_local NodeManager* s_current;
118
119
  StatisticsRegistry* d_statisticsRegistry;
120
121
  /** The skolem manager */
122
  std::unique_ptr<SkolemManager> d_skManager;
123
  /** The bound variable manager */
124
  std::unique_ptr<BoundVarManager> d_bvManager;
125
126
  NodeValuePool d_nodeValuePool;
127
128
  size_t next_id;
129
130
  expr::attr::AttributeManager* d_attrManager;
131
132
  /**
133
   * The node value we're currently freeing.  This unique node value
134
   * is permitted to have outstanding TNodes to it (in "soft"
135
   * contexts, like as a key in attribute tables), even though
136
   * normally it's an error to have a TNode to a node value with a
137
   * reference count of 0.  Being "under deletion" also enables
138
   * assertions that inc() is not called on it.
139
   */
140
  expr::NodeValue* d_nodeUnderDeletion;
141
142
  /**
143
   * True iff we are in reclaimZombies().  This avoids unnecessary
144
   * recursion; a NodeValue being deleted might zombify other
145
   * NodeValues, but these shouldn't trigger a (recursive) call to
146
   * reclaimZombies().
147
   */
148
  bool d_inReclaimZombies;
149
150
  /**
151
   * The set of zombie nodes.  We may want to revisit this design, as
152
   * we might like to delete nodes in least-recently-used order.  But
153
   * we also need to avoid processing a zombie twice.
154
   */
155
  NodeValueIDSet d_zombies;
156
157
  /**
158
   * NodeValues with maxed out reference counts. These live as long as the
159
   * NodeManager. They have a custom deallocation procedure at the very end.
160
   */
161
  std::vector<expr::NodeValue*> d_maxedOut;
162
163
  /**
164
   * A set of operator singletons (w.r.t.  to this NodeManager
165
   * instance) for operators.  Conceptually, Nodes with kind, say,
166
   * PLUS, are APPLYs of a PLUS operator to arguments.  This array
167
   * holds the set of operators for these things.  A PLUS operator is
168
   * a Node with kind "BUILTIN", and if you call
169
   * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
170
   */
171
  Node d_operators[kind::LAST_KIND];
172
173
  /** unique vars per (Kind,Type) */
174
  std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
175
176
  /**
177
   * A list of subscribers for NodeManager events.
178
   */
179
  std::vector<NodeManagerListener*> d_listeners;
180
181
  /** A list of datatypes owned by this node manager */
182
  std::vector<std::unique_ptr<DType> > d_dtypes;
183
184
  /**
185
   * A map of tuple and record types to their corresponding datatype.
186
   */
187
15953
  class TupleTypeCache {
188
  public:
189
    std::map< TypeNode, TupleTypeCache > d_children;
190
    TypeNode d_data;
191
    TypeNode getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index = 0 );
192
  };
193
14483
  class RecTypeCache {
194
  public:
195
    std::map< TypeNode, std::map< std::string, RecTypeCache > > d_children;
196
    TypeNode d_data;
197
    TypeNode getRecordType( NodeManager * nm, const Record& rec, unsigned index = 0 );
198
  };
199
  TupleTypeCache d_tt_cache;
200
  RecTypeCache d_rt_cache;
201
202
  /**
203
   * Keep a count of all abstract values produced by this NodeManager.
204
   * Abstract values have a type attribute, so if multiple SmtEngines
205
   * are attached to this NodeManager, we don't want their abstract
206
   * values to overlap.
207
   */
208
  unsigned d_abstractValueCount;
209
210
  /**
211
   * A counter used to produce unique skolem names.
212
   *
213
   * Note that it is NOT incremented when skolems are created using
214
   * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
215
   * by this node manager.
216
   */
217
  unsigned d_skolemCounter;
218
219
  /**
220
   * Look up a NodeValue in the pool associated to this NodeManager.
221
   * The NodeValue argument need not be a "completely-constructed"
222
   * NodeValue.  In particular, "non-inlined" constants are permitted
223
   * (see below).
224
   *
225
   * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
226
   * correctly set, and d_children[0..n-1] should be valid (extant)
227
   * NodeValues for lookup.
228
   *
229
   * For CONSTANT metakinds, nv's d_kind should be set correctly.
230
   * Normally a CONSTANT would have d_nchildren == 0 and the constant
231
   * value inlined in the d_children space.  However, here we permit
232
   * "non-inlined" NodeValues to avoid unnecessary copying.  For
233
   * these, d_nchildren == 1, and d_nchildren is a pointer to the
234
   * constant value.
235
   *
236
   * The point of this complex design is to permit efficient lookups
237
   * (without fully constructing a NodeValue).  In the case that the
238
   * argument is not fully constructed, and this function returns
239
   * NULL, the caller should fully construct an equivalent one before
240
   * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
241
   * permitted in the pool!
242
   */
243
  inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
244
245
  /**
246
   * Insert a NodeValue into the NodeManager's pool.
247
   *
248
   * It is an error to insert a NodeValue already in the pool.
249
   * Enquire first with poolLookup().
250
   */
251
  inline void poolInsert(expr::NodeValue* nv);
252
253
  /**
254
   * Remove a NodeValue from the NodeManager's pool.
255
   *
256
   * It is an error to request the removal of a NodeValue from the
257
   * pool that is not in the pool.
258
   */
259
  inline void poolRemove(expr::NodeValue* nv);
260
261
  /**
262
   * Determine if nv is currently being deleted by the NodeManager.
263
   */
264
16185241593
  inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
265
16185241593
    return d_nodeUnderDeletion == nv;
266
  }
267
268
  /**
269
   * Register a NodeValue as a zombie.
270
   */
271
47487848
  inline void markForDeletion(expr::NodeValue* nv) {
272
47487848
    Assert(nv->d_rc == 0);
273
274
    // if d_reclaiming is set, make sure we don't call
275
    // reclaimZombies(), because it's already running.
276
47487848
    if(Debug.isOn("gc")) {
277
      Debug("gc") << "zombifying node value " << nv
278
                  << " [" << nv->d_id << "]: ";
279
      nv->printAst(Debug("gc"));
280
      Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
281
                  << std::endl;
282
    }
283
284
    // `d_zombies` uses the node id to hash and compare nodes. If `d_zombies`
285
    // already contains a node value with the same id as `nv`, but the pointers
286
    // are different, then the wrong `NodeManager` was in scope for one of the
287
    // two nodes when it reached refcount zero.
288
47487848
    Assert(d_zombies.find(nv) == d_zombies.end() || *d_zombies.find(nv) == nv);
289
290
47487848
    d_zombies.insert(nv);
291
292
47487848
    if(safeToReclaimZombies()) {
293
30757865
      if(d_zombies.size() > 5000) {
294
2621
        reclaimZombies();
295
      }
296
    }
297
47487848
  }
298
299
  /**
300
   * Register a NodeValue as having a maxed out reference count. This NodeValue
301
   * will live as long as its containing NodeManager.
302
   */
303
7
  inline void markRefCountMaxedOut(expr::NodeValue* nv) {
304
7
    Assert(nv->HasMaximizedReferenceCount());
305
7
    if(Debug.isOn("gc")) {
306
      Debug("gc") << "marking node value " << nv
307
                  << " [" << nv->d_id << "]: as maxed out" << std::endl;
308
    }
309
7
    d_maxedOut.push_back(nv);
310
7
  }
311
312
  /**
313
   * Reclaim all zombies.
314
   */
315
  void reclaimZombies();
316
317
  /**
318
   * It is safe to collect zombies.
319
   */
320
  bool safeToReclaimZombies() const;
321
322
  /**
323
   * Returns a reverse topological sort of a list of NodeValues. The NodeValues
324
   * must be valid and have ids. The NodeValues are not modified (including ref
325
   * counts).
326
   */
327
  static std::vector<expr::NodeValue*> TopologicalSort(
328
      const std::vector<expr::NodeValue*>& roots);
329
330
  /**
331
   * This template gives a mechanism to stack-allocate a NodeValue
332
   * with enough space for N children (where N is a compile-time
333
   * constant).  You use it like this:
334
   *
335
   *   NVStorage<4> nvStorage;
336
   *   NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
337
   *
338
   * ...and then you can use nvStack as a NodeValue that you know has
339
   * room for 4 children.
340
   */
341
  template <size_t N>
342
215394141
  struct NVStorage {
343
    expr::NodeValue nv;
344
    expr::NodeValue* child[N];
345
  };/* struct NodeManager::NVStorage<N> */
346
347
  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
348
   *
349
   * It has been decided for now to hold off on implementations of
350
   * these functions, as they may only be needed in CNF conversion,
351
   * where it's pointless to do a lazy isAtomic determination by
352
   * searching through the DAG, and storing it, since the result will
353
   * only be used once.  For more details see the 4/27/2010 CVC4
354
   * developer's meeting notes at:
355
   *
356
   * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
357
   */
358
  // bool containsDecision(TNode); // is "atomic"
359
  // bool properlyContainsDecision(TNode); // all children are atomic
360
361
  // undefined private copy constructor (disallow copy)
362
  NodeManager(const NodeManager&) = delete;
363
364
  NodeManager& operator=(const NodeManager&) = delete;
365
366
  void init();
367
368
  /**
369
   * Create a variable with the given name and type.  NOTE that no
370
   * lookup is done on the name.  If you mkVar("a", type) and then
371
   * mkVar("a", type) again, you have two variables.  The NodeManager
372
   * version of this is private to avoid internal uses of mkVar() from
373
   * within CVC4.  Such uses should employ mkSkolem() instead.
374
   */
375
  Node mkVar(const std::string& name, const TypeNode& type);
376
  Node* mkVarPtr(const std::string& name, const TypeNode& type);
377
378
  /** Create a variable with the given type. */
379
  Node mkVar(const TypeNode& type);
380
  Node* mkVarPtr(const TypeNode& type);
381
382
 public:
383
  explicit NodeManager();
384
  ~NodeManager();
385
386
  /** The node manager in the current public-facing CVC4 library context */
387
74520203348
  static NodeManager* currentNM() { return s_current; }
388
  /** Get this node manager's skolem manager */
389
73580
  SkolemManager* getSkolemManager() { return d_skManager.get(); }
390
  /** Get this node manager's bound variable manager */
391
701372
  BoundVarManager* getBoundVarManager() { return d_bvManager.get(); }
392
393
  /** Get this node manager's statistics registry */
394
18355
  StatisticsRegistry* getStatisticsRegistry() const
395
  {
396
18355
    return d_statisticsRegistry;
397
  }
398
399
  /** Subscribe to NodeManager events */
400
17085
  void subscribeEvents(NodeManagerListener* listener) {
401
17085
    Assert(std::find(d_listeners.begin(), d_listeners.end(), listener)
402
           == d_listeners.end())
403
        << "listener already subscribed";
404
17085
    d_listeners.push_back(listener);
405
17085
  }
406
407
  /** Unsubscribe from NodeManager events */
408
17061
  void unsubscribeEvents(NodeManagerListener* listener) {
409
17061
    std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
410
17061
    Assert(elt != d_listeners.end()) << "listener not subscribed";
411
17061
    d_listeners.erase(elt);
412
17061
  }
413
414
  /**
415
   * Return the datatype at the given index owned by this class. Type nodes are
416
   * associated with datatypes through the DatatypeIndexConstant class. The
417
   * argument index is intended to be a value taken from that class.
418
   *
419
   * Type nodes must access their DTypes through a level of indirection to
420
   * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
421
   * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
422
   * which is used as an index to retrieve the DType via this call.
423
   */
424
  const DType& getDTypeForIndex(size_t index) const;
425
426
  /** Get a Kind from an operator expression */
427
  static inline Kind operatorToKind(TNode n);
428
429
  /** Get corresponding application kind for function
430
   *
431
   * Different functional nodes are applied differently, according to their
432
   * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied
433
   * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via
434
   * APPLY_CONSTRUCTOR. This method provides the correct application according
435
   * to which functional type fun has.
436
   *
437
   * @param fun The functional node
438
   * @return the correct application kind for fun. If fun's type is not function
439
   * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned.
440
   */
441
  static Kind getKindForFunction(TNode fun);
442
443
  // general expression-builders
444
445
  /** Create a node with one child. */
446
  Node mkNode(Kind kind, TNode child1);
447
  Node* mkNodePtr(Kind kind, TNode child1);
448
449
  /** Create a node with two children. */
450
  Node mkNode(Kind kind, TNode child1, TNode child2);
451
  Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
452
453
  /** Create a node with three children. */
454
  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
455
  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
456
457
  /** Create a node with four children. */
458
  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
459
              TNode child4);
460
  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
461
              TNode child4);
462
463
  /** Create a node with five children. */
464
  Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
465
              TNode child4, TNode child5);
466
  Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
467
              TNode child4, TNode child5);
468
469
  /** Create a node with an arbitrary number of children. */
470
  template <bool ref_count>
471
  Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
472
  template <bool ref_count>
473
  Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
474
475
  /**
476
   * Create an AND node with arbitrary number of children. This returns the
477
   * true node if children is empty, or the single node in children if
478
   * it contains only one node.
479
   *
480
   * We define construction of AND as a special case here since it is widely
481
   * used for e.g. constructing explanations.
482
   */
483
  template <bool ref_count>
484
  Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children);
485
486
  /**
487
   * Create an OR node with arbitrary number of children. This returns the
488
   * false node if children is empty, or the single node in children if
489
   * it contains only one node.
490
   *
491
   * We define construction of OR as a special case here since it is widely
492
   * used for e.g. constructing explanations or lemmas.
493
   */
494
  template <bool ref_count>
495
  Node mkOr(const std::vector<NodeTemplate<ref_count> >& children);
496
497
  /** Create a node (with no children) by operator. */
498
  Node mkNode(TNode opNode);
499
  Node* mkNodePtr(TNode opNode);
500
501
  /** Create a node with one child by operator. */
502
  Node mkNode(TNode opNode, TNode child1);
503
  Node* mkNodePtr(TNode opNode, TNode child1);
504
505
  /** Create a node with two children by operator. */
506
  Node mkNode(TNode opNode, TNode child1, TNode child2);
507
  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
508
509
  /** Create a node with three children by operator. */
510
  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
511
  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
512
513
  /** Create a node with four children by operator. */
514
  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
515
              TNode child4);
516
  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
517
              TNode child4);
518
519
  /** Create a node with five children by operator. */
520
  Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
521
              TNode child4, TNode child5);
522
  Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
523
              TNode child4, TNode child5);
524
525
  /** Create a node by applying an operator to the children. */
526
  template <bool ref_count>
527
  Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
528
  template <bool ref_count>
529
  Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
530
531
  Node mkBoundVar(const std::string& name, const TypeNode& type);
532
  Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
533
534
  Node mkBoundVar(const TypeNode& type);
535
  Node* mkBoundVarPtr(const TypeNode& type);
536
537
  /** get the canonical bound variable list for function type tn */
538
  Node getBoundVarListForFunctionType( TypeNode tn );
539
540
  /**
541
   * Create an Node by applying an associative operator to the children.
542
   * If <code>children.size()</code> is greater than the max arity for
543
   * <code>kind</code>, then the expression will be broken up into
544
   * suitably-sized chunks, taking advantage of the associativity of
545
   * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
546
   * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
547
   * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
548
   * The order of the arguments will be preserved in a left-to-right
549
   * traversal of the resulting tree.
550
   */
551
  Node mkAssociative(Kind kind, const std::vector<Node>& children);
552
553
  /**
554
   * Create an Node by applying an binary left-associative operator to the
555
   * children. For example, mkLeftAssociative( f, { a, b, c } ) returns
556
   * f( f( a, b ), c ).
557
   */
558
  Node mkLeftAssociative(Kind kind, const std::vector<Node>& children);
559
  /**
560
   * Create an Node by applying an binary right-associative operator to the
561
   * children. For example, mkRightAssociative( f, { a, b, c } ) returns
562
   * f( a, f( b, c ) ).
563
   */
564
  Node mkRightAssociative(Kind kind, const std::vector<Node>& children);
565
566
  /** make chain
567
   *
568
   * Given a kind k and arguments t_1, ..., t_n, this returns the
569
   * conjunction of:
570
   *  (k t_1 t_2) .... (k t_{n-1} t_n)
571
   * It is expected that k is a kind denoting a predicate, and args is a list
572
   * of terms of size >= 2 such that the terms above are well-typed.
573
   */
574
  Node mkChain(Kind kind, const std::vector<Node>& children);
575
576
  /**
577
   * Optional flags used to control behavior of NodeManager::mkSkolem().
578
   * They should be composed with a bitwise OR (e.g.,
579
   * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
580
   * cannot be composed in such a manner.
581
   */
582
  enum SkolemFlags
583
  {
584
    SKOLEM_DEFAULT = 0,    /**< default behavior */
585
    SKOLEM_NO_NOTIFY = 1,  /**< do not notify subscribers */
586
    SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
587
    SKOLEM_IS_GLOBAL = 4,  /**< global vars appear in models even after a pop */
588
    SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
589
  };                         /* enum SkolemFlags */
590
591
  /**
592
   * Create a skolem constant with the given name, type, and comment.
593
   *
594
   * @param prefix the name of the new skolem variable is the prefix
595
   * appended with a unique ID.  This way a family of skolem variables
596
   * can be made with unique identifiers, used in dump, tracing, and
597
   * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
598
   * a unique ID appended and use prefix as the name.
599
   *
600
   * @param type the type of the skolem variable to create
601
   *
602
   * @param comment a comment for dumping output; if declarations are
603
   * being dumped, this is included in a comment before the declaration
604
   * and can be quite useful for debugging
605
   *
606
   * @param flags an optional mask of bits from SkolemFlags to control
607
   * mkSkolem() behavior
608
   */
609
  Node mkSkolem(const std::string& prefix, const TypeNode& type,
610
                const std::string& comment = "", int flags = SKOLEM_DEFAULT);
611
612
  /** Create a instantiation constant with the given type. */
613
  Node mkInstConstant(const TypeNode& type);
614
615
  /** Create a boolean term variable. */
616
  Node mkBooleanTermVariable();
617
618
  /** Make a new abstract value with the given type. */
619
  Node mkAbstractValue(const TypeNode& type);
620
621
  /** make unique (per Type,Kind) variable. */
622
  Node mkNullaryOperator(const TypeNode& type, Kind k);
623
624
  /**
625
  * Create a singleton set from the given element n.
626
  * @param t the element type of the returned set.
627
  *          Note that the type of n needs to be a subtype of t.
628
  * @param n the single element in the singleton.
629
  * @return a singleton set constructed from the element n.
630
  */
631
  Node mkSingleton(const TypeNode& t, const TNode n);
632
633
  /**
634
  * Create a bag from the given element n along with its multiplicity m.
635
  * @param t the element type of the returned bag.
636
  *          Note that the type of n needs to be a subtype of t.
637
  * @param n the element that is used to to construct the bag
638
  * @param m the multiplicity of the element n
639
  * @return a bag that contains m occurrences of n.
640
  */
641
  Node mkBag(const TypeNode& t, const TNode n, const TNode m);
642
643
  /**
644
   * Create a constant of type T.  It will have the appropriate
645
   * CONST_* kind defined for T.
646
   */
647
  template <class T>
648
  Node mkConst(const T&);
649
650
  template <class T>
651
  TypeNode mkTypeConst(const T&);
652
653
  template <class NodeClass, class T>
654
  NodeClass mkConstInternal(const T&);
655
656
  /** Create a node with children. */
657
  TypeNode mkTypeNode(Kind kind, TypeNode child1);
658
  TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
659
  TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
660
                      TypeNode child3);
661
  TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
662
663
  /**
664
   * Determine whether Nodes of a particular Kind have operators.
665
   * @returns true if Nodes of Kind k have operators.
666
   */
667
  static inline bool hasOperator(Kind k);
668
669
  /**
670
   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
671
   * returned node n will have kind BUILTIN, and calling
672
   * n.getConst<CVC4::Kind>() will yield k.
673
   */
674
5993020
  inline TNode operatorOf(Kind k) {
675
5993020
    AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
676
                    "Kind is not an OPERATOR-kinded kind "
677
                    "in NodeManager::operatorOf()" );
678
5993020
    return d_operators[k];
679
  }
680
681
  /**
682
   * Retrieve an attribute for a node.
683
   *
684
   * @param nv the node value
685
   * @param attr an instance of the attribute kind to retrieve.
686
   * @returns the attribute, if set, or a default-constructed
687
   * <code>AttrKind::value_type</code> if not.
688
   */
689
  template <class AttrKind>
690
  inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
691
                                                    const AttrKind& attr) const;
692
693
  /**
694
   * Check whether an attribute is set for a node.
695
   *
696
   * @param nv the node value
697
   * @param attr an instance of the attribute kind to check
698
   * @returns <code>true</code> iff <code>attr</code> is set for
699
   * <code>nv</code>.
700
   */
701
  template <class AttrKind>
702
  inline bool hasAttribute(expr::NodeValue* nv,
703
                           const AttrKind& attr) const;
704
705
  /**
706
   * Check whether an attribute is set for a node, and, if so,
707
   * retrieve it.
708
   *
709
   * @param nv the node value
710
   * @param attr an instance of the attribute kind to check
711
   * @param value a reference to an object of the attribute's value type.
712
   * <code>value</code> will be set to the value of the attribute, if it is
713
   * set for <code>nv</code>; otherwise, it will be set to the default
714
   * value of the attribute.
715
   * @returns <code>true</code> iff <code>attr</code> is set for
716
   * <code>nv</code>.
717
   */
718
  template <class AttrKind>
719
  inline bool getAttribute(expr::NodeValue* nv,
720
                           const AttrKind& attr,
721
                           typename AttrKind::value_type& value) const;
722
723
  /**
724
   * Set an attribute for a node.  If the node doesn't have the
725
   * attribute, this function assigns one.  If the node has one, this
726
   * overwrites it.
727
   *
728
   * @param nv the node value
729
   * @param attr an instance of the attribute kind to set
730
   * @param value the value of <code>attr</code> for <code>nv</code>
731
   */
732
  template <class AttrKind>
733
  inline void setAttribute(expr::NodeValue* nv,
734
                           const AttrKind& attr,
735
                           const typename AttrKind::value_type& value);
736
737
  /**
738
   * Retrieve an attribute for a TNode.
739
   *
740
   * @param n the node
741
   * @param attr an instance of the attribute kind to retrieve.
742
   * @returns the attribute, if set, or a default-constructed
743
   * <code>AttrKind::value_type</code> if not.
744
   */
745
  template <class AttrKind>
746
  inline typename AttrKind::value_type
747
  getAttribute(TNode n, const AttrKind& attr) const;
748
749
  /**
750
   * Check whether an attribute is set for a TNode.
751
   *
752
   * @param n the node
753
   * @param attr an instance of the attribute kind to check
754
   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
755
   */
756
  template <class AttrKind>
757
  inline bool hasAttribute(TNode n,
758
                           const AttrKind& attr) const;
759
760
  /**
761
   * Check whether an attribute is set for a TNode and, if so, retieve
762
   * it.
763
   *
764
   * @param n the node
765
   * @param attr an instance of the attribute kind to check
766
   * @param value a reference to an object of the attribute's value type.
767
   * <code>value</code> will be set to the value of the attribute, if it is
768
   * set for <code>nv</code>; otherwise, it will be set to the default value of
769
   * the attribute.
770
   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
771
   */
772
  template <class AttrKind>
773
  inline bool getAttribute(TNode n,
774
                           const AttrKind& attr,
775
                           typename AttrKind::value_type& value) const;
776
777
  /**
778
   * Set an attribute for a node.  If the node doesn't have the
779
   * attribute, this function assigns one.  If the node has one, this
780
   * overwrites it.
781
   *
782
   * @param n the node
783
   * @param attr an instance of the attribute kind to set
784
   * @param value the value of <code>attr</code> for <code>n</code>
785
   */
786
  template <class AttrKind>
787
  inline void setAttribute(TNode n,
788
                           const AttrKind& attr,
789
                           const typename AttrKind::value_type& value);
790
791
  /**
792
   * Retrieve an attribute for a TypeNode.
793
   *
794
   * @param n the type node
795
   * @param attr an instance of the attribute kind to retrieve.
796
   * @returns the attribute, if set, or a default-constructed
797
   * <code>AttrKind::value_type</code> if not.
798
   */
799
  template <class AttrKind>
800
  inline typename AttrKind::value_type
801
  getAttribute(TypeNode n, const AttrKind& attr) const;
802
803
  /**
804
   * Check whether an attribute is set for a TypeNode.
805
   *
806
   * @param n the type node
807
   * @param attr an instance of the attribute kind to check
808
   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
809
   */
810
  template <class AttrKind>
811
  inline bool hasAttribute(TypeNode n,
812
                           const AttrKind& attr) const;
813
814
  /**
815
   * Check whether an attribute is set for a TypeNode and, if so, retieve
816
   * it.
817
   *
818
   * @param n the type node
819
   * @param attr an instance of the attribute kind to check
820
   * @param value a reference to an object of the attribute's value type.
821
   * <code>value</code> will be set to the value of the attribute, if it is
822
   * set for <code>nv</code>; otherwise, it will be set to the default value of
823
   * the attribute.
824
   * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
825
   */
826
  template <class AttrKind>
827
  inline bool getAttribute(TypeNode n,
828
                           const AttrKind& attr,
829
                           typename AttrKind::value_type& value) const;
830
831
  /**
832
   * Set an attribute for a type node.  If the node doesn't have the
833
   * attribute, this function assigns one.  If the type node has one,
834
   * this overwrites it.
835
   *
836
   * @param n the type node
837
   * @param attr an instance of the attribute kind to set
838
   * @param value the value of <code>attr</code> for <code>n</code>
839
   */
840
  template <class AttrKind>
841
  inline void setAttribute(TypeNode n,
842
                           const AttrKind& attr,
843
                           const typename AttrKind::value_type& value);
844
845
  /** Get the (singleton) type for Booleans. */
846
  TypeNode booleanType();
847
848
  /** Get the (singleton) type for integers. */
849
  TypeNode integerType();
850
851
  /** Get the (singleton) type for reals. */
852
  TypeNode realType();
853
854
  /** Get the (singleton) type for strings. */
855
  TypeNode stringType();
856
857
  /** Get the (singleton) type for RegExp. */
858
  TypeNode regExpType();
859
860
  /** Get the (singleton) type for rounding modes. */
861
  TypeNode roundingModeType();
862
863
  /** Get the bound var list type. */
864
  TypeNode boundVarListType();
865
866
  /** Get the instantiation pattern type. */
867
  TypeNode instPatternType();
868
869
  /** Get the instantiation pattern type. */
870
  TypeNode instPatternListType();
871
872
  /**
873
   * Get the (singleton) type for builtin operators (that is, the type
874
   * of the Node returned from Node::getOperator() when the operator
875
   * is built-in, like EQUAL). */
876
  TypeNode builtinOperatorType();
877
878
  /**
879
   * Make a function type from domain to range.
880
   *
881
   * @param domain the domain type
882
   * @param range the range type
883
   * @param reqFlat If true, we require flat function types, e.g. the
884
   * range type cannot be a function. User-generated function types and those
885
   * used in solving must be flat, although some use cases (e.g. LFSC proof
886
   * conversion) require non-flat function types.
887
   * @returns the functional type domain -> range
888
   */
889
  TypeNode mkFunctionType(const TypeNode& domain,
890
                          const TypeNode& range,
891
                          bool reqFlat = true);
892
893
  /**
894
   * Make a function type with input types from
895
   * argTypes. <code>argTypes</code> must have at least one element.
896
   *
897
   * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
898
   * @param range the range type
899
   * @param reqFlat Same as above
900
   * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
901
   */
902
  TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
903
                          const TypeNode& range,
904
                          bool reqFlat = true);
905
906
  /**
907
   * Make a function type with input types from
908
   * <code>sorts[0..sorts.size()-2]</code> and result type
909
   * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
910
   * at least 2 elements.
911
   *
912
   * @param sorts The argument and range sort of the function type, where the
913
   * range type is the last in this vector.
914
   * @param reqFlat Same as above
915
   */
916
  TypeNode mkFunctionType(const std::vector<TypeNode>& sorts,
917
                          bool reqFlat = true);
918
919
  /**
920
   * Make a predicate type with input types from
921
   * <code>sorts</code>. The result with be a function type with range
922
   * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
923
   * element.
924
   */
925
  TypeNode mkPredicateType(const std::vector<TypeNode>& sorts,
926
                           bool reqFlat = true);
927
928
  /**
929
   * Make a tuple type with types from
930
   * <code>types</code>. <code>types</code> must have at least one
931
   * element.
932
   *
933
   * @param types a vector of types
934
   * @returns the tuple type (types[0], ..., types[n])
935
   */
936
  TypeNode mkTupleType(const std::vector<TypeNode>& types);
937
938
  /**
939
   * Make a record type with the description from rec.
940
   *
941
   * @param rec a description of the record
942
   * @returns the record type
943
   */
944
  TypeNode mkRecordType(const Record& rec);
945
946
  /**
947
   * Make a symbolic expression type with types from
948
   * <code>types</code>. <code>types</code> may have any number of
949
   * elements.
950
   *
951
   * @param types a vector of types
952
   * @returns the symbolic expression type (types[0], ..., types[n])
953
   */
954
  inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
955
956
  /** Make the type of floating-point with <code>exp</code> bit exponent and
957
      <code>sig</code> bit significand */
958
  TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
959
  TypeNode mkFloatingPointType(FloatingPointSize fs);
960
961
  /** Make the type of bitvectors of size <code>size</code> */
962
  TypeNode mkBitVectorType(unsigned size);
963
964
  /** Make the type of arrays with the given parameterization */
965
  inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
966
967
  /** Make the type of set with the given parameterization */
968
  inline TypeNode mkSetType(TypeNode elementType);
969
970
  /** Make the type of bags with the given parameterization */
971
  TypeNode mkBagType(TypeNode elementType);
972
973
  /** Make the type of sequences with the given parameterization */
974
  TypeNode mkSequenceType(TypeNode elementType);
975
976
  /** Bits for use in mkDatatypeType() flags.
977
   *
978
   * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
979
   * out as a definition, for example, in models or during dumping.
980
   */
981
  enum
982
  {
983
    DATATYPE_FLAG_NONE = 0,
984
    DATATYPE_FLAG_PLACEHOLDER = 1
985
  }; /* enum */
986
987
  /** Make a type representing the given datatype. */
988
  TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE);
989
990
  /**
991
   * Make a set of types representing the given datatypes, which may be
992
   * mutually recursive.
993
   */
994
  std::vector<TypeNode> mkMutualDatatypeTypes(
995
      const std::vector<DType>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
996
997
  /**
998
   * Make a set of types representing the given datatypes, which may
999
   * be mutually recursive.  unresolvedTypes is a set of SortTypes
1000
   * that were used as placeholders in the Datatypes for the Datatypes
1001
   * of the same name.  This is just a more complicated version of the
1002
   * above mkMutualDatatypeTypes() function, but is required to handle
1003
   * complex types.
1004
   *
1005
   * For example, unresolvedTypes might contain the single sort "list"
1006
   * (with that name reported from SortType::getName()).  The
1007
   * datatypes list might have the single datatype
1008
   *
1009
   *   DATATYPE
1010
   *     list = cons(car:ARRAY INT OF list, cdr:list) | nil;
1011
   *   END;
1012
   *
1013
   * To represent the Type of the array, the user had to create a
1014
   * placeholder type (an uninterpreted sort) to stand for "list" in
1015
   * the type of "car".  It is this placeholder sort that should be
1016
   * passed in unresolvedTypes.  If the datatype was of the simpler
1017
   * form:
1018
   *
1019
   *   DATATYPE
1020
   *     list = cons(car:list, cdr:list) | nil;
1021
   *   END;
1022
   *
1023
   * then no complicated Type needs to be created, and the above,
1024
   * simpler form of mkMutualDatatypeTypes() is enough.
1025
   */
1026
  std::vector<TypeNode> mkMutualDatatypeTypes(
1027
      const std::vector<DType>& datatypes,
1028
      const std::set<TypeNode>& unresolvedTypes,
1029
      uint32_t flags = DATATYPE_FLAG_NONE);
1030
1031
  /**
1032
   * Make a type representing a constructor with the given argument (subfield)
1033
   * types and return type range.
1034
   */
1035
  TypeNode mkConstructorType(const std::vector<TypeNode>& args, TypeNode range);
1036
1037
  /** Make a type representing a selector with the given parameterization */
1038
  inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
1039
1040
  /** Make a type representing a tester with given parameterization */
1041
  inline TypeNode mkTesterType(TypeNode domain);
1042
1043
  /** Bits for use in mkSort() flags. */
1044
  enum
1045
  {
1046
    SORT_FLAG_NONE = 0,
1047
    SORT_FLAG_PLACEHOLDER = 1
1048
  }; /* enum */
1049
1050
  /** Make a new (anonymous) sort of arity 0. */
1051
  TypeNode mkSort(uint32_t flags = SORT_FLAG_NONE);
1052
1053
  /** Make a new sort with the given name of arity 0. */
1054
  TypeNode mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE);
1055
1056
  /** Make a new sort by parameterizing the given sort constructor. */
1057
  TypeNode mkSort(TypeNode constructor,
1058
                  const std::vector<TypeNode>& children,
1059
                  uint32_t flags = SORT_FLAG_NONE);
1060
1061
  /** Make a new sort with the given name and arity. */
1062
  TypeNode mkSortConstructor(const std::string& name,
1063
                             size_t arity,
1064
                             uint32_t flags = SORT_FLAG_NONE);
1065
1066
  /**
1067
   * Get the type for the given node and optionally do type checking.
1068
   *
1069
   * Initial type computation will be near-constant time if
1070
   * type checking is not requested. Results are memoized, so that
1071
   * subsequent calls to getType() without type checking will be
1072
   * constant time.
1073
   *
1074
   * Initial type checking is linear in the size of the expression.
1075
   * Again, the results are memoized, so that subsequent calls to
1076
   * getType(), with or without type checking, will be constant
1077
   * time.
1078
   *
1079
   * NOTE: A TypeCheckingException can be thrown even when type
1080
   * checking is not requested. getType() will always return a
1081
   * valid and correct type and, thus, an exception will be thrown
1082
   * when no valid or correct type can be computed (e.g., if the
1083
   * arguments to a bit-vector operation aren't bit-vectors). When
1084
   * type checking is not requested, getType() will do the minimum
1085
   * amount of checking required to return a valid result.
1086
   *
1087
   * @param n the Node for which we want a type
1088
   * @param check whether we should check the type as we compute it
1089
   * (default: false)
1090
   */
1091
  TypeNode getType(TNode n, bool check = false);
1092
1093
  /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
1094
  void reclaimZombiesUntil(uint32_t k);
1095
1096
  /** Reclaims all zombies (if possible).*/
1097
  void reclaimAllZombies();
1098
1099
  /** Size of the node pool. */
1100
  size_t poolSize() const;
1101
1102
  /** Deletes a list of attributes from the NM's AttributeManager.*/
1103
  void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
1104
1105
  /**
1106
   * This function gives developers a hook into the NodeManager.
1107
   * This can be changed in node_manager.cpp without recompiling most of cvc4.
1108
   *
1109
   * debugHook is a debugging only function, and should not be present in
1110
   * any published code!
1111
   */
1112
  void debugHook(int debugFlag);
1113
}; /* class NodeManager */
1114
1115
/**
1116
 * This class changes the "current" thread-global
1117
 * <code>NodeManager</code> when it is created and reinstates the
1118
 * previous thread-global <code>NodeManager</code> when it is
1119
 * destroyed, effectively maintaining a set of nested
1120
 * <code>NodeManager</code> scopes.  This is especially useful on
1121
 * public-interface calls into the CVC4 library, where CVC4's notion
1122
 * of the "current" <code>NodeManager</code> should be set to match
1123
 * the calling context.  See, for example, the implementations of
1124
 * public calls in the <code>SmtEngine</code> class.
1125
 *
1126
 * The client must be careful to create and destroy
1127
 * <code>NodeManagerScope</code> objects in a well-nested manner (such
1128
 * as on the stack). You may create a <code>NodeManagerScope</code>
1129
 * with <code>new</code> and destroy it with <code>delete</code>, or
1130
 * place it as a data member of an object that is, but if the scope of
1131
 * these <code>new</code>/<code>delete</code> pairs isn't properly
1132
 * maintained, the incorrect "current" <code>NodeManager</code>
1133
 * pointer may be restored after a delete.
1134
 */
1135
class NodeManagerScope {
1136
  /** The old NodeManager, to be restored on destruction. */
1137
  NodeManager* d_oldNodeManager;
1138
public:
1139
992765796
 NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
1140
 {
1141
992765796
   NodeManager::s_current = nm;
1142
992765796
   Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
1143
992765796
  }
1144
1145
1985531550
  ~NodeManagerScope() {
1146
992765775
    NodeManager::s_current = d_oldNodeManager;
1147
1985531550
    Debug("current") << "node manager scope: "
1148
992765775
                     << "returning to " << NodeManager::s_current << "\n";
1149
992765775
  }
1150
};/* class NodeManagerScope */
1151
1152
778782
inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
1153
1557564
  std::vector<TypeNode> typeNodes;
1154
2508463
  for (unsigned i = 0; i < types.size(); ++ i) {
1155
1729681
    typeNodes.push_back(types[i]);
1156
  }
1157
1557564
  return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
1158
}
1159
1160
10852
inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
1161
                                         TypeNode constituentType) {
1162
10852
  CheckArgument(!indexType.isNull(), indexType,
1163
                "unexpected NULL index type");
1164
10852
  CheckArgument(!constituentType.isNull(), constituentType,
1165
                "unexpected NULL constituent type");
1166
10852
  CheckArgument(indexType.isFirstClass(),
1167
                indexType,
1168
                "cannot index arrays by types that are not first-class. Try "
1169
                "option --uf-ho.");
1170
10852
  CheckArgument(constituentType.isFirstClass(),
1171
                constituentType,
1172
                "cannot store types that are not first-class in arrays. Try "
1173
                "option --uf-ho.");
1174
21704
  Debug("arrays") << "making array type " << indexType << " "
1175
10852
                  << constituentType << std::endl;
1176
10852
  return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
1177
}
1178
1179
13328
inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
1180
13328
  CheckArgument(!elementType.isNull(), elementType,
1181
                "unexpected NULL element type");
1182
13328
  CheckArgument(elementType.isFirstClass(),
1183
                elementType,
1184
                "cannot store types that are not first-class in sets. Try "
1185
                "option --uf-ho.");
1186
13328
  Debug("sets") << "making sets type " << elementType << std::endl;
1187
13328
  return mkTypeNode(kind::SET_TYPE, elementType);
1188
}
1189
1190
22341
inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
1191
22341
  CheckArgument(domain.isDatatype(), domain,
1192
                "cannot create non-datatype selector type");
1193
22341
  CheckArgument(range.isFirstClass(),
1194
                range,
1195
                "cannot have selector fields that are not first-class types. "
1196
                "Try option --uf-ho.");
1197
22341
  return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
1198
}
1199
1200
19296
inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
1201
19296
  CheckArgument(domain.isDatatype(), domain,
1202
                "cannot create non-datatype tester");
1203
19296
  return mkTypeNode(kind::TESTER_TYPE, domain );
1204
}
1205
1206
472127588
inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
1207
472127588
  NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
1208
472127588
  if(find == d_nodeValuePool.end()) {
1209
28498540
    return NULL;
1210
  } else {
1211
443629048
    return *find;
1212
  }
1213
}
1214
1215
28505705
inline void NodeManager::poolInsert(expr::NodeValue* nv) {
1216
28505705
  Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end())
1217
      << "NodeValue already in the pool!";
1218
28505705
  d_nodeValuePool.insert(nv);// FIXME multithreading
1219
28505705
}
1220
1221
28498973
inline void NodeManager::poolRemove(expr::NodeValue* nv) {
1222
28498973
  Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end())
1223
      << "NodeValue is not in the pool!";
1224
1225
28498973
  d_nodeValuePool.erase(nv);// FIXME multithreading
1226
28498973
}
1227
1228
}/* CVC4 namespace */
1229
1230
#define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1231
#include "expr/metakind.h"
1232
#undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1233
1234
#include "expr/node_builder.h"
1235
1236
namespace CVC4 {
1237
1238
// general expression-builders
1239
1240
17082492
inline bool NodeManager::hasOperator(Kind k) {
1241
17082492
  switch(kind::MetaKind mk = kind::metaKindOf(k)) {
1242
1243
1880808
  case kind::metakind::INVALID:
1244
  case kind::metakind::VARIABLE:
1245
  case kind::metakind::NULLARY_OPERATOR:
1246
1880808
    return false;
1247
1248
13532411
  case kind::metakind::OPERATOR:
1249
  case kind::metakind::PARAMETERIZED:
1250
13532411
    return true;
1251
1252
1669273
  case kind::metakind::CONSTANT:
1253
1669273
    return false;
1254
1255
  default: Unhandled() << mk;
1256
  }
1257
}
1258
1259
638779
inline Kind NodeManager::operatorToKind(TNode n) {
1260
638779
  return kind::operatorToKind(n.d_nv);
1261
}
1262
1263
70091789
inline Node NodeManager::mkNode(Kind kind, TNode child1) {
1264
140183578
  NodeBuilder<1> nb(this, kind);
1265
70091789
  nb << child1;
1266
140183566
  return nb.constructNode();
1267
}
1268
1269
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
1270
  NodeBuilder<1> nb(this, kind);
1271
  nb << child1;
1272
  return nb.constructNodePtr();
1273
}
1274
1275
100539681
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
1276
201079362
  NodeBuilder<2> nb(this, kind);
1277
100539681
  nb << child1 << child2;
1278
201078988
  return nb.constructNode();
1279
}
1280
1281
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
1282
  NodeBuilder<2> nb(this, kind);
1283
  nb << child1 << child2;
1284
  return nb.constructNodePtr();
1285
}
1286
1287
716487
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1288
                                TNode child3) {
1289
1432974
  NodeBuilder<3> nb(this, kind);
1290
716487
  nb << child1 << child2 << child3;
1291
1432944
  return nb.constructNode();
1292
}
1293
1294
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1295
                                TNode child3) {
1296
  NodeBuilder<3> nb(this, kind);
1297
  nb << child1 << child2 << child3;
1298
  return nb.constructNodePtr();
1299
}
1300
1301
1071
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1302
                                TNode child3, TNode child4) {
1303
2142
  NodeBuilder<4> nb(this, kind);
1304
1071
  nb << child1 << child2 << child3 << child4;
1305
2142
  return nb.constructNode();
1306
}
1307
1308
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1309
                                TNode child3, TNode child4) {
1310
  NodeBuilder<4> nb(this, kind);
1311
  nb << child1 << child2 << child3 << child4;
1312
  return nb.constructNodePtr();
1313
}
1314
1315
28
inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1316
                                TNode child3, TNode child4, TNode child5) {
1317
56
  NodeBuilder<5> nb(this, kind);
1318
28
  nb << child1 << child2 << child3 << child4 << child5;
1319
56
  return nb.constructNode();
1320
}
1321
1322
inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1323
                                    TNode child3, TNode child4, TNode child5) {
1324
  NodeBuilder<5> nb(this, kind);
1325
  nb << child1 << child2 << child3 << child4 << child5;
1326
  return nb.constructNodePtr();
1327
}
1328
1329
// N-ary version
1330
template <bool ref_count>
1331
16138980
inline Node NodeManager::mkNode(Kind kind,
1332
                                const std::vector<NodeTemplate<ref_count> >&
1333
                                children) {
1334
32277960
  NodeBuilder<> nb(this, kind);
1335
16138980
  nb.append(children);
1336
32277930
  return nb.constructNode();
1337
}
1338
1339
template <bool ref_count>
1340
765372
Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children)
1341
{
1342
765372
  if (children.empty())
1343
  {
1344
28092
    return mkConst(true);
1345
  }
1346
737280
  else if (children.size() == 1)
1347
  {
1348
520169
    return children[0];
1349
  }
1350
217111
  return mkNode(kind::AND, children);
1351
}
1352
1353
template <bool ref_count>
1354
Node NodeManager::mkOr(const std::vector<NodeTemplate<ref_count> >& children)
1355
{
1356
  if (children.empty())
1357
  {
1358
    return mkConst(false);
1359
  }
1360
  else if (children.size() == 1)
1361
  {
1362
    return children[0];
1363
  }
1364
  return mkNode(kind::OR, children);
1365
}
1366
1367
template <bool ref_count>
1368
inline Node* NodeManager::mkNodePtr(Kind kind,
1369
                                const std::vector<NodeTemplate<ref_count> >&
1370
                                children) {
1371
  NodeBuilder<> nb(this, kind);
1372
  nb.append(children);
1373
  return nb.constructNodePtr();
1374
}
1375
1376
// for operators
1377
inline Node NodeManager::mkNode(TNode opNode) {
1378
  NodeBuilder<1> nb(this, operatorToKind(opNode));
1379
  if(opNode.getKind() != kind::BUILTIN) {
1380
    nb << opNode;
1381
  }
1382
  return nb.constructNode();
1383
}
1384
1385
inline Node* NodeManager::mkNodePtr(TNode opNode) {
1386
  NodeBuilder<1> nb(this, operatorToKind(opNode));
1387
  if(opNode.getKind() != kind::BUILTIN) {
1388
    nb << opNode;
1389
  }
1390
  return nb.constructNodePtr();
1391
}
1392
1393
246249
inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
1394
492498
  NodeBuilder<2> nb(this, operatorToKind(opNode));
1395
246249
  if(opNode.getKind() != kind::BUILTIN) {
1396
246249
    nb << opNode;
1397
  }
1398
246249
  nb << child1;
1399
492498
  return nb.constructNode();
1400
}
1401
1402
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
1403
  NodeBuilder<2> nb(this, operatorToKind(opNode));
1404
  if(opNode.getKind() != kind::BUILTIN) {
1405
    nb << opNode;
1406
  }
1407
  nb << child1;
1408
  return nb.constructNodePtr();
1409
}
1410
1411
22
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
1412
44
  NodeBuilder<3> nb(this, operatorToKind(opNode));
1413
22
  if(opNode.getKind() != kind::BUILTIN) {
1414
22
    nb << opNode;
1415
  }
1416
22
  nb << child1 << child2;
1417
44
  return nb.constructNode();
1418
}
1419
1420
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
1421
  NodeBuilder<3> nb(this, operatorToKind(opNode));
1422
  if(opNode.getKind() != kind::BUILTIN) {
1423
    nb << opNode;
1424
  }
1425
  nb << child1 << child2;
1426
  return nb.constructNodePtr();
1427
}
1428
1429
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1430
                                TNode child3) {
1431
  NodeBuilder<4> nb(this, operatorToKind(opNode));
1432
  if(opNode.getKind() != kind::BUILTIN) {
1433
    nb << opNode;
1434
  }
1435
  nb << child1 << child2 << child3;
1436
  return nb.constructNode();
1437
}
1438
1439
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1440
                                TNode child3) {
1441
  NodeBuilder<4> nb(this, operatorToKind(opNode));
1442
  if(opNode.getKind() != kind::BUILTIN) {
1443
    nb << opNode;
1444
  }
1445
  nb << child1 << child2 << child3;
1446
  return nb.constructNodePtr();
1447
}
1448
1449
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1450
                                TNode child3, TNode child4) {
1451
  NodeBuilder<5> nb(this, operatorToKind(opNode));
1452
  if(opNode.getKind() != kind::BUILTIN) {
1453
    nb << opNode;
1454
  }
1455
  nb << child1 << child2 << child3 << child4;
1456
  return nb.constructNode();
1457
}
1458
1459
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1460
                                TNode child3, TNode child4) {
1461
  NodeBuilder<5> nb(this, operatorToKind(opNode));
1462
  if(opNode.getKind() != kind::BUILTIN) {
1463
    nb << opNode;
1464
  }
1465
  nb << child1 << child2 << child3 << child4;
1466
  return nb.constructNodePtr();
1467
}
1468
1469
inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1470
                                TNode child3, TNode child4, TNode child5) {
1471
  NodeBuilder<6> nb(this, operatorToKind(opNode));
1472
  if(opNode.getKind() != kind::BUILTIN) {
1473
    nb << opNode;
1474
  }
1475
  nb << child1 << child2 << child3 << child4 << child5;
1476
  return nb.constructNode();
1477
}
1478
1479
inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1480
                                    TNode child3, TNode child4, TNode child5) {
1481
  NodeBuilder<6> nb(this, operatorToKind(opNode));
1482
  if(opNode.getKind() != kind::BUILTIN) {
1483
    nb << opNode;
1484
  }
1485
  nb << child1 << child2 << child3 << child4 << child5;
1486
  return nb.constructNodePtr();
1487
}
1488
1489
// N-ary version for operators
1490
template <bool ref_count>
1491
66500
inline Node NodeManager::mkNode(TNode opNode,
1492
                                const std::vector<NodeTemplate<ref_count> >&
1493
                                children) {
1494
133000
  NodeBuilder<> nb(this, operatorToKind(opNode));
1495
66500
  if(opNode.getKind() != kind::BUILTIN) {
1496
865
    nb << opNode;
1497
  }
1498
66500
  nb.append(children);
1499
133000
  return nb.constructNode();
1500
}
1501
1502
template <bool ref_count>
1503
inline Node* NodeManager::mkNodePtr(TNode opNode,
1504
                                    const std::vector<NodeTemplate<ref_count> >&
1505
                                    children) {
1506
  NodeBuilder<> nb(this, operatorToKind(opNode));
1507
  if(opNode.getKind() != kind::BUILTIN) {
1508
    nb << opNode;
1509
  }
1510
  nb.append(children);
1511
  return nb.constructNodePtr();
1512
}
1513
1514
1515
33753
inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
1516
33753
  return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
1517
}
1518
1519
33193
inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1520
                                        TypeNode child2) {
1521
33193
  return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
1522
}
1523
1524
inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1525
                                        TypeNode child2, TypeNode child3) {
1526
  return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
1527
}
1528
1529
// N-ary version for types
1530
854288
inline TypeNode NodeManager::mkTypeNode(Kind kind,
1531
                                        const std::vector<TypeNode>& children) {
1532
854288
  return NodeBuilder<>(this, kind).append(children).constructTypeNode();
1533
}
1534
1535
template <class T>
1536
186303156
Node NodeManager::mkConst(const T& val) {
1537
186303156
  return mkConstInternal<Node, T>(val);
1538
}
1539
1540
template <class T>
1541
29090985
TypeNode NodeManager::mkTypeConst(const T& val) {
1542
29090985
  return mkConstInternal<TypeNode, T>(val);
1543
}
1544
1545
template <class NodeClass, class T>
1546
215394141
NodeClass NodeManager::mkConstInternal(const T& val) {
1547
  // This method indirectly calls `NodeValue::inc()`, which relies on having
1548
  // the correct `NodeManager` in scope.
1549
430788282
  NodeManagerScope nms(this);
1550
1551
  // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1552
215394141
  NVStorage<1> nvStorage;
1553
215394141
  expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
1554
1555
215394141
  nvStack.d_id = 0;
1556
215394141
  nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
1557
215394141
  nvStack.d_rc = 0;
1558
215394141
  nvStack.d_nchildren = 1;
1559
1560
#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1561
#pragma GCC diagnostic push
1562
#pragma GCC diagnostic ignored "-Warray-bounds"
1563
#endif
1564
1565
215394141
  nvStack.d_children[0] =
1566
    const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
1567
215394141
  expr::NodeValue* nv = poolLookup(&nvStack);
1568
1569
#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1570
#pragma GCC diagnostic pop
1571
#endif
1572
1573
215394141
  if(nv != NULL) {
1574
212954445
    return NodeClass(nv);
1575
  }
1576
1577
2439696
  nv = (expr::NodeValue*)
1578
2439696
    std::malloc(sizeof(expr::NodeValue) + sizeof(T));
1579
2439696
  if(nv == NULL) {
1580
    throw std::bad_alloc();
1581
  }
1582
1583
2439696
  nv->d_nchildren = 0;
1584
2439696
  nv->d_kind = kind::metakind::ConstantMap<T>::kind;
1585
2439696
  nv->d_id = next_id++;// FIXME multithreading
1586
2439696
  nv->d_rc = 0;
1587
1588
  //OwningTheory::mkConst(val);
1589
2439696
  new (&nv->d_children) T(val);
1590
1591
2439696
  poolInsert(nv);
1592
2439696
  if(Debug.isOn("gc")) {
1593
    Debug("gc") << "creating node value " << nv
1594
                << " [" << nv->d_id << "]: ";
1595
    nv->printAst(Debug("gc"));
1596
    Debug("gc") << std::endl;
1597
  }
1598
1599
2439696
  return NodeClass(nv);
1600
}
1601
1602
}/* CVC4 namespace */
1603
1604
#endif /* CVC4__NODE_MANAGER_H */