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