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