src/expr/node_manager.h

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