src/expr/node.h

   1 /*********************                                                        */
   2 /*! \file node.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan
   6  ** Minor contributors (to current version): taking, cconway
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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 Reference-counted encapsulation of a pointer to node information
  15  **
  16  ** Reference-counted encapsulation of a pointer to node information.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 // circular dependency
  22 #include "expr/node_value.h"
  23
  24 #ifndef __CVC4__NODE_H
  25 #define __CVC4__NODE_H
  26
  27 #include <vector>
  28 #include <string>
  29 #include <iostream>
  30 #include <utility>
  31 #include <algorithm>
  32 #include <functional>
  33 #include <stdint.h>
  34
  35 #include "expr/type.h"
  36 #include "expr/kind.h"
  37 #include "expr/metakind.h"
  38 #include "expr/expr.h"
  39 #include "util/Assert.h"
  40 #include "util/configuration.h"
  41 #include "util/output.h"
  42 #include "util/exception.h"
  43 #include "util/language.h"
  44 #include "util/utility.h"
  45 #include "util/hash.h"
  46
  47 namespace CVC4 {
  48
  49 class TypeNode;
  50 class NodeManager;
  51
  52 namespace expr {
  53   namespace pickle {
  54     class PicklerPrivate;
  55   }/* CVC4::expr::pickle namespace */
  56 }/* CVC4::expr namespace */
  57
  58 template <bool ref_count>
  59 class NodeTemplate;
  60
  61 /**
  62  * Exception thrown during the type-checking phase, it can be
  63  * thrown by node.getType().
  64  */
  65 class TypeCheckingExceptionPrivate : public Exception {
  66
  67 private:
  68
  69   /** The node responsible for the failure */
  70   NodeTemplate<true>* d_node;
  71
  72 protected:
  73
  74   TypeCheckingExceptionPrivate() throw() : Exception() {}
  75
  76 public:
  77
  78   /**
  79    * Construct the exception with the problematic node and the message
  80    * @param node the problematic node
  81    * @param message the message explaining the failure
  82    */
  83   TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw();
  84
  85   /** Destructor */
  86   ~TypeCheckingExceptionPrivate() throw ();
  87
  88   /**
  89    * Get the Node that caused the type-checking to fail.
  90    * @return the node
  91    */
  92   NodeTemplate<true> getNode() const throw();
  93
  94   /**
  95    * Returns the message corresponding to the type-checking failure.
  96    * We prefer toStream() to toString() because that keeps the expr-depth
  97    * and expr-language settings present in the stream.
  98    */
  99   void toStream(std::ostream& out) const throw();
 100
 101 };/* class TypeCheckingExceptionPrivate */
 102
 103 /**
 104  * \typedef NodeTemplate<true> Node;
 105  *
 106  * The Node class encapsulates the NodeValue with reference counting.
 107  *
 108  * One should use generally use Nodes to manipulate expressions, to be safe.
 109  * Every outstanding Node that references a NodeValue is counted in that
 110  * NodeValue's reference count.  Reference counts are maintained correctly
 111  * on assignment of the Node object (to point to another NodeValue), and,
 112  * upon destruction of the Node object, the NodeValue's reference count is
 113  * decremented and, if zero, it becomes eligible for reclamation by the
 114  * system.
 115  */
 116 typedef NodeTemplate<true> Node;
 117
 118 /**
 119  * \typedef NodeTemplate<false> TNode;
 120  *
 121  * The TNode class encapsulates the NodeValue but doesn't count references.
 122  *
 123  * TNodes are just like Nodes, but they don't update the reference count.
 124  * Therefore, there is less overhead (copying a TNode is just the cost of
 125  * the underlying pointer copy).  Generally speaking, this is unsafe!
 126  * However, there are certain situations where a TNode can be used safely.
 127  *
 128  * The largest class of uses for TNodes are when you need to use them in a
 129  * "temporary," scoped fashion (hence the "T" in "TNode").  In general,
 130  * it is safe to use TNode as a function parameter type, since the calling
 131  * function (or some other function on the call stack) presumably has a Node
 132  * reference to the expression data.  It is generally _not_ safe, however,
 133  * to return a TNode _from_ a function.  (Functions that return Nodes often
 134  * create the expression they return; such new expressions may not be
 135  * referenced on the call stack, and have a reference count of 1 on
 136  * creation.  If this is returned as a TNode rather than a Node, the
 137  * count drops to zero, marking the expression as eligible for reclamation.)
 138  *
 139  * More guidelines on when to use TNodes is available in the CVC4
 140  * Developer's Guide:
 141  * http://goedel.cims.nyu.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29
 142  */
 143 typedef NodeTemplate<false> TNode;
 144
 145 namespace expr {
 146
 147 class NodeValue;
 148
 149   namespace attr {
 150     class AttributeManager;
 151   }/* CVC4::expr::attr namespace */
 152
 153   class ExprSetDepth;
 154 }/* CVC4::expr namespace */
 155
 156 namespace kind {
 157   namespace metakind {
 158     struct NodeValueConstPrinter;
 159   }/* CVC4::kind::metakind namespace */
 160 }/* CVC4::kind namespace */
 161
 162 /**
 163  * Encapsulation of an NodeValue pointer.  The reference count is
 164  * maintained in the NodeValue if ref_count is true.
 165  * @param ref_count if true reference are counted in the NodeValue
 166  */
 167 template <bool ref_count>
 168 class NodeTemplate {
 169
 170   // for hash_maps, hash_sets..
 171   template <bool ref_count1>
 172   struct HashFunction {
 173     size_t operator()(CVC4::NodeTemplate<ref_count1> node) const {
 174       return (size_t) node.getId();
 175     }
 176   };/* struct HashFunction */
 177
 178   typedef HashFunction<false> TNodeHashFunction;
 179
 180   /**
 181    * The NodeValue has access to the private constructors, so that the
 182    * iterators can can create new nodes.
 183    */
 184   friend class expr::NodeValue;
 185
 186   friend class expr::pickle::PicklerPrivate;
 187   friend Node expr::exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap);
 188
 189   /** A convenient null-valued encapsulated pointer */
 190   static NodeTemplate s_null;
 191
 192   /** The referenced NodeValue */
 193   expr::NodeValue* d_nv;
 194
 195   /**
 196    * This constructor is reserved for use by the NodeTemplate package; one
 197    * must construct an NodeTemplate using one of the build mechanisms of the
 198    * NodeTemplate package.
 199    *
 200    * FIXME: there's a type-system escape here to cast away the const,
 201    * since the refcount needs to be updated.  But conceptually Nodes
 202    * don't change their arguments, and it's nice to have
 203    * const_iterators over them.
 204    *
 205    * This really does needs to be explicit to avoid hard to track errors with
 206    * Nodes implicitly wrapping NodeValues
 207    */
 208   explicit NodeTemplate(const expr::NodeValue*);
 209
 210   friend class NodeTemplate<true>;
 211   friend class NodeTemplate<false>;
 212   friend class TypeNode;
 213   friend class NodeManager;
 214
 215   template <unsigned nchild_thresh>
 216   friend class NodeBuilder;
 217
 218   friend class ::CVC4::expr::attr::AttributeManager;
 219
 220   friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
 221
 222   /**
 223    * Assigns the expression value and does reference counting. No assumptions
 224    * are made on the expression, and should only be used if we know what we
 225    * are doing.
 226    *
 227    * @param ev the expression value to assign
 228    */
 229   void assignNodeValue(expr::NodeValue* ev);
 230
 231   inline void assertTNodeNotExpired() const throw(AssertionException) {
 232     if(!ref_count) {
 233       Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
 234     }
 235   }
 236
 237   /**
 238    * Cache-aware, recursive version of substitute() used by the public
 239    * member function with a similar signature.
 240    */
 241   Node substitute(TNode node, TNode replacement,
 242                   std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
 243
 244   /**
 245    * Cache-aware, recursive version of substitute() used by the public
 246    * member function with a similar signature.
 247    */
 248   template <class Iterator1, class Iterator2>
 249   Node substitute(Iterator1 nodesBegin, Iterator1 nodesEnd,
 250                   Iterator2 replacementsBegin, Iterator2 replacementsEnd,
 251                   std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
 252
 253   /**
 254    * Cache-aware, recursive version of substitute() used by the public
 255    * member function with a similar signature.
 256    */
 257   template <class Iterator>
 258   Node substitute(Iterator substitutionsBegin, Iterator substitutionsEnd,
 259                   std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const;
 260
 261 public:
 262
 263   /** Default constructor, makes a null expression. */
 264   NodeTemplate() : d_nv(&expr::NodeValue::s_null) { }
 265
 266   /**
 267    * Conversion between nodes that are reference-counted and those that are
 268    * not.
 269    * @param node the node to make copy of
 270    */
 271   NodeTemplate(const NodeTemplate<!ref_count>& node);
 272
 273   /**
 274    * Copy constructor.  Note that GCC does NOT recognize an instantiation of
 275    * the above template as a copy constructor and problems ensue.  So we
 276    * provide an explicit one here.
 277    * @param node the node to make copy of
 278    */
 279   NodeTemplate(const NodeTemplate& node);
 280
 281   /**
 282    * Allow Exprs to become Nodes.  This permits flexible translation of
 283    * Exprs -> Nodes inside the CVC4 library without exposing a toNode()
 284    * function in the public interface, or requiring lots of "friend"
 285    * relationships.
 286    */
 287   NodeTemplate(const Expr& e);
 288
 289   /**
 290    * Assignment operator for nodes, copies the relevant information from node
 291    * to this node.
 292    * @param node the node to copy
 293    * @return reference to this node
 294    */
 295   NodeTemplate& operator=(const NodeTemplate& node);
 296
 297   /**
 298    * Assignment operator for nodes, copies the relevant information from node
 299    * to this node.
 300    * @param node the node to copy
 301    * @return reference to this node
 302    */
 303   NodeTemplate& operator=(const NodeTemplate<!ref_count>& node);
 304
 305   /**
 306    * Destructor. If ref_count is true it will decrement the reference count
 307    * and, if zero, collect the NodeValue.
 308    */
 309   ~NodeTemplate() throw(AssertionException);
 310
 311   /**
 312    * Return the null node.
 313    * @return the null node
 314    */
 315   static NodeTemplate null() {
 316     return s_null;
 317   }
 318
 319   /**
 320    * Returns true if this expression is a null expression.
 321    * @return true if null
 322    */
 323   bool isNull() const {
 324     assertTNodeNotExpired();
 325     return d_nv == &expr::NodeValue::s_null;
 326   }
 327
 328   /**
 329    * Structural comparison operator for expressions.
 330    * @param node the node to compare to
 331    * @return true if expressions are equal, false otherwise
 332    */
 333   template <bool ref_count_1>
 334   bool operator==(const NodeTemplate<ref_count_1>& node) const {
 335     assertTNodeNotExpired();
 336     node.assertTNodeNotExpired();
 337     return d_nv == node.d_nv;
 338   }
 339
 340   /**
 341    * Structural comparison operator for expressions.
 342    * @param node the node to compare to
 343    * @return false if expressions are equal, true otherwise
 344    */
 345   template <bool ref_count_1>
 346   bool operator!=(const NodeTemplate<ref_count_1>& node) const {
 347     assertTNodeNotExpired();
 348     node.assertTNodeNotExpired();
 349     return d_nv != node.d_nv;
 350   }
 351
 352   /**
 353    * We compare by expression ids so, keeping things deterministic and having
 354    * that subexpressions have to be smaller than the enclosing expressions.
 355    * @param node the node to compare to
 356    * @return true if this expression is smaller
 357    */
 358   template <bool ref_count_1>
 359   inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
 360     assertTNodeNotExpired();
 361     node.assertTNodeNotExpired();
 362     return d_nv->d_id < node.d_nv->d_id;
 363   }
 364
 365   /**
 366    * We compare by expression ids so, keeping things deterministic and having
 367    * that subexpressions have to be smaller than the enclosing expressions.
 368    * @param node the node to compare to
 369    * @return true if this expression is greater
 370    */
 371   template <bool ref_count_1>
 372   inline bool operator>(const NodeTemplate<ref_count_1>& node) const {
 373     assertTNodeNotExpired();
 374     node.assertTNodeNotExpired();
 375     return d_nv->d_id > node.d_nv->d_id;
 376   }
 377
 378   /**
 379    * We compare by expression ids so, keeping things deterministic and having
 380    * that subexpressions have to be smaller than the enclosing expressions.
 381    * @param node the node to compare to
 382    * @return true if this expression is smaller than or equal to
 383    */
 384   template <bool ref_count_1>
 385   inline bool operator<=(const NodeTemplate<ref_count_1>& node) const {
 386     assertTNodeNotExpired();
 387     node.assertTNodeNotExpired();
 388     return d_nv->d_id <= node.d_nv->d_id;
 389   }
 390
 391   /**
 392    * We compare by expression ids so, keeping things deterministic and having
 393    * that subexpressions have to be smaller than the enclosing expressions.
 394    * @param node the node to compare to
 395    * @return true if this expression is greater than or equal to
 396    */
 397   template <bool ref_count_1>
 398   inline bool operator>=(const NodeTemplate<ref_count_1>& node) const {
 399     assertTNodeNotExpired();
 400     node.assertTNodeNotExpired();
 401     return d_nv->d_id >= node.d_nv->d_id;
 402   }
 403
 404   /**
 405    * Returns the i-th child of this node.
 406    * @param i the index of the child
 407    * @return the node representing the i-th child
 408    */
 409   NodeTemplate operator[](int i) const {
 410     assertTNodeNotExpired();
 411     return NodeTemplate(d_nv->getChild(i));
 412   }
 413
 414   /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
 415    *
 416    * It has been decided for now to hold off on implementations of
 417    * these functions, as they may only be needed in CNF conversion,
 418    * where it's pointless to do a lazy isAtomic determination by
 419    * searching through the DAG, and storing it, since the result will
 420    * only be used once.  For more details see the 4/27/2010 CVC4
 421    * developer's meeting notes at:
 422    *
 423    * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
 424    */
 425   // bool containsDecision(); // is "atomic"
 426   // bool properlyContainsDecision(); // maybe not atomic but all children are
 427
 428   /**
 429    * Convert this Node into an Expr using the currently-in-scope
 430    * manager.  Essentially this is like an "operator Expr()" but we
 431    * don't want it to compete with implicit conversions between e.g.
 432    * Node and TNode, and we want internal-to-external interface
 433    * (Node -> Expr) points to be explicit.  We could write an
 434    * explicit Expr(Node) constructor---but that dirties the public
 435    * interface.
 436    */
 437   inline Expr toExpr();
 438
 439   /**
 440    * Convert an Expr into a Node.
 441    */
 442   static inline Node fromExpr(const Expr& e);
 443
 444   /**
 445    * Returns true if this node represents a constant
 446    * @return true if const
 447    */
 448   inline bool isConst() const {
 449     assertTNodeNotExpired();
 450     return getMetaKind() == kind::metakind::CONSTANT;
 451   }
 452
 453   /**
 454    * Returns the unique id of this node
 455    * @return the ud
 456    */
 457   unsigned getId() const {
 458     assertTNodeNotExpired();
 459     return d_nv->getId();
 460   }
 461
 462   /**
 463    * Returns a node representing the operator of this expression.
 464    * If this is an APPLY, then the operator will be a functional term.
 465    * Otherwise, it will be a node with kind BUILTIN.
 466    */
 467   NodeTemplate<true> getOperator() const;
 468
 469   /**
 470    * Returns true if the node has an operator (i.e., it's not a
 471    * variable or a constant).
 472    */
 473   inline bool hasOperator() const;
 474
 475   /**
 476    * Get the type for the node and optionally do type checking.
 477    *
 478    * Initial type computation will be near-constant time if
 479    * type checking is not requested. Results are memoized, so that
 480    * subsequent calls to getType() without type checking will be
 481    * constant time.
 482    *
 483    * Initial type checking is linear in the size of the expression.
 484    * Again, the results are memoized, so that subsequent calls to
 485    * getType(), with or without type checking, will be constant
 486    * time.
 487    *
 488    * NOTE: A TypeCheckingException can be thrown even when type
 489    * checking is not requested. getType() will always return a
 490    * valid and correct type and, thus, an exception will be thrown
 491    * when no valid or correct type can be computed (e.g., if the
 492    * arguments to a bit-vector operation aren't bit-vectors). When
 493    * type checking is not requested, getType() will do the minimum
 494    * amount of checking required to return a valid result.
 495    *
 496    * @param check whether we should check the type as we compute it
 497    * (default: false)
 498    */
 499   TypeNode getType(bool check = false) const
 500     throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException);
 501
 502   /**
 503    * Substitution of Nodes.
 504    */
 505   Node substitute(TNode node, TNode replacement) const;
 506
 507   /**
 508    * Simultaneous substitution of Nodes.  Elements in the Iterator1
 509    * range will be replaced by their corresponding element in the
 510    * Iterator2 range.  Both ranges should have the same size.
 511    */
 512   template <class Iterator1, class Iterator2>
 513   Node substitute(Iterator1 nodesBegin,
 514                   Iterator1 nodesEnd,
 515                   Iterator2 replacementsBegin,
 516                   Iterator2 replacementsEnd) const;
 517
 518   /**
 519    * Simultaneous substitution of Nodes.  Iterators should be over
 520    * pairs (x,y) for the rewrites [x->y].
 521    */
 522   template <class Iterator>
 523   Node substitute(Iterator substitutionsBegin,
 524                   Iterator substitutionsEnd) const;
 525
 526   /**
 527    * Returns the kind of this node.
 528    * @return the kind
 529    */
 530   inline Kind getKind() const {
 531     assertTNodeNotExpired();
 532     return Kind(d_nv->d_kind);
 533   }
 534
 535   /**
 536    * Returns the metakind of this node.
 537    * @return the metakind
 538    */
 539   inline kind::MetaKind getMetaKind() const {
 540     assertTNodeNotExpired();
 541     return kind::metaKindOf(getKind());
 542   }
 543
 544   /**
 545    * Returns the number of children this node has.
 546    * @return the number of children
 547    */
 548   inline size_t getNumChildren() const;
 549
 550   /**
 551    * If this is a CONST_* Node, extract the constant from it.
 552    */
 553   template <class T>
 554   inline const T& getConst() const;
 555
 556   /**
 557    * Returns the value of the given attribute that this has been attached.
 558    * @param attKind the kind of the attribute
 559    * @return the value of the attribute
 560    */
 561   template <class AttrKind>
 562   inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
 563
 564   // Note that there are two, distinct hasAttribute() declarations for
 565   // a reason (rather than using a pointer-valued argument with a
 566   // default value): they permit more optimized code in the underlying
 567   // hasAttribute() implementations.
 568
 569   /**
 570    * Returns true if this node has been associated an attribute of given kind.
 571    * Additionaly, if a pointer to the value_kind is give, and the attribute
 572    * value has been set for this node, it will be returned.
 573    * @param attKind the kind of the attribute
 574    * @return true if this node has the requested attribute
 575    */
 576   template <class AttrKind>
 577   inline bool hasAttribute(const AttrKind& attKind) const;
 578
 579   /**
 580    * Returns true if this node has been associated an attribute of given kind.
 581    * Additionaly, if a pointer to the value_kind is give, and the attribute
 582    * value has been set for this node, it will be returned.
 583    * @param attKind the kind of the attribute
 584    * @param value where to store the value if it exists
 585    * @return true if this node has the requested attribute
 586    */
 587   template <class AttrKind>
 588   inline bool getAttribute(const AttrKind& attKind,
 589                            typename AttrKind::value_type& value) const;
 590
 591   /**
 592    * Sets the given attribute of this node to the given value.
 593    * @param attKind the kind of the atribute
 594    * @param value the value to set the attribute to
 595    */
 596   template <class AttrKind>
 597   inline void setAttribute(const AttrKind& attKind,
 598                            const typename AttrKind::value_type& value);
 599
 600   /** Iterator allowing for scanning through the children. */
 601   typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > iterator;
 602   /** Constant iterator allowing for scanning through the children. */
 603   typedef typename expr::NodeValue::iterator< NodeTemplate<ref_count> > const_iterator;
 604
 605   class kinded_iterator {
 606     friend class NodeTemplate<ref_count>;
 607
 608     NodeTemplate<ref_count> d_node;
 609     ssize_t d_child;
 610
 611     kinded_iterator(TNode node, ssize_t child) :
 612       d_node(node),
 613       d_child(child) {
 614     }
 615
 616     // These are factories to serve as clients to Node::begin<K>() and
 617     // Node::end<K>().
 618     static kinded_iterator begin(TNode n, Kind k) {
 619       return kinded_iterator(n, n.getKind() == k ? 0 : -2);
 620     }
 621     static kinded_iterator end(TNode n, Kind k) {
 622       return kinded_iterator(n, n.getKind() == k ? n.getNumChildren() : -1);
 623     }
 624
 625   public:
 626     typedef NodeTemplate<ref_count> value_type;
 627     typedef std::ptrdiff_t difference_type;
 628     typedef NodeTemplate<ref_count>* pointer;
 629     typedef NodeTemplate<ref_count>& reference;
 630
 631     kinded_iterator() :
 632       d_node(NodeTemplate<ref_count>::null()),
 633       d_child(-2) {
 634     }
 635
 636     kinded_iterator(const kinded_iterator& i) :
 637       d_node(i.d_node),
 638       d_child(i.d_child) {
 639     }
 640
 641     NodeTemplate<ref_count> operator*() {
 642       return d_child < 0 ? d_node : d_node[d_child];
 643     }
 644
 645     bool operator==(const kinded_iterator& i) {
 646       return d_node == i.d_node && d_child == i.d_child;
 647     }
 648
 649     bool operator!=(const kinded_iterator& i) {
 650       return !(*this == i);
 651     }
 652
 653     kinded_iterator& operator++() {
 654       if(d_child != -1) {
 655         ++d_child;
 656       }
 657       return *this;
 658     }
 659
 660     kinded_iterator operator++(int) {
 661       kinded_iterator i = *this;
 662       ++*this;
 663       return i;
 664     }
 665   };/* class NodeTemplate<ref_count>::kinded_iterator */
 666
 667   typedef kinded_iterator const_kinded_iterator;
 668
 669   /**
 670    * Returns the iterator pointing to the first child.
 671    * @return the iterator
 672    */
 673   inline iterator begin() {
 674     assertTNodeNotExpired();
 675     return d_nv->begin< NodeTemplate<ref_count> >();
 676   }
 677
 678   /**
 679    * Returns the iterator pointing to the end of the children (one beyond the
 680    * last one).
 681    * @return the end of the children iterator.
 682    */
 683   inline iterator end() {
 684     assertTNodeNotExpired();
 685     return d_nv->end< NodeTemplate<ref_count> >();
 686   }
 687
 688   /**
 689    * Returns the iterator pointing to the first child, if the node's
 690    * kind is the same as the parameter, otherwise returns the iterator
 691    * pointing to the node itself.  This is useful if you want to
 692    * pretend to iterate over a "unary" PLUS, for instance, since unary
 693    * PLUSes don't exist---begin(PLUS) will give an iterator over the
 694    * children if the node's a PLUS node, otherwise give an iterator
 695    * over the node itself, as if it were a unary PLUS.
 696    * @param kind the kind to match
 697    * @return the kinded_iterator iterating over this Node (if its kind
 698    * is not the passed kind) or its children
 699    */
 700   inline kinded_iterator begin(Kind kind) {
 701     assertTNodeNotExpired();
 702     return kinded_iterator::begin(*this, kind);
 703   }
 704
 705   /**
 706    * Returns the iterator pointing to the end of the children (one
 707    * beyond the last one), if the node's kind is the same as the
 708    * parameter, otherwise returns the iterator pointing to the
 709    * one-of-the-node-itself.  This is useful if you want to pretend to
 710    * iterate over a "unary" PLUS, for instance, since unary PLUSes
 711    * don't exist---begin(PLUS) will give an iterator over the children
 712    * if the node's a PLUS node, otherwise give an iterator over the
 713    * node itself, as if it were a unary PLUS.
 714    * @param kind the kind to match
 715    * @return the kinded_iterator pointing off-the-end of this Node (if
 716    * its kind is not the passed kind) or off-the-end of its children
 717    */
 718   inline kinded_iterator end(Kind kind) {
 719     assertTNodeNotExpired();
 720     return kinded_iterator::end(*this, kind);
 721   }
 722
 723   /**
 724    * Returns the const_iterator pointing to the first child.
 725    * @return the const_iterator
 726    */
 727   inline const_iterator begin() const {
 728     assertTNodeNotExpired();
 729     return d_nv->begin< NodeTemplate<ref_count> >();
 730   }
 731
 732   /**
 733    * Returns the const_iterator pointing to the end of the children (one
 734    * beyond the last one.
 735    * @return the end of the children const_iterator.
 736    */
 737   inline const_iterator end() const {
 738     assertTNodeNotExpired();
 739     return d_nv->end< NodeTemplate<ref_count> >();
 740   }
 741
 742   /**
 743    * Returns the iterator pointing to the first child, if the node's
 744    * kind is the same as the parameter, otherwise returns the iterator
 745    * pointing to the node itself.  This is useful if you want to
 746    * pretend to iterate over a "unary" PLUS, for instance, since unary
 747    * PLUSes don't exist---begin(PLUS) will give an iterator over the
 748    * children if the node's a PLUS node, otherwise give an iterator
 749    * over the node itself, as if it were a unary PLUS.
 750    * @param kind the kind to match
 751    * @return the kinded_iterator iterating over this Node (if its kind
 752    * is not the passed kind) or its children
 753    */
 754   inline const_kinded_iterator begin(Kind kind) const {
 755     assertTNodeNotExpired();
 756     return const_kinded_iterator::begin(*this, kind);
 757   }
 758
 759   /**
 760    * Returns the iterator pointing to the end of the children (one
 761    * beyond the last one), if the node's kind is the same as the
 762    * parameter, otherwise returns the iterator pointing to the
 763    * one-of-the-node-itself.  This is useful if you want to pretend to
 764    * iterate over a "unary" PLUS, for instance, since unary PLUSes
 765    * don't exist---begin(PLUS) will give an iterator over the children
 766    * if the node's a PLUS node, otherwise give an iterator over the
 767    * node itself, as if it were a unary PLUS.
 768    * @param kind the kind to match
 769    * @return the kinded_iterator pointing off-the-end of this Node (if
 770    * its kind is not the passed kind) or off-the-end of its children
 771    */
 772   inline const_kinded_iterator end(Kind kind) const {
 773     assertTNodeNotExpired();
 774     return const_kinded_iterator::end(*this, kind);
 775   }
 776
 777   /**
 778    * Converts this node into a string representation.
 779    * @return the string representation of this node.
 780    */
 781   inline std::string toString() const {
 782     assertTNodeNotExpired();
 783     return d_nv->toString();
 784   }
 785
 786   /**
 787    * Converts this node into a string representation and sends it to the
 788    * given stream
 789    *
 790    * @param out the stream to serialize this node to
 791    * @param toDepth the depth to which to print this expression, or -1 to
 792    * print it fully
 793    * @param types set to true to ascribe types to the output expressions
 794    * (might break language compliance, but good for debugging expressions)
 795    * @param language the language in which to output
 796    */
 797   inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
 798                        OutputLanguage language = language::output::LANG_AST) const {
 799     assertTNodeNotExpired();
 800     d_nv->toStream(out, toDepth, types, language);
 801   }
 802
 803   /**
 804    * IOStream manipulator to set the maximum depth of Nodes when
 805    * pretty-printing.  -1 means print to any depth.  E.g.:
 806    *
 807    *   // let a, b, c, and d be VARIABLEs
 808    *   Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
 809    *   out << setdepth(3) << n;
 810    *
 811    * gives "(OR a b (AND c (NOT d)))", but
 812    *
 813    *   out << setdepth(1) << [same node as above]
 814    *
 815    * gives "(OR a b (...))"
 816    */
 817   typedef expr::ExprSetDepth setdepth;
 818
 819   /**
 820    * IOStream manipulator to print type ascriptions or not.
 821    *
 822    *   // let a, b, c, and d be variables of sort U
 823    *   Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
 824    *   out << n;
 825    *
 826    * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
 827    */
 828   typedef expr::ExprPrintTypes printtypes;
 829
 830   /**
 831    * IOStream manipulator to set the output language for Exprs.
 832    */
 833   typedef expr::ExprSetLanguage setlanguage;
 834
 835   /**
 836    * Very basic pretty printer for Node.
 837    * @param out output stream to print to.
 838    * @param indent number of spaces to indent the formula by.
 839    */
 840   inline void printAst(std::ostream& out, int indent = 0) const;
 841
 842   /**
 843    * Check if the node has a subterm t.
 844    */
 845   inline bool hasSubterm(NodeTemplate<false> t, bool strict = false) const;
 846
 847   template <bool ref_count2>
 848   NodeTemplate<true> eqNode(const NodeTemplate<ref_count2>& right) const;
 849
 850   NodeTemplate<true> notNode() const;
 851   NodeTemplate<true> negate() const;
 852   template <bool ref_count2>
 853   NodeTemplate<true> andNode(const NodeTemplate<ref_count2>& right) const;
 854   template <bool ref_count2>
 855   NodeTemplate<true> orNode(const NodeTemplate<ref_count2>& right) const;
 856   template <bool ref_count2, bool ref_count3>
 857   NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
 858                              const NodeTemplate<ref_count3>& elsepart) const;
 859   template <bool ref_count2>
 860   NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
 861   template <bool ref_count2>
 862   NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
 863   template <bool ref_count2>
 864   NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
 865
 866 };/* class NodeTemplate<ref_count> */
 867
 868 /**
 869  * Serializes a given node to the given stream.
 870  *
 871  * @param out the output stream to use
 872  * @param n the node to output to the stream
 873  * @return the stream
 874  */
 875 inline std::ostream& operator<<(std::ostream& out, TNode n) {
 876   n.toStream(out,
 877              Node::setdepth::getDepth(out),
 878              Node::printtypes::getPrintTypes(out),
 879              Node::setlanguage::getLanguage(out));
 880   return out;
 881 }
 882
 883 }/* CVC4 namespace */
 884
 885 #include <ext/hash_map>
 886
 887 #include "expr/attribute.h"
 888 #include "expr/node_manager.h"
 889
 890 namespace CVC4 {
 891
 892 // for hash_maps, hash_sets..
 893 struct NodeHashFunction {
 894   size_t operator()(CVC4::Node node) const {
 895     return (size_t) node.getId();
 896   }
 897 };/* struct NodeHashFunction */
 898
 899 // for hash_maps, hash_sets..
 900 struct TNodeHashFunction {
 901   size_t operator()(CVC4::TNode node) const {
 902     return (size_t) node.getId();
 903   }
 904 };/* struct TNodeHashFunction */
 905
 906 struct TNodePairHashFunction {
 907   size_t operator()(const std::pair<CVC4::TNode, CVC4::TNode>& pair ) const {
 908     TNode n1 = pair.first;
 909     TNode n2 = pair.second;
 910
 911     return (size_t) (n1.getId() * 0x9e3779b9 + n2.getId());
 912   }
 913 };/* struct TNodePairHashFunction */
 914
 915 template <bool ref_count>
 916 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
 917   assertTNodeNotExpired();
 918   return d_nv->getNumChildren();
 919 }
 920
 921 template <bool ref_count>
 922 template <class T>
 923 inline const T& NodeTemplate<ref_count>::getConst() const {
 924   assertTNodeNotExpired();
 925   return d_nv->getConst<T>();
 926 }
 927
 928 template <bool ref_count>
 929 template <class AttrKind>
 930 inline typename AttrKind::value_type NodeTemplate<ref_count>::
 931 getAttribute(const AttrKind&) const {
 932   Assert( NodeManager::currentNM() != NULL,
 933           "There is no current CVC4::NodeManager associated to this thread.\n"
 934           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 935
 936   assertTNodeNotExpired();
 937
 938   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
 939 }
 940
 941 template <bool ref_count>
 942 template <class AttrKind>
 943 inline bool NodeTemplate<ref_count>::
 944 hasAttribute(const AttrKind&) const {
 945   Assert( NodeManager::currentNM() != NULL,
 946           "There is no current CVC4::NodeManager associated to this thread.\n"
 947           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 948
 949   assertTNodeNotExpired();
 950
 951   return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
 952 }
 953
 954 template <bool ref_count>
 955 template <class AttrKind>
 956 inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
 957                                                   typename AttrKind::value_type& ret) const {
 958   Assert( NodeManager::currentNM() != NULL,
 959           "There is no current CVC4::NodeManager associated to this thread.\n"
 960           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 961
 962   assertTNodeNotExpired();
 963
 964   return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret);
 965 }
 966
 967 template <bool ref_count>
 968 template <class AttrKind>
 969 inline void NodeTemplate<ref_count>::
 970 setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
 971   Assert( NodeManager::currentNM() != NULL,
 972           "There is no current CVC4::NodeManager associated to this thread.\n"
 973           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 974
 975   assertTNodeNotExpired();
 976
 977   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 978 }
 979
 980 template <bool ref_count>
 981 NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
 982
 983 // FIXME: escape from type system convenient but is there a better
 984 // way?  Nodes conceptually don't change their expr values but of
 985 // course they do modify the refcount.  But it's nice to be able to
 986 // support node_iterators over const NodeValue*.  So.... hm.
 987 template <bool ref_count>
 988 NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
 989   d_nv(const_cast<expr::NodeValue*> (ev)) {
 990   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
 991   if(ref_count) {
 992     d_nv->inc();
 993   } else {
 994     Assert(d_nv->d_rc > 0, "TNode constructed from NodeValue with rc == 0");
 995   }
 996 }
 997
 998 // the code for these two following constructors ("conversion/copy
 999 // constructors") is identical, but we need both.  see comment in the
1000 // class.
1001
1002 template <bool ref_count>
1003 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
1004   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
1005   d_nv = e.d_nv;
1006   if(ref_count) {
1007     Assert(d_nv->d_rc > 0, "Node constructed from TNode with rc == 0");
1008     d_nv->inc();
1009   } else {
1010     // shouldn't ever fail
1011     Assert(d_nv->d_rc > 0, "TNode constructed from Node with rc == 0");
1012   }
1013 }
1014
1015 template <bool ref_count>
1016 NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
1017   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
1018   d_nv = e.d_nv;
1019   if(ref_count) {
1020     // shouldn't ever fail
1021     Assert(d_nv->d_rc > 0, "Node constructed from Node with rc == 0");
1022     d_nv->inc();
1023   } else {
1024     Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0");
1025   }
1026 }
1027
1028 template <bool ref_count>
1029 NodeTemplate<ref_count>::NodeTemplate(const Expr& e) {
1030   Assert(e.d_node != NULL, "Expecting a non-NULL expression value!");
1031   Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!");
1032   d_nv = e.d_node->d_nv;
1033   // shouldn't ever fail
1034   Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0");
1035   if(ref_count) {
1036     d_nv->inc();
1037   }
1038 }
1039
1040 template <bool ref_count>
1041 NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
1042   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
1043   if(ref_count) {
1044     // shouldn't ever fail
1045     Assert(d_nv->d_rc > 0, "Node reference count would be negative");
1046     d_nv->dec();
1047   }
1048 }
1049
1050 template <bool ref_count>
1051 void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
1052   d_nv = ev;
1053   if(ref_count) {
1054     d_nv->inc();
1055   } else {
1056     Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0");
1057   }
1058 }
1059
1060 template <bool ref_count>
1061 NodeTemplate<ref_count>& NodeTemplate<ref_count>::
1062 operator=(const NodeTemplate& e) {
1063   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
1064   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
1065   if(EXPECT_TRUE( d_nv != e.d_nv )) {
1066     if(ref_count) {
1067       // shouldn't ever fail
1068       Assert(d_nv->d_rc > 0,
1069              "Node reference count would be negative");
1070       d_nv->dec();
1071     }
1072     d_nv = e.d_nv;
1073     if(ref_count) {
1074       // shouldn't ever fail
1075       Assert(d_nv->d_rc > 0, "Node assigned from Node with rc == 0");
1076       d_nv->inc();
1077     } else {
1078       Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0");
1079     }
1080   }
1081   return *this;
1082 }
1083
1084 template <bool ref_count>
1085 NodeTemplate<ref_count>& NodeTemplate<ref_count>::
1086 operator=(const NodeTemplate<!ref_count>& e) {
1087   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
1088   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
1089   if(EXPECT_TRUE( d_nv != e.d_nv )) {
1090     if(ref_count) {
1091       // shouldn't ever fail
1092       Assert(d_nv->d_rc > 0, "Node reference count would be negative");
1093       d_nv->dec();
1094     }
1095     d_nv = e.d_nv;
1096     if(ref_count) {
1097       Assert(d_nv->d_rc > 0, "Node assigned from TNode with rc == 0");
1098       d_nv->inc();
1099     } else {
1100       // shouldn't ever happen
1101       Assert(d_nv->d_rc > 0, "TNode assigned from Node with rc == 0");
1102     }
1103   }
1104   return *this;
1105 }
1106
1107 template <bool ref_count>
1108 template <bool ref_count2>
1109 NodeTemplate<true>
1110 NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count2>& right) const {
1111   assertTNodeNotExpired();
1112   return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
1113 }
1114
1115 template <bool ref_count>
1116 NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
1117   assertTNodeNotExpired();
1118   return NodeManager::currentNM()->mkNode(kind::NOT, *this);
1119 }
1120
1121 template <bool ref_count>
1122 NodeTemplate<true> NodeTemplate<ref_count>::negate() const {
1123   assertTNodeNotExpired();
1124   return (getKind() == kind::NOT) ? NodeTemplate<true>(d_nv->getChild(0)) : NodeManager::currentNM()->mkNode(kind::NOT, *this);
1125 }
1126
1127 template <bool ref_count>
1128 template <bool ref_count2>
1129 NodeTemplate<true>
1130 NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count2>& right) const {
1131   assertTNodeNotExpired();
1132   return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
1133 }
1134
1135 template <bool ref_count>
1136 template <bool ref_count2>
1137 NodeTemplate<true>
1138 NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count2>& right) const {
1139   assertTNodeNotExpired();
1140   return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
1141 }
1142
1143 template <bool ref_count>
1144 template <bool ref_count2, bool ref_count3>
1145 NodeTemplate<true>
1146 NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
1147                                  const NodeTemplate<ref_count3>& elsepart) const {
1148   assertTNodeNotExpired();
1149   return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
1150 }
1151
1152 template <bool ref_count>
1153 template <bool ref_count2>
1154 NodeTemplate<true>
1155 NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
1156   assertTNodeNotExpired();
1157   return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
1158 }
1159
1160 template <bool ref_count>
1161 template <bool ref_count2>
1162 NodeTemplate<true>
1163 NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
1164   assertTNodeNotExpired();
1165   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
1166 }
1167
1168 template <bool ref_count>
1169 template <bool ref_count2>
1170 NodeTemplate<true>
1171 NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count2>& right) const {
1172   assertTNodeNotExpired();
1173   return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
1174 }
1175
1176 template <bool ref_count>
1177 inline void
1178 NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
1179   assertTNodeNotExpired();
1180   d_nv->printAst(out, indent);
1181 }
1182
1183 /**
1184  * Returns a node representing the operator of this expression.
1185  * If this is an APPLY, then the operator will be a functional term.
1186  * Otherwise, it will be a node with kind BUILTIN.
1187  */
1188 template <bool ref_count>
1189 NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
1190   Assert( NodeManager::currentNM() != NULL,
1191           "There is no current CVC4::NodeManager associated to this thread.\n"
1192           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
1193
1194   assertTNodeNotExpired();
1195
1196   switch(kind::MetaKind mk = getMetaKind()) {
1197   case kind::metakind::INVALID:
1198     IllegalArgument(*this, "getOperator() called on Node with INVALID-kinded kind");
1199
1200   case kind::metakind::VARIABLE:
1201     IllegalArgument(*this, "getOperator() called on Node with VARIABLE-kinded kind");
1202
1203   case kind::metakind::OPERATOR: {
1204     /* Returns a BUILTIN node. */
1205     return NodeManager::currentNM()->operatorOf(getKind());
1206   }
1207
1208   case kind::metakind::PARAMETERIZED:
1209     /* The operator is the first child. */
1210     return Node(d_nv->d_children[0]);
1211
1212   case kind::metakind::CONSTANT:
1213     IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
1214
1215   default:
1216     Unhandled(mk);
1217   }
1218 }
1219
1220 /**
1221  * Returns true if the node has an operator (i.e., it's not a variable
1222  * or a constant).
1223  */
1224 template <bool ref_count>
1225 inline bool NodeTemplate<ref_count>::hasOperator() const {
1226   assertTNodeNotExpired();
1227   return NodeManager::hasOperator(getKind());
1228 }
1229
1230 template <bool ref_count>
1231 TypeNode NodeTemplate<ref_count>::getType(bool check) const
1232   throw (CVC4::TypeCheckingExceptionPrivate, CVC4::AssertionException) {
1233   Assert( NodeManager::currentNM() != NULL,
1234           "There is no current CVC4::NodeManager associated to this thread.\n"
1235           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
1236
1237   assertTNodeNotExpired();
1238
1239   return NodeManager::currentNM()->getType(*this, check);
1240 }
1241
1242 template <bool ref_count>
1243 inline Node
1244 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement) const {
1245   if (node == *this) {
1246     return replacement;
1247   }
1248   std::hash_map<TNode, TNode, TNodeHashFunction> cache;
1249   return substitute(node, replacement, cache);
1250 }
1251
1252 template <bool ref_count>
1253 Node
1254 NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
1255                                     std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
1256   Assert(node != *this);
1257
1258   if (getNumChildren() == 0) {
1259     return *this;
1260   }
1261
1262   // in cache?
1263   typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
1264   if(i != cache.end()) {
1265     return (*i).second;
1266   }
1267
1268   // otherwise compute
1269   NodeBuilder<> nb(getKind());
1270   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1271     // push the operator
1272     nb << getOperator();
1273   }
1274   for(const_iterator i = begin(),
1275         iend = end();
1276       i != iend;
1277       ++i) {
1278     if(*i == node) {
1279       nb << replacement;
1280     } else {
1281       nb << (*i).substitute(node, replacement, cache);
1282     }
1283   }
1284
1285   // put in cache
1286   Node n = nb;
1287   Assert(node != n);
1288   cache[*this] = n;
1289   return n;
1290 }
1291
1292 template <bool ref_count>
1293 template <class Iterator1, class Iterator2>
1294 inline Node
1295 NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
1296                                     Iterator1 nodesEnd,
1297                                     Iterator2 replacementsBegin,
1298                                     Iterator2 replacementsEnd) const {
1299   std::hash_map<TNode, TNode, TNodeHashFunction> cache;
1300   return substitute(nodesBegin, nodesEnd,
1301                     replacementsBegin, replacementsEnd, cache);
1302 }
1303
1304 template <bool ref_count>
1305 template <class Iterator1, class Iterator2>
1306 Node
1307 NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin,
1308                                     Iterator1 nodesEnd,
1309                                     Iterator2 replacementsBegin,
1310                                     Iterator2 replacementsEnd,
1311                                     std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
1312   // in cache?
1313   typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
1314   if(i != cache.end()) {
1315     return (*i).second;
1316   }
1317
1318   // otherwise compute
1319   Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd),
1320           "Substitution iterator ranges must be equal size" );
1321   Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this));
1322   if(j != nodesEnd) {
1323     Iterator2 b = replacementsBegin;
1324     std::advance(b, std::distance(nodesBegin, j));
1325     Node n = *b;
1326     cache[*this] = n;
1327     return n;
1328   } else if(getNumChildren() == 0) {
1329     cache[*this] = *this;
1330     return *this;
1331   } else {
1332     NodeBuilder<> nb(getKind());
1333     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1334       // push the operator
1335       nb << getOperator();
1336     }
1337     for(const_iterator i = begin(),
1338           iend = end();
1339         i != iend;
1340         ++i) {
1341       nb << (*i).substitute(nodesBegin, nodesEnd,
1342                             replacementsBegin, replacementsEnd,
1343                             cache);
1344     }
1345     Node n = nb;
1346     cache[*this] = n;
1347     return n;
1348   }
1349 }
1350
1351 template <bool ref_count>
1352 template <class Iterator>
1353 inline Node
1354 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
1355                                     Iterator substitutionsEnd) const {
1356   std::hash_map<TNode, TNode, TNodeHashFunction> cache;
1357   return substitute(substitutionsBegin, substitutionsEnd, cache);
1358 }
1359
1360 template <bool ref_count>
1361 template <class Iterator>
1362 Node
1363 NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
1364                                     Iterator substitutionsEnd,
1365                                     std::hash_map<TNode, TNode, TNodeHashFunction>& cache) const {
1366   // in cache?
1367   typename std::hash_map<TNode, TNode, TNodeHashFunction>::const_iterator i = cache.find(*this);
1368   if(i != cache.end()) {
1369     return (*i).second;
1370   }
1371
1372   // otherwise compute
1373   Iterator j = find_if(substitutionsBegin, substitutionsEnd,
1374                        bind2nd(first_equal_to<typename Iterator::value_type::first_type, typename Iterator::value_type::second_type>(), *this));
1375   if(j != substitutionsEnd) {
1376     Node n = (*j).second;
1377     cache[*this] = n;
1378     return n;
1379   } else if(getNumChildren() == 0) {
1380     cache[*this] = *this;
1381     return *this;
1382   } else {
1383     NodeBuilder<> nb(getKind());
1384     if(getMetaKind() == kind::metakind::PARAMETERIZED) {
1385       // push the operator
1386       nb << getOperator();
1387     }
1388     for(const_iterator i = begin(),
1389           iend = end();
1390         i != iend;
1391         ++i) {
1392       nb << (*i).substitute(substitutionsBegin, substitutionsEnd, cache);
1393     }
1394     Node n = nb;
1395     cache[*this] = n;
1396     return n;
1397   }
1398 }
1399
1400 template <bool ref_count>
1401 inline Expr NodeTemplate<ref_count>::toExpr() {
1402   assertTNodeNotExpired();
1403   return NodeManager::currentNM()->toExpr(*this);
1404 }
1405
1406 // intentionally not defined for TNode
1407 template <>
1408 inline Node NodeTemplate<true>::fromExpr(const Expr& e) {
1409   return NodeManager::fromExpr(e);
1410 }
1411
1412 template<bool ref_count>
1413 bool NodeTemplate<ref_count>::hasSubterm(NodeTemplate<false> t, bool strict) const {
1414   typedef std::hash_set<TNode, TNodeHashFunction> node_set;
1415
1416   if (!strict && *this == t) {
1417     return true;
1418   }
1419
1420   node_set visited;
1421   std::vector<TNode> toProcess;
1422
1423   toProcess.push_back(*this);
1424
1425   for (unsigned i = 0; i < toProcess.size(); ++ i) {
1426     TNode current = toProcess[i];
1427     for(unsigned j = 0, j_end = current.getNumChildren(); j < j_end; ++ j) {
1428       TNode child = current[j];
1429       if (child == t) {
1430         return true;
1431       }
1432       if (visited.find(child) != visited.end()) {
1433         continue;
1434       } else {
1435         visited.insert(child);
1436         toProcess.push_back(child);
1437       }
1438     }
1439   }
1440
1441   return false;
1442 }
1443
1444 #ifdef CVC4_DEBUG
1445 /**
1446  * Pretty printer for use within gdb.  This is not intended to be used
1447  * outside of gdb.  This writes to the Warning() stream and immediately
1448  * flushes the stream.
1449  *
1450  * Note that this function cannot be a template, since the compiler
1451  * won't instantiate it.  Even if we explicitly instantiate.  (Odd?)
1452  * So we implement twice.  We mark as __attribute__((used)) so that
1453  * GCC emits code for it even though static analysis indicates it's
1454  * never called.
1455  *
1456  * Tim's Note: I moved this into the node.h file because this allows gdb
1457  * to find the symbol, and use it, which is the first standard this code needs
1458  * to meet. A cleaner solution is welcomed.
1459  */
1460 static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) {
1461   Warning() << Node::setdepth(-1)
1462             << Node::setlanguage(language::output::LANG_AST)
1463             << n << std::endl;
1464   Warning().flush();
1465 }
1466 static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) {
1467   n.printAst(Warning(), 0);
1468   Warning().flush();
1469 }
1470
1471 static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) {
1472   Warning() << Node::setdepth(-1)
1473             << Node::setlanguage(language::output::LANG_AST)
1474             << n << std::endl;
1475   Warning().flush();
1476 }
1477 static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) {
1478   n.printAst(Warning(), 0);
1479   Warning().flush();
1480 }
1481 #endif /* CVC4_DEBUG */
1482
1483 }/* CVC4 namespace */
1484
1485 #endif /* __CVC4__NODE_H */