src/expr/node_manager.h

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