cosmetic changes, comments, and renaming of Expr related stuff to Node (leftovers from before switching to Node)

8 files changed, 487 insertions, 426 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 46ffcef35..e1085a32a 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -30,15 +30,20 @@
 
 namespace CVC4 {
 
+class Type;
+class NodeManager;
 template<bool ref_count>
   class NodeTemplate;
-typedef NodeTemplate<true> Node;
-typedef NodeTemplate<false> TNode;
 
-inline std::ostream& operator<<(std::ostream&, const Node&);
+/**
+ * The Node class encapsulates the NodeValue with reference counting.
+ */
+typedef NodeTemplate<true> Node;
 
-class NodeManager;
-class Type;
+/**
+ * The TNode class encapsulates the NodeValue but doesn't count references.
+ */
+typedef NodeTemplate<false> TNode;
 
 namespace expr {
 class NodeValue;
@@ -48,44 +53,45 @@ using CVC4::expr::NodeValue;
 
 /**
  * Encapsulation of an NodeValue pointer.  The reference count is
- * maintained in the NodeValue.
+ * maintained in the NodeValue if ref_count is true.
+ * @param ref_count if true reference are counted in the NodeValue
  */
 template<bool ref_count>
   class NodeTemplate {
 
-  friend class NodeValue;
+    /**
+     * The NodeValue has access to the private constructors, so that the iterators
+     * can can create new nodes.
+     */
+    friend class NodeValue;
 
     /** A convenient null-valued encapsulated pointer */
     static NodeTemplate s_null;
 
     /** The referenced NodeValue */
-    NodeValue* d_ev;
-
-    bool d_count_ref;
+    NodeValue* d_nv;
 
-    /** 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.
+    /**
+     * 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.
      *
-     *  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
+     * This really does needs to be explicit to avoid hard to track errors with
+     * Nodes implicitly wrapping NodeValues
+     */
     explicit NodeTemplate(const NodeValue*);
 
+    friend class NodeTemplate<true> ;
+    friend class NodeTemplate<false> ;
+    friend class NodeManager;
     template<unsigned>
       friend class NodeBuilder;
 
-    friend class NodeTemplate<true>;
-    friend class NodeTemplate<false>;
-
-    friend class NodeManager;
-
     /**
      * 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
@@ -95,127 +101,271 @@ template<bool ref_count>
      */
     void assignNodeValue(NodeValue* ev);
 
-    typedef NodeValue::ev_iterator ev_iterator;
-    typedef NodeValue::const_ev_iterator const_ev_iterator;
-
-    inline ev_iterator ev_begin();
-    inline ev_iterator ev_end();
-    inline const_ev_iterator ev_begin() const;
-    inline const_ev_iterator ev_end() const;
-
   public:
 
     /** Default constructor, makes a null expression. */
-    NodeTemplate();
+    NodeTemplate() : d_nv(&NodeValue::s_null) { }
 
-    NodeTemplate operator[](int i) const {
-      Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
-      return NodeTemplate(d_ev->d_children[i]);
-    }
+    /**
+     * Copy constructor for nodes that can accept the nodes that are reference
+     * counted or not.
+     * @param node the node to make copy of
+     */
+    template<bool ref_count_1>
+      NodeTemplate(const NodeTemplate<ref_count_1>& node);
 
-    template <bool ref_count_1>
-    NodeTemplate(const NodeTemplate<ref_count_1>&);
+    /**
+     * Assignment operator for nodes, copies the relevant information from node
+     * to this node.
+     * @param node the node to copy
+     * @return reference to this node
+     */
+    template<bool ref_count_1>
+      NodeTemplate& operator=(const NodeTemplate<ref_count_1>& node);
 
-    /** Destructor.  Decrements the reference count and, if zero,
-     *  collects the NodeValue. */
+    /**
+     * Destructor. If ref_count is true it will decrement the reference count
+     * and, if zero, collect the NodeValue.
+     */
     ~NodeTemplate();
 
-    bool operator==(const NodeTemplate& e) const {
-      return d_ev == e.d_ev;
+    /**
+     * Return the null node.
+     * @return the null node
+     */
+    static NodeTemplate null() {
+      return s_null;
+    }
+
+    /**
+     * Returns true if this expression is a null expression.
+     * @return true if null
+     */
+    bool isNull() const {
+      return d_nv == &NodeValue::s_null;
+    }
+
+    /**
+     * Structural comparison operator for expressions.
+     * @param node the node to compare to
+     * @return true if expressions are equal, false otherwise
+     */
+    template <bool ref_count_1>
+    bool operator==(const NodeTemplate<ref_count_1>& node) const {
+      return d_nv == node.d_nv;
     }
-    bool operator!=(const NodeTemplate& e) const {
-      return d_ev != e.d_ev;
+
+    /**
+     * Structural comparison operator for expressions.
+     * @param node the node to compare to
+     * @return false if expressions are equal, true otherwise
+     */
+    template <bool ref_count_1>
+    bool operator!=(const NodeTemplate<ref_count_1>& node) const {
+      return d_nv != node.d_nv;
     }
 
     /**
      * We compare by expression ids so, keeping things deterministic and having
      * that subexpressions have to be smaller than the enclosing expressions.
+     * @param node the node to compare to
+     * @return true if this expression is smaller
      */
-    inline bool operator<(const NodeTemplate& e) const;
-
     template <bool ref_count_1>
-    NodeTemplate& operator=(const NodeTemplate<ref_count_1>&);
+    inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
+      return d_nv->d_id < node.d_nv->d_id;
+    }
 
+    /**
+     * Returns the i-th child of this node.
+     * @param i the index of the child
+     * @return the node representing the i-th child
+     */
+    NodeTemplate operator[](int i) const {
+      Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren);
+      return NodeTemplate(d_nv->d_children[i]);
+    }
+
+    /**
+     * Returns true if this node is atomic (has no more Boolean structure)
+     * @return true if atomic
+     */
+    bool isAtomic() const;
+
+    /**
+     * Returns the hash value of this node.
+     * @return the hash value
+     */
     size_t hash() const {
-      return d_ev->getId();
+      return d_nv->getId();
     }
 
+    /**
+     * Returns the unique id of this node
+     * @return the ud
+     */
     uint64_t getId() const {
-      return d_ev->getId();
+      return d_nv->getId();
     }
 
+    /**
+     * Returns the type of this node.
+     * @return the type
+     */
     const Type* getType() const;
 
-    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;
-
-    NodeTemplate plusExpr(const NodeTemplate& right) const;
-    NodeTemplate uMinusExpr() const;
-    NodeTemplate multExpr(const NodeTemplate& right) const;
-
-    inline Kind getKind() const;
+    /**
+     * Returns the kind of this node.
+     * @return the kind
+     */
+    inline Kind getKind() const {
+      return Kind(d_nv->d_kind);
+    }
 
+    /**
+     * Returns the number of children this node has.
+     * @return the number of children
+     */
     inline size_t getNumChildren() const;
 
+    /**
+     * Returns the value of the given attribute that this has been attached.
+     * @param attKind the kind of the attribute
+     * @return the value of the attribute
+     */
+    template<class AttrKind>
+      inline typename AttrKind::value_type getAttribute(const AttrKind& attKind) const;
 
-    static NodeTemplate null();
+    /**
+     * Returns true if this node has been associated an attribute of given kind.
+     * Additionaly, if a pointer to the value_kind is give, and the attribute
+     * value has been set for this node, it will be returned.
+     * @param attKind the kind of the attribute
+     * @param value where to store the value if it exists
+     * @return true if this node has the requested attribute
+     */
+    template<class AttrKind>
+      inline bool hasAttribute(const AttrKind& attKind, typename AttrKind::value_type* value = NULL) const;
 
+    /** Iterator allowing for scanning through the children. */
     typedef typename NodeValue::iterator<ref_count> iterator;
+    /** Constant iterator allowing for scanning through the children. */
     typedef typename NodeValue::iterator<ref_count> const_iterator;
 
-    inline iterator begin();
-    inline iterator end();
-    inline const_iterator begin() const;
-    inline const_iterator end() const;
+    /**
+     * Returns the iterator pointing to the first child.
+     * @return the iterator
+     */
+    inline iterator begin() {
+      return d_nv->begin<ref_count>();
+    }
+
+    /**
+     * Returns the iterator pointing to the end of the children (one beyond the
+     * last one.
+     * @return the end of the children iterator.
+     */
+    inline iterator end() {
+      return d_nv->end<ref_count>();
+    }
 
-    template <class AttrKind>
-    inline typename AttrKind::value_type getAttribute(const AttrKind&) const;
+    /**
+     * Returns the const_iterator pointing to the first child.
+     * @return the const_iterator
+     */
+    inline const_iterator begin() const {
+      return d_nv->begin<ref_count>();
+    }
 
-    template <class AttrKind>
-    inline bool hasAttribute(const AttrKind&, typename AttrKind::value_type* = NULL) const;
+    /**
+     * Returns the const_iterator pointing to the end of the children (one
+     * beyond the last one.
+     * @return the end of the children const_iterator.
+     */
+    inline const_iterator end() const {
+      return d_nv->end<ref_count>();
+    }
 
-    inline std::string toString() const;
-    inline void toStream(std::ostream&) const;
+    /**
+     * Converts this node into a string representation.
+     * @return the string representation of this node.
+     */
+    inline std::string toString() const {
+      return d_nv->toString();
+    }
 
+    /**
+     * Converst this node into a string representation and sends it to the
+     * given stream
+     * @param out the sream to serialise this node to
+     */
+    inline void toStream(std::ostream& out) const {
+      d_nv->toStream(out);
+    }
 
-    bool isNull() const;
-    bool isAtomic() const;
+    /**
+     * Very basic pretty printer for Node.
+     * @param o output stream to print to.
+     * @param indent number of spaces to indent the formula by.
+     */
+    void printAst(std::ostream & o, int indent = 0) const;
 
-  /**
-   * Very basic pretty printer for Node.
-   * @param o output stream to print to.
-   * @param indent number of spaces to indent the formula by.
-   */
-  void printAst(std::ostream & o, int indent = 0) const;
+    NodeTemplate eqNode(const NodeTemplate& right) const;
 
-private:
+    NodeTemplate notNode() const;
+    NodeTemplate andNode(const NodeTemplate& right) const;
+    NodeTemplate orNode(const NodeTemplate& right) const;
+    NodeTemplate iteNode(const NodeTemplate& thenpart,
+                         const NodeTemplate& elsepart) const;
+    NodeTemplate iffNode(const NodeTemplate& right) const;
+    NodeTemplate impNode(const NodeTemplate& right) const;
+    NodeTemplate xorNode(const NodeTemplate& right) const;
 
-  /**
-   * Pretty printer for use within gdb
-   * This is not intended to be used outside of gdb.
-   * This writes to the ostream Warning() and immediately flushes
-   * the ostream.
-   */
-  void debugPrint();
+    NodeTemplate plusNode(const NodeTemplate& right) const;
+    NodeTemplate uMinusNode() const;
+    NodeTemplate multNode(const NodeTemplate& right) const;
 
-  template<class AttrKind>
-  inline void setAttribute(
-      const AttrKind&, const typename AttrKind::value_type& value);
+  private:
 
-    static void indent(std::ostream & o, int indent) {
+    /**
+     * Pretty printer for use within gdb.  This is not intended to be used
+     * outside of gdb.  This writes to the Warning() stream and immediately
+     * flushes the stream.
+     */
+    void debugPrint();
+
+    /**
+     * Sets the given attribute of this node to the given value.
+     * @param attKind the kind of the atribute
+     * @param value the value to set the attribute to
+     */
+    template<class AttrKind>
+      inline void setAttribute(const AttrKind& attKind,
+                               const typename AttrKind::value_type& value);
+
+    /**
+     * Indents the given stream a given amount of spaces.
+     * @param out the stream to indent
+     * @param indent the numer of spaces
+     */
+    static void indent(std::ostream& out, int indent) {
       for(int i = 0; i < indent; i++)
-        o << ' ';
+        out << ' ';
     }
 
   };/* class NodeTemplate */
 
+/**
+ * Serializes a given node to the given stream.
+ * @param out the output stream to use
+ * @param node the node to output to the stream
+ * @return the changed stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, const Node& node) {
+  node.toStream(out);
+  return out;
+}
+
 }/* CVC4 namespace */
 
 #include <ext/hash_map>
@@ -236,124 +386,43 @@ template<>
 namespace CVC4 {
 
 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;
-}
-
-template<bool ref_count>
-  inline Kind NodeTemplate<ref_count>::getKind() const {
-    return Kind(d_ev->d_kind);
-  }
-
-template<bool ref_count>
-  inline std::string NodeTemplate<ref_count>::toString() const {
-    return d_ev->toString();
-  }
-
-template<bool ref_count>
-  inline void NodeTemplate<ref_count>::toStream(std::ostream& out) const {
-    d_ev->toStream(out);
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_begin() {
-    return d_ev->ev_begin();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::ev_iterator NodeTemplate<ref_count>::ev_end() {
-    return d_ev->ev_end();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate<
-      ref_count>::ev_begin() const {
-    return d_ev->ev_begin();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::const_ev_iterator NodeTemplate<
-      ref_count>::ev_end() const {
-    return d_ev->ev_end();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::begin() {
-    return d_ev->begin<ref_count> ();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::iterator NodeTemplate<ref_count>::end() {
-    return d_ev->end<ref_count> ();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate<
-      ref_count>::begin() const {
-    return d_ev->begin<ref_count> ();
-  }
-
-template<bool ref_count>
-  inline typename NodeTemplate<ref_count>::const_iterator NodeTemplate<
-      ref_count>::end() const {
-    return d_ev->end<ref_count> ();
-  }
-
-template<bool ref_count>
   inline size_t NodeTemplate<ref_count>::getNumChildren() const {
-    return d_ev->d_nchildren;
+    return d_nv->d_nchildren;
   }
 
-template <bool ref_count>
-template <class AttrKind>
-inline typename AttrKind::value_type NodeTemplate<ref_count>::getAttribute(const AttrKind&) const {
-  Assert( NodeManager::currentNM() != NULL,
+template<bool ref_count>
+  template<class AttrKind>
+    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 ?" );
+      return NodeManager::currentNM()->getAttribute(*this, AttrKind());
+    }
 
-  return NodeManager::currentNM()->getAttribute(*this, AttrKind());
-}
-
-template <bool ref_count>
-template <class AttrKind>
-inline bool NodeTemplate<ref_count>::hasAttribute(const AttrKind&,
-                               typename AttrKind::value_type* ret) const {
-  Assert( NodeManager::currentNM() != NULL,
+template<bool ref_count>
+  template<class AttrKind>
+    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 ?" );
+      return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
+    }
 
-  return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
-}
-
-template <bool ref_count>
-template <class AttrKind>
-inline void NodeTemplate<ref_count>::setAttribute(const AttrKind&,
-                               const typename AttrKind::value_type& value) {
-  Assert( NodeManager::currentNM() != NULL,
+template<bool ref_count>
+  template<class 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"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
-
-  NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
-}
+      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>
@@ -372,114 +441,106 @@ template<bool ref_count>
     }
   }
 
-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!");
+    d_nv(const_cast<NodeValue*> (ev)) {
+    Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
     if(ref_count)
-      d_ev->inc();
+      d_nv->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_1>
+    NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<ref_count_1>& e) {
+      Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
+      d_nv = e.d_nv;
+      if(ref_count)
+        d_nv->inc();
+    }
 
 template<bool ref_count>
   NodeTemplate<ref_count>::~NodeTemplate() {
-    Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+    Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
     if(ref_count)
-      d_ev->dec();
-    Assert(ref_count || d_ev->d_rc > 0,
+      d_nv->dec();
+    Assert(ref_count || d_nv->d_rc > 0,
         "Temporary node pointing to an expired node");
   }
 
 template<bool ref_count>
   void NodeTemplate<ref_count>::assignNodeValue(NodeValue* ev) {
-    d_ev = ev;
+    d_nv = ev;
     if(ref_count)
-      d_ev->inc();
+      d_nv->inc();
   }
 
 template<bool ref_count>
-template<bool ref_count_1>
-  NodeTemplate<ref_count>& NodeTemplate<ref_count>::operator=
-      (const NodeTemplate<ref_count_1>& 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();
+  template<bool ref_count_1>
+    NodeTemplate<ref_count>& NodeTemplate<ref_count>::
+    operator=(const NodeTemplate<ref_count_1>& e) {
+      Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
+      Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
+      if(EXPECT_TRUE( d_nv != e.d_nv )) {
+        if(ref_count)
+          d_nv->dec();
+        d_nv = e.d_nv;
+        if(ref_count)
+          d_nv->inc();
+      }
+      return *this;
     }
-    return *this;
-  }
 
 template<bool ref_count>
-  NodeTemplate<ref_count> NodeTemplate<ref_count>::eqExpr(const NodeTemplate<
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::eqNode(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 {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::notNode() const {
     return NodeManager::currentNM()->mkNode(NOT, *this);
   }
 
 template<bool ref_count>
-  NodeTemplate<ref_count> NodeTemplate<ref_count>::andExpr(
-      const NodeTemplate<ref_count>& right) const {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::andNode(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 {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::orNode(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 {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::iteNode(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 {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::iffNode(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 {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::impNode(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 {
+  NodeTemplate<ref_count> NodeTemplate<ref_count>::xorNode(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);
@@ -506,12 +567,12 @@ template<bool ref_count>
   }
 
 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);
-}
+  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 */
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 093f09a79..61b048a5b 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -57,21 +57,21 @@ class NodeBuilder {
   // extract another
   bool d_used;
 
-  NodeValue *d_ev;
-  NodeValue d_inlineEv;
+  NodeValue *d_nv;
+  NodeValue d_inlineNv;
   NodeValue *d_childrenStorage[nchild_thresh];
 
-  bool evIsAllocated() {
-    return d_ev->d_nchildren > nchild_thresh;
+  bool nvIsAllocated() {
+    return d_nv->d_nchildren > nchild_thresh;
   }
 
   template <unsigned N>
-  bool evIsAllocated(const NodeBuilder<N>& nb) {
-    return nb.d_ev->d_nchildren > N;
+  bool nvIsAllocated(const NodeBuilder<N>& nb) {
+    return nb.d_nv->d_nchildren > N;
   }
 
   bool evNeedsToBeAllocated() {
-    return d_ev->d_nchildren == d_size;
+    return d_nv->d_nchildren == d_size;
   }
 
   // realloc in the default way
@@ -86,15 +86,15 @@ class NodeBuilder {
     }
   }
 
-  // dealloc: only call this with d_used == false and evIsAllocated()
+  // dealloc: only call this with d_used == false and nvIsAllocated()
   inline void dealloc();
 
   void crop() {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    if(EXPECT_FALSE( evIsAllocated() ) && EXPECT_TRUE( d_size > d_ev->d_nchildren )) {
-      d_ev = (NodeValue*)
-        std::realloc(d_ev, sizeof(NodeValue) +
-                     ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) ));
+    if(EXPECT_FALSE( nvIsAllocated() ) && EXPECT_TRUE( d_size > d_nv->d_nchildren )) {
+      d_nv = (NodeValue*)
+        std::realloc(d_nv, sizeof(NodeValue) +
+                     ( sizeof(NodeValue*) * (d_size = d_nv->d_nchildren) ));
     }
   }
 
@@ -108,37 +108,37 @@ public:
   inline NodeBuilder(NodeManager* nm, Kind k);
   inline ~NodeBuilder();
 
-  typedef NodeValue::ev_iterator iterator;
-  typedef NodeValue::const_ev_iterator const_iterator;
+  typedef NodeValue::nv_iterator iterator;
+  typedef NodeValue::const_nv_iterator const_iterator;
 
   iterator begin() {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_ev->ev_begin();
+    return d_nv->nv_begin();
   }
   iterator end() {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_ev->ev_end();
+    return d_nv->nv_end();
   }
   const_iterator begin() const {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_ev->ev_begin();
+    return d_nv->nv_begin();
   }
   const_iterator end() const {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    return d_ev->ev_end();
+    return d_nv->nv_end();
   }
 
   Kind getKind() const {
-    return d_ev->getKind();
+    return d_nv->getKind();
   }
 
   unsigned getNumChildren() const {
-    return d_ev->getNumChildren();
+    return d_nv->getNumChildren();
   }
 
   Node operator[](int i) const {
-    Assert(i >= 0 && i < d_ev->getNumChildren());
-    return Node(d_ev->d_children[i]);
+    Assert(i >= 0 && i < d_nv->getNumChildren());
+    return Node(d_nv->d_children[i]);
   }
 
   void clear(Kind k = UNDEFINED_KIND);
@@ -171,8 +171,8 @@ public:
 
   NodeBuilder& operator<<(const Kind& k) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    Assert(d_ev->getKind() == UNDEFINED_KIND);
-    d_ev->d_kind = k;
+    Assert(d_nv->getKind() == UNDEFINED_KIND);
+    d_nv->d_kind = k;
     return *this;
   }
 
@@ -189,11 +189,11 @@ public:
 
   NodeBuilder& append(const Node& n) {
     Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-    Debug("prop") << "append: " << this << " " << n << "[" << n.d_ev << "]" << std::endl;
+    Debug("prop") << "append: " << this << " " << n << "[" << n.d_nv << "]" << std::endl;
     allocateEvIfNecessaryForAppend();
-    NodeValue* ev = n.d_ev;
+    NodeValue* ev = n.d_nv;
     ev->inc();
-    d_ev->d_children[d_ev->d_nchildren++] = ev;
+    d_nv->d_children[d_nv->d_nchildren++] = ev;
     return *this;
   }
 
@@ -210,7 +210,7 @@ public:
   operator Node();
 
   inline void toStream(std::ostream& out) const {
-    d_ev->toStream(out);
+    d_nv->toStream(out);
   }
 
   /*
@@ -388,8 +388,8 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder() :
   d_hash(0),
   d_nm(NodeManager::currentNM()),
   d_used(false),
-  d_ev(&d_inlineEv),
-  d_inlineEv(0),
+  d_nv(&d_inlineNv),
+  d_inlineNv(0),
   d_childrenStorage() {}
 
 template <unsigned nchild_thresh>
@@ -398,12 +398,12 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
   d_hash(0),
   d_nm(NodeManager::currentNM()),
   d_used(false),
-  d_ev(&d_inlineEv),
-  d_inlineEv(0),
+  d_nv(&d_inlineNv),
+  d_inlineNv(0),
   d_childrenStorage() {
 
   //Message() << "kind " << k << std::endl;
-  d_inlineEv.d_kind = k;
+  d_inlineNv.d_kind = k;
 }
 
 template <unsigned nchild_thresh>
@@ -412,18 +412,18 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>&
   d_hash(0),
   d_nm(nb.d_nm),
   d_used(nb.d_used),
-  d_ev(&d_inlineEv),
-  d_inlineEv(0),
+  d_nv(&d_inlineNv),
+  d_inlineNv(0),
   d_childrenStorage() {
 
-  if(evIsAllocated(nb)) {
+  if(nvIsAllocated(nb)) {
     realloc(nb.d_size, false);
-    std::copy(nb.d_ev->ev_begin(), nb.d_ev->ev_end(), d_ev->ev_begin());
+    std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin());
   } else {
-    std::copy(nb.d_ev->ev_begin(), nb.d_ev->ev_end(), d_inlineEv.ev_begin());
+    std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_inlineNv.nv_begin());
   }
-  d_ev->d_kind = nb.d_ev->d_kind;
-  d_ev->d_nchildren = nb.d_ev->d_nchildren;
+  d_nv->d_kind = nb.d_nv->d_kind;
+  d_nv->d_nchildren = nb.d_nv->d_nchildren;
 }
 
 template <unsigned nchild_thresh>
@@ -433,18 +433,18 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
   d_hash(0),
   d_nm(NodeManager::currentNM()),
   d_used(nb.d_used),
-  d_ev(&d_inlineEv),
-  d_inlineEv(0),
+  d_nv(&d_inlineNv),
+  d_inlineNv(0),
   d_childrenStorage() {
 
-  if(nb.d_ev->d_nchildren > nchild_thresh) {
+  if(nb.d_nv->d_nchildren > nchild_thresh) {
     realloc(nb.d_size, false);
-    std::copy(nb.d_ev->ev_begin(), nb.d_ev->end(), d_ev->ev_begin());
+    std::copy(nb.d_nv->ev_begin(), nb.d_nv->end(), d_nv->nv_begin());
   } else {
-    std::copy(nb.d_ev->ev_begin(), nb.d_ev->end(), d_inlineEv.ev_begin());
+    std::copy(nb.d_nv->ev_begin(), nb.d_nv->end(), d_inlineNv.nv_begin());
   }
-  d_ev->d_kind = nb.d_ev->d_kind;
-  d_ev->d_nchildren = nb.d_ev->d_nchildren;
+  d_nv->d_kind = nb.d_nv->d_kind;
+  d_nv->d_nchildren = nb.d_nv->d_nchildren;
 }
 
 template <unsigned nchild_thresh>
@@ -453,10 +453,10 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
   d_hash(0),
   d_nm(nm),
   d_used(false),
-  d_ev(&d_inlineEv),
-  d_inlineEv(0),
+  d_nv(&d_inlineNv),
+  d_inlineNv(0),
   d_childrenStorage() {
-  d_inlineEv.d_kind = UNDEFINED_KIND;
+  d_inlineNv.d_kind = UNDEFINED_KIND;
 }
 
 template <unsigned nchild_thresh>
@@ -465,12 +465,12 @@ inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
   d_hash(0),
   d_nm(nm),
   d_used(false),
-  d_ev(&d_inlineEv),
-  d_inlineEv(0),
+  d_nv(&d_inlineNv),
+  d_inlineNv(0),
   d_childrenStorage() {
 
   //Message() << "kind " << k << std::endl;
-  d_inlineEv.d_kind = k;
+  d_inlineNv.d_kind = k;
 }
 
 template <unsigned nchild_thresh>
@@ -494,27 +494,27 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) {
   d_hash = 0;
   d_nm = NodeManager::currentNM();
   d_used = false;
-  d_ev = &d_inlineEv;
-  d_inlineEv.d_kind = k;
-  d_inlineEv.d_nchildren = 0;
+  d_nv = &d_inlineNv;
+  d_inlineNv.d_kind = k;
+  d_inlineNv.d_nchildren = 0;
 }
 
 template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc() {
-  if(EXPECT_FALSE( evIsAllocated() )) {
-    d_ev = (NodeValue*)
-      std::realloc(d_ev,
+  if(EXPECT_FALSE( nvIsAllocated() )) {
+    d_nv = (NodeValue*)
+      std::realloc(d_nv,
                    sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
   } else {
-    d_ev = (NodeValue*)
+    d_nv = (NodeValue*)
       std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
-    d_ev->d_id = 0;
-    d_ev->d_rc = 0;
-    d_ev->d_kind = d_inlineEv.d_kind;
-    d_ev->d_nchildren = nchild_thresh;
-    std::copy(d_inlineEv.d_children,
-              d_inlineEv.d_children + nchild_thresh,
-              d_ev->d_children);
+    d_nv->d_id = 0;
+    d_nv->d_rc = 0;
+    d_nv->d_kind = d_inlineNv.d_kind;
+    d_nv->d_nchildren = nchild_thresh;
+    std::copy(d_inlineNv.d_children,
+              d_inlineNv.d_children + nchild_thresh,
+              d_nv->d_children);
   }
 }
 
@@ -522,22 +522,22 @@ template <unsigned nchild_thresh>
 void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) {
   Assert( d_size < toSize );
 
-  if(EXPECT_FALSE( evIsAllocated() )) {
-    d_ev = (NodeValue*)
-      std::realloc(d_ev, sizeof(NodeValue) +
+  if(EXPECT_FALSE( nvIsAllocated() )) {
+    d_nv = (NodeValue*)
+      std::realloc(d_nv, sizeof(NodeValue) +
                    ( sizeof(NodeValue*) * (d_size = toSize) ));
   } else {
-    d_ev = (NodeValue*)
+    d_nv = (NodeValue*)
       std::malloc(sizeof(NodeValue) +
                   ( sizeof(NodeValue*) * (d_size = toSize) ));
-    d_ev->d_id = 0;
-    d_ev->d_rc = 0;
-    d_ev->d_kind = d_inlineEv.d_kind;
-    d_ev->d_nchildren = nchild_thresh;
+    d_nv->d_id = 0;
+    d_nv->d_rc = 0;
+    d_nv->d_kind = d_inlineNv.d_kind;
+    d_nv->d_nchildren = nchild_thresh;
     if(copy) {
-      std::copy(d_inlineEv.d_children,
-                d_inlineEv.d_children + nchild_thresh,
-                d_ev->d_children);
+      std::copy(d_inlineNv.d_children,
+                d_inlineNv.d_children + nchild_thresh,
+                d_nv->d_children);
     }
   }
 }
@@ -550,64 +550,64 @@ inline void NodeBuilder<nchild_thresh>::dealloc() {
   Assert(!d_used,
          "Internal error: NodeBuilder: dealloc() called with d_used");
 
-  for(iterator i = d_ev->ev_begin();
-      i != d_ev->ev_end();
+  for(iterator i = d_nv->nv_begin();
+      i != d_nv->nv_end();
       ++i) {
     (*i)->dec();
   }
-  if(evIsAllocated()) {
-    free(d_ev);
+  if(nvIsAllocated()) {
+    free(d_nv);
   }
 }
 
 template <unsigned nchild_thresh>
 NodeBuilder<nchild_thresh>::operator Node() {// not const
   Assert(!d_used, "NodeBuilder is one-shot only; tried to access it after conversion");
-  Assert(d_ev->getKind() != UNDEFINED_KIND,
+  Assert(d_nv->getKind() != UNDEFINED_KIND,
          "Can't make an expression of an undefined kind!");
 
-  if(d_ev->d_kind == VARIABLE) {
-    Assert(d_ev->d_nchildren == 0);
-    NodeValue *ev = (NodeValue*)
+  if(d_nv->d_kind == VARIABLE) {
+    Assert(d_nv->d_nchildren == 0);
+    NodeValue *nv = (NodeValue*)
       std::malloc(sizeof(NodeValue) +
-                  ( sizeof(NodeValue*) * d_inlineEv.d_nchildren ));
-    ev->d_nchildren = 0;
-    ev->d_kind = VARIABLE;
-    ev->d_id = NodeValue::next_id++;// FIXME multithreading
-    ev->d_rc = 0;
+                  ( sizeof(NodeValue*) * d_inlineNv.d_nchildren ));
+    nv->d_nchildren = 0;
+    nv->d_kind = VARIABLE;
+    nv->d_id = NodeValue::next_id++;// FIXME multithreading
+    nv->d_rc = 0;
     d_used = true;
-    d_ev = NULL;
-    Debug("prop") << "result: " << Node(ev) << std::endl;
-    return Node(ev);
+    d_nv = NULL;
+    Debug("prop") << "result: " << Node(nv) << std::endl;
+    return Node(nv);
   }
 
   // implementation differs depending on whether the expression value
   // was malloc'ed or not
 
-  if(EXPECT_FALSE( evIsAllocated() )) {
+  if(EXPECT_FALSE( nvIsAllocated() )) {
     // Lookup the expression value in the pool we already have (with insert)
-    NodeValue* ev = d_nm->poolLookup(d_ev);
+    NodeValue* nv = d_nm->poolLookup(d_nv);
     // If something else is there, we reuse it
-    if(ev != NULL) {
+    if(nv != NULL) {
       // expression already exists in node manager
       dealloc();
       d_used = true;
-      Debug("prop") << "result: " << Node(ev) << std::endl;
-      return Node(ev);
+      Debug("prop") << "result: " << Node(nv) << std::endl;
+      return Node(nv);
     }
     // Otherwise crop and set the expression value to the allocate one
     crop();
-    ev = d_ev;
-    d_ev = NULL;
+    nv = d_nv;
+    d_nv = NULL;
     d_used = true;
-    d_nm->poolInsert(ev);
-    Node n(ev);
+    d_nm->poolInsert(nv);
+    Node n(nv);
     Debug("prop") << "result: " << n << std::endl;
     return n;
   }
 
   // Lookup the expression value in the pool we already have
-  NodeValue* ev = d_nm->poolLookup(&d_inlineEv);
+  NodeValue* ev = d_nm->poolLookup(&d_inlineNv);
   if(ev != NULL) {
     // expression already exists in node manager
     d_used = true;
@@ -618,16 +618,16 @@ NodeBuilder<nchild_thresh>::operator Node() {// not const
   // otherwise create the canonical expression value for this node
   ev = (NodeValue*)
     std::malloc(sizeof(NodeValue) +
-                ( sizeof(NodeValue*) * d_inlineEv.d_nchildren ));
-  ev->d_nchildren = d_inlineEv.d_nchildren;
-  ev->d_kind = d_inlineEv.d_kind;
+                ( sizeof(NodeValue*) * d_inlineNv.d_nchildren ));
+  ev->d_nchildren = d_inlineNv.d_nchildren;
+  ev->d_kind = d_inlineNv.d_kind;
   ev->d_id = NodeValue::next_id++;// FIXME multithreading
   ev->d_rc = 0;
-  std::copy(d_inlineEv.d_children,
-            d_inlineEv.d_children + d_inlineEv.d_nchildren,
+  std::copy(d_inlineNv.d_children,
+            d_inlineNv.d_children + d_inlineNv.d_nchildren,
             ev->d_children);
   d_used = true;
-  d_ev = NULL;
+  d_nv = NULL;
 
   // Make the new expression
   d_nm->poolInsert(ev);
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 52e995bf4..863ddf649 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -44,7 +44,7 @@ NodeValue::NodeValue(int) :
 }
 
 NodeValue::~NodeValue() {
-  for(ev_iterator i = ev_begin(); i != ev_end(); ++i) {
+  for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
   }
 }
@@ -66,19 +66,19 @@ void NodeValue::dec() {
   }
 }
 
-NodeValue::ev_iterator NodeValue::ev_begin() {
+NodeValue::nv_iterator NodeValue::nv_begin() {
   return d_children;
 }
 
-NodeValue::ev_iterator NodeValue::ev_end() {
+NodeValue::nv_iterator NodeValue::nv_end() {
   return d_children + d_nchildren;
 }
 
-NodeValue::const_ev_iterator NodeValue::ev_begin() const {
+NodeValue::const_nv_iterator NodeValue::nv_begin() const {
   return d_children;
 }
 
-NodeValue::const_ev_iterator NodeValue::ev_end() const {
+NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
@@ -99,8 +99,8 @@ void NodeValue::toStream(std::ostream& out) const {
       out << ":" << this;
     }
   } else {
-    for(const_ev_iterator i = ev_begin(); i != ev_end(); ++i) {
-      if(i != ev_end()) {
+    for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+      if(i != nv_end()) {
         out << " ";
       }
       out << *i;
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 73418b06d..f0220d37a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -94,20 +94,20 @@ class NodeValue {
   /** Destructor decrements the ref counts of its children */
   ~NodeValue();
 
-  typedef NodeValue** ev_iterator;
-  typedef NodeValue const* const* const_ev_iterator;
+  typedef NodeValue** nv_iterator;
+  typedef NodeValue const* const* const_nv_iterator;
 
-  ev_iterator ev_begin();
-  ev_iterator ev_end();
+  nv_iterator nv_begin();
+  nv_iterator nv_end();
 
-  const_ev_iterator ev_begin() const;
-  const_ev_iterator ev_end() const;
+  const_nv_iterator nv_begin() const;
+  const_nv_iterator nv_end() const;
 
   template <bool ref_count>
   class iterator {
-    const_ev_iterator d_i;
+    const_nv_iterator d_i;
   public:
-    explicit iterator(const_ev_iterator i) : d_i(i) {}
+    explicit iterator(const_nv_iterator i) : d_i(i) {}
 
     inline CVC4::NodeTemplate<ref_count> operator*();
 
@@ -149,8 +149,8 @@ public:
    */
   size_t hash() const {
     size_t hash = d_kind;
-    const_ev_iterator i = ev_begin();
-    const_ev_iterator i_end = ev_end();
+    const_nv_iterator i = nv_begin();
+    const_nv_iterator i_end = nv_end();
     while (i != i_end) {
       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
       ++ i;
@@ -163,9 +163,9 @@ public:
       return false;
     if(d_nchildren != nv->d_nchildren)
       return false;
-    const_ev_iterator i = ev_begin();
-    const_ev_iterator j = nv->ev_begin();
-    const_ev_iterator i_end = ev_end();
+    const_nv_iterator i = nv_begin();
+    const_nv_iterator j = nv->nv_begin();
+    const_nv_iterator i_end = nv_end();
     while(i != i_end) {
       if ((*i) != (*j)) return false;
       ++i; ++j;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bb3e8c058..ea1fe0306 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -76,7 +76,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << std::endl;
-  addFormula(e.getNode().notExpr());
+  addFormula(e.getNode().notNode());
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl;
   return r;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1f4d80b9b..6f9171f36 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -95,7 +95,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){
   for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->next ){
     for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->next ){
       if(equiv(Px->data,Py->data)){
-        d_pending.push_back((Px->data).eqExpr(Py->data));
+        d_pending.push_back((Px->data).eqNode(Py->data));
       }
     }
   }
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 102549c42..75ab25f4c 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -170,7 +170,7 @@ public:
     Node tb = d_nm->mkNode(TRUE);
     Node eb = d_nm->mkNode(FALSE);
     Node cnd = d_nm->mkNode(XOR, tb, eb);
-    Node ite = cnd.iteExpr(tb,eb);
+    Node ite = cnd.iteNode(tb,eb);
 
     TS_ASSERT(tb == cnd[0]);
     TS_ASSERT(eb == cnd[1]);
@@ -261,12 +261,12 @@ public:
 
   
 
-  void testEqExpr() {
-    /*Node eqExpr(const Node& right) const;*/
+  void testEqNode() {
+    /*Node eqNode(const Node& right) const;*/
 
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node eq = left.eqExpr(right);
+    Node eq = left.eqNode(right);
     
 
     TS_ASSERT(EQUAL == eq.getKind());
@@ -276,11 +276,11 @@ public:
     TS_ASSERT(eq[1] == right);
   }
 
-  void testNotExpr() {
-    /*  Node notExpr() const;*/
+  void testNotNode() {
+    /*  Node notNode() const;*/
 
     Node child = d_nm->mkNode(TRUE);
-    Node parent = child.notExpr();
+    Node parent = child.notNode();
 
     TS_ASSERT(NOT == parent.getKind());
     TS_ASSERT(1   == parent.getNumChildren());
@@ -288,12 +288,12 @@ public:
     TS_ASSERT(parent[0] == child);
     
   }
-  void testAndExpr() {
-    /*Node andExpr(const Node& right) const;*/
+  void testAndNode() {
+    /*Node andNode(const Node& right) const;*/
     
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node eq = left.andExpr(right);
+    Node eq = left.andNode(right);
     
 
     TS_ASSERT(AND == eq.getKind());
@@ -304,12 +304,12 @@ public:
     
   }
 
-  void testOrExpr() {
-    /*Node orExpr(const Node& right) const;*/
+  void testOrNode() {
+    /*Node orNode(const Node& right) const;*/
      
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node eq = left.orExpr(right);
+    Node eq = left.orNode(right);
     
 
     TS_ASSERT(OR  == eq.getKind());
@@ -320,13 +320,13 @@ public:
 
   }
 
-  void testIteExpr() {
-    /*Node iteExpr(const Node& thenpart, const Node& elsepart) const;*/
+  void testIteNode() {
+    /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
 
     Node cnd = d_nm->mkNode(PLUS);
     Node thenBranch = d_nm->mkNode(TRUE);
     Node elseBranch = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node ite = cnd.iteExpr(thenBranch,elseBranch);
+    Node ite = cnd.iteNode(thenBranch,elseBranch);
     
 
     TS_ASSERT(ITE  == ite.getKind());
@@ -337,12 +337,12 @@ public:
     TS_ASSERT(*(++(++ite.begin())) == elseBranch);
   }
 
-  void testIffExpr() {
-    /*  Node iffExpr(const Node& right) const; */
+  void testIffNode() {
+    /*  Node iffNode(const Node& right) const; */
      
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node eq = left.iffExpr(right);
+    Node eq = left.iffNode(right);
     
 
     TS_ASSERT(IFF == eq.getKind());
@@ -353,11 +353,11 @@ public:
   }
 
   
-  void testImpExpr() {
-    /* Node impExpr(const Node& right) const; */
+  void testImpNode() {
+    /* Node impNode(const Node& right) const; */
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node eq = left.impExpr(right);
+    Node eq = left.impNode(right);
     
 
     TS_ASSERT(IMPLIES == eq.getKind());
@@ -367,11 +367,11 @@ public:
     TS_ASSERT(*(++eq.begin()) == right);
   }
 
-  void testXorExpr() {
-    /*Node xorExpr(const Node& right) const;*/
+  void testXorNode() {
+    /*Node xorNode(const Node& right) const;*/
     Node left = d_nm->mkNode(TRUE);
     Node right = d_nm->mkNode(NOT,(d_nm->mkNode(FALSE)));
-    Node eq = left.xorExpr(right);
+    Node eq = left.xorNode(right);
     
 
     TS_ASSERT(XOR == eq.getKind());
@@ -381,17 +381,17 @@ public:
     TS_ASSERT(*(++eq.begin()) == right);
   }
 
-  void testPlusExpr() {
-    /*Node plusExpr(const Node& right) const;*/
+  void testPlusNode() {
+    /*Node plusNode(const Node& right) const;*/
     TS_WARN( "TODO: No implementation to test." );
   }
 
-  void testUMinusExpr() {
-    /*Node uMinusExpr() const;*/
+  void testUMinusNode() {
+    /*Node uMinusNode() const;*/
     TS_WARN( "TODO: No implementation to test." );
   }
-  void testMultExpr() {
-    /*  Node multExpr(const Node& right) const;*/
+  void testMultNode() {
+    /*  Node multNode(const Node& right) const;*/
     TS_WARN( "TODO: No implementation to test." );    
   }
 
@@ -425,10 +425,10 @@ public:
     TS_ASSERT(0 == (Node::null()).getNumChildren());
 
     //test 1
-    TS_ASSERT(1 == (Node::null().notExpr()).getNumChildren());
+    TS_ASSERT(1 == (Node::null().notNode()).getNumChildren());
 
     //test 2
-    TS_ASSERT(2 == (Node::null().andExpr(Node::null())).getNumChildren() );
+    TS_ASSERT(2 == (Node::null().andNode(Node::null())).getNumChildren() );
 
     //Bigger tests
 
diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h
index 788c71d9b..1b57d01df 100644
--- a/test/unit/expr/node_white.h
+++ b/test/unit/expr/node_white.h
@@ -69,9 +69,9 @@ public:
 
   void testBuilder() {
     NodeBuilder<> b;
-    TS_ASSERT(b.d_ev->getId() == 0);
-    TS_ASSERT(b.d_ev->getKind() == UNDEFINED_KIND);
-    TS_ASSERT(b.d_ev->getNumChildren() == 0);
+    TS_ASSERT(b.d_nv->getId() == 0);
+    TS_ASSERT(b.d_nv->getKind() == UNDEFINED_KIND);
+    TS_ASSERT(b.d_nv->getNumChildren() == 0);
     /* etc. */
   }