src/expr/node_manager.h

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