src/expr/node_manager.h

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