src/expr/node.h

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