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