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