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