src/expr/node_manager.h

   1 /*********************                                                        */
   2 /*! \file node_manager.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Christopher L. Conway, Morgan Deters
   6  ** Minor contributors (to current version): ACSYS, Tianyi Liang, Kshitij Bansal, Tim King
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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 #include "expr/expr.h"
  26 #include "expr/expr_manager.h"
  27
  28 #ifndef __CVC4__NODE_MANAGER_H
  29 #define __CVC4__NODE_MANAGER_H
  30
  31 #include <vector>
  32 #include <string>
  33 #include <ext/hash_set>
  34
  35 #include "expr/kind.h"
  36 #include "expr/metakind.h"
  37 #include "expr/node_value.h"
  38 #include "util/subrange_bound.h"
  39 #include "util/tls.h"
  40 #include "options/options.h"
  41
  42 namespace CVC4 {
  43
  44 class StatisticsRegistry;
  45
  46 namespace expr {
  47   namespace attr {
  48     class AttributeUniqueId;
  49     class AttributeManager;
  50   }/* CVC4::expr::attr namespace */
  51
  52   class TypeChecker;
  53 }/* CVC4::expr namespace */
  54
  55 /**
  56  * An interface that an interested party can implement and then subscribe
  57  * to NodeManager events via NodeManager::subscribeEvents(this).
  58  */
  59 class NodeManagerListener {
  60 public:
  61   virtual ~NodeManagerListener() { }
  62   virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) { }
  63   virtual void nmNotifyNewSortConstructor(TypeNode tn) { }
  64   virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) { }
  65   virtual void nmNotifyNewDatatypes(const std::vector<DatatypeType>& datatypes) { }
  66   virtual void nmNotifyNewVar(TNode n, uint32_t flags) { }
  67   virtual void nmNotifyNewSkolem(TNode n, const std::string& comment, uint32_t flags) { }
  68   /**
  69    * Notify a listener of a Node that's being GCed.  If this function stores a reference
  70    * to the Node somewhere, very bad things will happen.
  71    */
  72   virtual void nmNotifyDeleteNode(TNode n) { }
  73 };/* class NodeManagerListener */
  74
  75 class NodeManager {
  76   template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
  77   friend class NodeManagerScope;
  78   friend class expr::NodeValue;
  79   friend class expr::TypeChecker;
  80
  81   // friends so they can access mkVar() here, which is private
  82   friend Expr ExprManager::mkVar(const std::string&, Type, uint32_t flags);
  83   friend Expr ExprManager::mkVar(Type, uint32_t flags);
  84
  85   // friend so it can access NodeManager's d_listeners and notify clients
  86   friend std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(const std::vector<Datatype>&, const std::set<Type>&);
  87
  88   /** Predicate for use with STL algorithms */
  89   struct NodeValueReferenceCountNonZero {
  90     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
  91   };
  92
  93   typedef __gnu_cxx::hash_set<expr::NodeValue*,
  94                               expr::NodeValuePoolHashFunction,
  95                               expr::NodeValuePoolEq> NodeValuePool;
  96   typedef __gnu_cxx::hash_set<expr::NodeValue*,
  97                               expr::NodeValueIDHashFunction,
  98                               expr::NodeValueEq> ZombieSet;
  99
 100   static CVC4_THREADLOCAL(NodeManager*) s_current;
 101
 102   Options* d_options;
 103   StatisticsRegistry* d_statisticsRegistry;
 104
 105   NodeValuePool d_nodeValuePool;
 106
 107   size_t next_id;
 108
 109   expr::attr::AttributeManager* d_attrManager;
 110
 111   /** The associated ExprManager */
 112   ExprManager* d_exprManager;
 113
 114   /**
 115    * The node value we're currently freeing.  This unique node value
 116    * is permitted to have outstanding TNodes to it (in "soft"
 117    * contexts, like as a key in attribute tables), even though
 118    * normally it's an error to have a TNode to a node value with a
 119    * reference count of 0.  Being "under deletion" also enables
 120    * assertions that inc() is not called on it.  (A poorly-behaving
 121    * attribute cleanup function could otherwise create a "Node" that
 122    * points to the node value that is in the process of being deleted,
 123    * springing it back to life.)
 124    */
 125   expr::NodeValue* d_nodeUnderDeletion;
 126
 127   /**
 128    * True iff we are in reclaimZombies().  This avoids unnecessary
 129    * recursion; a NodeValue being deleted might zombify other
 130    * NodeValues, but these shouldn't trigger a (recursive) call to
 131    * reclaimZombies().
 132    */
 133   bool d_inReclaimZombies;
 134
 135   /**
 136    * The set of zombie nodes.  We may want to revisit this design, as
 137    * we might like to delete nodes in least-recently-used order.  But
 138    * we also need to avoid processing a zombie twice.
 139    */
 140   ZombieSet d_zombies;
 141
 142   /**
 143    * A set of operator singletons (w.r.t.  to this NodeManager
 144    * instance) for operators.  Conceptually, Nodes with kind, say,
 145    * PLUS, are APPLYs of a PLUS operator to arguments.  This array
 146    * holds the set of operators for these things.  A PLUS operator is
 147    * a Node with kind "BUILTIN", and if you call
 148    * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
 149    */
 150   Node d_operators[kind::LAST_KIND];
 151
 152   /**
 153    * A list of subscribers for NodeManager events.
 154    */
 155   std::vector<NodeManagerListener*> d_listeners;
 156
 157   /**
 158    * A map of tuple and record types to their corresponding datatype.
 159    */
 160   std::hash_map<TypeNode, TypeNode, TypeNodeHashFunction> d_tupleAndRecordTypes;
 161
 162   /**
 163    * Keep a count of all abstract values produced by this NodeManager.
 164    * Abstract values have a type attribute, so if multiple SmtEngines
 165    * are attached to this NodeManager, we don't want their abstract
 166    * values to overlap.
 167    */
 168   unsigned d_abstractValueCount;
 169
 170   /**
 171    * A counter used to produce unique skolem names.
 172    *
 173    * Note that it is NOT incremented when skolems are created using
 174    * SKOLEM_EXACT_NAME, so it is NOT a count of the skolems produced
 175    * by this node manager.
 176    */
 177   unsigned d_skolemCounter;
 178
 179   /**
 180    * Look up a NodeValue in the pool associated to this NodeManager.
 181    * The NodeValue argument need not be a "completely-constructed"
 182    * NodeValue.  In particular, "non-inlined" constants are permitted
 183    * (see below).
 184    *
 185    * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
 186    * correctly set, and d_children[0..n-1] should be valid (extant)
 187    * NodeValues for lookup.
 188    *
 189    * For CONSTANT metakinds, nv's d_kind should be set correctly.
 190    * Normally a CONSTANT would have d_nchildren == 0 and the constant
 191    * value inlined in the d_children space.  However, here we permit
 192    * "non-inlined" NodeValues to avoid unnecessary copying.  For
 193    * these, d_nchildren == 1, and d_nchildren is a pointer to the
 194    * constant value.
 195    *
 196    * The point of this complex design is to permit efficient lookups
 197    * (without fully constructing a NodeValue).  In the case that the
 198    * argument is not fully constructed, and this function returns
 199    * NULL, the caller should fully construct an equivalent one before
 200    * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
 201    * permitted in the pool!
 202    */
 203   inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
 204
 205   /**
 206    * Insert a NodeValue into the NodeManager's pool.
 207    *
 208    * It is an error to insert a NodeValue already in the pool.
 209    * Enquire first with poolLookup().
 210    */
 211   inline void poolInsert(expr::NodeValue* nv);
 212
 213   /**
 214    * Remove a NodeValue from the NodeManager's pool.
 215    *
 216    * It is an error to request the removal of a NodeValue from the
 217    * pool that is not in the pool.
 218    */
 219   inline void poolRemove(expr::NodeValue* nv);
 220
 221   /**
 222    * Determine if nv is currently being deleted by the NodeManager.
 223    */
 224   inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
 225     return d_nodeUnderDeletion == nv;
 226   }
 227
 228   /**
 229    * Register a NodeValue as a zombie.
 230    */
 231   inline void markForDeletion(expr::NodeValue* nv) {
 232     Assert(nv->d_rc == 0);
 233
 234     // if d_reclaiming is set, make sure we don't call
 235     // reclaimZombies(), because it's already running.
 236     if(Debug.isOn("gc")) {
 237       Debug("gc") << "zombifying node value " << nv
 238                   << " [" << nv->d_id << "]: ";
 239       nv->printAst(Debug("gc"));
 240       Debug("gc") << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "")
 241                   << std::endl;
 242     }
 243     d_zombies.insert(nv);// FIXME multithreading
 244
 245     if(safeToReclaimZombies()) {
 246       if(d_zombies.size() > 5000) {
 247         reclaimZombies();
 248       }
 249     }
 250   }
 251
 252   /**
 253    * Reclaim all zombies.
 254    */
 255   void reclaimZombies();
 256
 257   /**
 258    * It is safe to collect zombies.
 259    */
 260   bool safeToReclaimZombies() const;
 261
 262   /**
 263    * This template gives a mechanism to stack-allocate a NodeValue
 264    * with enough space for N children (where N is a compile-time
 265    * constant).  You use it like this:
 266    *
 267    *   NVStorage<4> nvStorage;
 268    *   NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
 269    *
 270    * ...and then you can use nvStack as a NodeValue that you know has
 271    * room for 4 children.
 272    */
 273   template <size_t N>
 274   struct NVStorage {
 275     expr::NodeValue nv;
 276     expr::NodeValue* child[N];
 277   };/* struct NodeManager::NVStorage<N> */
 278
 279   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
 280    *
 281    * It has been decided for now to hold off on implementations of
 282    * these functions, as they may only be needed in CNF conversion,
 283    * where it's pointless to do a lazy isAtomic determination by
 284    * searching through the DAG, and storing it, since the result will
 285    * only be used once.  For more details see the 4/27/2010 CVC4
 286    * developer's meeting notes at:
 287    *
 288    * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
 289    */
 290   // bool containsDecision(TNode); // is "atomic"
 291   // bool properlyContainsDecision(TNode); // all children are atomic
 292
 293   // undefined private copy constructor (disallow copy)
 294   NodeManager(const NodeManager&) CVC4_UNDEFINED;
 295
 296   void init();
 297
 298   /**
 299    * Create a variable with the given name and type.  NOTE that no
 300    * lookup is done on the name.  If you mkVar("a", type) and then
 301    * mkVar("a", type) again, you have two variables.  The NodeManager
 302    * version of this is private to avoid internal uses of mkVar() from
 303    * within CVC4.  Such uses should employ mkSkolem() instead.
 304    */
 305   Node mkVar(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 306   Node* mkVarPtr(const std::string& name, const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 307
 308   /** Create a variable with the given type. */
 309   Node mkVar(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 310   Node* mkVarPtr(const TypeNode& type, uint32_t flags = ExprManager::VAR_FLAG_NONE);
 311
 312 public:
 313
 314   explicit NodeManager(ExprManager* exprManager);
 315   explicit NodeManager(ExprManager* exprManager, const Options& options);
 316   ~NodeManager();
 317
 318   /** The node manager in the current public-facing CVC4 library context */
 319   static NodeManager* currentNM() { return s_current; }
 320
 321   /** Get this node manager's options (const version) */
 322   const Options& getOptions() const {
 323     return *d_options;
 324   }
 325
 326   /** Get this node manager's options (non-const version) */
 327   Options& getOptions() {
 328     return *d_options;
 329   }
 330
 331   /** Get this node manager's statistics registry */
 332   StatisticsRegistry* getStatisticsRegistry() const throw() {
 333     return d_statisticsRegistry;
 334   }
 335
 336   /** Subscribe to NodeManager events */
 337   void subscribeEvents(NodeManagerListener* listener) {
 338     Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed");
 339     d_listeners.push_back(listener);
 340   }
 341
 342   /** Unsubscribe from NodeManager events */
 343   void unsubscribeEvents(NodeManagerListener* listener) {
 344     std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener);
 345     Assert(elt != d_listeners.end(), "listener not subscribed");
 346     d_listeners.erase(elt);
 347   }
 348
 349   /** Get a Kind from an operator expression */
 350   static inline Kind operatorToKind(TNode n);
 351
 352   // general expression-builders
 353
 354   /** Create a node with one child. */
 355   Node mkNode(Kind kind, TNode child1);
 356   Node* mkNodePtr(Kind kind, TNode child1);
 357
 358   /** Create a node with two children. */
 359   Node mkNode(Kind kind, TNode child1, TNode child2);
 360   Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
 361
 362   /** Create a node with three children. */
 363   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 364   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
 365
 366   /** Create a node with four children. */
 367   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 368               TNode child4);
 369   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 370               TNode child4);
 371
 372   /** Create a node with five children. */
 373   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 374               TNode child4, TNode child5);
 375   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 376               TNode child4, TNode child5);
 377
 378   /** Create a node with an arbitrary number of children. */
 379   template <bool ref_count>
 380   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 381   template <bool ref_count>
 382   Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 383
 384   /** Create a node (with no children) by operator. */
 385   Node mkNode(TNode opNode);
 386   Node* mkNodePtr(TNode opNode);
 387
 388   /** Create a node with one child by operator. */
 389   Node mkNode(TNode opNode, TNode child1);
 390   Node* mkNodePtr(TNode opNode, TNode child1);
 391
 392   /** Create a node with two children by operator. */
 393   Node mkNode(TNode opNode, TNode child1, TNode child2);
 394   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
 395
 396   /** Create a node with three children by operator. */
 397   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
 398   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
 399
 400   /** Create a node with four children by operator. */
 401   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
 402               TNode child4);
 403   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
 404               TNode child4);
 405
 406   /** Create a node with five children by operator. */
 407   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
 408               TNode child4, TNode child5);
 409   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
 410               TNode child4, TNode child5);
 411
 412   /** Create a node by applying an operator to the children. */
 413   template <bool ref_count>
 414   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 415   template <bool ref_count>
 416   Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 417
 418   Node mkBoundVar(const std::string& name, const TypeNode& type);
 419   Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
 420
 421   Node mkBoundVar(const TypeNode& type);
 422   Node* mkBoundVarPtr(const TypeNode& type);
 423
 424   /**
 425    * Optional flags used to control behavior of NodeManager::mkSkolem().
 426    * They should be composed with a bitwise OR (e.g.,
 427    * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
 428    * cannot be composed in such a manner.
 429    */
 430   enum SkolemFlags {
 431     SKOLEM_DEFAULT = 0,   /**< default behavior */
 432     SKOLEM_NO_NOTIFY = 1, /**< do not notify subscribers */
 433     SKOLEM_EXACT_NAME = 2,/**< do not make the name unique by adding the id */
 434     SKOLEM_IS_GLOBAL = 4  /**< global vars appear in models even after a pop */
 435   };/* enum SkolemFlags */
 436
 437   /**
 438    * Create a skolem constant with the given name, type, and comment.
 439    *
 440    * @param prefix the name of the new skolem variable is the prefix
 441    * appended with a unique ID.  This way a family of skolem variables
 442    * can be made with unique identifiers, used in dump, tracing, and
 443    * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
 444    * a unique ID appended and use prefix as the name.
 445    *
 446    * @param type the type of the skolem variable to create
 447    *
 448    * @param comment a comment for dumping output; if declarations are
 449    * being dumped, this is included in a comment before the declaration
 450    * and can be quite useful for debugging
 451    *
 452    * @param flags an optional mask of bits from SkolemFlags to control
 453    * mkSkolem() behavior
 454    */
 455   Node mkSkolem(const std::string& prefix, const TypeNode& type,
 456                 const std::string& comment = "", int flags = SKOLEM_DEFAULT);
 457
 458   /** Create a instantiation constant with the given type. */
 459   Node mkInstConstant(const TypeNode& type);
 460
 461   /** Make a new abstract value with the given type. */
 462   Node mkAbstractValue(const TypeNode& type);
 463
 464   /**
 465    * Create a constant of type T.  It will have the appropriate
 466    * CONST_* kind defined for T.
 467    */
 468   template <class T>
 469   Node mkConst(const T&);
 470
 471   template <class T>
 472   TypeNode mkTypeConst(const T&);
 473
 474   template <class NodeClass, class T>
 475   NodeClass mkConstInternal(const T&);
 476
 477   /** Create a node with children. */
 478   TypeNode mkTypeNode(Kind kind, TypeNode child1);
 479   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
 480   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
 481                       TypeNode child3);
 482   TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
 483
 484   /**
 485    * Determine whether Nodes of a particular Kind have operators.
 486    * @returns true if Nodes of Kind k have operators.
 487    */
 488   static inline bool hasOperator(Kind k);
 489
 490   /**
 491    * Get the (singleton) operator of an OPERATOR-kinded kind.  The
 492    * returned node n will have kind BUILTIN, and calling
 493    * n.getConst<CVC4::Kind>() will yield k.
 494    */
 495   inline TNode operatorOf(Kind k) {
 496     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
 497                     "Kind is not an OPERATOR-kinded kind "
 498                     "in NodeManager::operatorOf()" );
 499     return d_operators[k];
 500   }
 501
 502   /**
 503    * Retrieve an attribute for a node.
 504    *
 505    * @param nv the node value
 506    * @param attr an instance of the attribute kind to retrieve.
 507    * @returns the attribute, if set, or a default-constructed
 508    * <code>AttrKind::value_type</code> if not.
 509    */
 510   template <class AttrKind>
 511   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
 512                                                     const AttrKind& attr) const;
 513
 514   /**
 515    * Check whether an attribute is set for a node.
 516    *
 517    * @param nv the node value
 518    * @param attr an instance of the attribute kind to check
 519    * @returns <code>true</code> iff <code>attr</code> is set for
 520    * <code>nv</code>.
 521    */
 522   template <class AttrKind>
 523   inline bool hasAttribute(expr::NodeValue* nv,
 524                            const AttrKind& attr) const;
 525
 526   /**
 527    * Check whether an attribute is set for a node, and, if so,
 528    * retrieve it.
 529    *
 530    * @param nv the node value
 531    * @param attr an instance of the attribute kind to check
 532    * @param value a reference to an object of the attribute's value type.
 533    * <code>value</code> will be set to the value of the attribute, if it is
 534    * set for <code>nv</code>; otherwise, it will be set to the default
 535    * value of the attribute.
 536    * @returns <code>true</code> iff <code>attr</code> is set for
 537    * <code>nv</code>.
 538    */
 539   template <class AttrKind>
 540   inline bool getAttribute(expr::NodeValue* nv,
 541                            const AttrKind& attr,
 542                            typename AttrKind::value_type& value) const;
 543
 544   /**
 545    * Set an attribute for a node.  If the node doesn't have the
 546    * attribute, this function assigns one.  If the node has one, this
 547    * overwrites it.
 548    *
 549    * @param nv the node value
 550    * @param attr an instance of the attribute kind to set
 551    * @param value the value of <code>attr</code> for <code>nv</code>
 552    */
 553   template <class AttrKind>
 554   inline void setAttribute(expr::NodeValue* nv,
 555                            const AttrKind& attr,
 556                            const typename AttrKind::value_type& value);
 557
 558   /**
 559    * Retrieve an attribute for a TNode.
 560    *
 561    * @param n the node
 562    * @param attr an instance of the attribute kind to retrieve.
 563    * @returns the attribute, if set, or a default-constructed
 564    * <code>AttrKind::value_type</code> if not.
 565    */
 566   template <class AttrKind>
 567   inline typename AttrKind::value_type
 568   getAttribute(TNode n, const AttrKind& attr) const;
 569
 570   /**
 571    * Check whether an attribute is set for a TNode.
 572    *
 573    * @param n the node
 574    * @param attr an instance of the attribute kind to check
 575    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 576    */
 577   template <class AttrKind>
 578   inline bool hasAttribute(TNode n,
 579                            const AttrKind& attr) const;
 580
 581   /**
 582    * Check whether an attribute is set for a TNode and, if so, retieve
 583    * it.
 584    *
 585    * @param n the node
 586    * @param attr an instance of the attribute kind to check
 587    * @param value a reference to an object of the attribute's value type.
 588    * <code>value</code> will be set to the value of the attribute, if it is
 589    * set for <code>nv</code>; otherwise, it will be set to the default value of
 590    * the attribute.
 591    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 592    */
 593   template <class AttrKind>
 594   inline bool getAttribute(TNode n,
 595                            const AttrKind& attr,
 596                            typename AttrKind::value_type& value) const;
 597
 598   /**
 599    * Set an attribute for a node.  If the node doesn't have the
 600    * attribute, this function assigns one.  If the node has one, this
 601    * overwrites it.
 602    *
 603    * @param n the node
 604    * @param attr an instance of the attribute kind to set
 605    * @param value the value of <code>attr</code> for <code>n</code>
 606    */
 607   template <class AttrKind>
 608   inline void setAttribute(TNode n,
 609                            const AttrKind& attr,
 610                            const typename AttrKind::value_type& value);
 611
 612   /**
 613    * Retrieve an attribute for a TypeNode.
 614    *
 615    * @param n the type node
 616    * @param attr an instance of the attribute kind to retrieve.
 617    * @returns the attribute, if set, or a default-constructed
 618    * <code>AttrKind::value_type</code> if not.
 619    */
 620   template <class AttrKind>
 621   inline typename AttrKind::value_type
 622   getAttribute(TypeNode n, const AttrKind& attr) const;
 623
 624   /**
 625    * Check whether an attribute is set for a TypeNode.
 626    *
 627    * @param n the type node
 628    * @param attr an instance of the attribute kind to check
 629    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 630    */
 631   template <class AttrKind>
 632   inline bool hasAttribute(TypeNode n,
 633                            const AttrKind& attr) const;
 634
 635   /**
 636    * Check whether an attribute is set for a TypeNode and, if so, retieve
 637    * it.
 638    *
 639    * @param n the type node
 640    * @param attr an instance of the attribute kind to check
 641    * @param value a reference to an object of the attribute's value type.
 642    * <code>value</code> will be set to the value of the attribute, if it is
 643    * set for <code>nv</code>; otherwise, it will be set to the default value of
 644    * the attribute.
 645    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 646    */
 647   template <class AttrKind>
 648   inline bool getAttribute(TypeNode n,
 649                            const AttrKind& attr,
 650                            typename AttrKind::value_type& value) const;
 651
 652   /**
 653    * Set an attribute for a type node.  If the node doesn't have the
 654    * attribute, this function assigns one.  If the type node has one,
 655    * this overwrites it.
 656    *
 657    * @param n the type node
 658    * @param attr an instance of the attribute kind to set
 659    * @param value the value of <code>attr</code> for <code>n</code>
 660    */
 661   template <class AttrKind>
 662   inline void setAttribute(TypeNode n,
 663                            const AttrKind& attr,
 664                            const typename AttrKind::value_type& value);
 665
 666   /** Get the (singleton) type for Booleans. */
 667   inline TypeNode booleanType();
 668
 669   /** Get the (singleton) type for integers. */
 670   inline TypeNode integerType();
 671
 672   /** Get the (singleton) type for reals. */
 673   inline TypeNode realType();
 674
 675   /** Get the (singleton) type for strings. */
 676   inline TypeNode stringType();
 677
 678   /** Get the (singleton) type for RegExp. */
 679   inline TypeNode regexpType();
 680
 681   /** Get the bound var list type. */
 682   inline TypeNode boundVarListType();
 683
 684   /** Get the instantiation pattern type. */
 685   inline TypeNode instPatternType();
 686
 687   /** Get the instantiation pattern type. */
 688   inline TypeNode instPatternListType();
 689
 690   /**
 691    * Get the (singleton) type for builtin operators (that is, the type
 692    * of the Node returned from Node::getOperator() when the operator
 693    * is built-in, like EQUAL). */
 694   inline TypeNode builtinOperatorType();
 695
 696   /**
 697    * Make a function type from domain to range.
 698    *
 699    * @param domain the domain type
 700    * @param range the range type
 701    * @returns the functional type domain -> range
 702    */
 703   inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 704
 705   /**
 706    * Make a function type with input types from
 707    * argTypes. <code>argTypes</code> must have at least one element.
 708    *
 709    * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
 710    * @param range the range type
 711    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
 712    */
 713   inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
 714                                  const TypeNode& range);
 715
 716   /**
 717    * Make a function type with input types from
 718    * <code>sorts[0..sorts.size()-2]</code> and result type
 719    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
 720    * at least 2 elements.
 721    */
 722   inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 723
 724   /**
 725    * Make a predicate type with input types from
 726    * <code>sorts</code>. The result with be a function type with range
 727    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
 728    * element.
 729    */
 730   inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 731
 732   /**
 733    * Make a tuple type with types from
 734    * <code>types</code>. <code>types</code> must have at least one
 735    * element.
 736    *
 737    * @param types a vector of types
 738    * @returns the tuple type (types[0], ..., types[n])
 739    */
 740   inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
 741
 742   /**
 743    * Make a record type with the description from rec.
 744    *
 745    * @param rec a description of the record
 746    * @returns the record type
 747    */
 748   inline TypeNode mkRecordType(const Record& rec);
 749
 750   /**
 751    * Make a symbolic expression type with types from
 752    * <code>types</code>. <code>types</code> may have any number of
 753    * elements.
 754    *
 755    * @param types a vector of types
 756    * @returns the symbolic expression type (types[0], ..., types[n])
 757    */
 758   inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
 759
 760   /** Make the type of bitvectors of size <code>size</code> */
 761   inline TypeNode mkBitVectorType(unsigned size);
 762
 763   /** Make the type of arrays with the given parameterization */
 764   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 765
 766   /** Make the type of arrays with the given parameterization */
 767   inline TypeNode mkSetType(TypeNode elementType);
 768
 769   /** Make a type representing a constructor with the given parameterization */
 770   TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
 771
 772   /** Make a type representing a selector with the given parameterization */
 773   inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
 774
 775   /** Make a type representing a tester with given parameterization */
 776   inline TypeNode mkTesterType(TypeNode domain);
 777
 778   /** Make a new (anonymous) sort of arity 0. */
 779   TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
 780
 781   /** Make a new sort with the given name of arity 0. */
 782   TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
 783
 784   /** Make a new sort by parameterizing the given sort constructor. */
 785   TypeNode mkSort(TypeNode constructor,
 786                   const std::vector<TypeNode>& children,
 787                   uint32_t flags = ExprManager::SORT_FLAG_NONE);
 788
 789   /** Make a new sort with the given name and arity. */
 790   TypeNode mkSortConstructor(const std::string& name, size_t arity);
 791
 792   /**
 793    * Make a predicate subtype type defined by the given LAMBDA
 794    * expression.  A TypeCheckingExceptionPrivate can be thrown if
 795    * lambda is not a LAMBDA, or is ill-typed, or if CVC4 fails at
 796    * proving that the resulting predicate subtype is inhabited.
 797    */
 798   TypeNode mkPredicateSubtype(Expr lambda)
 799     throw(TypeCheckingExceptionPrivate);
 800
 801   /**
 802    * Make a predicate subtype type defined by the given LAMBDA
 803    * expression and whose non-emptiness is witnessed by the given
 804    * witness.  A TypeCheckingExceptionPrivate can be thrown if lambda
 805    * is not a LAMBDA, or is ill-typed, or if the witness is not a
 806    * witness or ill-typed.
 807    */
 808   TypeNode mkPredicateSubtype(Expr lambda, Expr witness)
 809     throw(TypeCheckingExceptionPrivate);
 810
 811   /**
 812    * Make an integer subrange type as defined by the argument.
 813    */
 814   TypeNode mkSubrangeType(const SubrangeBounds& bounds)
 815     throw(TypeCheckingExceptionPrivate);
 816
 817   /**
 818    * Given a tuple or record type, get the internal datatype used for
 819    * it.  Makes the DatatypeType if necessary.
 820    */
 821   TypeNode getDatatypeForTupleRecord(TypeNode tupleRecordType);
 822
 823   /**
 824    * Get the type for the given node and optionally do type checking.
 825    *
 826    * Initial type computation will be near-constant time if
 827    * type checking is not requested. Results are memoized, so that
 828    * subsequent calls to getType() without type checking will be
 829    * constant time.
 830    *
 831    * Initial type checking is linear in the size of the expression.
 832    * Again, the results are memoized, so that subsequent calls to
 833    * getType(), with or without type checking, will be constant
 834    * time.
 835    *
 836    * NOTE: A TypeCheckingException can be thrown even when type
 837    * checking is not requested. getType() will always return a
 838    * valid and correct type and, thus, an exception will be thrown
 839    * when no valid or correct type can be computed (e.g., if the
 840    * arguments to a bit-vector operation aren't bit-vectors). When
 841    * type checking is not requested, getType() will do the minimum
 842    * amount of checking required to return a valid result.
 843    *
 844    * @param n the Node for which we want a type
 845    * @param check whether we should check the type as we compute it
 846    * (default: false)
 847    */
 848   TypeNode getType(TNode n, bool check = false)
 849     throw(TypeCheckingExceptionPrivate, AssertionException);
 850
 851   /**
 852    * Convert a node to an expression.  Uses the ExprManager
 853    * associated to this NodeManager.
 854    */
 855   inline Expr toExpr(TNode n);
 856
 857   /**
 858    * Convert an expression to a node.
 859    */
 860   static inline Node fromExpr(const Expr& e);
 861
 862   /**
 863    * Convert a node manager to an expression manager.
 864    */
 865   inline ExprManager* toExprManager();
 866
 867   /**
 868    * Convert an expression manager to a node manager.
 869    */
 870   static inline NodeManager* fromExprManager(ExprManager* exprManager);
 871
 872   /**
 873    * Convert a type node to a type.
 874    */
 875   inline Type toType(TypeNode tn);
 876
 877   /**
 878    * Convert a type to a type node.
 879    */
 880   static inline TypeNode fromType(Type t);
 881
 882   /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
 883   void reclaimZombiesUntil(uint32_t k);
 884
 885   /** Reclaims all zombies (if possible).*/
 886   void reclaimAllZombies();
 887
 888   /** Size of the node pool. */
 889   size_t poolSize() const;
 890
 891   /** Deletes a list of attributes from the NM's AttributeManager.*/
 892   void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
 893
 894   /**
 895    * This function gives developers a hook into the NodeManager.
 896    * This can be changed in node_manager.cpp without recompiling most of cvc4.
 897    *
 898    * debugHook is a debugging only function, and should not be present in
 899    * any published code!
 900    */
 901   void debugHook(int debugFlag);
 902 };/* class NodeManager */
 903
 904 /**
 905  * This class changes the "current" thread-global
 906  * <code>NodeManager</code> when it is created and reinstates the
 907  * previous thread-global <code>NodeManager</code> when it is
 908  * destroyed, effectively maintaining a set of nested
 909  * <code>NodeManager</code> scopes.  This is especially useful on
 910  * public-interface calls into the CVC4 library, where CVC4's notion
 911  * of the "current" <code>NodeManager</code> should be set to match
 912  * the calling context.  See, for example, the implementations of
 913  * public calls in the <code>ExprManager</code> and
 914  * <code>SmtEngine</code> classes.
 915  *
 916  * The client must be careful to create and destroy
 917  * <code>NodeManagerScope</code> objects in a well-nested manner (such
 918  * as on the stack). You may create a <code>NodeManagerScope</code>
 919  * with <code>new</code> and destroy it with <code>delete</code>, or
 920  * place it as a data member of an object that is, but if the scope of
 921  * these <code>new</code>/<code>delete</code> pairs isn't properly
 922  * maintained, the incorrect "current" <code>NodeManager</code>
 923  * pointer may be restored after a delete.
 924  */
 925 class NodeManagerScope {
 926   /** The old NodeManager, to be restored on destruction. */
 927   NodeManager* d_oldNodeManager;
 928
 929 public:
 930
 931   NodeManagerScope(NodeManager* nm) :
 932     d_oldNodeManager(NodeManager::s_current) {
 933     // There are corner cases where nm can be NULL and it's ok.
 934     // For example, if you write { Expr e; }, then when the null
 935     // Expr is destructed, there's no active node manager.
 936     //Assert(nm != NULL);
 937     NodeManager::s_current = nm;
 938     Options::s_current = nm ? nm->d_options : NULL;
 939     Debug("current") << "node manager scope: "
 940                      << NodeManager::s_current << "\n";
 941   }
 942
 943   ~NodeManagerScope() {
 944     NodeManager::s_current = d_oldNodeManager;
 945     Options::s_current = d_oldNodeManager ? d_oldNodeManager->d_options : NULL;
 946     Debug("current") << "node manager scope: "
 947                      << "returning to " << NodeManager::s_current << "\n";
 948   }
 949 };/* class NodeManagerScope */
 950
 951 /** Get the (singleton) type for booleans. */
 952 inline TypeNode NodeManager::booleanType() {
 953   return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
 954 }
 955
 956 /** Get the (singleton) type for integers. */
 957 inline TypeNode NodeManager::integerType() {
 958   return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
 959 }
 960
 961 /** Get the (singleton) type for reals. */
 962 inline TypeNode NodeManager::realType() {
 963   return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
 964 }
 965
 966 /** Get the (singleton) type for strings. */
 967 inline TypeNode NodeManager::stringType() {
 968   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
 969 }
 970
 971 /** Get the (singleton) type for regexps. */
 972 inline TypeNode NodeManager::regexpType() {
 973   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
 974 }
 975
 976 /** Get the bound var list type. */
 977 inline TypeNode NodeManager::boundVarListType() {
 978   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
 979 }
 980
 981 /** Get the instantiation pattern type. */
 982 inline TypeNode NodeManager::instPatternType() {
 983   return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
 984 }
 985
 986 /** Get the instantiation pattern type. */
 987 inline TypeNode NodeManager::instPatternListType() {
 988   return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
 989 }
 990
 991 /** Get the (singleton) type for builtin operators. */
 992 inline TypeNode NodeManager::builtinOperatorType() {
 993   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
 994 }
 995
 996 /** Make a function type from domain to range. */
 997 inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
 998   std::vector<TypeNode> sorts;
 999   sorts.push_back(domain);
1000   sorts.push_back(range);
1001   return mkFunctionType(sorts);
1002 }
1003
1004 inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
1005   Assert(argTypes.size() >= 1);
1006   std::vector<TypeNode> sorts(argTypes);
1007   sorts.push_back(range);
1008   return mkFunctionType(sorts);
1009 }
1010
1011 inline TypeNode
1012 NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
1013   Assert(sorts.size() >= 2);
1014   std::vector<TypeNode> sortNodes;
1015   for (unsigned i = 0; i < sorts.size(); ++ i) {
1016     CheckArgument(!sorts[i].isFunctionLike(), sorts,
1017                   "cannot create higher-order function types");
1018     sortNodes.push_back(sorts[i]);
1019   }
1020   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
1021 }
1022
1023 inline TypeNode
1024 NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
1025   Assert(sorts.size() >= 1);
1026   std::vector<TypeNode> sortNodes;
1027   for (unsigned i = 0; i < sorts.size(); ++ i) {
1028     CheckArgument(!sorts[i].isFunctionLike(), sorts,
1029                   "cannot create higher-order function types");
1030     sortNodes.push_back(sorts[i]);
1031   }
1032   sortNodes.push_back(booleanType());
1033   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
1034 }
1035
1036 inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
1037   std::vector<TypeNode> typeNodes;
1038   for (unsigned i = 0; i < types.size(); ++ i) {
1039     CheckArgument(!types[i].isFunctionLike(), types,
1040                   "cannot put function-like types in tuples");
1041     typeNodes.push_back(types[i]);
1042   }
1043   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
1044 }
1045
1046 inline TypeNode NodeManager::mkRecordType(const Record& rec) {
1047   return mkTypeConst(rec);
1048 }
1049
1050 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
1051   std::vector<TypeNode> typeNodes;
1052   for (unsigned i = 0; i < types.size(); ++ i) {
1053     typeNodes.push_back(types[i]);
1054   }
1055   return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
1056 }
1057
1058 inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
1059   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
1060 }
1061
1062 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
1063                                          TypeNode constituentType) {
1064   CheckArgument(!indexType.isNull(), indexType,
1065                 "unexpected NULL index type");
1066   CheckArgument(!constituentType.isNull(), constituentType,
1067                 "unexpected NULL constituent type");
1068   CheckArgument(!indexType.isFunctionLike(), indexType,
1069                 "cannot index arrays by a function-like type");
1070   CheckArgument(!constituentType.isFunctionLike(), constituentType,
1071                 "cannot store function-like types in arrays");
1072   Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
1073   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
1074 }
1075
1076 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
1077   CheckArgument(!elementType.isNull(), elementType,
1078                 "unexpected NULL element type");
1079   // TODO: Confirm meaning of isFunctionLike(). --K
1080   CheckArgument(!elementType.isFunctionLike(), elementType,
1081                 "cannot store function-like types in sets");
1082   Debug("sets") << "making sets type " << elementType << std::endl;
1083   return mkTypeNode(kind::SET_TYPE, elementType);
1084 }
1085
1086 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
1087   CheckArgument(!domain.isFunctionLike(), domain,
1088                 "cannot create higher-order function types");
1089   CheckArgument(!range.isFunctionLike(), range,
1090                 "cannot create higher-order function types");
1091   return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
1092 }
1093
1094 inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
1095   CheckArgument(!domain.isFunctionLike(), domain,
1096                 "cannot create higher-order function types");
1097   return mkTypeNode(kind::TESTER_TYPE, domain );
1098 }
1099
1100 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
1101   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
1102   if(find == d_nodeValuePool.end()) {
1103     return NULL;
1104   } else {
1105     return *find;
1106   }
1107 }
1108
1109 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
1110   Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
1111          "NodeValue already in the pool!");
1112   d_nodeValuePool.insert(nv);// FIXME multithreading
1113 }
1114
1115 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
1116   Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
1117          "NodeValue is not in the pool!");
1118
1119   d_nodeValuePool.erase(nv);// FIXME multithreading
1120 }
1121
1122 inline Expr NodeManager::toExpr(TNode n) {
1123   return Expr(d_exprManager, new Node(n));
1124 }
1125
1126 inline Node NodeManager::fromExpr(const Expr& e) {
1127   return e.getNode();
1128 }
1129
1130 inline ExprManager* NodeManager::toExprManager() {
1131   return d_exprManager;
1132 }
1133
1134 inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
1135   return exprManager->getNodeManager();
1136 }
1137
1138 inline Type NodeManager::toType(TypeNode tn) {
1139   return Type(this, new TypeNode(tn));
1140 }
1141
1142 inline TypeNode NodeManager::fromType(Type t) {
1143   return *Type::getTypeNode(t);
1144 }
1145
1146 }/* CVC4 namespace */
1147
1148 #define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1149 #include "expr/metakind.h"
1150 #undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1151
1152 #include "expr/node_builder.h"
1153
1154 namespace CVC4 {
1155
1156 // general expression-builders
1157
1158 inline bool NodeManager::hasOperator(Kind k) {
1159   switch(kind::MetaKind mk = kind::metaKindOf(k)) {
1160
1161   case kind::metakind::INVALID:
1162   case kind::metakind::VARIABLE:
1163     return false;
1164
1165   case kind::metakind::OPERATOR:
1166   case kind::metakind::PARAMETERIZED:
1167     return true;
1168
1169   case kind::metakind::CONSTANT:
1170     return false;
1171
1172   default:
1173     Unhandled(mk);
1174   }
1175 }
1176
1177 inline Kind NodeManager::operatorToKind(TNode n) {
1178   return kind::operatorToKind(n.d_nv);
1179 }
1180
1181 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
1182   NodeBuilder<1> nb(this, kind);
1183   nb << child1;
1184   return nb.constructNode();
1185 }
1186
1187 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
1188   NodeBuilder<1> nb(this, kind);
1189   nb << child1;
1190   return nb.constructNodePtr();
1191 }
1192
1193 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
1194   NodeBuilder<2> nb(this, kind);
1195   nb << child1 << child2;
1196   return nb.constructNode();
1197 }
1198
1199 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
1200   NodeBuilder<2> nb(this, kind);
1201   nb << child1 << child2;
1202   return nb.constructNodePtr();
1203 }
1204
1205 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1206                                 TNode child3) {
1207   NodeBuilder<3> nb(this, kind);
1208   nb << child1 << child2 << child3;
1209   return nb.constructNode();
1210 }
1211
1212 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1213                                 TNode child3) {
1214   NodeBuilder<3> nb(this, kind);
1215   nb << child1 << child2 << child3;
1216   return nb.constructNodePtr();
1217 }
1218
1219 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1220                                 TNode child3, TNode child4) {
1221   NodeBuilder<4> nb(this, kind);
1222   nb << child1 << child2 << child3 << child4;
1223   return nb.constructNode();
1224 }
1225
1226 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1227                                 TNode child3, TNode child4) {
1228   NodeBuilder<4> nb(this, kind);
1229   nb << child1 << child2 << child3 << child4;
1230   return nb.constructNodePtr();
1231 }
1232
1233 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1234                                 TNode child3, TNode child4, TNode child5) {
1235   NodeBuilder<5> nb(this, kind);
1236   nb << child1 << child2 << child3 << child4 << child5;
1237   return nb.constructNode();
1238 }
1239
1240 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1241                                     TNode child3, TNode child4, TNode child5) {
1242   NodeBuilder<5> nb(this, kind);
1243   nb << child1 << child2 << child3 << child4 << child5;
1244   return nb.constructNodePtr();
1245 }
1246
1247 // N-ary version
1248 template <bool ref_count>
1249 inline Node NodeManager::mkNode(Kind kind,
1250                                 const std::vector<NodeTemplate<ref_count> >&
1251                                 children) {
1252   NodeBuilder<> nb(this, kind);
1253   nb.append(children);
1254   return nb.constructNode();
1255 }
1256
1257 template <bool ref_count>
1258 inline Node* NodeManager::mkNodePtr(Kind kind,
1259                                 const std::vector<NodeTemplate<ref_count> >&
1260                                 children) {
1261   NodeBuilder<> nb(this, kind);
1262   nb.append(children);
1263   return nb.constructNodePtr();
1264 }
1265
1266 // for operators
1267 inline Node NodeManager::mkNode(TNode opNode) {
1268   NodeBuilder<1> nb(this, operatorToKind(opNode));
1269   if(opNode.getKind() != kind::BUILTIN) {
1270     nb << opNode;
1271   }
1272   return nb.constructNode();
1273 }
1274
1275 inline Node* NodeManager::mkNodePtr(TNode opNode) {
1276   NodeBuilder<1> nb(this, operatorToKind(opNode));
1277   if(opNode.getKind() != kind::BUILTIN) {
1278     nb << opNode;
1279   }
1280   return nb.constructNodePtr();
1281 }
1282
1283 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
1284   NodeBuilder<2> nb(this, operatorToKind(opNode));
1285   if(opNode.getKind() != kind::BUILTIN) {
1286     nb << opNode;
1287   }
1288   nb << child1;
1289   return nb.constructNode();
1290 }
1291
1292 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
1293   NodeBuilder<2> nb(this, operatorToKind(opNode));
1294   if(opNode.getKind() != kind::BUILTIN) {
1295     nb << opNode;
1296   }
1297   nb << child1;
1298   return nb.constructNodePtr();
1299 }
1300
1301 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
1302   NodeBuilder<3> nb(this, operatorToKind(opNode));
1303   if(opNode.getKind() != kind::BUILTIN) {
1304     nb << opNode;
1305   }
1306   nb << child1 << child2;
1307   return nb.constructNode();
1308 }
1309
1310 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
1311   NodeBuilder<3> nb(this, operatorToKind(opNode));
1312   if(opNode.getKind() != kind::BUILTIN) {
1313     nb << opNode;
1314   }
1315   nb << child1 << child2;
1316   return nb.constructNodePtr();
1317 }
1318
1319 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1320                                 TNode child3) {
1321   NodeBuilder<4> nb(this, operatorToKind(opNode));
1322   if(opNode.getKind() != kind::BUILTIN) {
1323     nb << opNode;
1324   }
1325   nb << child1 << child2 << child3;
1326   return nb.constructNode();
1327 }
1328
1329 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1330                                 TNode child3) {
1331   NodeBuilder<4> nb(this, operatorToKind(opNode));
1332   if(opNode.getKind() != kind::BUILTIN) {
1333     nb << opNode;
1334   }
1335   nb << child1 << child2 << child3;
1336   return nb.constructNodePtr();
1337 }
1338
1339 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1340                                 TNode child3, TNode child4) {
1341   NodeBuilder<5> nb(this, operatorToKind(opNode));
1342   if(opNode.getKind() != kind::BUILTIN) {
1343     nb << opNode;
1344   }
1345   nb << child1 << child2 << child3 << child4;
1346   return nb.constructNode();
1347 }
1348
1349 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1350                                 TNode child3, TNode child4) {
1351   NodeBuilder<5> nb(this, operatorToKind(opNode));
1352   if(opNode.getKind() != kind::BUILTIN) {
1353     nb << opNode;
1354   }
1355   nb << child1 << child2 << child3 << child4;
1356   return nb.constructNodePtr();
1357 }
1358
1359 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1360                                 TNode child3, TNode child4, TNode child5) {
1361   NodeBuilder<6> nb(this, operatorToKind(opNode));
1362   if(opNode.getKind() != kind::BUILTIN) {
1363     nb << opNode;
1364   }
1365   nb << child1 << child2 << child3 << child4 << child5;
1366   return nb.constructNode();
1367 }
1368
1369 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1370                                     TNode child3, TNode child4, TNode child5) {
1371   NodeBuilder<6> nb(this, operatorToKind(opNode));
1372   if(opNode.getKind() != kind::BUILTIN) {
1373     nb << opNode;
1374   }
1375   nb << child1 << child2 << child3 << child4 << child5;
1376   return nb.constructNodePtr();
1377 }
1378
1379 // N-ary version for operators
1380 template <bool ref_count>
1381 inline Node NodeManager::mkNode(TNode opNode,
1382                                 const std::vector<NodeTemplate<ref_count> >&
1383                                 children) {
1384   NodeBuilder<> nb(this, operatorToKind(opNode));
1385   if(opNode.getKind() != kind::BUILTIN) {
1386     nb << opNode;
1387   }
1388   nb.append(children);
1389   return nb.constructNode();
1390 }
1391
1392 template <bool ref_count>
1393 inline Node* NodeManager::mkNodePtr(TNode opNode,
1394                                     const std::vector<NodeTemplate<ref_count> >&
1395                                     children) {
1396   NodeBuilder<> nb(this, operatorToKind(opNode));
1397   if(opNode.getKind() != kind::BUILTIN) {
1398     nb << opNode;
1399   }
1400   nb.append(children);
1401   return nb.constructNodePtr();
1402 }
1403
1404
1405 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
1406   return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
1407 }
1408
1409 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1410                                         TypeNode child2) {
1411   return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
1412 }
1413
1414 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1415                                         TypeNode child2, TypeNode child3) {
1416   return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
1417 }
1418
1419 // N-ary version for types
1420 inline TypeNode NodeManager::mkTypeNode(Kind kind,
1421                                         const std::vector<TypeNode>& children) {
1422   return NodeBuilder<>(this, kind).append(children).constructTypeNode();
1423 }
1424
1425 template <class T>
1426 Node NodeManager::mkConst(const T& val) {
1427   return mkConstInternal<Node, T>(val);
1428 }
1429
1430 template <class T>
1431 TypeNode NodeManager::mkTypeConst(const T& val) {
1432   return mkConstInternal<TypeNode, T>(val);
1433 }
1434
1435 template <class NodeClass, class T>
1436 NodeClass NodeManager::mkConstInternal(const T& val) {
1437
1438   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1439   NVStorage<1> nvStorage;
1440   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
1441
1442   nvStack.d_id = 0;
1443   nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
1444   nvStack.d_rc = 0;
1445   nvStack.d_nchildren = 1;
1446
1447 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1448 #pragma GCC diagnostic push
1449 #pragma GCC diagnostic ignored "-Warray-bounds"
1450 #endif
1451
1452   nvStack.d_children[0] =
1453     const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
1454   expr::NodeValue* nv = poolLookup(&nvStack);
1455
1456 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1457 #pragma GCC diagnostic pop
1458 #endif
1459
1460   if(nv != NULL) {
1461     return NodeClass(nv);
1462   }
1463
1464   nv = (expr::NodeValue*)
1465     std::malloc(sizeof(expr::NodeValue) + sizeof(T));
1466   if(nv == NULL) {
1467     throw std::bad_alloc();
1468   }
1469
1470   nv->d_nchildren = 0;
1471   nv->d_kind = kind::metakind::ConstantMap<T>::kind;
1472   nv->d_id = next_id++;// FIXME multithreading
1473   nv->d_rc = 0;
1474
1475   //OwningTheory::mkConst(val);
1476   new (&nv->d_children) T(val);
1477
1478   poolInsert(nv);
1479   if(Debug.isOn("gc")) {
1480     Debug("gc") << "creating node value " << nv
1481                 << " [" << nv->d_id << "]: ";
1482     nv->printAst(Debug("gc"));
1483     Debug("gc") << std::endl;
1484   }
1485
1486   return NodeClass(nv);
1487 }
1488
1489 }/* CVC4 namespace */
1490
1491 #endif /* __CVC4__NODE_MANAGER_H */