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, Andrew Reynolds
   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<TypeNode>& 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   /** Predicate for use with STL algorithms */
  95   struct NodeValueReferenceCountNonZero {
  96     bool operator()(expr::NodeValue* nv) { return nv->d_rc > 0; }
  97   };
  98
  99   typedef std::unordered_set<expr::NodeValue*,
 100                              expr::NodeValuePoolHashFunction,
 101                              expr::NodeValuePoolEq> NodeValuePool;
 102   typedef std::unordered_set<expr::NodeValue*,
 103                              expr::NodeValueIDHashFunction,
 104                              expr::NodeValueIDEquality> NodeValueIDSet;
 105
 106   static thread_local NodeManager* s_current;
 107
 108   StatisticsRegistry* d_statisticsRegistry;
 109
 110   /** The skolem manager */
 111   std::shared_ptr<SkolemManager> d_skManager;
 112
 113   NodeValuePool d_nodeValuePool;
 114
 115   size_t next_id;
 116
 117   expr::attr::AttributeManager* d_attrManager;
 118
 119   /** The associated ExprManager */
 120   ExprManager* d_exprManager;
 121
 122   /**
 123    * The node value we're currently freeing.  This unique node value
 124    * is permitted to have outstanding TNodes to it (in "soft"
 125    * contexts, like as a key in attribute tables), even though
 126    * normally it's an error to have a TNode to a node value with a
 127    * reference count of 0.  Being "under deletion" also enables
 128    * assertions that inc() is not called on it.
 129    */
 130   expr::NodeValue* d_nodeUnderDeletion;
 131
 132   /**
 133    * True iff we are in reclaimZombies().  This avoids unnecessary
 134    * recursion; a NodeValue being deleted might zombify other
 135    * NodeValues, but these shouldn't trigger a (recursive) call to
 136    * reclaimZombies().
 137    */
 138   bool d_inReclaimZombies;
 139
 140   /**
 141    * The set of zombie nodes.  We may want to revisit this design, as
 142    * we might like to delete nodes in least-recently-used order.  But
 143    * we also need to avoid processing a zombie twice.
 144    */
 145   NodeValueIDSet d_zombies;
 146
 147   /**
 148    * NodeValues with maxed out reference counts. These live as long as the
 149    * NodeManager. They have a custom deallocation procedure at the very end.
 150    */
 151   std::vector<expr::NodeValue*> d_maxedOut;
 152
 153   /**
 154    * A set of operator singletons (w.r.t.  to this NodeManager
 155    * instance) for operators.  Conceptually, Nodes with kind, say,
 156    * PLUS, are APPLYs of a PLUS operator to arguments.  This array
 157    * holds the set of operators for these things.  A PLUS operator is
 158    * a Node with kind "BUILTIN", and if you call
 159    * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
 160    */
 161   Node d_operators[kind::LAST_KIND];
 162
 163   /** unique vars per (Kind,Type) */
 164   std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
 165
 166   /**
 167    * A list of subscribers for NodeManager events.
 168    */
 169   std::vector<NodeManagerListener*> d_listeners;
 170
 171   /** A list of datatypes registered by its corresponding expr manager.
 172    * !!! this member should be deleted when the Expr-layer is deleted.
 173    */
 174   std::vector<std::shared_ptr<DType> > d_registeredDTypes;
 175   /** A list of datatypes owned by this node manager */
 176   std::vector<std::unique_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 that datatype dt was constructed by the expression manager
 412    * !!! this interface should be deleted when the Expr-layer is deleted.
 413    */
 414   size_t registerDatatype(std::shared_ptr<DType> dt);
 415   /**
 416    * Return the datatype at the given index owned by this class. Type nodes are
 417    * associated with datatypes through the DatatypeIndexConstant class. The
 418    * argument index is intended to be a value taken from that class.
 419    *
 420    * Type nodes must access their DTypes through a level of indirection to
 421    * prevent cycles in the Node AST (as DTypes themselves contain Nodes), which
 422    * would lead to memory leaks. Thus TypeNode are given a DatatypeIndexConstant
 423    * which is used as an index to retrieve the DType via this call.
 424    */
 425   const DType& getDTypeForIndex(size_t index) const;
 426
 427   /** Get a Kind from an operator expression */
 428   static inline Kind operatorToKind(TNode n);
 429
 430   /** Get corresponding application kind for function
 431    *
 432    * Different functional nodes are applied differently, according to their
 433    * type. For example, uninterpreted functions (of FUNCTION_TYPE) are applied
 434    * via APPLY_UF, while constructors (of CONSTRUCTOR_TYPE) via
 435    * APPLY_CONSTRUCTOR. This method provides the correct application according
 436    * to which functional type fun has.
 437    *
 438    * @param fun The functional node
 439    * @return the correct application kind for fun. If fun's type is not function
 440    * like (see TypeNode::isFunctionLike), then UNDEFINED_KIND is returned.
 441    */
 442   static Kind getKindForFunction(TNode fun);
 443
 444   // general expression-builders
 445
 446   /** Create a node with one child. */
 447   Node mkNode(Kind kind, TNode child1);
 448   Node* mkNodePtr(Kind kind, TNode child1);
 449
 450   /** Create a node with two children. */
 451   Node mkNode(Kind kind, TNode child1, TNode child2);
 452   Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
 453
 454   /** Create a node with three children. */
 455   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 456   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
 457
 458   /** Create a node with four children. */
 459   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 460               TNode child4);
 461   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 462               TNode child4);
 463
 464   /** Create a node with five children. */
 465   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 466               TNode child4, TNode child5);
 467   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 468               TNode child4, TNode child5);
 469
 470   /** Create a node with an arbitrary number of children. */
 471   template <bool ref_count>
 472   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 473   template <bool ref_count>
 474   Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 475
 476   /**
 477    * Create an AND node with arbitrary number of children. This returns the
 478    * true node if children is empty, or the single node in children if
 479    * it contains only one node.
 480    *
 481    * We define construction of AND as a special case here since it is widely
 482    * used for e.g. constructing explanations.
 483    */
 484   template <bool ref_count>
 485   Node mkAnd(const std::vector<NodeTemplate<ref_count> >& children);
 486
 487   /** Create a node (with no children) by operator. */
 488   Node mkNode(TNode opNode);
 489   Node* mkNodePtr(TNode opNode);
 490
 491   /** Create a node with one child by operator. */
 492   Node mkNode(TNode opNode, TNode child1);
 493   Node* mkNodePtr(TNode opNode, TNode child1);
 494
 495   /** Create a node with two children by operator. */
 496   Node mkNode(TNode opNode, TNode child1, TNode child2);
 497   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2);
 498
 499   /** Create a node with three children by operator. */
 500   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3);
 501   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3);
 502
 503   /** Create a node with four children by operator. */
 504   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
 505               TNode child4);
 506   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
 507               TNode child4);
 508
 509   /** Create a node with five children by operator. */
 510   Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3,
 511               TNode child4, TNode child5);
 512   Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3,
 513               TNode child4, TNode child5);
 514
 515   /** Create a node by applying an operator to the children. */
 516   template <bool ref_count>
 517   Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 518   template <bool ref_count>
 519   Node* mkNodePtr(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
 520
 521   Node mkBoundVar(const std::string& name, const TypeNode& type);
 522   Node* mkBoundVarPtr(const std::string& name, const TypeNode& type);
 523
 524   Node mkBoundVar(const TypeNode& type);
 525   Node* mkBoundVarPtr(const TypeNode& type);
 526
 527   /** get the canonical bound variable list for function type tn */
 528   Node getBoundVarListForFunctionType( TypeNode tn );
 529
 530   /**
 531    * Optional flags used to control behavior of NodeManager::mkSkolem().
 532    * They should be composed with a bitwise OR (e.g.,
 533    * "SKOLEM_NO_NOTIFY | SKOLEM_EXACT_NAME").  Of course, SKOLEM_DEFAULT
 534    * cannot be composed in such a manner.
 535    */
 536   enum SkolemFlags
 537   {
 538     SKOLEM_DEFAULT = 0,    /**< default behavior */
 539     SKOLEM_NO_NOTIFY = 1,  /**< do not notify subscribers */
 540     SKOLEM_EXACT_NAME = 2, /**< do not make the name unique by adding the id */
 541     SKOLEM_IS_GLOBAL = 4,  /**< global vars appear in models even after a pop */
 542     SKOLEM_BOOL_TERM_VAR = 8 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */
 543   };                         /* enum SkolemFlags */
 544
 545   /**
 546    * Create a skolem constant with the given name, type, and comment.
 547    *
 548    * @param prefix the name of the new skolem variable is the prefix
 549    * appended with a unique ID.  This way a family of skolem variables
 550    * can be made with unique identifiers, used in dump, tracing, and
 551    * debugging output.  Use SKOLEM_EXECT_NAME flag if you don't want
 552    * a unique ID appended and use prefix as the name.
 553    *
 554    * @param type the type of the skolem variable to create
 555    *
 556    * @param comment a comment for dumping output; if declarations are
 557    * being dumped, this is included in a comment before the declaration
 558    * and can be quite useful for debugging
 559    *
 560    * @param flags an optional mask of bits from SkolemFlags to control
 561    * mkSkolem() behavior
 562    */
 563   Node mkSkolem(const std::string& prefix, const TypeNode& type,
 564                 const std::string& comment = "", int flags = SKOLEM_DEFAULT);
 565
 566   /** Create a instantiation constant with the given type. */
 567   Node mkInstConstant(const TypeNode& type);
 568
 569   /** Create a boolean term variable. */
 570   Node mkBooleanTermVariable();
 571
 572   /** Make a new abstract value with the given type. */
 573   Node mkAbstractValue(const TypeNode& type);
 574
 575   /** make unique (per Type,Kind) variable. */
 576   Node mkNullaryOperator(const TypeNode& type, Kind k);
 577
 578   /**
 579   * Create a singleton set from the given element n.
 580   * @param t the element type of the returned set.
 581   * Note that the type of n needs to be a subtype of t.
 582   * @param n the single element in the singleton.
 583   * @return a singleton set constructed from the element n.
 584   */
 585   Node mkSingleton(const TypeNode& t, const TNode n);
 586
 587   /**
 588    * Create a constant of type T.  It will have the appropriate
 589    * CONST_* kind defined for T.
 590    */
 591   template <class T>
 592   Node mkConst(const T&);
 593
 594   template <class T>
 595   TypeNode mkTypeConst(const T&);
 596
 597   template <class NodeClass, class T>
 598   NodeClass mkConstInternal(const T&);
 599
 600   /** Create a node with children. */
 601   TypeNode mkTypeNode(Kind kind, TypeNode child1);
 602   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);
 603   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2,
 604                       TypeNode child3);
 605   TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
 606
 607   /**
 608    * Determine whether Nodes of a particular Kind have operators.
 609    * @returns true if Nodes of Kind k have operators.
 610    */
 611   static inline bool hasOperator(Kind k);
 612
 613   /**
 614    * Get the (singleton) operator of an OPERATOR-kinded kind.  The
 615    * returned node n will have kind BUILTIN, and calling
 616    * n.getConst<CVC4::Kind>() will yield k.
 617    */
 618   inline TNode operatorOf(Kind k) {
 619     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
 620                     "Kind is not an OPERATOR-kinded kind "
 621                     "in NodeManager::operatorOf()" );
 622     return d_operators[k];
 623   }
 624
 625   /**
 626    * Retrieve an attribute for a node.
 627    *
 628    * @param nv the node value
 629    * @param attr an instance of the attribute kind to retrieve.
 630    * @returns the attribute, if set, or a default-constructed
 631    * <code>AttrKind::value_type</code> if not.
 632    */
 633   template <class AttrKind>
 634   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
 635                                                     const AttrKind& attr) const;
 636
 637   /**
 638    * Check whether an attribute is set for a node.
 639    *
 640    * @param nv the node value
 641    * @param attr an instance of the attribute kind to check
 642    * @returns <code>true</code> iff <code>attr</code> is set for
 643    * <code>nv</code>.
 644    */
 645   template <class AttrKind>
 646   inline bool hasAttribute(expr::NodeValue* nv,
 647                            const AttrKind& attr) const;
 648
 649   /**
 650    * Check whether an attribute is set for a node, and, if so,
 651    * retrieve it.
 652    *
 653    * @param nv the node value
 654    * @param attr an instance of the attribute kind to check
 655    * @param value a reference to an object of the attribute's value type.
 656    * <code>value</code> will be set to the value of the attribute, if it is
 657    * set for <code>nv</code>; otherwise, it will be set to the default
 658    * value of the attribute.
 659    * @returns <code>true</code> iff <code>attr</code> is set for
 660    * <code>nv</code>.
 661    */
 662   template <class AttrKind>
 663   inline bool getAttribute(expr::NodeValue* nv,
 664                            const AttrKind& attr,
 665                            typename AttrKind::value_type& value) const;
 666
 667   /**
 668    * Set an attribute for a node.  If the node doesn't have the
 669    * attribute, this function assigns one.  If the node has one, this
 670    * overwrites it.
 671    *
 672    * @param nv the node value
 673    * @param attr an instance of the attribute kind to set
 674    * @param value the value of <code>attr</code> for <code>nv</code>
 675    */
 676   template <class AttrKind>
 677   inline void setAttribute(expr::NodeValue* nv,
 678                            const AttrKind& attr,
 679                            const typename AttrKind::value_type& value);
 680
 681   /**
 682    * Retrieve an attribute for a TNode.
 683    *
 684    * @param n the node
 685    * @param attr an instance of the attribute kind to retrieve.
 686    * @returns the attribute, if set, or a default-constructed
 687    * <code>AttrKind::value_type</code> if not.
 688    */
 689   template <class AttrKind>
 690   inline typename AttrKind::value_type
 691   getAttribute(TNode n, const AttrKind& attr) const;
 692
 693   /**
 694    * Check whether an attribute is set for a TNode.
 695    *
 696    * @param n the node
 697    * @param attr an instance of the attribute kind to check
 698    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 699    */
 700   template <class AttrKind>
 701   inline bool hasAttribute(TNode n,
 702                            const AttrKind& attr) const;
 703
 704   /**
 705    * Check whether an attribute is set for a TNode and, if so, retieve
 706    * it.
 707    *
 708    * @param n the node
 709    * @param attr an instance of the attribute kind to check
 710    * @param value a reference to an object of the attribute's value type.
 711    * <code>value</code> will be set to the value of the attribute, if it is
 712    * set for <code>nv</code>; otherwise, it will be set to the default value of
 713    * the attribute.
 714    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 715    */
 716   template <class AttrKind>
 717   inline bool getAttribute(TNode n,
 718                            const AttrKind& attr,
 719                            typename AttrKind::value_type& value) const;
 720
 721   /**
 722    * Set an attribute for a node.  If the node doesn't have the
 723    * attribute, this function assigns one.  If the node has one, this
 724    * overwrites it.
 725    *
 726    * @param n the node
 727    * @param attr an instance of the attribute kind to set
 728    * @param value the value of <code>attr</code> for <code>n</code>
 729    */
 730   template <class AttrKind>
 731   inline void setAttribute(TNode n,
 732                            const AttrKind& attr,
 733                            const typename AttrKind::value_type& value);
 734
 735   /**
 736    * Retrieve an attribute for a TypeNode.
 737    *
 738    * @param n the type node
 739    * @param attr an instance of the attribute kind to retrieve.
 740    * @returns the attribute, if set, or a default-constructed
 741    * <code>AttrKind::value_type</code> if not.
 742    */
 743   template <class AttrKind>
 744   inline typename AttrKind::value_type
 745   getAttribute(TypeNode n, const AttrKind& attr) const;
 746
 747   /**
 748    * Check whether an attribute is set for a TypeNode.
 749    *
 750    * @param n the type node
 751    * @param attr an instance of the attribute kind to check
 752    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 753    */
 754   template <class AttrKind>
 755   inline bool hasAttribute(TypeNode n,
 756                            const AttrKind& attr) const;
 757
 758   /**
 759    * Check whether an attribute is set for a TypeNode and, if so, retieve
 760    * it.
 761    *
 762    * @param n the type node
 763    * @param attr an instance of the attribute kind to check
 764    * @param value a reference to an object of the attribute's value type.
 765    * <code>value</code> will be set to the value of the attribute, if it is
 766    * set for <code>nv</code>; otherwise, it will be set to the default value of
 767    * the attribute.
 768    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 769    */
 770   template <class AttrKind>
 771   inline bool getAttribute(TypeNode n,
 772                            const AttrKind& attr,
 773                            typename AttrKind::value_type& value) const;
 774
 775   /**
 776    * Set an attribute for a type node.  If the node doesn't have the
 777    * attribute, this function assigns one.  If the type node has one,
 778    * this overwrites it.
 779    *
 780    * @param n the type node
 781    * @param attr an instance of the attribute kind to set
 782    * @param value the value of <code>attr</code> for <code>n</code>
 783    */
 784   template <class AttrKind>
 785   inline void setAttribute(TypeNode n,
 786                            const AttrKind& attr,
 787                            const typename AttrKind::value_type& value);
 788
 789   /** Get the (singleton) type for Booleans. */
 790   inline TypeNode booleanType();
 791
 792   /** Get the (singleton) type for integers. */
 793   inline TypeNode integerType();
 794
 795   /** Get the (singleton) type for reals. */
 796   inline TypeNode realType();
 797
 798   /** Get the (singleton) type for strings. */
 799   inline TypeNode stringType();
 800
 801   /** Get the (singleton) type for RegExp. */
 802   inline TypeNode regExpType();
 803
 804   /** Get the (singleton) type for rounding modes. */
 805   inline TypeNode roundingModeType();
 806
 807   /** Get the bound var list type. */
 808   inline TypeNode boundVarListType();
 809
 810   /** Get the instantiation pattern type. */
 811   inline TypeNode instPatternType();
 812
 813   /** Get the instantiation pattern type. */
 814   inline TypeNode instPatternListType();
 815
 816   /**
 817    * Get the (singleton) type for builtin operators (that is, the type
 818    * of the Node returned from Node::getOperator() when the operator
 819    * is built-in, like EQUAL). */
 820   inline TypeNode builtinOperatorType();
 821
 822   /**
 823    * Make a function type from domain to range.
 824    *
 825    * @param domain the domain type
 826    * @param range the range type
 827    * @returns the functional type domain -> range
 828    */
 829   TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 830
 831   /**
 832    * Make a function type with input types from
 833    * argTypes. <code>argTypes</code> must have at least one element.
 834    *
 835    * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
 836    * @param range the range type
 837    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
 838    */
 839   TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
 840                           const TypeNode& range);
 841
 842   /**
 843    * Make a function type with input types from
 844    * <code>sorts[0..sorts.size()-2]</code> and result type
 845    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
 846    * at least 2 elements.
 847    */
 848   TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 849
 850   /**
 851    * Make a predicate type with input types from
 852    * <code>sorts</code>. The result with be a function type with range
 853    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
 854    * element.
 855    */
 856   TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 857
 858   /**
 859    * Make a tuple type with types from
 860    * <code>types</code>. <code>types</code> must have at least one
 861    * element.
 862    *
 863    * @param types a vector of types
 864    * @returns the tuple type (types[0], ..., types[n])
 865    */
 866   TypeNode mkTupleType(const std::vector<TypeNode>& types);
 867
 868   /**
 869    * Make a record type with the description from rec.
 870    *
 871    * @param rec a description of the record
 872    * @returns the record type
 873    */
 874   TypeNode mkRecordType(const Record& rec);
 875
 876   /**
 877    * Make a symbolic expression type with types from
 878    * <code>types</code>. <code>types</code> may have any number of
 879    * elements.
 880    *
 881    * @param types a vector of types
 882    * @returns the symbolic expression type (types[0], ..., types[n])
 883    */
 884   inline TypeNode mkSExprType(const std::vector<TypeNode>& types);
 885
 886   /** Make the type of floating-point with <code>exp</code> bit exponent and
 887       <code>sig</code> bit significand */
 888   inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
 889   inline TypeNode mkFloatingPointType(FloatingPointSize fs);
 890
 891   /** Make the type of bitvectors of size <code>size</code> */
 892   inline TypeNode mkBitVectorType(unsigned size);
 893
 894   /** Make the type of arrays with the given parameterization */
 895   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 896
 897   /** Make the type of set with the given parameterization */
 898   inline TypeNode mkSetType(TypeNode elementType);
 899
 900   /** Make the type of bags with the given parameterization */
 901   TypeNode mkBagType(TypeNode elementType);
 902
 903   /** Make the type of sequences with the given parameterization */
 904   TypeNode mkSequenceType(TypeNode elementType);
 905
 906   /** Bits for use in mkDatatypeType() flags.
 907    *
 908    * DATATYPE_FLAG_PLACEHOLDER indicates that the type should not be printed
 909    * out as a definition, for example, in models or during dumping.
 910    */
 911   enum
 912   {
 913     DATATYPE_FLAG_NONE = 0,
 914     DATATYPE_FLAG_PLACEHOLDER = 1
 915   }; /* enum */
 916
 917   /** Make a type representing the given datatype. */
 918   TypeNode mkDatatypeType(DType& datatype, uint32_t flags = DATATYPE_FLAG_NONE);
 919
 920   /**
 921    * Make a set of types representing the given datatypes, which may be
 922    * mutually recursive.
 923    */
 924   std::vector<TypeNode> mkMutualDatatypeTypes(
 925       const std::vector<DType>& datatypes, uint32_t flags = DATATYPE_FLAG_NONE);
 926
 927   /**
 928    * Make a set of types representing the given datatypes, which may
 929    * be mutually recursive.  unresolvedTypes is a set of SortTypes
 930    * that were used as placeholders in the Datatypes for the Datatypes
 931    * of the same name.  This is just a more complicated version of the
 932    * above mkMutualDatatypeTypes() function, but is required to handle
 933    * complex types.
 934    *
 935    * For example, unresolvedTypes might contain the single sort "list"
 936    * (with that name reported from SortType::getName()).  The
 937    * datatypes list might have the single datatype
 938    *
 939    *   DATATYPE
 940    *     list = cons(car:ARRAY INT OF list, cdr:list) | nil;
 941    *   END;
 942    *
 943    * To represent the Type of the array, the user had to create a
 944    * placeholder type (an uninterpreted sort) to stand for "list" in
 945    * the type of "car".  It is this placeholder sort that should be
 946    * passed in unresolvedTypes.  If the datatype was of the simpler
 947    * form:
 948    *
 949    *   DATATYPE
 950    *     list = cons(car:list, cdr:list) | nil;
 951    *   END;
 952    *
 953    * then no complicated Type needs to be created, and the above,
 954    * simpler form of mkMutualDatatypeTypes() is enough.
 955    */
 956   std::vector<TypeNode> mkMutualDatatypeTypes(
 957       const std::vector<DType>& datatypes,
 958       const std::set<TypeNode>& unresolvedTypes,
 959       uint32_t flags = DATATYPE_FLAG_NONE);
 960
 961   /**
 962    * Make a type representing a constructor with the given argument (subfield)
 963    * types and return type range.
 964    */
 965   TypeNode mkConstructorType(const std::vector<TypeNode>& args, TypeNode range);
 966
 967   /** Make a type representing a selector with the given parameterization */
 968   inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
 969
 970   /** Make a type representing a tester with given parameterization */
 971   inline TypeNode mkTesterType(TypeNode domain);
 972
 973   /** Make a new (anonymous) sort of arity 0. */
 974   TypeNode mkSort(uint32_t flags = ExprManager::SORT_FLAG_NONE);
 975
 976   /** Make a new sort with the given name of arity 0. */
 977   TypeNode mkSort(const std::string& name, uint32_t flags = ExprManager::SORT_FLAG_NONE);
 978
 979   /** Make a new sort by parameterizing the given sort constructor. */
 980   TypeNode mkSort(TypeNode constructor,
 981                   const std::vector<TypeNode>& children,
 982                   uint32_t flags = ExprManager::SORT_FLAG_NONE);
 983
 984   /** Make a new sort with the given name and arity. */
 985   TypeNode mkSortConstructor(const std::string& name,
 986                              size_t arity,
 987                              uint32_t flags = ExprManager::SORT_FLAG_NONE);
 988
 989   /**
 990    * Get the type for the given node and optionally do type checking.
 991    *
 992    * Initial type computation will be near-constant time if
 993    * type checking is not requested. Results are memoized, so that
 994    * subsequent calls to getType() without type checking will be
 995    * constant time.
 996    *
 997    * Initial type checking is linear in the size of the expression.
 998    * Again, the results are memoized, so that subsequent calls to
 999    * getType(), with or without type checking, will be constant
1000    * time.
1001    *
1002    * NOTE: A TypeCheckingException can be thrown even when type
1003    * checking is not requested. getType() will always return a
1004    * valid and correct type and, thus, an exception will be thrown
1005    * when no valid or correct type can be computed (e.g., if the
1006    * arguments to a bit-vector operation aren't bit-vectors). When
1007    * type checking is not requested, getType() will do the minimum
1008    * amount of checking required to return a valid result.
1009    *
1010    * @param n the Node for which we want a type
1011    * @param check whether we should check the type as we compute it
1012    * (default: false)
1013    */
1014   TypeNode getType(TNode n, bool check = false);
1015
1016   /**
1017    * Convert a node to an expression.  Uses the ExprManager
1018    * associated to this NodeManager.
1019    */
1020   inline Expr toExpr(TNode n);
1021
1022   /**
1023    * Convert an expression to a node.
1024    */
1025   static inline Node fromExpr(const Expr& e);
1026
1027   /**
1028    * Convert a node manager to an expression manager.
1029    */
1030   inline ExprManager* toExprManager();
1031
1032   /**
1033    * Convert an expression manager to a node manager.
1034    */
1035   static inline NodeManager* fromExprManager(ExprManager* exprManager);
1036
1037   /**
1038    * Convert a type node to a type.
1039    */
1040   inline Type toType(const TypeNode& tn);
1041
1042   /**
1043    * Convert a type to a type node.
1044    */
1045   static inline TypeNode fromType(Type t);
1046
1047   /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
1048   void reclaimZombiesUntil(uint32_t k);
1049
1050   /** Reclaims all zombies (if possible).*/
1051   void reclaimAllZombies();
1052
1053   /** Size of the node pool. */
1054   size_t poolSize() const;
1055
1056   /** Deletes a list of attributes from the NM's AttributeManager.*/
1057   void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
1058
1059   /**
1060    * This function gives developers a hook into the NodeManager.
1061    * This can be changed in node_manager.cpp without recompiling most of cvc4.
1062    *
1063    * debugHook is a debugging only function, and should not be present in
1064    * any published code!
1065    */
1066   void debugHook(int debugFlag);
1067 };/* class NodeManager */
1068
1069 /**
1070  * This class changes the "current" thread-global
1071  * <code>NodeManager</code> when it is created and reinstates the
1072  * previous thread-global <code>NodeManager</code> when it is
1073  * destroyed, effectively maintaining a set of nested
1074  * <code>NodeManager</code> scopes.  This is especially useful on
1075  * public-interface calls into the CVC4 library, where CVC4's notion
1076  * of the "current" <code>NodeManager</code> should be set to match
1077  * the calling context.  See, for example, the implementations of
1078  * public calls in the <code>ExprManager</code> and
1079  * <code>SmtEngine</code> classes.
1080  *
1081  * The client must be careful to create and destroy
1082  * <code>NodeManagerScope</code> objects in a well-nested manner (such
1083  * as on the stack). You may create a <code>NodeManagerScope</code>
1084  * with <code>new</code> and destroy it with <code>delete</code>, or
1085  * place it as a data member of an object that is, but if the scope of
1086  * these <code>new</code>/<code>delete</code> pairs isn't properly
1087  * maintained, the incorrect "current" <code>NodeManager</code>
1088  * pointer may be restored after a delete.
1089  */
1090 class NodeManagerScope {
1091   /** The old NodeManager, to be restored on destruction. */
1092   NodeManager* d_oldNodeManager;
1093 public:
1094  NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current)
1095  {
1096    // There are corner cases where nm can be NULL and it's ok.
1097    // For example, if you write { Expr e; }, then when the null
1098    // Expr is destructed, there's no active node manager.
1099    // Assert(nm != NULL);
1100    NodeManager::s_current = nm;
1101    Debug("current") << "node manager scope: " << NodeManager::s_current << "\n";
1102   }
1103
1104   ~NodeManagerScope() {
1105     NodeManager::s_current = d_oldNodeManager;
1106     Debug("current") << "node manager scope: "
1107                      << "returning to " << NodeManager::s_current << "\n";
1108   }
1109 };/* class NodeManagerScope */
1110
1111 /** Get the (singleton) type for booleans. */
1112 inline TypeNode NodeManager::booleanType() {
1113   return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
1114 }
1115
1116 /** Get the (singleton) type for integers. */
1117 inline TypeNode NodeManager::integerType() {
1118   return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
1119 }
1120
1121 /** Get the (singleton) type for reals. */
1122 inline TypeNode NodeManager::realType() {
1123   return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
1124 }
1125
1126 /** Get the (singleton) type for strings. */
1127 inline TypeNode NodeManager::stringType() {
1128   return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
1129 }
1130
1131 /** Get the (singleton) type for regexps. */
1132 inline TypeNode NodeManager::regExpType() {
1133   return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
1134 }
1135
1136 /** Get the (singleton) type for rounding modes. */
1137 inline TypeNode NodeManager::roundingModeType() {
1138   return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
1139 }
1140
1141 /** Get the bound var list type. */
1142 inline TypeNode NodeManager::boundVarListType() {
1143   return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
1144 }
1145
1146 /** Get the instantiation pattern type. */
1147 inline TypeNode NodeManager::instPatternType() {
1148   return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
1149 }
1150
1151 /** Get the instantiation pattern type. */
1152 inline TypeNode NodeManager::instPatternListType() {
1153   return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
1154 }
1155
1156 /** Get the (singleton) type for builtin operators. */
1157 inline TypeNode NodeManager::builtinOperatorType() {
1158   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
1159 }
1160
1161 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
1162   std::vector<TypeNode> typeNodes;
1163   for (unsigned i = 0; i < types.size(); ++ i) {
1164     typeNodes.push_back(types[i]);
1165   }
1166   return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
1167 }
1168
1169 inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
1170   return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
1171 }
1172
1173 inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
1174   return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
1175 }
1176
1177 inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
1178   return TypeNode(mkTypeConst<FloatingPointSize>(fs));
1179 }
1180
1181 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
1182                                          TypeNode constituentType) {
1183   CheckArgument(!indexType.isNull(), indexType,
1184                 "unexpected NULL index type");
1185   CheckArgument(!constituentType.isNull(), constituentType,
1186                 "unexpected NULL constituent type");
1187   CheckArgument(indexType.isFirstClass(),
1188                 indexType,
1189                 "cannot index arrays by types that are not first-class. Try "
1190                 "option --uf-ho.");
1191   CheckArgument(constituentType.isFirstClass(),
1192                 constituentType,
1193                 "cannot store types that are not first-class in arrays. Try "
1194                 "option --uf-ho.");
1195   Debug("arrays") << "making array type " << indexType << " "
1196                   << constituentType << std::endl;
1197   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
1198 }
1199
1200 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
1201   CheckArgument(!elementType.isNull(), elementType,
1202                 "unexpected NULL element type");
1203   CheckArgument(elementType.isFirstClass(),
1204                 elementType,
1205                 "cannot store types that are not first-class in sets. Try "
1206                 "option --uf-ho.");
1207   Debug("sets") << "making sets type " << elementType << std::endl;
1208   return mkTypeNode(kind::SET_TYPE, elementType);
1209 }
1210
1211 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
1212   CheckArgument(domain.isDatatype(), domain,
1213                 "cannot create non-datatype selector type");
1214   CheckArgument(range.isFirstClass(),
1215                 range,
1216                 "cannot have selector fields that are not first-class types. "
1217                 "Try option --uf-ho.");
1218   return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
1219 }
1220
1221 inline TypeNode NodeManager::mkTesterType(TypeNode domain) {
1222   CheckArgument(domain.isDatatype(), domain,
1223                 "cannot create non-datatype tester");
1224   return mkTypeNode(kind::TESTER_TYPE, domain );
1225 }
1226
1227 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
1228   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
1229   if(find == d_nodeValuePool.end()) {
1230     return NULL;
1231   } else {
1232     return *find;
1233   }
1234 }
1235
1236 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
1237   Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end())
1238       << "NodeValue already in the pool!";
1239   d_nodeValuePool.insert(nv);// FIXME multithreading
1240 }
1241
1242 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
1243   Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end())
1244       << "NodeValue is not in the pool!";
1245
1246   d_nodeValuePool.erase(nv);// FIXME multithreading
1247 }
1248
1249 inline Expr NodeManager::toExpr(TNode n) {
1250   return Expr(d_exprManager, new Node(n));
1251 }
1252
1253 inline Node NodeManager::fromExpr(const Expr& e) {
1254   return e.getNode();
1255 }
1256
1257 inline ExprManager* NodeManager::toExprManager() {
1258   return d_exprManager;
1259 }
1260
1261 inline NodeManager* NodeManager::fromExprManager(ExprManager* exprManager) {
1262   return exprManager->getNodeManager();
1263 }
1264
1265 inline Type NodeManager::toType(const TypeNode& tn)
1266 {
1267   return Type(this, new TypeNode(tn));
1268 }
1269
1270 inline TypeNode NodeManager::fromType(Type t) {
1271   return *Type::getTypeNode(t);
1272 }
1273
1274 }/* CVC4 namespace */
1275
1276 #define CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1277 #include "expr/metakind.h"
1278 #undef CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
1279
1280 #include "expr/node_builder.h"
1281
1282 namespace CVC4 {
1283
1284 // general expression-builders
1285
1286 inline bool NodeManager::hasOperator(Kind k) {
1287   switch(kind::MetaKind mk = kind::metaKindOf(k)) {
1288
1289   case kind::metakind::INVALID:
1290   case kind::metakind::VARIABLE:
1291   case kind::metakind::NULLARY_OPERATOR:
1292     return false;
1293
1294   case kind::metakind::OPERATOR:
1295   case kind::metakind::PARAMETERIZED:
1296     return true;
1297
1298   case kind::metakind::CONSTANT:
1299     return false;
1300
1301   default: Unhandled() << mk;
1302   }
1303 }
1304
1305 inline Kind NodeManager::operatorToKind(TNode n) {
1306   return kind::operatorToKind(n.d_nv);
1307 }
1308
1309 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
1310   NodeBuilder<1> nb(this, kind);
1311   nb << child1;
1312   return nb.constructNode();
1313 }
1314
1315 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
1316   NodeBuilder<1> nb(this, kind);
1317   nb << child1;
1318   return nb.constructNodePtr();
1319 }
1320
1321 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
1322   NodeBuilder<2> nb(this, kind);
1323   nb << child1 << child2;
1324   return nb.constructNode();
1325 }
1326
1327 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
1328   NodeBuilder<2> nb(this, kind);
1329   nb << child1 << child2;
1330   return nb.constructNodePtr();
1331 }
1332
1333 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1334                                 TNode child3) {
1335   NodeBuilder<3> nb(this, kind);
1336   nb << child1 << child2 << child3;
1337   return nb.constructNode();
1338 }
1339
1340 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1341                                 TNode child3) {
1342   NodeBuilder<3> nb(this, kind);
1343   nb << child1 << child2 << child3;
1344   return nb.constructNodePtr();
1345 }
1346
1347 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1348                                 TNode child3, TNode child4) {
1349   NodeBuilder<4> nb(this, kind);
1350   nb << child1 << child2 << child3 << child4;
1351   return nb.constructNode();
1352 }
1353
1354 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1355                                 TNode child3, TNode child4) {
1356   NodeBuilder<4> nb(this, kind);
1357   nb << child1 << child2 << child3 << child4;
1358   return nb.constructNodePtr();
1359 }
1360
1361 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
1362                                 TNode child3, TNode child4, TNode child5) {
1363   NodeBuilder<5> nb(this, kind);
1364   nb << child1 << child2 << child3 << child4 << child5;
1365   return nb.constructNode();
1366 }
1367
1368 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
1369                                     TNode child3, TNode child4, TNode child5) {
1370   NodeBuilder<5> nb(this, kind);
1371   nb << child1 << child2 << child3 << child4 << child5;
1372   return nb.constructNodePtr();
1373 }
1374
1375 // N-ary version
1376 template <bool ref_count>
1377 inline Node NodeManager::mkNode(Kind kind,
1378                                 const std::vector<NodeTemplate<ref_count> >&
1379                                 children) {
1380   NodeBuilder<> nb(this, kind);
1381   nb.append(children);
1382   return nb.constructNode();
1383 }
1384
1385 template <bool ref_count>
1386 Node NodeManager::mkAnd(const std::vector<NodeTemplate<ref_count> >& children)
1387 {
1388   if (children.empty())
1389   {
1390     return mkConst(true);
1391   }
1392   else if (children.size() == 1)
1393   {
1394     return children[0];
1395   }
1396   return mkNode(kind::AND, children);
1397 }
1398
1399 template <bool ref_count>
1400 inline Node* NodeManager::mkNodePtr(Kind kind,
1401                                 const std::vector<NodeTemplate<ref_count> >&
1402                                 children) {
1403   NodeBuilder<> nb(this, kind);
1404   nb.append(children);
1405   return nb.constructNodePtr();
1406 }
1407
1408 // for operators
1409 inline Node NodeManager::mkNode(TNode opNode) {
1410   NodeBuilder<1> nb(this, operatorToKind(opNode));
1411   if(opNode.getKind() != kind::BUILTIN) {
1412     nb << opNode;
1413   }
1414   return nb.constructNode();
1415 }
1416
1417 inline Node* NodeManager::mkNodePtr(TNode opNode) {
1418   NodeBuilder<1> nb(this, operatorToKind(opNode));
1419   if(opNode.getKind() != kind::BUILTIN) {
1420     nb << opNode;
1421   }
1422   return nb.constructNodePtr();
1423 }
1424
1425 inline Node NodeManager::mkNode(TNode opNode, TNode child1) {
1426   NodeBuilder<2> nb(this, operatorToKind(opNode));
1427   if(opNode.getKind() != kind::BUILTIN) {
1428     nb << opNode;
1429   }
1430   nb << child1;
1431   return nb.constructNode();
1432 }
1433
1434 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) {
1435   NodeBuilder<2> nb(this, operatorToKind(opNode));
1436   if(opNode.getKind() != kind::BUILTIN) {
1437     nb << opNode;
1438   }
1439   nb << child1;
1440   return nb.constructNodePtr();
1441 }
1442
1443 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) {
1444   NodeBuilder<3> nb(this, operatorToKind(opNode));
1445   if(opNode.getKind() != kind::BUILTIN) {
1446     nb << opNode;
1447   }
1448   nb << child1 << child2;
1449   return nb.constructNode();
1450 }
1451
1452 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) {
1453   NodeBuilder<3> nb(this, operatorToKind(opNode));
1454   if(opNode.getKind() != kind::BUILTIN) {
1455     nb << opNode;
1456   }
1457   nb << child1 << child2;
1458   return nb.constructNodePtr();
1459 }
1460
1461 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1462                                 TNode child3) {
1463   NodeBuilder<4> nb(this, operatorToKind(opNode));
1464   if(opNode.getKind() != kind::BUILTIN) {
1465     nb << opNode;
1466   }
1467   nb << child1 << child2 << child3;
1468   return nb.constructNode();
1469 }
1470
1471 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1472                                 TNode child3) {
1473   NodeBuilder<4> nb(this, operatorToKind(opNode));
1474   if(opNode.getKind() != kind::BUILTIN) {
1475     nb << opNode;
1476   }
1477   nb << child1 << child2 << child3;
1478   return nb.constructNodePtr();
1479 }
1480
1481 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1482                                 TNode child3, TNode child4) {
1483   NodeBuilder<5> nb(this, operatorToKind(opNode));
1484   if(opNode.getKind() != kind::BUILTIN) {
1485     nb << opNode;
1486   }
1487   nb << child1 << child2 << child3 << child4;
1488   return nb.constructNode();
1489 }
1490
1491 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1492                                 TNode child3, TNode child4) {
1493   NodeBuilder<5> nb(this, operatorToKind(opNode));
1494   if(opNode.getKind() != kind::BUILTIN) {
1495     nb << opNode;
1496   }
1497   nb << child1 << child2 << child3 << child4;
1498   return nb.constructNodePtr();
1499 }
1500
1501 inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2,
1502                                 TNode child3, TNode child4, TNode child5) {
1503   NodeBuilder<6> nb(this, operatorToKind(opNode));
1504   if(opNode.getKind() != kind::BUILTIN) {
1505     nb << opNode;
1506   }
1507   nb << child1 << child2 << child3 << child4 << child5;
1508   return nb.constructNode();
1509 }
1510
1511 inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2,
1512                                     TNode child3, TNode child4, TNode child5) {
1513   NodeBuilder<6> nb(this, operatorToKind(opNode));
1514   if(opNode.getKind() != kind::BUILTIN) {
1515     nb << opNode;
1516   }
1517   nb << child1 << child2 << child3 << child4 << child5;
1518   return nb.constructNodePtr();
1519 }
1520
1521 // N-ary version for operators
1522 template <bool ref_count>
1523 inline Node NodeManager::mkNode(TNode opNode,
1524                                 const std::vector<NodeTemplate<ref_count> >&
1525                                 children) {
1526   NodeBuilder<> nb(this, operatorToKind(opNode));
1527   if(opNode.getKind() != kind::BUILTIN) {
1528     nb << opNode;
1529   }
1530   nb.append(children);
1531   return nb.constructNode();
1532 }
1533
1534 template <bool ref_count>
1535 inline Node* NodeManager::mkNodePtr(TNode opNode,
1536                                     const std::vector<NodeTemplate<ref_count> >&
1537                                     children) {
1538   NodeBuilder<> nb(this, operatorToKind(opNode));
1539   if(opNode.getKind() != kind::BUILTIN) {
1540     nb << opNode;
1541   }
1542   nb.append(children);
1543   return nb.constructNodePtr();
1544 }
1545
1546
1547 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1) {
1548   return (NodeBuilder<1>(this, kind) << child1).constructTypeNode();
1549 }
1550
1551 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1552                                         TypeNode child2) {
1553   return (NodeBuilder<2>(this, kind) << child1 << child2).constructTypeNode();
1554 }
1555
1556 inline TypeNode NodeManager::mkTypeNode(Kind kind, TypeNode child1,
1557                                         TypeNode child2, TypeNode child3) {
1558   return (NodeBuilder<3>(this, kind) << child1 << child2 << child3).constructTypeNode();
1559 }
1560
1561 // N-ary version for types
1562 inline TypeNode NodeManager::mkTypeNode(Kind kind,
1563                                         const std::vector<TypeNode>& children) {
1564   return NodeBuilder<>(this, kind).append(children).constructTypeNode();
1565 }
1566
1567 template <class T>
1568 Node NodeManager::mkConst(const T& val) {
1569   return mkConstInternal<Node, T>(val);
1570 }
1571
1572 template <class T>
1573 TypeNode NodeManager::mkTypeConst(const T& val) {
1574   return mkConstInternal<TypeNode, T>(val);
1575 }
1576
1577 template <class NodeClass, class T>
1578 NodeClass NodeManager::mkConstInternal(const T& val) {
1579   // This method indirectly calls `NodeValue::inc()`, which relies on having
1580   // the correct `NodeManager` in scope.
1581   NodeManagerScope nms(this);
1582
1583   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
1584   NVStorage<1> nvStorage;
1585   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
1586
1587   nvStack.d_id = 0;
1588   nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
1589   nvStack.d_rc = 0;
1590   nvStack.d_nchildren = 1;
1591
1592 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1593 #pragma GCC diagnostic push
1594 #pragma GCC diagnostic ignored "-Warray-bounds"
1595 #endif
1596
1597   nvStack.d_children[0] =
1598     const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
1599   expr::NodeValue* nv = poolLookup(&nvStack);
1600
1601 #if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6))
1602 #pragma GCC diagnostic pop
1603 #endif
1604
1605   if(nv != NULL) {
1606     return NodeClass(nv);
1607   }
1608
1609   nv = (expr::NodeValue*)
1610     std::malloc(sizeof(expr::NodeValue) + sizeof(T));
1611   if(nv == NULL) {
1612     throw std::bad_alloc();
1613   }
1614
1615   nv->d_nchildren = 0;
1616   nv->d_kind = kind::metakind::ConstantMap<T>::kind;
1617   nv->d_id = next_id++;// FIXME multithreading
1618   nv->d_rc = 0;
1619
1620   //OwningTheory::mkConst(val);
1621   new (&nv->d_children) T(val);
1622
1623   poolInsert(nv);
1624   if(Debug.isOn("gc")) {
1625     Debug("gc") << "creating node value " << nv
1626                 << " [" << nv->d_id << "]: ";
1627     nv->printAst(Debug("gc"));
1628     Debug("gc") << std::endl;
1629   }
1630
1631   return NodeClass(nv);
1632 }
1633
1634 }/* CVC4 namespace */
1635
1636 #endif /* CVC4__NODE_MANAGER_H */