src/expr/node_manager.h

   1 /*********************                                                        */
   2 /** node_manager.h
   3  ** Original author: mdeters
   4  ** Major contributors: cconway
   5  ** Minor contributors (to current version): taking, dejan
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** A manager for Nodes.
  14  **
  15  ** Reviewed by Chris Conway, Apr 5 2010 (bug #65).
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 /* circular dependency; force node.h first */
  21 #include "expr/attribute.h"
  22 #include "expr/node.h"
  23 #include "expr/type_node.h"
  24
  25 #ifndef __CVC4__NODE_MANAGER_H
  26 #define __CVC4__NODE_MANAGER_H
  27
  28 #include <vector>
  29 #include <string>
  30 #include <ext/hash_set>
  31
  32 #include "expr/kind.h"
  33 #include "expr/metakind.h"
  34 #include "expr/node_value.h"
  35 #include "context/context.h"
  36
  37 namespace CVC4 {
  38
  39 namespace expr {
  40
  41 // Definition of an attribute for the variable name.
  42 // TODO: hide this attribute behind a NodeManager interface.
  43 namespace attr {
  44   struct VarNameTag {};
  45 }/* CVC4::expr::attr namespace */
  46
  47 typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr;
  48
  49 }/* CVC4::expr namespace */
  50
  51 class NodeManager {
  52   template <class Builder> friend class CVC4::NodeBuilderBase;
  53   friend class NodeManagerScope;
  54   friend class expr::NodeValue;
  55
  56   typedef __gnu_cxx::hash_set<expr::NodeValue*,
  57                               expr::NodeValuePoolHashFcn,
  58                               expr::NodeValuePoolEq> NodeValuePool;
  59   typedef __gnu_cxx::hash_set<expr::NodeValue*,
  60                               expr::NodeValueIDHashFunction,
  61                               expr::NodeValueEq> ZombieSet;
  62
  63   static __thread NodeManager* s_current;
  64
  65   NodeValuePool d_nodeValuePool;
  66
  67   expr::attr::AttributeManager d_attrManager;
  68
  69   /**
  70    * The node value we're currently freeing.  This unique node value
  71    * is permitted to have outstanding TNodes to it (in "soft"
  72    * contexts, like as a key in attribute tables), even though
  73    * normally it's an error to have a TNode to a node value with a
  74    * reference count of 0.  Being "under deletion" also enables
  75    * assertions that inc() is not called on it.  (A poorly-behaving
  76    * attribute cleanup function could otherwise create a "Node" that
  77    * points to the node value that is in the process of being deleted,
  78    * springing it back to life.)
  79    */
  80   expr::NodeValue* d_nodeUnderDeletion;
  81
  82   /**
  83    * True iff we are in reclaimZombies().  This avoids unnecessary
  84    * recursion; a NodeValue being deleted might zombify other
  85    * NodeValues, but these shouldn't trigger a (recursive) call to
  86    * reclaimZombies().
  87    */
  88   bool d_dontGC;
  89
  90   /**
  91    * Marks that we are in the Destructor currently.
  92    */
  93   bool d_inDestruction;
  94
  95   /**
  96    * The set of zombie nodes.  We may want to revisit this design, as
  97    * we might like to delete nodes in least-recently-used order.  But
  98    * we also need to avoid processing a zombie twice.
  99    */
 100   ZombieSet d_zombies;
 101
 102   /**
 103    * A set of operator singletons (w.r.t.  to this NodeManager
 104    * instance) for operators.  Conceptually, Nodes with kind, say,
 105    * PLUS, are APPLYs of a PLUS operator to arguments.  This array
 106    * holds the set of operators for these things.  A PLUS operator is
 107    * a Node with kind "BUILTIN", and if you call
 108    * plusOperator->getConst<CVC4::Kind>(), you get kind::PLUS back.
 109    */
 110   Node d_operators[kind::LAST_KIND];
 111
 112   /**
 113    * Look up a NodeValue in the pool associated to this NodeManager.
 114    * The NodeValue argument need not be a "completely-constructed"
 115    * NodeValue.  In particular, "non-inlined" constants are permitted
 116    * (see below).
 117    *
 118    * For non-CONSTANT metakinds, nv's d_kind and d_nchildren should be
 119    * correctly set, and d_children[0..n-1] should be valid (extant)
 120    * NodeValues for lookup.
 121    *
 122    * For CONSTANT metakinds, nv's d_kind should be set correctly.
 123    * Normally a CONSTANT would have d_nchildren == 0 and the constant
 124    * value inlined in the d_children space.  However, here we permit
 125    * "non-inlined" NodeValues to avoid unnecessary copying.  For
 126    * these, d_nchildren == 1, and d_nchildren is a pointer to the
 127    * constant value.
 128    *
 129    * The point of this complex design is to permit efficient lookups
 130    * (without fully constructing a NodeValue).  In the case that the
 131    * argument is not fully constructed, and this function returns
 132    * NULL, the caller should fully construct an equivalent one before
 133    * calling poolInsert().  NON-FULLY-CONSTRUCTED NODEVALUES are not
 134    * permitted in the pool!
 135    */
 136   inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
 137
 138   /**
 139    * Insert a NodeValue into the NodeManager's pool.
 140    *
 141    * It is an error to insert a NodeValue already in the pool.
 142    * Enquire first with poolLookup().
 143    */
 144   inline void poolInsert(expr::NodeValue* nv);
 145
 146   /**
 147    * Remove a NodeValue from the NodeManager's pool.
 148    *
 149    * It is an error to request the removal of a NodeValue from the
 150    * pool that is not in the pool.
 151    */
 152   inline void poolRemove(expr::NodeValue* nv);
 153
 154   /**
 155    * Determine if nv is currently being deleted by the NodeManager.
 156    */
 157   inline bool isCurrentlyDeleting(const expr::NodeValue* nv) const {
 158     return d_nodeUnderDeletion == nv;
 159   }
 160
 161   /**
 162    * Register a NodeValue as a zombie.
 163    */
 164   inline void markForDeletion(expr::NodeValue* nv) {
 165     Assert(nv->d_rc == 0);
 166
 167     // if d_reclaiming is set, make sure we don't call
 168     // reclaimZombies(), because it's already running.
 169     Debug("gc") << "zombifying node value " << nv
 170                 << " [" << nv->d_id << "]: " << *nv
 171                 << (d_dontGC ? " [CURRENTLY-RECLAIMING]" : "")
 172                 << std::endl;
 173     d_zombies.insert(nv);// FIXME multithreading
 174
 175     if(!d_dontGC) {// FIXME multithreading
 176       // for now, collect eagerly.  can add heuristic here later..
 177       reclaimZombies();
 178     }
 179   }
 180
 181   /**
 182    * Reclaim all zombies.
 183    */
 184   void reclaimZombies();
 185
 186   /**
 187    * This template gives a mechanism to stack-allocate a NodeValue
 188    * with enough space for N children (where N is a compile-time
 189    * constant).  You use it like this:
 190    *
 191    *   NVStorage<4> nvStorage;
 192    *   NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
 193    *
 194    * ...and then you can use nvStack as a NodeValue that you know has
 195    * room for 4 children.
 196    */
 197   template <size_t N>
 198   struct NVStorage {
 199     expr::NodeValue nv;
 200     expr::NodeValue* child[N];
 201   };/* struct NodeManager::NVStorage<N> */
 202
 203   // attribute tags
 204   struct TypeTag {};
 205   struct AtomicTag {};
 206
 207   // NodeManager's attributes.  These aren't exposed outside of this
 208   // class; use the getters.
 209   typedef expr::Attribute<TypeTag, TypeNode> TypeAttr;
 210   typedef expr::Attribute<AtomicTag, bool> AtomicAttr;
 211
 212   /**
 213    * Returns true if this node is atomic (has no more Boolean
 214    * structure).  This is the NodeValue version for NodeManager's
 215    * internal use.  There's a public version of this function below
 216    * that takes a TNode.
 217    * @param nv the node to check for atomicity
 218    * @return true if atomic
 219    */
 220   inline bool isAtomic(expr::NodeValue* nv) const {
 221     // The kindCanBeAtomic() and metakind checking are just optimizations
 222     // (to avoid the hashtable lookup).  We assume that all nodes have
 223     // the atomic attribute pre-computed and set at their time of
 224     // creation.  This is because:
 225     // (1) it's super cheap to do it bottom-up.
 226     // (2) if we computed it lazily, we'd need a second attribute to
 227     //     tell us whether we had computed it yet or not.
 228     // The pre-computation and registration occurs in poolInsert().
 229     AssertArgument(nv->getMetaKind() != kind::metakind::INVALID, *nv,
 230                    "NodeManager::isAtomic() called on INVALID node (%s)",
 231                    kind::kindToString(nv->getKind()).c_str());
 232     return
 233       nv->getMetaKind() == kind::metakind::VARIABLE ||
 234       nv->getMetaKind() == kind::metakind::CONSTANT ||
 235       ( kind::kindCanBeAtomic(nv->getKind()) &&
 236         getAttribute(nv, AtomicAttr()) );
 237   }
 238
 239 public:
 240
 241   NodeManager(context::Context* ctxt);
 242   ~NodeManager();
 243
 244   /**
 245    * Return true if we are in destruction.
 246    */
 247   bool inDestruction() const { return d_inDestruction; }
 248
 249   /** The node manager in the current context. */
 250   static NodeManager* currentNM() { return s_current; }
 251
 252   // general expression-builders
 253
 254   /** Create a node with no children. */
 255   Node mkNode(Kind kind);
 256   Node* mkNodePtr(Kind kind);
 257
 258   /** Create a node with one child. */
 259   Node mkNode(Kind kind, TNode child1);
 260   Node* mkNodePtr(Kind kind, TNode child1);
 261
 262   /** Create a node with two children. */
 263   Node mkNode(Kind kind, TNode child1, TNode child2);
 264   Node* mkNodePtr(Kind kind, TNode child1, TNode child2);
 265
 266   /** Create a node with three children. */
 267   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3);
 268   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3);
 269
 270   /** Create a node with four children. */
 271   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 272               TNode child4);
 273   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 274               TNode child4);
 275
 276   /** Create a node with five children. */
 277   Node mkNode(Kind kind, TNode child1, TNode child2, TNode child3,
 278               TNode child4, TNode child5);
 279   Node* mkNodePtr(Kind kind, TNode child1, TNode child2, TNode child3,
 280               TNode child4, TNode child5);
 281
 282   /** Create a node with an arbitrary number of children. */
 283   template <bool ref_count>
 284   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 285   template <bool ref_count>
 286   Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 287
 288   /**
 289    * Create a variable with the given name and type.  NOTE that no
 290    * lookup is done on the name.  If you mkVar("a", type) and then
 291    * mkVar("a", type) again, you have two variables.
 292    */
 293   Node mkVar(const std::string& name, const TypeNode& type);
 294   Node* mkVarPtr(const std::string& name, const TypeNode& type);
 295
 296   /** Create a variable with the given type. */
 297   Node mkVar(const TypeNode& type);
 298   Node* mkVarPtr(const TypeNode& type);
 299
 300
 301   /**
 302    * Create a constant of type T.  It will have the appropriate
 303    * CONST_* kind defined for T.
 304    */
 305   template <class T>
 306   Node mkConst(const T&);
 307
 308   template <class T>
 309   TypeNode mkTypeConst(const T&);
 310
 311   template <class NodeClass, class T>
 312   NodeClass mkConstInternal(const T&);
 313
 314   /** Create a type-variable */
 315   TypeNode mkTypeVar();
 316   TypeNode mkTypeVar(const std::string& name);
 317
 318   /** Create a node with no children. */
 319   TypeNode mkTypeNode(Kind kind, const std::vector<TypeNode>& children);
 320
 321   /**
 322    * Determine whether Nodes of a particular Kind have operators.
 323    * @returns true if Nodes of Kind k have operators.
 324    */
 325   static inline bool hasOperator(Kind k);
 326
 327   /**
 328    * Get the (singleton) operator of an OPERATOR-kinded kind.  The
 329    * returned node n will have kind BUILTIN, and calling
 330    * n.getConst<CVC4::Kind>() will yield k.
 331    */
 332   inline TNode operatorOf(Kind k) {
 333     AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
 334                     "Kind is not an OPERATOR-kinded kind "
 335                     "in NodeManager::operatorOf()" );
 336     return d_operators[k];
 337   }
 338
 339   /**
 340    * Retrieve an attribute for a node.
 341    *
 342    * @param nv the node value
 343    * @param attr an instance of the attribute kind to retrieve.
 344    * @returns the attribute, if set, or a default-constructed
 345    * <code>AttrKind::value_type</code> if not.
 346    */
 347   template <class AttrKind>
 348   inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
 349                                                     const AttrKind& attr) const;
 350
 351   /**
 352    * Check whether an attribute is set for a node.
 353    *
 354    * @param nv the node value
 355    * @param attr an instance of the attribute kind to check
 356    * @returns <code>true</code> iff <code>attr</code> is set for
 357    * <code>nv</code>.
 358    */
 359   template <class AttrKind>
 360   inline bool hasAttribute(expr::NodeValue* nv,
 361                            const AttrKind& attr) const;
 362
 363   /**
 364    * Check whether an attribute is set for a node, and, if so,
 365    * retrieve it.
 366    *
 367    * @param nv the node value
 368    * @param attr an instance of the attribute kind to check
 369    * @param value a reference to an object of the attribute's value type.
 370    * <code>value</code> will be set to the value of the attribute, if it is
 371    * set for <code>nv</code>; otherwise, it will be set to the default
 372    * value of the attribute.
 373    * @returns <code>true</code> iff <code>attr</code> is set for
 374    * <code>nv</code>.
 375    */
 376   template <class AttrKind>
 377   inline bool getAttribute(expr::NodeValue* nv,
 378                            const AttrKind& attr,
 379                            typename AttrKind::value_type& value) const;
 380
 381   /**
 382    * Set an attribute for a node.  If the node doesn't have the
 383    * attribute, this function assigns one.  If the node has one, this
 384    * overwrites it.
 385    *
 386    * @param nv the node value
 387    * @param attr an instance of the attribute kind to set
 388    * @param value the value of <code>attr</code> for <code>nv</code>
 389    */
 390   template <class AttrKind>
 391   inline void setAttribute(expr::NodeValue* nv,
 392                            const AttrKind& attr,
 393                            const typename AttrKind::value_type& value);
 394
 395   /**
 396    * Retrieve an attribute for a TNode.
 397    *
 398    * @param n the node
 399    * @param attr an instance of the attribute kind to retrieve.
 400    * @returns the attribute, if set, or a default-constructed
 401    * <code>AttrKind::value_type</code> if not.
 402    */
 403   template <class AttrKind>
 404   inline typename AttrKind::value_type
 405   getAttribute(TNode n, const AttrKind& attr) const;
 406
 407   /**
 408    * Check whether an attribute is set for a TNode.
 409    *
 410    * @param n the node
 411    * @param attr an instance of the attribute kind to check
 412    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 413    */
 414   template <class AttrKind>
 415   inline bool hasAttribute(TNode n,
 416                            const AttrKind& attr) const;
 417
 418   /**
 419    * Check whether an attribute is set for a TNode and, if so, retieve
 420    * it.
 421    *
 422    * @param n the node
 423    * @param attr an instance of the attribute kind to check
 424    * @param value a reference to an object of the attribute's value type.
 425    * <code>value</code> will be set to the value of the attribute, if it is
 426    * set for <code>nv</code>; otherwise, it will be set to the default value of
 427    * the attribute.
 428    * @returns <code>true</code> iff <code>attr</code> is set for <code>n</code>.
 429    */
 430   template <class AttrKind>
 431   inline bool getAttribute(TNode n,
 432                            const AttrKind& attr,
 433                            typename AttrKind::value_type& value) const;
 434
 435   /**
 436    * Set an attribute for a node.  If the node doesn't have the
 437    * attribute, this function assigns one.  If the node has one, this
 438    * overwrites it.
 439    *
 440    * @param n the node
 441    * @param attr an instance of the attribute kind to set
 442    * @param value the value of <code>attr</code> for <code>n</code>
 443    */
 444   template <class AttrKind>
 445   inline void setAttribute(TNode n,
 446                            const AttrKind& attr,
 447                            const typename AttrKind::value_type& value);
 448
 449   /** Get the (singleton) type for booleans. */
 450   inline TypeNode booleanType();
 451
 452   /** Get the (singleton) type for sorts. */
 453   inline TypeNode kindType();
 454
 455   /**
 456    * Make a function type from domain to range.
 457    *
 458    * @param domain the domain type
 459    * @param range the range type
 460    * @returns the functional type domain -> range
 461    */
 462   inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 463
 464   /**
 465    * Make a function type with input types from
 466    * argTypes. <code>argTypes</code> must have at least one element.
 467    *
 468    * @param argTypes the domain is a tuple (argTypes[0], ..., argTypes[n])
 469    * @param range the range type
 470    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
 471    */
 472   inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range);
 473
 474   /**
 475    * Make a function type with input types from
 476    * <code>sorts[0..sorts.size()-2]</code> and result type
 477    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
 478    * at least 2 elements.
 479    */
 480   inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 481
 482   /**
 483    * Make a predicate type with input types from
 484    * <code>sorts</code>. The result with be a function type with range
 485    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
 486    * element.
 487    */
 488   inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 489
 490   /** Make a new sort. */
 491   inline TypeNode mkSort();
 492
 493   /** Make a new sort with the given name. */
 494   inline TypeNode mkSort(const std::string& name);
 495
 496   /**
 497    * Get the type for the given node.
 498    */
 499   inline TypeNode getType(TNode n);
 500
 501   /**
 502    * Returns true if this node is atomic (has no more Boolean structure)
 503    * @param n the node to check for atomicity
 504    * @return true if atomic
 505    */
 506   inline bool isAtomic(TNode n) const {
 507     return isAtomic(n.d_nv);
 508   }
 509 };
 510
 511 /**
 512  * This class changes the "current" thread-global
 513  * <code>NodeManager</code> when it is created and reinstates the
 514  * previous thread-global <code>NodeManager</code> when it is
 515  * destroyed, effectively maintaining a set of nested
 516  * <code>NodeManager</code> scopes.  This is especially useful on
 517  * public-interface calls into the CVC4 library, where CVC4's notion
 518  * of the "current" <code>NodeManager</code> should be set to match
 519  * the calling context.  See, for example, the implementations of
 520  * public calls in the <code>ExprManager</code> and
 521  * <code>SmtEngine</code> classes.
 522  *
 523  * The client must be careful to create and destroy
 524  * <code>NodeManagerScope</code> objects in a well-nested manner (such
 525  * as on the stack). You may create a <code>NodeManagerScope</code>
 526  * with <code>new</code> and destroy it with <code>delete</code>, or
 527  * place it as a data member of an object that is, but if the scope of
 528  * these <code>new</code>/<code>delete</code> pairs isn't properly
 529  * maintained, the incorrect "current" <code>NodeManager</code>
 530  * pointer may be restored after a delete.
 531  */
 532 class NodeManagerScope {
 533   /** The old NodeManager, to be restored on destruction. */
 534   NodeManager *d_oldNodeManager;
 535
 536 public:
 537
 538   NodeManagerScope(NodeManager* nm) : d_oldNodeManager(NodeManager::s_current) {
 539     NodeManager::s_current = nm;
 540     Debug("current") << "node manager scope: "
 541                      << NodeManager::s_current << "\n";
 542   }
 543
 544   ~NodeManagerScope() {
 545     NodeManager::s_current = d_oldNodeManager;
 546     Debug("current") << "node manager scope: "
 547                      << "returning to " << NodeManager::s_current << "\n";
 548   }
 549 };
 550
 551
 552 template <class AttrKind>
 553 inline typename AttrKind::value_type
 554 NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&) const {
 555   return d_attrManager.getAttribute(nv, AttrKind());
 556 }
 557
 558 template <class AttrKind>
 559 inline bool NodeManager::hasAttribute(expr::NodeValue* nv,
 560                                       const AttrKind&) const {
 561   return d_attrManager.hasAttribute(nv, AttrKind());
 562 }
 563
 564 template <class AttrKind>
 565 inline bool
 566 NodeManager::getAttribute(expr::NodeValue* nv, const AttrKind&,
 567                           typename AttrKind::value_type& ret) const {
 568   return d_attrManager.getAttribute(nv, AttrKind(), ret);
 569 }
 570
 571 template <class AttrKind>
 572 inline void
 573 NodeManager::setAttribute(expr::NodeValue* nv, const AttrKind&,
 574                           const typename AttrKind::value_type& value) {
 575   d_attrManager.setAttribute(nv, AttrKind(), value);
 576 }
 577
 578 template <class AttrKind>
 579 inline typename AttrKind::value_type
 580 NodeManager::getAttribute(TNode n, const AttrKind&) const {
 581   return d_attrManager.getAttribute(n.d_nv, AttrKind());
 582 }
 583
 584 template <class AttrKind>
 585 inline bool
 586 NodeManager::hasAttribute(TNode n, const AttrKind&) const {
 587   return d_attrManager.hasAttribute(n.d_nv, AttrKind());
 588 }
 589
 590 template <class AttrKind>
 591 inline bool
 592 NodeManager::getAttribute(TNode n, const AttrKind&,
 593                           typename AttrKind::value_type& ret) const {
 594   return d_attrManager.getAttribute(n.d_nv, AttrKind(), ret);
 595 }
 596
 597 template <class AttrKind>
 598 inline void
 599 NodeManager::setAttribute(TNode n, const AttrKind&,
 600                           const typename AttrKind::value_type& value) {
 601   d_attrManager.setAttribute(n.d_nv, AttrKind(), value);
 602 }
 603
 604
 605 /** Get the (singleton) type for booleans. */
 606 inline TypeNode NodeManager::booleanType() {
 607   return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
 608 }
 609
 610 /** Get the (singleton) type for sorts. */
 611 inline TypeNode NodeManager::kindType() {
 612   return TypeNode(mkTypeConst<TypeConstant>(KIND_TYPE));
 613 }
 614
 615 /** Make a function type from domain to range. */
 616 inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
 617   std::vector<TypeNode> sorts;
 618   sorts.push_back(domain);
 619   sorts.push_back(range);
 620   return mkFunctionType(sorts);
 621 }
 622
 623 inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
 624   Assert(argTypes.size() >= 1);
 625   std::vector<TypeNode> sorts(argTypes);
 626   sorts.push_back(range);
 627   return mkFunctionType(sorts);
 628 }
 629
 630 inline TypeNode
 631 NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
 632   Assert(sorts.size() >= 2);
 633   std::vector<TypeNode> sortNodes;
 634   for (unsigned i = 0; i < sorts.size(); ++ i) {
 635     sortNodes.push_back(sorts[i]);
 636   }
 637   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 638 }
 639
 640 inline TypeNode
 641 NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
 642   Assert(sorts.size() >= 1);
 643   std::vector<TypeNode> sortNodes;
 644   for (unsigned i = 0; i < sorts.size(); ++ i) {
 645     sortNodes.push_back(sorts[i]);
 646   }
 647   sortNodes.push_back(booleanType());
 648   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
 649 }
 650
 651 inline TypeNode NodeManager::mkSort() {
 652   return mkTypeVar();
 653 }
 654
 655 inline TypeNode NodeManager::mkSort(const std::string& name) {
 656   return mkTypeVar(name);
 657 }
 658
 659 inline TypeNode NodeManager::getType(TNode n)  {
 660   TypeNode typeNode;
 661   getAttribute(n, TypeAttr(), typeNode);
 662   // TODO: Type computation
 663   return typeNode;
 664 }
 665
 666 inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
 667   NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
 668   if(find == d_nodeValuePool.end()) {
 669     return NULL;
 670   } else {
 671     return *find;
 672   }
 673 }
 674
 675 inline void NodeManager::poolInsert(expr::NodeValue* nv) {
 676   Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
 677          "NodeValue already in the pool!");
 678   d_nodeValuePool.insert(nv);// FIXME multithreading
 679
 680   switch(nv->getMetaKind()) {
 681   case kind::metakind::INVALID:
 682   case kind::metakind::VARIABLE:
 683   case kind::metakind::CONSTANT:
 684     // nothing to do (don't bother setting the attribute, isAtomic()
 685     // on VARIABLEs and CONSTANTs is always true)
 686     break;
 687
 688   case kind::metakind::OPERATOR:
 689   case kind::metakind::PARAMETERIZED:
 690     {
 691       // register this NodeValue as atomic or not; use nv_begin/end
 692       // because we need to consider the operator too in the case of
 693       // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a
 694       // buried ITE.
 695
 696       // assume it's atomic if its kind can be atomic, check children
 697       // to see if that is actually true
 698       bool atomic = kind::kindCanBeAtomic(nv->getKind());
 699       if(atomic) {
 700         for(expr::NodeValue::nv_iterator i = nv->nv_begin();
 701             i != nv->nv_end();
 702             ++i) {
 703           if(!(atomic = isAtomic(*i))) {
 704             break;
 705           }
 706         }
 707       }
 708
 709       setAttribute(nv, AtomicAttr(), atomic);
 710     }
 711   }
 712 }
 713
 714 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
 715   Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(),
 716          "NodeValue is not in the pool!");
 717
 718   d_nodeValuePool.erase(nv);// FIXME multithreading
 719 }
 720
 721 }/* CVC4 namespace */
 722
 723 #define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 724 #include "expr/metakind.h"
 725 #undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
 726
 727 #include "expr/node_builder.h"
 728
 729 namespace CVC4 {
 730
 731 // general expression-builders
 732
 733 inline bool NodeManager::hasOperator(Kind k) {
 734   switch(kind::MetaKind mk = kind::metaKindOf(k)) {
 735
 736   case kind::metakind::INVALID:
 737   case kind::metakind::VARIABLE:
 738     return false;
 739
 740   case kind::metakind::OPERATOR:
 741   case kind::metakind::PARAMETERIZED:
 742     return true;
 743
 744   case kind::metakind::CONSTANT:
 745     return false;
 746
 747   default:
 748     Unhandled(mk);
 749   }
 750 }
 751
 752 inline Node NodeManager::mkNode(Kind kind) {
 753   return NodeBuilder<0>(this, kind);
 754 }
 755
 756 inline Node* NodeManager::mkNodePtr(Kind kind) {
 757   NodeBuilder<0> nb(this, kind);
 758   return nb.constructNodePtr();
 759 }
 760
 761 inline Node NodeManager::mkNode(Kind kind, TNode child1) {
 762   return NodeBuilder<1>(this, kind) << child1;
 763 }
 764
 765 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1) {
 766   NodeBuilder<1> nb(this, kind);
 767   nb << child1;
 768   return nb.constructNodePtr();
 769 }
 770
 771 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2) {
 772   return NodeBuilder<2>(this, kind) << child1 << child2;
 773 }
 774
 775 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2) {
 776   NodeBuilder<2> nb(this, kind);
 777   nb << child1 << child2;
 778   return nb.constructNodePtr();
 779 }
 780
 781 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
 782                                 TNode child3) {
 783   return NodeBuilder<3>(this, kind) << child1 << child2 << child3;
 784 }
 785
 786 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
 787                                 TNode child3) {
 788   NodeBuilder<3> nb(this, kind);
 789   nb << child1 << child2 << child3;
 790   return nb.constructNodePtr();
 791 }
 792
 793 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
 794                                 TNode child3, TNode child4) {
 795   return NodeBuilder<4>(this, kind) << child1 << child2 << child3 << child4;
 796 }
 797
 798 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
 799                                 TNode child3, TNode child4) {
 800   NodeBuilder<4> nb(this, kind);
 801   nb << child1 << child2 << child3 << child4;
 802   return nb.constructNodePtr();
 803 }
 804
 805 inline Node NodeManager::mkNode(Kind kind, TNode child1, TNode child2,
 806                                 TNode child3, TNode child4, TNode child5) {
 807   return NodeBuilder<5>(this, kind) << child1 << child2 << child3 << child4
 808                                    << child5;
 809 }
 810
 811 inline Node* NodeManager::mkNodePtr(Kind kind, TNode child1, TNode child2,
 812                                 TNode child3, TNode child4, TNode child5) {
 813   NodeBuilder<5> nb(this, kind);
 814   nb << child1 << child2 << child3 << child4 << child5;
 815   return nb.constructNodePtr();
 816 }
 817
 818 // N-ary version
 819 template <bool ref_count>
 820 inline Node NodeManager::mkNode(Kind kind,
 821                                 const std::vector<NodeTemplate<ref_count> >&
 822                                 children) {
 823   return NodeBuilder<>(this, kind).append(children);
 824 }
 825
 826 template <bool ref_count>
 827 inline Node* NodeManager::mkNodePtr(Kind kind,
 828                                 const std::vector<NodeTemplate<ref_count> >&
 829                                 children) {
 830   return NodeBuilder<>(this, kind).append(children).constructNodePtr();
 831 }
 832
 833 // N-ary version for types
 834 inline TypeNode NodeManager::mkTypeNode(Kind kind, const std::vector<TypeNode>& children) {
 835   return NodeBuilder<>(this, kind).append(children).constructTypeNode();
 836 }
 837
 838
 839 inline Node NodeManager::mkVar(const std::string& name, const TypeNode& type) {
 840   Node n = mkVar(type);
 841   n.setAttribute(expr::VarNameAttr(), name);
 842   return n;
 843 }
 844
 845 inline Node* NodeManager::mkVarPtr(const std::string& name, const TypeNode& type) {
 846   Node* n = mkVarPtr(type);
 847   n->setAttribute(expr::VarNameAttr(), name);
 848   return n;
 849 }
 850
 851 inline Node NodeManager::mkVar(const TypeNode& type) {
 852   Node n = NodeBuilder<0>(this, kind::VARIABLE);
 853   n.setAttribute(TypeAttr(), type);
 854   return n;
 855 }
 856
 857 inline TypeNode NodeManager::mkTypeVar(const std::string& name) {
 858   TypeNode type = mkTypeVar();
 859   type.setAttribute(expr::VarNameAttr(), name);
 860   return type;
 861 }
 862
 863 inline TypeNode NodeManager::mkTypeVar() {
 864   TypeNode type = NodeBuilder<0>(this, kind::VARIABLE).constructTypeNode();
 865   return type;
 866 }
 867
 868 inline Node* NodeManager::mkVarPtr(const TypeNode& type) {
 869   Node* n = NodeBuilder<0>(this, kind::VARIABLE).constructNodePtr();
 870   n->setAttribute(TypeAttr(), type);
 871   return n;
 872 }
 873
 874 template <class T>
 875 Node NodeManager::mkConst(const T& val) {
 876   return mkConstInternal<Node, T>(val);
 877 }
 878
 879 template <class T>
 880 TypeNode NodeManager::mkTypeConst(const T& val) {
 881   return mkConstInternal<TypeNode, T>(val);
 882 }
 883
 884 template <class NodeClass, class T>
 885 NodeClass NodeManager::mkConstInternal(const T& val) {
 886
 887   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
 888   NVStorage<1> nvStorage;
 889   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
 890
 891   nvStack.d_id = 0;
 892   nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
 893   nvStack.d_rc = 0;
 894   nvStack.d_nchildren = 1;
 895   nvStack.d_children[0] =
 896     const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
 897   expr::NodeValue* nv = poolLookup(&nvStack);
 898
 899   if(nv != NULL) {
 900     return NodeClass(nv);
 901   }
 902
 903   nv = (expr::NodeValue*)
 904     std::malloc(sizeof(expr::NodeValue) + sizeof(T));
 905   if(nv == NULL) {
 906     throw std::bad_alloc();
 907   }
 908
 909   nv->d_nchildren = 0;
 910   nv->d_kind = kind::metakind::ConstantMap<T>::kind;
 911   nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
 912   nv->d_rc = 0;
 913
 914   //OwningTheory::mkConst(val);
 915   new (&nv->d_children) T(val);
 916
 917   poolInsert(nv);
 918   Debug("gc") << "creating node value " << nv
 919               << " [" << nv->d_id << "]: " << *nv << "\n";
 920
 921   return NodeClass(nv);
 922 }
 923
 924 }/* CVC4 namespace */
 925
 926 #endif /* __CVC4__EXPR_MANAGER_H */