From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 22 Feb 2010 23:01:16 +0000 (+0000)
Subject: Merging from branch branches/Liana r241
X-Git-Tag: cvc5-1.0.0~9230
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ca8427a5c79e2e0425a55bc83fe8572055e1660;p=cvc5.git

Merging from branch branches/Liana r241
---

diff --git a/src/expr/expr.h b/src/expr/expr.h
index 27b7846db..6c615d391 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -28,7 +28,8 @@
 namespace CVC4 {
 
 // The internal expression representation
-class Node;
+template <bool count_ref>
+class NodeTemplate;
 
 /**
  * Class encapsulating CVC4 expressions and methods for constructing new
@@ -161,10 +162,10 @@ protected:
    * @param em the expression manager that handles this expression
    * @param node the actual expression node pointer
    */
-  Expr(ExprManager* em, Node* node);
+  Expr(ExprManager* em, NodeTemplate<true>* node);
 
   /** The internal expression representation */
-  Node* d_node;
+  NodeTemplate<true>* d_node;
 
   /** The responsible expression manager */
   ExprManager* d_exprManager;
@@ -173,7 +174,7 @@ protected:
    * Returns the actual internal node.
    * @return the internal node
    */
-  Node getNode() const;
+  NodeTemplate<true> getNode() const;
 
   // Friend to access the actual internal node information and private methods
   friend class SmtEngine;
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 080623e21..b9d3d13bb 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,3 +1,4 @@
+<<<<<<< .working
 /*********************                                                        */
 /** node.cpp
  ** Original author: mdeters
@@ -198,3 +199,5 @@ void Node::debugPrint() {
 }
 
 }/* CVC4 namespace */
+=======
+>>>>>>> .merge-right.r241
diff --git a/src/expr/node.h b/src/expr/node.h
index 77f9141f1..280c85fb3 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -30,7 +30,10 @@
 
 namespace CVC4 {
 
-class Node;
+template<bool ref_count>
+  class NodeTemplate;
+typedef NodeTemplate<true> Node;
+typedef NodeTemplate<false> TNode;
 
 inline std::ostream& operator<<(std::ostream&, const Node&);
 
@@ -38,7 +41,7 @@ class NodeManager;
 class Type;
 
 namespace expr {
-  class NodeValue;
+class NodeValue;
 }/* CVC4::expr namespace */
 
 using CVC4::expr::NodeValue;
@@ -47,127 +50,168 @@ using CVC4::expr::NodeValue;
  * Encapsulation of an NodeValue pointer.  The reference count is
  * maintained in the NodeValue.
  */
-class Node {
+template<bool ref_count>
+  class NodeTemplate {
 
   friend class NodeValue;
 
-  /** A convenient null-valued encapsulated pointer */
-  static Node s_null;
-
-  /** The referenced NodeValue */
-  NodeValue* d_ev;
-
-  /** This constructor is reserved for use by the Node package; one
-   *  must construct an Node using one of the build mechanisms of the
-   *  Node package.
-   *
-   *  Increments the reference count.
-   *
-   *  FIXME: there's a type-system escape here to cast away the const,
-   *  since the refcount needs to be updated.  But conceptually Nodes
-   *  don't change their arguments, and it's nice to have
-   *  const_iterators over them.  See notes in .cpp file for
-   *  details. */
-  // this really does needs to be explicit to avoid hard to track
-  // errors with Nodes implicitly wrapping NodeValues
-  explicit Node(const NodeValue*);
-
-  template <unsigned> friend class NodeBuilder;
-  friend class NodeManager;
+    /** A convenient null-valued encapsulated pointer */
+    static NodeTemplate s_null;
 
-  /**
-   * Assigns the expression value and does reference counting. No assumptions
-   * are made on the expression, and should only be used if we know what we are
-   * doing.
-   *
-   * @param ev the expression value to assign
-   */
-  void assignNodeValue(NodeValue* ev);
+    /** The referenced NodeValue */
+    NodeValue* d_ev;
+
+    bool d_count_ref;
+
+    /** This constructor is reserved for use by the NodeTemplate package; one
+     *  must construct an NodeTemplate using one of the build mechanisms of the
+     *  NodeTemplate package.
+     *
+     *  Increments the reference count.
+     *
+     *  FIXME: there's a type-system escape here to cast away the const,
+     *  since the refcount needs to be updated.  But conceptually Nodes
+     *  don't change their arguments, and it's nice to have
+     *  const_iterators over them.  See notes in .cpp file for
+     *  details. */
+    // this really does needs to be explicit to avoid hard to track
+    // errors with Nodes implicitly wrapping NodeValues
+    explicit NodeTemplate(const NodeValue*);
 
-  typedef NodeValue::ev_iterator ev_iterator;
-  typedef NodeValue::const_ev_iterator const_ev_iterator;
+    template<unsigned>
+      friend class NodeBuilder;
 
-  inline ev_iterator ev_begin();
-  inline ev_iterator ev_end();
-  inline const_ev_iterator ev_begin() const;
-  inline const_ev_iterator ev_end() const;
+    friend class NodeTemplate<true>;
+    friend class NodeTemplate<false>;
 
-public:
+    friend class NodeManager;
 
-  /** Default constructor, makes a null expression. */
-  Node();
+    /**
+     * Assigns the expression value and does reference counting. No assumptions
+     * are made on the expression, and should only be used if we know what we are
+     * doing.
+     *
+     * @param ev the expression value to assign
+     */
+    void assignNodeValue(NodeValue* ev);
 
-  Node(const Node&);
+    typedef NodeValue::ev_iterator ev_iterator;
+    typedef NodeValue::const_ev_iterator const_ev_iterator;
 
-  /** Destructor.  Decrements the reference count and, if zero,
-   *  collects the NodeValue. */
-  ~Node();
+    inline ev_iterator ev_begin();
+    inline ev_iterator ev_end();
+    inline const_ev_iterator ev_begin() const;
+    inline const_ev_iterator ev_end() const;
 
-  bool operator==(const Node& e) const { return d_ev == e.d_ev; }
-  bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
+  public:
 
+    /** Default constructor, makes a null expression. */
+    NodeTemplate();
+
+<<<<<<< .working
   Node operator[](int i) const {
     Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
     return Node(d_ev->d_children[i]);
   }
+=======
+    template <bool ref_count_1>
+    NodeTemplate(const NodeTemplate<ref_count_1>&);
+>>>>>>> .merge-right.r241
 
-  /**
-   * We compare by expression ids so, keeping things deterministic and having
-   * that subexpressions have to be smaller than the enclosing expressions.
-   */
-  inline bool operator<(const Node& e) const;
+    /** Destructor.  Decrements the reference count and, if zero,
+     *  collects the NodeValue. */
+    ~NodeTemplate();
 
-  Node& operator=(const Node&);
+    bool operator==(const NodeTemplate& e) const {
+      return d_ev == e.d_ev;
+    }
+    bool operator!=(const NodeTemplate& e) const {
+      return d_ev != e.d_ev;
+    }
 
-  size_t hash() const { return d_ev->getId(); }
-  uint64_t getId() const { return d_ev->getId(); }
+    NodeTemplate operator[](int i) const {
+      Assert(i >= 0 && i < d_ev->d_nchildren);
+      return NodeTemplate(d_ev->d_children[i]);
+    }
 
-  Node eqExpr(const Node& right) const;
-  Node notExpr() const;
-  Node andExpr(const Node& right) const;
-  Node orExpr(const Node& right) const;
-  Node iteExpr(const Node& thenpart, const Node& elsepart) const;
-  Node iffExpr(const Node& right) const;
-  Node impExpr(const Node& right) const;
-  Node xorExpr(const Node& right) const;
+    /**
+     * We compare by expression ids so, keeping things deterministic and having
+     * that subexpressions have to be smaller than the enclosing expressions.
+     */
+    inline bool operator<(const NodeTemplate& e) const;
 
+<<<<<<< .working
   /*
   Node plusExpr(const Node& right) const;
   Node uMinusExpr() const;
   Node multExpr(const Node& right) const;
+=======
+    NodeTemplate& operator=(const NodeTemplate&);
+>>>>>>> .merge-right.r241
   */
 
-  inline Kind getKind() const;
+    size_t hash() const {
+      return d_ev->getId();
+    }
 
-  inline size_t getNumChildren() const;
+    uint64_t getId() const {
+      return d_ev->getId();
+    }
   const Type* getType() const;
 
-  static Node null();
+    const Type* getType() const;
 
-  typedef NodeValue::node_iterator iterator;
-  typedef NodeValue::node_iterator const_iterator;
+    NodeTemplate eqExpr(const NodeTemplate& right) const;
+    NodeTemplate notExpr() const;
+    NodeTemplate andExpr(const NodeTemplate& right) const;
+    NodeTemplate orExpr(const NodeTemplate& right) const;
+    NodeTemplate iteExpr(const NodeTemplate& thenpart,
+                         const NodeTemplate& elsepart) const;
+    NodeTemplate iffExpr(const NodeTemplate& right) const;
+    NodeTemplate impExpr(const NodeTemplate& right) const;
+    NodeTemplate xorExpr(const NodeTemplate& right) const;
 
-  inline iterator begin();
-  inline iterator end();
-  inline const_iterator begin() const;
-  inline const_iterator end() const;
+    NodeTemplate plusExpr(const NodeTemplate& right) const;
+    NodeTemplate uMinusExpr() const;
+    NodeTemplate multExpr(const NodeTemplate& right) const;
 
-  inline std::string toString() const;
-  inline void toStream(std::ostream&) const;
+    inline Kind getKind() const;
 
-  bool isNull() const;
-  bool isAtomic() const;
+    inline size_t getNumChildren() const;
 
+<<<<<<< .working
   template <class AttrKind>
   inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
+=======
+    static NodeTemplate null();
+>>>>>>> .merge-right.r241
 
+<<<<<<< .working
   template <class AttrKind>
   inline bool hasAttribute(const AttrKind&,
                            typename AttrKind::value_type* = NULL) const;
+=======
+    typedef typename NodeValue::iterator<ref_count> iterator;
+    typedef typename NodeValue::iterator<ref_count> const_iterator;
+>>>>>>> .merge-right.r241
 
-  template <class AttrKind>
-  inline void setAttribute(const AttrKind&,
-                           const typename AttrKind::value_type& value);
+    inline iterator begin();
+    inline iterator end();
+    inline const_iterator begin() const;
+    inline const_iterator end() const;
+
+    template <class AttrKind>
+    inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
+
+    template <class AttrKind>
+    inline bool hasAttribute(const AttrKind&, typename AttrKind::value_type* = NULL) const;
+
+    inline std::string toString() const;
+    inline void toStream(std::ostream&) const;
+
+
+    bool isNull() const;
+    bool isAtomic() const;
 
   /**
    * Very basic pretty printer for Node.
@@ -186,7 +230,16 @@ private:
    */
   void debugPrint();
 
-};/* class Node */
+  template<class AttrKind>
+  inline void setAttribute(
+      const AttrKind&, const typename AttrKind::value_type& value);
+
+    static void indent(std::ostream & o, int indent) {
+      for(int i = 0; i < indent; i++)
+        o << ' ';
+    }
+
+  };/* class NodeTemplate */
 
 }/* CVC4 namespace */
 
@@ -194,10 +247,10 @@ private:
 
 // for hashtables
 namespace __gnu_cxx {
-  template <>
+template<>
   struct hash<CVC4::Node> {
     size_t operator()(const CVC4::Node& node) const {
-      return (size_t)node.hash();
+      return (size_t) node.hash();
     }
   };
 }/* __gnu_cxx namespace */
@@ -207,84 +260,121 @@ namespace __gnu_cxx {
 
 namespace CVC4 {
 
-inline bool Node::operator<(const Node& e) const {
-  return d_ev->d_id < e.d_ev->d_id;
-}
+template<bool ref_count>
+  inline bool NodeTemplate<ref_count>::operator<(const NodeTemplate& e) const {
+    return d_ev->d_id < e.d_ev->d_id;
+  }
 
 inline std::ostream& operator<<(std::ostream& out, const Node& e) {
   e.toStream(out);
   return out;
 }
 
-inline Kind Node::getKind() const {
-  return Kind(d_ev->d_kind);
-}
+template<bool ref_count>
+  inline Kind NodeTemplate<ref_count>::getKind() const {
+    return Kind(d_ev->d_kind);
+  }
 
-inline std::string Node::toString() const {
-  return d_ev->toString();
-}
+template<bool ref_count>
+  inline std::string NodeTemplate<ref_count>::toString() const {
+    return d_ev->toString();
+  }
 
-inline void Node::toStream(std::ostream& out) const {
-  d_ev->toStream(out);
-}
+template<bool ref_count>
+  inline void NodeTemplate<ref_count>::toStream(std::ostream& out) const {
+    d_ev->toStream(out);
+  }
 
-inline Node::ev_iterator Node::ev_begin() {
-  return d_ev->ev_begin();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_begin() {
+    return d_ev->ev_begin();
+  }
 
-inline Node::ev_iterator Node::ev_end() {
-  return d_ev->ev_end();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_end() {
+    return d_ev->ev_end();
+  }
 
-inline Node::const_ev_iterator Node::ev_begin() const {
-  return d_ev->ev_begin();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate<
+      ref_count>::ev_begin() const {
+    return d_ev->ev_begin();
+  }
 
-inline Node::const_ev_iterator Node::ev_end() const {
-  return d_ev->ev_end();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate<
+      ref_count>::ev_end() const {
+    return d_ev->ev_end();
+  }
 
-inline Node::iterator Node::begin() {
-  return d_ev->begin();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::begin() {
+    return d_ev->begin<ref_count> ();
+  }
 
-inline Node::iterator Node::end() {
-  return d_ev->end();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::end() {
+    return d_ev->end<ref_count> ();
+  }
 
-inline Node::const_iterator Node::begin() const {
-  return d_ev->begin();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate<
+      ref_count>::begin() const {
+    return d_ev->begin<ref_count> ();
+  }
 
-inline Node::const_iterator Node::end() const {
-  return d_ev->end();
-}
+template<bool ref_count>
+  inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate<
+      ref_count>::end() const {
+    return d_ev->end<ref_count> ();
+  }
 
-inline size_t Node::getNumChildren() const {
-  return d_ev->d_nchildren;
-}
+template<bool ref_count>
+  inline size_t NodeTemplate<ref_count>::getNumChildren() const {
+    return d_ev->d_nchildren;
+  }
 
+template <bool ref_count>
 template <class AttrKind>
+<<<<<<< .working
 inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) const {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
+=======
+inline typename AttrKind::value_type NodeTemplate<ref_count>::getAttribute(const AttrKind&) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+>>>>>>> .merge-right.r241
   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
 }
 
+template <bool ref_count>
 template <class AttrKind>
+<<<<<<< .working
 inline bool Node::hasAttribute(const AttrKind&,
                                typename AttrKind::value_type* ret) const {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
+=======
+inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&,
+                               typename AttrKind::value_type* ret) const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+>>>>>>> .merge-right.r241
   return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
 }
 
+template <bool ref_count>
 template <class AttrKind>
-inline void Node::setAttribute(const AttrKind&,
+inline void NodeTemplate<ref_count>::setAttribute(const AttrKind&,
                                const typename AttrKind::value_type& value) {
   Assert( NodeManager::currentNM() != NULL,
           "There is no current CVC4::NodeManager associated to this thread.\n"
@@ -293,6 +383,177 @@ inline void Node::setAttribute(const AttrKind&,
   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 }
 
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&NodeValue::s_null);
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::null() {
+    return s_null;
+  }
+
+template<bool ref_count>
+  bool NodeTemplate<ref_count>::isNull() const {
+    return d_ev == &NodeValue::s_null;
+  }
+
+////FIXME: This function is a major hack! Should be changed ASAP
+////TODO: Should use positive definition, i.e. what kinds are atomic.
+template<bool ref_count>
+  bool NodeTemplate<ref_count>::isAtomic() const {
+    switch(getKind()) {
+    case NOT:
+    case XOR:
+    case ITE:
+    case IFF:
+    case IMPLIES:
+    case OR:
+    case AND:
+      return false;
+    default:
+      return true;
+    }
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count>::NodeTemplate() :
+    d_ev(&NodeValue::s_null) {
+    // No refcount needed
+  }
+
+// FIXME: escape from type system convenient but is there a better
+// way?  Nodes conceptually don't change their expr values but of
+// course they do modify the refcount.  But it's nice to be able to
+// support node_iterators over const NodeValue*.  So.... hm.
+template<bool ref_count>
+  NodeTemplate<ref_count>::NodeTemplate(const NodeValue* ev) :
+    d_ev(const_cast<NodeValue*> (ev)) {
+    Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+    if(ref_count)
+      d_ev->inc();
+  }
+
+template<bool ref_count>
+template<bool ref_count_1>
+  NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) {
+    Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
+    d_ev = e.d_ev;
+    if(ref_count)
+      d_ev->inc();
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count>::~NodeTemplate() {
+    Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+    if(ref_count)
+      d_ev->dec();
+    Assert(ref_count || d_ev->d_rc > 0,
+        "Temporary node pointing to an expired node");
+  }
+
+template<bool ref_count>
+  void NodeTemplate<ref_count>::assignNodeValue(NodeValue* ev) {
+    d_ev = ev;
+    if(ref_count)
+      d_ev->inc();
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator=
+      (const NodeTemplate<ref_count>& e) {
+    Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+    Assert(e.d_ev != NULL, "Expecting a non-NULL expression value on RHS!");
+    if(EXPECT_TRUE( d_ev != e.d_ev )) {
+      if(ref_count)
+        d_ev->dec();
+      d_ev = e.d_ev;
+      if(ref_count)
+        d_ev->inc();
+    }
+    return *this;
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::eqExpr(const NodeTemplate<
+      ref_count>& right) const {
+    return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::notExpr() const {
+    return NodeManager::currentNM()->mkNode(NOT, *this);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::andExpr(
+      const NodeTemplate<ref_count>& right) const {
+    return NodeManager::currentNM()->mkNode(AND, *this, right);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::orExpr(
+      const NodeTemplate<ref_count>& right) const {
+    return NodeManager::currentNM()->mkNode(OR, *this, right);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::iteExpr(
+      const NodeTemplate<ref_count>& thenpart,
+      const NodeTemplate<ref_count>& elsepart) const {
+    return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::iffExpr(
+      const NodeTemplate<ref_count>& right) const {
+    return NodeManager::currentNM()->mkNode(IFF, *this, right);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::impExpr(
+      const NodeTemplate<ref_count>& right) const {
+    return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
+  }
+
+template<bool ref_count>
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::xorExpr(
+      const NodeTemplate<ref_count>& right) const {
+    return NodeManager::currentNM()->mkNode(XOR, *this, right);
+  }
+
+
+template<bool ref_count>
+  void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
+    indent(out, ind);
+    out << '(';
+    out << getKind();
+    if(getKind() == VARIABLE) {
+      out << ' ' << getId();
+
+    } else if(getNumChildren() >= 1) {
+      for(const_iterator child = begin(); child != end(); ++child) {
+        out << std::endl;
+        NodeTemplate((*child)).printAst(out, ind + 1);
+      }
+      out << std::endl;
+      indent(out, ind);
+    }
+    out << ')';
+  }
+
+template<bool ref_count>
+  void NodeTemplate<ref_count>::debugPrint() {
+    printAst(Warning(), 0);
+    Warning().flush();
+  }
+
+template<bool ref_count>
+const Type* NodeTemplate<ref_count>::getType() const {
+  Assert( NodeManager::currentNM() != NULL,
+          "There is no current CVC4::NodeManager associated to this thread.\n"
+          "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+  return NodeManager::currentNM()->getType(*this);
+}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__NODE_H */
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
index 7b78093c9..a7bc5f67d 100644
--- a/src/expr/node_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -12,9 +12,3 @@
  **
  **/
 
-#include "expr/node_builder.h"
-#include "expr/node_manager.h"
-#include "expr/node_value.h"
-#include "util/output.h"
-
-using namespace std;
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 36d634b8b..52e995bf4 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -27,6 +27,8 @@ namespace CVC4 {
 
 size_t NodeValue::next_id = 1;
 
+NodeValue NodeValue::s_null;
+
 NodeValue::NodeValue() :
   d_id(0),
   d_rc(MAX_RC),
@@ -64,22 +66,6 @@ void NodeValue::dec() {
   }
 }
 
-NodeValue::iterator NodeValue::begin() {
-  return node_iterator(d_children);
-}
-
-NodeValue::iterator NodeValue::end() {
-  return node_iterator(d_children + d_nchildren);
-}
-
-NodeValue::const_iterator NodeValue::begin() const {
-  return const_node_iterator(d_children);
-}
-
-NodeValue::const_iterator NodeValue::end() const {
-  return const_node_iterator(d_children + d_nchildren);
-}
-
 NodeValue::ev_iterator NodeValue::ev_begin() {
   return d_children;
 }
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 2d84967c6..73418b06d 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -33,7 +33,7 @@
 
 namespace CVC4 {
 
-class Node;
+template <bool ref_count> class NodeTemplate;
 template <unsigned> class NodeBuilder;
 class NodeManager;
 
@@ -76,7 +76,7 @@ class NodeValue {
 
   // todo add exprMgr ref in debug case
 
-  friend class CVC4::Node;
+  template <bool> friend class CVC4::NodeTemplate;
   template <unsigned> friend class CVC4::NodeBuilder;
   friend class CVC4::NodeManager;
 
@@ -103,49 +103,45 @@ class NodeValue {
   const_ev_iterator ev_begin() const;
   const_ev_iterator ev_end() const;
 
-  class node_iterator {
+  template <bool ref_count>
+  class iterator {
     const_ev_iterator d_i;
   public:
-    explicit node_iterator(const_ev_iterator i) : d_i(i) {}
+    explicit iterator(const_ev_iterator i) : d_i(i) {}
 
-    inline Node operator*();
+    inline CVC4::NodeTemplate<ref_count> operator*();
 
-    bool operator==(const node_iterator& i) {
+    bool operator==(const iterator& i) {
       return d_i == i.d_i;
     }
 
-    bool operator!=(const node_iterator& i) {
+    bool operator!=(const iterator& i) {
       return d_i != i.d_i;
     }
 
-    node_iterator operator++() {
+    iterator operator++() {
       ++d_i;
       return *this;
     }
 
-    node_iterator operator++(int) {
-      return node_iterator(d_i++);
+    iterator operator++(int) {
+      return iterator(d_i++);
     }
 
     typedef std::input_iterator_tag iterator_category;
-    typedef Node value_type;
-    typedef ptrdiff_t difference_type;
-    typedef Node* pointer;
-    typedef Node& reference;
   };
-  typedef node_iterator const_node_iterator;
 
 public:
 
-  // Iterator support
-  typedef node_iterator iterator;
-  typedef node_iterator const_iterator;
-
-  iterator begin();
-  iterator end();
+  template <bool ref_count>
+  iterator<ref_count> begin() const {
+    return iterator<ref_count>(d_children);
+  }
 
-  const_iterator begin() const;
-  const_iterator end() const;
+  template <bool ref_count>
+  iterator<ref_count> end() const {
+    return iterator<ref_count>(d_children + d_nchildren);
+  }
 
   /**
    * Hash this expression.
@@ -207,8 +203,9 @@ public:
 namespace CVC4 {
 namespace expr {
 
-inline Node NodeValue::node_iterator::operator*() {
-  return Node(*d_i);
+template <bool ref_count>
+inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() {
+  return NodeTemplate<ref_count>(*d_i);
 }
 
 }/* CVC4::expr namespace */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index a96d499b6..a66e36a07 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -59,27 +59,27 @@ void CnfStream::assertClause(SatLiteral a, SatLiteral b, SatLiteral c) {
   assertClause(clause);
 }
 
-bool CnfStream::isCached(const Node& n) const {
+bool CnfStream::isCached(const TNode& n) const {
   return d_translationCache.find(n) != d_translationCache.end();
 }
 
-SatLiteral CnfStream::lookupInCache(const Node& n) const {
+SatLiteral CnfStream::lookupInCache(const TNode& n) const {
   Assert(isCached(n), "Node is not in CNF translation cache");
   return d_translationCache.find(n)->second;
 }
 
-void CnfStream::cacheTranslation(const Node& node, SatLiteral lit) {
+void CnfStream::cacheTranslation(const TNode& node, SatLiteral lit) {
   Debug("cnf") << "caching translation " << node << " to " << lit << endl;
-  d_translationCache.insert(make_pair(node, lit));
+  d_translationCache[node] = lit;
 }
 
-SatLiteral CnfStream::newLiteral(const Node& node) {
+SatLiteral CnfStream::newLiteral(const TNode& node) {
   SatLiteral lit = SatLiteral(d_satSolver->newVar());
   cacheTranslation(node, lit);
   return lit;
 }
 
-SatLiteral TseitinCnfStream::handleAtom(const Node& node) {
+SatLiteral TseitinCnfStream::handleAtom(const TNode& node) {
   Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
   Assert(!isCached(node), "atom already mapped!");
 
@@ -101,7 +101,7 @@ SatLiteral TseitinCnfStream::handleAtom(const Node& node) {
   return lit;
 }
 
-SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) {
+SatLiteral TseitinCnfStream::handleXor(const TNode& xorNode) {
   Assert(!isCached(xorNode), "Atom already mapped!");
   Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
   Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -119,7 +119,7 @@ SatLiteral TseitinCnfStream::handleXor(const Node& xorNode) {
   return xorLit;
 }
 
-SatLiteral TseitinCnfStream::handleOr(const Node& orNode) {
+SatLiteral TseitinCnfStream::handleOr(const TNode& orNode) {
   Assert(!isCached(orNode), "Atom already mapped!");
   Assert(orNode.getKind() == OR, "Expecting an OR expression!");
   Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
@@ -128,8 +128,8 @@ SatLiteral TseitinCnfStream::handleOr(const Node& orNode) {
   unsigned n_children = orNode.getNumChildren();
 
   // Transform all the children first
-  Node::iterator node_it = orNode.begin();
-  Node::iterator node_it_end = orNode.end();
+  TNode::const_iterator node_it = orNode.begin();
+  TNode::const_iterator node_it_end = orNode.end();
   SatClause clause(n_children + 1);
   for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
     clause[i] = toCNF(*node_it);
@@ -155,7 +155,7 @@ SatLiteral TseitinCnfStream::handleOr(const Node& orNode) {
   return orLit;
 }
 
-SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) {
+SatLiteral TseitinCnfStream::handleAnd(const TNode& andNode) {
   Assert(!isCached(andNode), "Atom already mapped!");
   Assert(andNode.getKind() == AND, "Expecting an AND expression!");
   Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
@@ -164,8 +164,8 @@ SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) {
   unsigned n_children = andNode.getNumChildren();
 
   // Transform all the children first (remembering the negation)
-  Node::iterator node_it = andNode.begin();
-  Node::iterator node_it_end = andNode.end();
+  TNode::const_iterator node_it = andNode.begin();
+  TNode::const_iterator node_it_end = andNode.end();
   SatClause clause(n_children + 1);
   for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
     clause[i] = ~toCNF(*node_it);
@@ -190,7 +190,7 @@ SatLiteral TseitinCnfStream::handleAnd(const Node& andNode) {
   return andLit;
 }
 
-SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) {
+SatLiteral TseitinCnfStream::handleImplies(const TNode& impliesNode) {
   Assert(!isCached(impliesNode), "Atom already mapped!");
   Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
   Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -215,7 +215,7 @@ SatLiteral TseitinCnfStream::handleImplies(const Node& impliesNode) {
 }
 
 
-SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) {
+SatLiteral TseitinCnfStream::handleIff(const TNode& iffNode) {
   Assert(!isCached(iffNode), "Atom already mapped!");
   Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
   Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
@@ -245,7 +245,7 @@ SatLiteral TseitinCnfStream::handleIff(const Node& iffNode) {
 }
 
 
-SatLiteral TseitinCnfStream::handleNot(const Node& notNode) {
+SatLiteral TseitinCnfStream::handleNot(const TNode& notNode) {
   Assert(!isCached(notNode), "Atom already mapped!");
   Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
   Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!");
@@ -258,7 +258,7 @@ SatLiteral TseitinCnfStream::handleNot(const Node& notNode) {
   return notLit;
 }
 
-SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) {
+SatLiteral TseitinCnfStream::handleIte(const TNode& iteNode) {
   Assert(iteNode.getKind() == ITE);
   Assert(iteNode.getNumChildren() == 3);
 
@@ -283,7 +283,7 @@ SatLiteral TseitinCnfStream::handleIte(const Node& iteNode) {
   return iteLit;
 }
 
-SatLiteral TseitinCnfStream::toCNF(const Node& node) {
+SatLiteral TseitinCnfStream::toCNF(const TNode& node) {
 
   // If the node has already been translated, return the previous translation
   if(isCached(node)) {
@@ -316,12 +316,12 @@ SatLiteral TseitinCnfStream::toCNF(const Node& node) {
   }
 }
 
-void TseitinCnfStream::convertAndAssert(const Node& node) {
+void TseitinCnfStream::convertAndAssert(const TNode& node) {
   Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
   // If the node is a conjuntion, we handle each conjunct separatelu
   if (node.getKind() == AND) {
-    Node::iterator conjunct = node.begin();
-    Node::iterator node_end = node.end();
+    TNode::const_iterator conjunct = node.begin();
+    TNode::const_iterator node_end = node.end();
     while (conjunct != node_end) {
       convertAndAssert(*conjunct);
       ++ conjunct;
@@ -332,7 +332,7 @@ void TseitinCnfStream::convertAndAssert(const Node& node) {
   if (node.getKind() == OR) {
     int nChildren = node.getNumChildren();
     SatClause clause(nChildren);
-    Node::iterator disjunct = node.begin();
+    TNode::const_iterator disjunct = node.begin();
     for (int i = 0; i < nChildren; ++ disjunct, ++ i) {
       clause[i] = toCNF(*disjunct);
     }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index d7bb3c265..83a6aa68f 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -81,14 +81,14 @@ protected:
    * @param node the node
    * @return true if the node has been cached
    */
-  bool isCached(const Node& node) const;
+  bool isCached(const TNode& node) const;
 
   /**
    * Returns the cashed literal corresponding to the given node.
    * @param node the node to lookup
    * @return returns the corresponding literal
    */
-  SatLiteral lookupInCache(const Node& n) const;
+  SatLiteral lookupInCache(const TNode& n) const;
 
   /**
    * Caches the pair of the node and the literal corresponding to the
@@ -96,7 +96,7 @@ protected:
    * @param node node
    * @param lit
    */
-  void cacheTranslation(const Node& node, SatLiteral lit);
+  void cacheTranslation(const TNode& node, SatLiteral lit);
 
   /**
    * Acquires a new variable from the SAT solver to represent the node and
@@ -104,7 +104,7 @@ protected:
    * @param node a formula
    * @return the literal corresponding to the formula
    */
-  SatLiteral newLiteral(const Node& node);
+  SatLiteral newLiteral(const TNode& node);
 
 public:
 
@@ -128,7 +128,7 @@ public:
    * @param node node to convert and assert
    * @param whether the sat solver can choose to remove this clause
    */
-  virtual void convertAndAssert(const Node& node) = 0;
+  virtual void convertAndAssert(const TNode& node) = 0;
 
 }; /* class CnfStream */
 
@@ -150,7 +150,7 @@ public:
    * Convert a given formula to CNF and assert it to the SAT solver.
    * @param node the formula to assert
    */
-  void convertAndAssert(const Node& node);
+  void convertAndAssert(const TNode& node);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -170,21 +170,21 @@ private:
   //   - returning l
   //
   // handleX( n ) can assume that n is not in d_translationCache
-  SatLiteral handleAtom(const Node& node);
-  SatLiteral handleNot(const Node& node);
-  SatLiteral handleXor(const Node& node);
-  SatLiteral handleImplies(const Node& node);
-  SatLiteral handleIff(const Node& node);
-  SatLiteral handleIte(const Node& node);
-  SatLiteral handleAnd(const Node& node);
-  SatLiteral handleOr(const Node& node);
+  SatLiteral handleAtom(const TNode& node);
+  SatLiteral handleNot(const TNode& node);
+  SatLiteral handleXor(const TNode& node);
+  SatLiteral handleImplies(const TNode& node);
+  SatLiteral handleIff(const TNode& node);
+  SatLiteral handleIte(const TNode& node);
+  SatLiteral handleAnd(const TNode& node);
+  SatLiteral handleOr(const TNode& node);
 
   /**
    * Transforms the node into CNF recursively.
    * @param node the formula to transform
    * @return the literal representing the root of the formula
    */
-  SatLiteral toCNF(const Node& node);
+  SatLiteral toCNF(const TNode& node);
 
 }; /* class TseitinCnfStream */