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