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