killing expr into node...

36 files changed, 555 insertions, 558 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 630850387..6ca68d35c 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -7,13 +7,13 @@ noinst_LTLIBRARIES = libexpr.la
 libexpr_la_SOURCES = \
 	attr_type.h \
 	attr_var_name.h \
-	expr.h \
-	expr_builder.h \
+	node.h \
+	node_builder.h \
 	expr_value.h \
-	expr_manager.h \
-	expr_attribute.h \
+	node_manager.h \
+	node_attribute.h \
 	kind.h \
-	expr.cpp \
-	expr_builder.cpp \
-	expr_manager.cpp \
+	node.cpp \
+	node_builder.cpp \
+	node_manager.cpp \
 	expr_value.cpp
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index 9d410cea8..de0bad1bd 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -52,7 +52,7 @@ CONFIG_CLEAN_FILES =
 CONFIG_CLEAN_VPATH_FILES =
 LTLIBRARIES = $(noinst_LTLIBRARIES)
 libexpr_la_LIBADD =
-am_libexpr_la_OBJECTS = expr.lo expr_builder.lo expr_manager.lo \
+am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \
 	expr_value.lo
 libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
@@ -223,15 +223,15 @@ noinst_LTLIBRARIES = libexpr.la
 libexpr_la_SOURCES = \
 	attr_type.h \
 	attr_var_name.h \
-	expr.h \
-	expr_builder.h \
+	node.h \
+	node_builder.h \
 	expr_value.h \
-	expr_manager.h \
-	expr_attribute.h \
+	node_manager.h \
+	node_attribute.h \
 	kind.h \
-	expr.cpp \
-	expr_builder.cpp \
-	expr_manager.cpp \
+	node.cpp \
+	node_builder.cpp \
+	node_manager.cpp \
 	expr_value.cpp
 
 all: all-am
@@ -286,10 +286,10 @@ mostlyclean-compile:
 distclean-compile:
 	-rm -f *.tab.c
 
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_builder.Plo@am__quote@
-@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_manager.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index 1d5e8eb0c..2e0a8b675 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -24,7 +24,7 @@ class Type;
 class Type_attr {
 public:
   enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
-  typedef Type value_type;//Expr?
+  typedef Type value_type;//Node?
   static const Type_attr marker;
 };
 
diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h
index a0780d575..13a2ec36f 100644
--- a/src/expr/attr_var_name.h
+++ b/src/expr/attr_var_name.h
@@ -24,7 +24,7 @@ class VarName;
 class VarName_attr {
 public:
   enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles
-  typedef Type value_type;//Expr?
+  typedef Type value_type;//Node?
   static const Type_attr marker;
 };
 
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
deleted file mode 100644
index fa273dfa5..000000000
--- a/src/expr/expr.cpp
+++ /dev/null
@@ -1,115 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Reference-counted encapsulation of a pointer to an expression.
- **/
-
-#include "expr/expr.h"
-#include "expr_value.h"
-#include "expr_builder.h"
-#include "util/Assert.h"
-
-using namespace CVC4::expr;
-
-namespace CVC4 {
-
-ExprValue ExprValue::s_null;
-
-Expr Expr::s_null(&ExprValue::s_null);
-
-bool Expr::isNull() const {
-  return d_ev == &ExprValue::s_null;
-}
-
-Expr::Expr() :
-  d_ev(&ExprValue::s_null) {
-  // No refcount needed
-}
-
-Expr::Expr(ExprValue* ev)
-  : d_ev(ev) {
-  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
-  d_ev->inc();
-}
-
-Expr::Expr(const Expr& e) {
-  Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!");
-  d_ev = e.d_ev;
-  d_ev->inc();
-}
-
-Expr::~Expr() {
-  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
-  d_ev->dec();
-}
-
-void Expr::assignExprValue(ExprValue* ev) {
-  d_ev = ev;
-  d_ev->inc();
-}
-
-Expr& Expr::operator=(const Expr& e) {
-  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
-  if(this != &e && d_ev != e.d_ev) {
-    d_ev->dec();
-    d_ev = e.d_ev;
-    d_ev->inc();
-  }
-  return *this;
-}
-
-ExprValue const* Expr::operator->() const {
-  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
-  return d_ev;
-}
-
-uint64_t Expr::hash() const {
-  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
-  return d_ev->hash();
-}
-
-Expr Expr::eqExpr(const Expr& right) const {
-  return ExprManager::currentEM()->mkExpr(EQUAL, *this, right);
-}
-
-Expr Expr::notExpr() const {
-  return ExprManager::currentEM()->mkExpr(NOT, *this);
-}
-
-// FIXME: What does this do and why?
-Expr Expr::negate() const { // avoid double-negatives
-  return ExprBuilder(*this).negate();
-}
-
-
-Expr Expr::andExpr(const Expr& right) const {
-  return ExprManager::currentEM()->mkExpr(AND, *this, right);
-}
-
-Expr Expr::orExpr(const Expr& right) const {
-  return ExprManager::currentEM()->mkExpr(OR, *this, right);
-}
-
-Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
-  return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
-}
-
-Expr Expr::iffExpr(const Expr& right) const {
-  return ExprManager::currentEM()->mkExpr(IFF, *this, right);
-}
-
-Expr Expr::impExpr(const Expr& right) const {
-  return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right);
-}
-
-Expr Expr::xorExpr(const Expr& right) const {
-  return ExprManager::currentEM()->mkExpr(XOR, *this, right);
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
deleted file mode 100644
index 3b5347301..000000000
--- a/src/expr/expr_manager.cpp
+++ /dev/null
@@ -1,93 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr_manager.cpp
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Expression manager implementation.
- **/
-
-#include "expr_builder.h"
-#include "expr_manager.h"
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-__thread ExprManager* ExprManager::s_current = 0;
-
-Expr ExprManager::lookup(uint64_t hash, const Expr& e) {
-  Assert(this != NULL, "Woops, we have a bad expression manager!");
-  hash_t::iterator i = d_hash.find(hash);
-  if(i == d_hash.end()) {
-    // insert
-    std::vector<Expr> v;
-    v.push_back(e);
-    d_hash.insert(std::make_pair(hash, v));
-    return e;
-  } else {
-    for(std::vector<Expr>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
-      if(e.getKind() != j->getKind())
-        continue;
-
-      if(e.numChildren() != j->numChildren())
-        continue;
-
-      Expr::const_iterator c1 = e.begin();
-      Expr::iterator c2 = j->begin();
-      for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
-        if(c1->d_ev != c2->d_ev)
-          break;
-      }
-
-      if(c1 != e.end() || c2 != j->end())
-        continue;
-
-      return *j;
-    }
-    // didn't find it, insert
-    std::vector<Expr> v;
-    v.push_back(e);
-    d_hash.insert(std::make_pair(hash, v));
-    return e;
-  }
-}
-
-// general expression-builders
-
-Expr ExprManager::mkExpr(Kind kind) {
-  return ExprBuilder(this, kind);
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
-  return ExprBuilder(this, kind) << child1;
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
-  return ExprBuilder(this, kind) << child1 << child2;
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3) {
-  return ExprBuilder(this, kind) << child1 << child2 << child3;
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4) {
-  return ExprBuilder(this, kind) << child1 << child2 << child3 << child4;
-}
-
-Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) {
-  return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
-}
-
-// N-ary version
-Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
-  return ExprBuilder(this, kind).append(children);
-}
-
-Expr ExprManager::mkVar() {
-  return ExprBuilder(this, VARIABLE);
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index 17f3b64c3..9ce7c3e12 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -10,7 +10,7 @@
  ** An expression node.
  **
  ** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
  ** reference count on ExprValue instances and
  **/
 
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index b334e1c2d..10f09e565 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -10,13 +10,13 @@
  ** An expression node.
  **
  ** Instances of this class are generally referenced through
- ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
  ** reference count on ExprValue instances and
  **/
 
 /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */
 /* to resolve a circular dependency */
-#include "expr/expr.h"
+#include "expr/node.h"
 
 #ifndef __CVC4__EXPR__EXPR_VALUE_H
 #define __CVC4__EXPR__EXPR_VALUE_H
@@ -27,8 +27,8 @@
 
 namespace CVC4 {
 
-class Expr;
-class ExprBuilder;
+class Node;
+class NodeBuilder;
 
 namespace expr {
 
@@ -49,7 +49,7 @@ class ExprValue {
   /** The ID (0 is reserved for the null value) */
   unsigned d_id        : 32;
 
-  /** The expression's reference count.  @see cvc4::Expr. */
+  /** The expression's reference count.  @see cvc4::Node. */
   unsigned d_rc        :  8;
 
   /** Kind of the expression */
@@ -59,12 +59,12 @@ class ExprValue {
   unsigned d_nchildren : 16;
 
   /** Variable number of child nodes */
-  Expr     d_children[0];
+  Node     d_children[0];
 
   // todo add exprMgr ref in debug case
 
-  friend class CVC4::Expr;
-  friend class CVC4::ExprBuilder;
+  friend class CVC4::Node;
+  friend class CVC4::NodeBuilder;
 
   ExprValue* inc();
   ExprValue* dec();
@@ -76,7 +76,7 @@ class ExprValue {
 
   /**
    * Computes the hash over the given iterator span of children, and the
-   * root hash. The iterator should be either over a range of Expr or pointers
+   * root hash. The iterator should be either over a range of Node or pointers
    * to ExprValue.
    * @param hash the initial value for the hash
    * @param begin the begining of the range
@@ -97,8 +97,8 @@ public:
 
   // Iterator support
 
-  typedef Expr* iterator;
-  typedef Expr const* const_iterator;
+  typedef Node* iterator;
+  typedef Node const* const_iterator;
 
   iterator begin();
   iterator end();
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
new file mode 100644
index 000000000..22a905470
--- /dev/null
+++ b/src/expr/node.cpp
@@ -0,0 +1,115 @@
+/*********************                                           -*- C++ -*-  */
+/** expr.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#include "expr/node.h"
+#include "expr/expr_value.h"
+#include "expr/node_builder.h"
+#include "util/Assert.h"
+
+using namespace CVC4::expr;
+
+namespace CVC4 {
+
+ExprValue ExprValue::s_null;
+
+Node Node::s_null(&ExprValue::s_null);
+
+bool Node::isNull() const {
+  return d_ev == &ExprValue::s_null;
+}
+
+Node::Node() :
+  d_ev(&ExprValue::s_null) {
+  // No refcount needed
+}
+
+Node::Node(ExprValue* ev)
+  : d_ev(ev) {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  d_ev->inc();
+}
+
+Node::Node(const Node& e) {
+  Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!");
+  d_ev = e.d_ev;
+  d_ev->inc();
+}
+
+Node::~Node() {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  d_ev->dec();
+}
+
+void Node::assignExprValue(ExprValue* ev) {
+  d_ev = ev;
+  d_ev->inc();
+}
+
+Node& Node::operator=(const Node& e) {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  if(this != &e && d_ev != e.d_ev) {
+    d_ev->dec();
+    d_ev = e.d_ev;
+    d_ev->inc();
+  }
+  return *this;
+}
+
+ExprValue const* Node::operator->() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  return d_ev;
+}
+
+uint64_t Node::hash() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
+  return d_ev->hash();
+}
+
+Node Node::eqExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
+}
+
+Node Node::notExpr() const {
+  return NodeManager::currentEM()->mkExpr(NOT, *this);
+}
+
+// FIXME: What does this do and why?
+Node Node::negate() const { // avoid double-negatives
+  return NodeBuilder(*this).negate();
+}
+
+
+Node Node::andExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(AND, *this, right);
+}
+
+Node Node::orExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(OR, *this, right);
+}
+
+Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
+  return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
+}
+
+Node Node::iffExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(IFF, *this, right);
+}
+
+Node Node::impExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
+}
+
+Node Node::xorExpr(const Node& right) const {
+  return NodeManager::currentEM()->mkExpr(XOR, *this, right);
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/expr.h b/src/expr/node.h
index 7440974d8..aec50000e 100644
--- a/src/expr/expr.h
+++ b/src/expr/node.h
@@ -21,14 +21,14 @@
 #include "expr/kind.h"
 
 namespace CVC4 {
-  class Expr;
+  class Node;
 }/* CVC4 namespace */
 
 namespace CVC4 {
 
-inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC;
 
-class ExprManager;
+class NodeManager;
 
 namespace expr {
   class ExprValue;
@@ -40,25 +40,25 @@ using CVC4::expr::ExprValue;
  * Encapsulation of an ExprValue pointer.  The reference count is
  * maintained in the ExprValue.
  */
-class CVC4_PUBLIC Expr {
+class CVC4_PUBLIC Node {
 
   friend class ExprValue;
 
   /** A convenient null-valued encapsulated pointer */
-  static Expr s_null;
+  static Node s_null;
 
   /** The referenced ExprValue */
   ExprValue* d_ev;
 
-  /** This constructor is reserved for use by the Expr package; one
-   *  must construct an Expr using one of the build mechanisms of the
-   *  Expr package.
+  /** 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. */
-  explicit Expr(ExprValue*);
+  explicit Node(ExprValue*);
 
-  friend class ExprBuilder;
-  friend class ExprManager;
+  friend class NodeBuilder;
+  friend class NodeManager;
 
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
@@ -76,49 +76,49 @@ class CVC4_PUBLIC Expr {
 public:
 
   /** Default constructor, makes a null expression. */
-  Expr();
+  Node();
 
-  Expr(const Expr&);
+  Node(const Node&);
 
   /** Destructor.  Decrements the reference count and, if zero,
    *  collects the ExprValue. */
-  ~Expr();
+  ~Node();
 
-  bool operator==(const Expr& e) const { return d_ev == e.d_ev; }
-  bool operator!=(const Expr& e) const { return d_ev != e.d_ev; }
+  bool operator==(const Node& e) const { return d_ev == e.d_ev; }
+  bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
 
   /**
    * 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 Expr& e) const;
+  inline bool operator<(const Node& e) const;
 
-  Expr& operator=(const Expr&);
+  Node& operator=(const Node&);
 
   uint64_t hash() const;
 
-  Expr eqExpr(const Expr& right) const;
-  Expr notExpr() const;
-  Expr negate() const; // avoid double-negatives
-  Expr andExpr(const Expr& right) const;
-  Expr orExpr(const Expr& right) const;
-  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
-  Expr iffExpr(const Expr& right) const;
-  Expr impExpr(const Expr& right) const;
-  Expr xorExpr(const Expr& right) const;
+  Node eqExpr(const Node& right) const;
+  Node notExpr() const;
+  Node negate() const; // avoid double-negatives
+  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;
 
-  Expr plusExpr(const Expr& right) const;
-  Expr uMinusExpr() const;
-  Expr multExpr(const Expr& right) const;
+  Node plusExpr(const Node& right) const;
+  Node uMinusExpr() const;
+  Node multExpr(const Node& right) const;
 
   inline Kind getKind() const;
 
   inline size_t numChildren() const;
 
-  static Expr null() { return s_null; }
+  static Node null() { return s_null; }
 
-  typedef Expr* iterator;
-  typedef Expr const* const_iterator;
+  typedef Node* iterator;
+  typedef Node const* const_iterator;
 
   inline iterator begin();
   inline iterator end();
@@ -129,7 +129,7 @@ public:
 
   bool isNull() const;
 
-};/* class Expr */
+};/* class Node */
 
 }/* CVC4 namespace */
 
@@ -137,42 +137,42 @@ public:
 
 namespace CVC4 {
 
-inline bool Expr::operator<(const Expr& e) const {
+inline bool Node::operator<(const Node& e) const {
   return d_ev->d_id < e.d_ev->d_id;
 }
 
-inline std::ostream& operator<<(std::ostream& out, const Expr& e) {
+inline std::ostream& operator<<(std::ostream& out, const Node& e) {
   e.toString(out);
   return out;
 }
 
-inline Kind Expr::getKind() const {
+inline Kind Node::getKind() const {
   return Kind(d_ev->d_kind);
 }
 
-inline void Expr::toString(std::ostream& out) const {
+inline void Node::toString(std::ostream& out) const {
   if(d_ev)
     d_ev->toString(out);
   else out << "null";
 }
 
-inline Expr::iterator Expr::begin() {
+inline Node::iterator Node::begin() {
   return d_ev->begin();
 }
 
-inline Expr::iterator Expr::end() {
+inline Node::iterator Node::end() {
   return d_ev->end();
 }
 
-inline Expr::const_iterator Expr::begin() const {
+inline Node::const_iterator Node::begin() const {
   return d_ev->begin();
 }
 
-inline Expr::const_iterator Expr::end() const {
+inline Node::const_iterator Node::end() const {
   return d_ev->end();
 }
 
-inline size_t Expr::numChildren() const {
+inline size_t Node::numChildren() const {
   return d_ev->d_nchildren;
 }
 
diff --git a/src/expr/expr_attribute.h b/src/expr/node_attribute.h
index b68a9d19d..b978f097d 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/node_attribute.h
@@ -15,7 +15,7 @@
 #include <stdint.h>
 #include "config.h"
 #include "context/context.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace expr {
@@ -26,7 +26,7 @@ class AttrTables;
 // global (or TSS)
 extern CDMap<uint64_t> g_hash_bool;
 extern CDMap<uint64_t> g_hash_int;
-extern CDMap<Expr>     g_hash_expr;
+extern CDMap<Node>     g_hash_expr;
 extern CDMap<void*>    g_hash_ptr;
 
 template <class T>
@@ -47,10 +47,10 @@ public:
   static CDMap<uint64_t> *s_hash;
 
   template <class Attr>
-  BitAccessor& find(Expr e, const Attr&);
+  BitAccessor& find(Node e, const Attr&);
 
   template <class Attr>
-  bool find(Expr e, const Attr&) const;
+  bool find(Node e, const Attr&) const;
 };
 
 template <>
@@ -58,8 +58,8 @@ class AttrTable<uint64_t> {
 public:  
   // int(egral) specialization
   static CDMap<uint64_t> *s_hash;
-  uint64_t& find(Expr);
-  uint64_t& find(Expr) const;
+  uint64_t& find(Node);
+  uint64_t& find(Node) const;
 };
 
 template <class T>
@@ -70,16 +70,16 @@ public:
 };
 
 template <>
-class AttrTable<Expr> {
+class AttrTable<Node> {
 public:
-  // Expr specialization
-  static CDMap<Expr> *s_hash;
-  Expr find(Expr);
+  // Node specialization
+  static CDMap<Node> *s_hash;
+  Node find(Node);
 };
 
 CDMap<uint64_t>* AttrTable<bool>::s_hash     = &g_hash_bool;
 CDMap<uint64_t>* AttrTable<uint64_t>::s_hash = &g_hash_int;
-CDMap<Expr>*     AttrTable<Expr>::s_hash     = &g_hash_expr;
+CDMap<Node>*     AttrTable<Node>::s_hash     = &g_hash_expr;
 
 template <class T>
 CDMap<void*>*    AttrTable<T*>::s_hash       = &g_hash_ptr;
diff --git a/src/expr/expr_builder.cpp b/src/expr/node_builder.cpp
index 10152a338..83d2ae41d 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -9,46 +9,46 @@
  **
  **/
 
-#include "expr_builder.h"
-#include "expr_manager.h"
-#include "expr_value.h"
+#include "expr/node_builder.h"
+#include "expr/node_manager.h"
+#include "expr/expr_value.h"
 #include "util/output.h"
 
 using namespace std;
 
 namespace CVC4 {
 
-ExprBuilder::ExprBuilder() :
-  d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false),
+NodeBuilder::NodeBuilder() :
+  d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false),
       d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(Kind k) :
-  d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {
+NodeBuilder::NodeBuilder(Kind k) :
+  d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(const Expr& e) :
-  d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+NodeBuilder::NodeBuilder(const Node& e) :
+  d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
   d_children.u_arr[0] = e.d_ev->inc();;
 }
 
-ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
-  this->~ExprBuilder();
+NodeBuilder& NodeBuilder::reset(const ExprValue* ev) {
+  this->~NodeBuilder();
   d_kind = Kind(ev->d_kind);
   d_used = false;
   d_nchildren = ev->d_nchildren;
-  for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i)
+  for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i)
     addChild(i->d_ev);
   return *this;
 }
 
-ExprBuilder::ExprBuilder(const ExprBuilder& eb) :
+NodeBuilder::NodeBuilder(const NodeBuilder& eb) :
   d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used),
       d_nchildren(eb.d_nchildren) {
   Assert( !d_used );
 
   if(d_nchildren > nchild_thresh) {
-    d_children.u_vec = new vector<Expr> ();
+    d_children.u_vec = new vector<Node> ();
     d_children.u_vec->reserve(d_nchildren + 5);
     copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(),
          back_inserter(*d_children.u_vec));
@@ -61,20 +61,20 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) :
   }
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em) :
+NodeBuilder::NodeBuilder(NodeManager* em) :
   d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em, Kind k) :
+NodeBuilder::NodeBuilder(NodeManager* em, Kind k) :
   d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) :
+NodeBuilder::NodeBuilder(NodeManager* em, const Node& e) :
   d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
   d_children.u_arr[0] = e.d_ev->inc();
 }
 
-ExprBuilder::~ExprBuilder() {
+NodeBuilder::~NodeBuilder() {
   if(d_nchildren > nchild_thresh) {
     delete d_children.u_vec;
   } else {
@@ -87,7 +87,7 @@ ExprBuilder::~ExprBuilder() {
 }
 
 // Compound expression constructors
-ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
+NodeBuilder& NodeBuilder::eqExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   if(EXPECT_TRUE( d_kind != EQUAL )) {
     collapse();
@@ -97,7 +97,7 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::notExpr() {
+NodeBuilder& NodeBuilder::notExpr() {
   Assert( d_kind != UNDEFINED_KIND );
   collapse();
   d_kind = NOT;
@@ -105,7 +105,7 @@ ExprBuilder& ExprBuilder::notExpr() {
 }
 
 // avoid double-negatives
-ExprBuilder& ExprBuilder::negate() {
+NodeBuilder& NodeBuilder::negate() {
   if(EXPECT_FALSE( d_kind == NOT ))
     return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND );
   collapse();
@@ -113,7 +113,7 @@ ExprBuilder& ExprBuilder::negate() {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
+NodeBuilder& NodeBuilder::andExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   if(d_kind != AND) {
     collapse();
@@ -123,7 +123,7 @@ ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
+NodeBuilder& NodeBuilder::orExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   if(EXPECT_TRUE( d_kind != OR )) {
     collapse();
@@ -133,7 +133,7 @@ ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
+NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) {
   Assert( d_kind != UNDEFINED_KIND );
   collapse();
   d_kind = ITE;
@@ -142,7 +142,7 @@ ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
+NodeBuilder& NodeBuilder::iffExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   if(EXPECT_TRUE( d_kind != IFF )) {
     collapse();
@@ -152,7 +152,7 @@ ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
+NodeBuilder& NodeBuilder::impExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   collapse();
   d_kind = IMPLIES;
@@ -160,7 +160,7 @@ ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
+NodeBuilder& NodeBuilder::xorExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   if(EXPECT_TRUE( d_kind != XOR )) {
     collapse();
@@ -171,12 +171,12 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
 }
 
 // "Stream" expression constructor syntax
-ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+NodeBuilder& NodeBuilder::operator<<(const Kind& op) {
   d_kind = op;
   return *this;
 }
 
-ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+NodeBuilder& NodeBuilder::operator<<(const Node& child) {
   addChild(child);
   return *this;
 }
@@ -190,28 +190,28 @@ ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
  *     reference count for each child.
  * (c) Otherwise we just add to the end of the vector.
  */
-void ExprBuilder::addChild(ExprValue* ev) {
+void NodeBuilder::addChild(ExprValue* ev) {
   Assert(d_nchildren <= nchild_thresh ||
          d_nchildren == d_children.u_vec->size(),
          "children count doesn't reflect the size of the vector!");
   Debug("expr") << "adding child ev " << ev << endl;
   if(d_nchildren == nchild_thresh) {
     Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
-    vector<Expr>* v = new vector<Expr> ();
+    vector<Node>* v = new vector<Node> ();
     v->reserve(nchild_thresh + 5);
     ExprValue** i = d_children.u_arr;
     ExprValue** i_end = i + nchild_thresh;
     for(;i != i_end; ++ i) {
-      v->push_back(Expr(*i));
+      v->push_back(Node(*i));
       (*i)->dec();
     }
-    v->push_back(Expr(ev));
+    v->push_back(Node(ev));
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
     Debug("expr") << "over thresh " << d_nchildren
                   << " > " << nchild_thresh << endl;
-    d_children.u_vec->push_back(Expr(ev));
+    d_children.u_vec->push_back(Node(ev));
     // ++d_nchildren; no need for this
   } else {
     Debug("expr") << "under thresh " << d_nchildren
@@ -220,9 +220,9 @@ void ExprBuilder::addChild(ExprValue* ev) {
   }
 }
 
-ExprBuilder& ExprBuilder::collapse() {
+NodeBuilder& NodeBuilder::collapse() {
   if(d_nchildren == nchild_thresh) {
-    vector<Expr>* v = new vector<Expr> ();
+    vector<Node>* v = new vector<Node> ();
     v->reserve(nchild_thresh + 5);
     //
     Unreachable();// unimplemented
diff --git a/src/expr/expr_builder.h b/src/expr/node_builder.h
index 34e34bf6e..be96c2e77 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/node_builder.h
@@ -15,8 +15,8 @@
 #include <vector>
 #include <cstdlib>
 
-#include "expr_manager.h"
-#include "kind.h"
+#include "expr/node_manager.h"
+#include "expr/kind.h"
 #include "util/Assert.h"
 
 namespace CVC4 {
@@ -27,12 +27,12 @@ class PlusExprBuilder;
 class MinusExprBuilder;
 class MultExprBuilder;
 
-class ExprBuilder {
-  ExprManager* d_em;
+class NodeBuilder {
+  NodeManager* d_em;
 
   Kind d_kind;
 
-  // initially false, when you extract the Expr this is set and you can't
+  // initially false, when you extract the Node this is set and you can't
   // extract another
   bool d_used;
 
@@ -41,12 +41,12 @@ class ExprBuilder {
   unsigned d_nchildren;
   union {
     ExprValue*         u_arr[nchild_thresh];
-    std::vector<Expr>* u_vec;
+    std::vector<Node>* u_vec;
   } d_children;
 
-  void addChild(const Expr& e) { addChild(e.d_ev); }
+  void addChild(const Node& e) { addChild(e.d_ev); }
   void addChild(ExprValue*);
-  ExprBuilder& collapse();
+  NodeBuilder& collapse();
 
   typedef ExprValue** ev_iterator;
   typedef ExprValue const** const_ev_iterator;
@@ -59,148 +59,148 @@ class ExprBuilder {
     return d_children.u_arr + d_nchildren;
   }
 
-  ExprBuilder& reset(const ExprValue*);
+  NodeBuilder& reset(const ExprValue*);
 
 public:
 
-  ExprBuilder();
-  ExprBuilder(Kind k);
-  ExprBuilder(const Expr&);
-  ExprBuilder(const ExprBuilder&);
+  NodeBuilder();
+  NodeBuilder(Kind k);
+  NodeBuilder(const Node&);
+  NodeBuilder(const NodeBuilder&);
 
-  ExprBuilder(ExprManager*);
-  ExprBuilder(ExprManager*, Kind k);
-  ExprBuilder(ExprManager*, const Expr&);
-  ExprBuilder(ExprManager*, const ExprBuilder&);
+  NodeBuilder(NodeManager*);
+  NodeBuilder(NodeManager*, Kind k);
+  NodeBuilder(NodeManager*, const Node&);
+  NodeBuilder(NodeManager*, const NodeBuilder&);
 
-  ~ExprBuilder();
+  ~NodeBuilder();
 
   // Compound expression constructors
-  ExprBuilder& eqExpr(const Expr& right);
-  ExprBuilder& notExpr();
-  ExprBuilder& negate(); // avoid double-negatives
-  ExprBuilder& andExpr(const Expr& right);
-  ExprBuilder& orExpr(const Expr& right);
-  ExprBuilder& iteExpr(const Expr& thenpart, const Expr& elsepart);
-  ExprBuilder& iffExpr(const Expr& right);
-  ExprBuilder& impExpr(const Expr& right);
-  ExprBuilder& xorExpr(const Expr& right);
-
-  /* TODO design: these modify ExprBuilder */
-  ExprBuilder& operator!() { return notExpr(); }
-  ExprBuilder& operator&&(const Expr& right) { return andExpr(right); }
-  ExprBuilder& operator||(const Expr& right) { return orExpr(right);  }
+  NodeBuilder& eqExpr(const Node& right);
+  NodeBuilder& notExpr();
+  NodeBuilder& negate(); // avoid double-negatives
+  NodeBuilder& andExpr(const Node& right);
+  NodeBuilder& orExpr(const Node& right);
+  NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart);
+  NodeBuilder& iffExpr(const Node& right);
+  NodeBuilder& impExpr(const Node& right);
+  NodeBuilder& xorExpr(const Node& right);
+
+  /* TODO design: these modify NodeBuilder */
+  NodeBuilder& operator!() { return notExpr(); }
+  NodeBuilder& operator&&(const Node& right) { return andExpr(right); }
+  NodeBuilder& operator||(const Node& right) { return orExpr(right);  }
 
   // "Stream" expression constructor syntax
-  ExprBuilder& operator<<(const Kind& op);
-  ExprBuilder& operator<<(const Expr& child);
+  NodeBuilder& operator<<(const Kind& op);
+  NodeBuilder& operator<<(const Node& child);
 
   // For pushing sequences of children
-  ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
-  ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); }
-  template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
+  NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); }
+  NodeBuilder& append(Node child) { return append(&child, (&child) + 1); }
+  template <class Iterator> NodeBuilder& append(const Iterator& begin, const Iterator& end);
 
-  operator Expr();// not const
+  operator Node();// not const
 
-  AndExprBuilder   operator&&(Expr);
-  OrExprBuilder    operator||(Expr);
-  PlusExprBuilder  operator+ (Expr);
-  PlusExprBuilder  operator- (Expr);
-  MultExprBuilder  operator* (Expr);
+  AndExprBuilder   operator&&(Node);
+  OrExprBuilder    operator||(Node);
+  PlusExprBuilder  operator+ (Node);
+  PlusExprBuilder  operator- (Node);
+  MultExprBuilder  operator* (Node);
 
   friend class AndExprBuilder;
   friend class OrExprBuilder;
   friend class PlusExprBuilder;
   friend class MultExprBuilder;
-};/* class ExprBuilder */
+};/* class NodeBuilder */
 
 class AndExprBuilder {
-  ExprBuilder d_eb;
+  NodeBuilder d_eb;
 
 public:
 
-  AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+  AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != AND) {
       d_eb.collapse();
       d_eb.d_kind = AND;
     }
   }
 
-  AndExprBuilder&   operator&&(Expr);
-  OrExprBuilder     operator||(Expr);
+  AndExprBuilder&   operator&&(Node);
+  OrExprBuilder     operator||(Node);
 
-  operator ExprBuilder() { return d_eb; }
+  operator NodeBuilder() { return d_eb; }
 
 };/* class AndExprBuilder */
 
 class OrExprBuilder {
-  ExprBuilder d_eb;
+  NodeBuilder d_eb;
 
 public:
 
-  OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+  OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != OR) {
       d_eb.collapse();
       d_eb.d_kind = OR;
     }
   }
 
-  AndExprBuilder    operator&&(Expr);
-  OrExprBuilder&    operator||(Expr);
+  AndExprBuilder    operator&&(Node);
+  OrExprBuilder&    operator||(Node);
 
-  operator ExprBuilder() { return d_eb; }
+  operator NodeBuilder() { return d_eb; }
 
 };/* class OrExprBuilder */
 
 class PlusExprBuilder {
-  ExprBuilder d_eb;
+  NodeBuilder d_eb;
 
 public:
 
-  PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+  PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != PLUS) {
       d_eb.collapse();
       d_eb.d_kind = PLUS;
     }
   }
 
-  PlusExprBuilder&  operator+(Expr);
-  PlusExprBuilder&  operator-(Expr);
-  MultExprBuilder   operator*(Expr);
+  PlusExprBuilder&  operator+(Node);
+  PlusExprBuilder&  operator-(Node);
+  MultExprBuilder   operator*(Node);
 
-  operator ExprBuilder() { return d_eb; }
+  operator NodeBuilder() { return d_eb; }
 
 };/* class PlusExprBuilder */
 
 class MultExprBuilder {
-  ExprBuilder d_eb;
+  NodeBuilder d_eb;
 
 public:
 
-  MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+  MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != MULT) {
       d_eb.collapse();
       d_eb.d_kind = MULT;
     }
   }
 
-  PlusExprBuilder   operator+(Expr);
-  PlusExprBuilder   operator-(Expr);
-  MultExprBuilder&  operator*(Expr);
+  PlusExprBuilder   operator+(Node);
+  PlusExprBuilder   operator-(Node);
+  MultExprBuilder&  operator*(Node);
 
-  operator ExprBuilder() { return d_eb; }
+  operator NodeBuilder() { return d_eb; }
 
 };/* class MultExprBuilder */
 
 template <class Iterator>
-inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) {
   for(Iterator i = begin; i != end; ++i)
     addChild(*i);
   return *this;
 }
 
 // not const
-inline ExprBuilder::operator Expr() {
+inline NodeBuilder::operator Node() {
   ExprValue *ev;
   uint64_t hash;
 
@@ -213,7 +213,7 @@ inline ExprBuilder::operator Expr() {
   } else {
     if(d_nchildren <= nchild_thresh) {
       hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end());
-      void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
+      void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node));
       ev = new (space) ExprValue;
       size_t nc = 0;
       ev_iterator i = ev_begin();
@@ -224,12 +224,12 @@ inline ExprBuilder::operator Expr() {
         ev->d_children[nc++].assignExprValue(*i);
       }
     } else {
-      hash = ExprValue::computeHash<std::vector<Expr>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end());
-      void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
+      hash = ExprValue::computeHash<std::vector<Node>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end());
+      void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node));
       ev = new (space) ExprValue;
       size_t nc = 0;
-      for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
-        ev->d_children[nc++] = Expr(*i);
+      for(std::vector<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
+        ev->d_children[nc++] = Node(*i);
     }
   }
 
@@ -237,72 +237,72 @@ inline ExprBuilder::operator Expr() {
   ev->d_kind = d_kind;
   ev->d_id = ExprValue::next_id++;// FIXME multithreading
   ev->d_rc = 0;
-  Expr e(ev);
+  Node e(ev);
 
   return d_em->lookup(hash, e);
 }
 
-inline AndExprBuilder   ExprBuilder::operator&&(Expr e) {
+inline AndExprBuilder   NodeBuilder::operator&&(Node e) {
   return AndExprBuilder(*this) && e;
 }
 
-inline OrExprBuilder    ExprBuilder::operator||(Expr e) {
+inline OrExprBuilder    NodeBuilder::operator||(Node e) {
   return OrExprBuilder(*this) || e;
 }
 
-inline PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
+inline PlusExprBuilder  NodeBuilder::operator+ (Node e) {
   return PlusExprBuilder(*this) + e;
 }
 
-inline PlusExprBuilder  ExprBuilder::operator- (Expr e) {
+inline PlusExprBuilder  NodeBuilder::operator- (Node e) {
   return PlusExprBuilder(*this) - e;
 }
 
-inline MultExprBuilder  ExprBuilder::operator* (Expr e) {
+inline MultExprBuilder  NodeBuilder::operator* (Node e) {
   return MultExprBuilder(*this) * e;
 }
 
-inline AndExprBuilder&  AndExprBuilder::operator&&(Expr e) {
+inline AndExprBuilder&  AndExprBuilder::operator&&(Node e) {
   d_eb.append(e);
   return *this;
 }
 
-inline OrExprBuilder    AndExprBuilder::operator||(Expr e) {
+inline OrExprBuilder    AndExprBuilder::operator||(Node e) {
   return OrExprBuilder(d_eb.collapse()) || e;
 }
 
-inline AndExprBuilder   OrExprBuilder::operator&&(Expr e) {
+inline AndExprBuilder   OrExprBuilder::operator&&(Node e) {
   return AndExprBuilder(d_eb.collapse()) && e;
 }
 
-inline OrExprBuilder&   OrExprBuilder::operator||(Expr e) {
+inline OrExprBuilder&   OrExprBuilder::operator||(Node e) {
   d_eb.append(e);
   return *this;
 }
 
-inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) {
+inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) {
   d_eb.append(e);
   return *this;
 }
 
-inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) {
+inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) {
   d_eb.append(e.negate());
   return *this;
 }
 
-inline MultExprBuilder  PlusExprBuilder::operator*(Expr e) {
+inline MultExprBuilder  PlusExprBuilder::operator*(Node e) {
   return MultExprBuilder(d_eb.collapse()) * e;
 }
 
-inline PlusExprBuilder  MultExprBuilder::operator+(Expr e) {
+inline PlusExprBuilder  MultExprBuilder::operator+(Node e) {
   return MultExprBuilder(d_eb.collapse()) + e;
 }
 
-inline PlusExprBuilder  MultExprBuilder::operator-(Expr e) {
+inline PlusExprBuilder  MultExprBuilder::operator-(Node e) {
   return MultExprBuilder(d_eb.collapse()) - e;
 }
 
-inline MultExprBuilder& MultExprBuilder::operator*(Expr e) {
+inline MultExprBuilder& MultExprBuilder::operator*(Node e) {
   d_eb.append(e);
   return *this;
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
new file mode 100644
index 000000000..3c15aa9c4
--- /dev/null
+++ b/src/expr/node_manager.cpp
@@ -0,0 +1,93 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Expression manager implementation.
+ **/
+
+#include "node_builder.h"
+#include "node_manager.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+
+__thread NodeManager* NodeManager::s_current = 0;
+
+Node NodeManager::lookup(uint64_t hash, const Node& e) {
+  Assert(this != NULL, "Woops, we have a bad expression manager!");
+  hash_t::iterator i = d_hash.find(hash);
+  if(i == d_hash.end()) {
+    // insert
+    std::vector<Node> v;
+    v.push_back(e);
+    d_hash.insert(std::make_pair(hash, v));
+    return e;
+  } else {
+    for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
+      if(e.getKind() != j->getKind())
+        continue;
+
+      if(e.numChildren() != j->numChildren())
+        continue;
+
+      Node::const_iterator c1 = e.begin();
+      Node::iterator c2 = j->begin();
+      for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
+        if(c1->d_ev != c2->d_ev)
+          break;
+      }
+
+      if(c1 != e.end() || c2 != j->end())
+        continue;
+
+      return *j;
+    }
+    // didn't find it, insert
+    std::vector<Node> v;
+    v.push_back(e);
+    d_hash.insert(std::make_pair(hash, v));
+    return e;
+  }
+}
+
+// general expression-builders
+
+Node NodeManager::mkExpr(Kind kind) {
+  return NodeBuilder(this, kind);
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1) {
+  return NodeBuilder(this, kind) << child1;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
+  return NodeBuilder(this, kind) << child1 << child2;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
+  return NodeBuilder(this, kind) << child1 << child2 << child3;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
+  return NodeBuilder(this, kind) << child1 << child2 << child3 << child4;
+}
+
+Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
+  return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+Node NodeManager::mkExpr(Kind kind, std::vector<Node> children) {
+  return NodeBuilder(this, kind).append(children);
+}
+
+Node NodeManager::mkVar() {
+  return NodeBuilder(this, VARIABLE);
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/node_manager.h
index 542d1040d..ca15d88b4 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/node_manager.h
@@ -15,7 +15,7 @@
 #include <vector>
 #include <map>
 
-#include "expr/expr.h"
+#include "node.h"
 #include "kind.h"
 
 namespace CVC4 {
@@ -24,45 +24,45 @@ namespace expr {
   class ExprBuilder;
 }/* CVC4::expr namespace */
 
-class CVC4_PUBLIC ExprManager {
-  static __thread ExprManager* s_current;
+class CVC4_PUBLIC NodeManager {
+  static __thread NodeManager* s_current;
 
-  friend class CVC4::ExprBuilder;
+  friend class CVC4::NodeBuilder;
 
-  typedef std::map<uint64_t, std::vector<Expr> > hash_t;
+  typedef std::map<uint64_t, std::vector<Node> > hash_t;
   hash_t d_hash;
 
-  Expr lookup(uint64_t hash, const Expr& e);
+  Node lookup(uint64_t hash, const Node& e);
 
 public:
-  static ExprManager* currentEM() { return s_current; }
+  static NodeManager* currentEM() { return s_current; }
 
   // general expression-builders
-  Expr mkExpr(Kind kind);
-  Expr mkExpr(Kind kind, const Expr& child1);
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3);
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4);
-  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5);
+  Node mkExpr(Kind kind);
+  Node mkExpr(Kind kind, const Node& child1);
+  Node mkExpr(Kind kind, const Node& child1, const Node& child2);
+  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3);
+  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
+  Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
   // N-ary version
-  Expr mkExpr(Kind kind, std::vector<Expr> children);
+  Node mkExpr(Kind kind, std::vector<Node> children);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar();
+  Node mkVar();
 
   // TODO: these use the current EM (but must be renamed)
   /*
-  static Expr mkExpr(Kind kind)
+  static Node mkExpr(Kind kind)
   { currentEM()->mkExpr(kind); }
-  static Expr mkExpr(Kind kind, Expr child1);
+  static Node mkExpr(Kind kind, Node child1);
   { currentEM()->mkExpr(kind, child1); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2);
+  static Node mkExpr(Kind kind, Node child1, Node child2);
   { currentEM()->mkExpr(kind, child1, child2); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
+  static Node mkExpr(Kind kind, Node child1, Node child2, Node child3);
   { currentEM()->mkExpr(kind, child1, child2, child3); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
+  static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4);
   { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+  static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5);
   { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
   */
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index d9d3988f1..c7e23aee2 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -22,7 +22,7 @@
 #include "parser/parser.h"
 #include "parser/smt/smt_parser.h"
 #include "parser/cvc/cvc_parser.h"
-#include "expr/expr_manager.h"
+#include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "util/command.h"
 #include "util/output.h"
@@ -53,7 +53,7 @@ int main(int argc, char *argv[]) {
       throw new Exception("Too many input files specified.");
 
     // Create the expression manager
-    ExprManager exprMgr;
+    NodeManager exprMgr;
 
     // Create the SmtEngine
     SmtEngine smt(&exprMgr, &options);
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 04a82f721..d81336b53 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -8,7 +8,6 @@
 #include <iostream>
 
 #include "antlr_parser.h"
-#include "expr/expr_manager.h"
 #include "util/output.h"
 
 using namespace std;
@@ -66,29 +65,29 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
   antlr::LLkParser(lexer, k) {
 }
 
-Expr AntlrParser::getVariable(std::string var_name) {
-  Expr e = d_var_symbol_table.getObject(var_name);
+Node AntlrParser::getVariable(std::string var_name) {
+  Node e = d_var_symbol_table.getObject(var_name);
   Debug("parser") << "getvar " << var_name << " gives " << e << endl;
   return e;
 }
 
-Expr AntlrParser::getTrueExpr() const {
+Node AntlrParser::getTrueExpr() const {
   return d_expr_manager->mkExpr(TRUE);
 }
 
-Expr AntlrParser::getFalseExpr() const {
+Node AntlrParser::getFalseExpr() const {
   return d_expr_manager->mkExpr(FALSE);
 }
 
-Expr AntlrParser::newExpression(Kind kind, const Expr& child) {
+Node AntlrParser::newExpression(Kind kind, const Node& child) {
   return d_expr_manager->mkExpr(kind, child);
 }
 
-Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) {
+Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) {
   return d_expr_manager->mkExpr(kind, child_1, child_2);
 }
 
-Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
+Node AntlrParser::newExpression(Kind kind, const std::vector<Node>& children) {
   return d_expr_manager->mkExpr(kind, children);
 }
 
@@ -113,7 +112,7 @@ void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) {
 void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) {
 }
 
-void AntlrParser::setExpressionManager(ExprManager* em) {
+void AntlrParser::setExpressionManager(NodeManager* em) {
   d_expr_manager = em;
 }
 
@@ -133,7 +132,7 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
                                  LT(0).get()->getColumn());
 }
 
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
+Node AntlrParser::createPrecedenceExpr(const vector<Node>& exprs, const vector<
     Kind>& kinds) {
   return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
 }
@@ -155,7 +154,7 @@ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds,
   return pivot;
 }
 
-Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
+Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs,
                                        const std::vector<Kind>& kinds,
                                        unsigned start_index, unsigned end_index) {
   if(start_index == end_index)
@@ -163,8 +162,8 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
 
   unsigned pivot = findPivot(kinds, start_index, end_index - 1);
 
-  Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
-  Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
+  Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
+  Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
   return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
 }
 
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index ad23d45f8..26f206e43 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -15,8 +15,8 @@
 #include <antlr/LLkParser.hpp>
 #include <antlr/SemanticException.hpp>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
 #include "util/command.h"
 #include "util/Assert.h"
 #include "parser/symbol_table.h"
@@ -48,7 +48,7 @@ public:
    * Set's the expression manager to use when creating/managing expression.
    * @param expr_manager the expression manager
    */
-  void setExpressionManager(ExprManager* expr_manager);
+  void setExpressionManager(NodeManager* expr_manager);
 
 protected:
 
@@ -89,7 +89,7 @@ protected:
    * @param var_name the name of the variable
    * @return the variable expression
    */
-  Expr getVariable(std::string var_name);
+  Node getVariable(std::string var_name);
 
   /**
    * Types of symbols.
@@ -113,40 +113,40 @@ protected:
    * Returns the true expression.
    * @return the true expression
    */
-  Expr getTrueExpr() const;
+  Node getTrueExpr() const;
 
   /**
    * Returns the false expression.
    * @return the false expression
    */
-  Expr getFalseExpr() const;
+  Node getFalseExpr() const;
 
   /**
    * Creates a new unary CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param child the child
    */
-  Expr newExpression(Kind kind, const Expr& child);
+  Node newExpression(Kind kind, const Node& child);
 
   /**
    * Creates a new binary CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param children the children of the expression
    */
-  Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2);
+  Node newExpression(Kind kind, const Node& child_1, const Node& child_2);
 
   /**
    * Creates a new CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param children the children of the expression
    */
-  Expr newExpression(Kind kind, const std::vector<Expr>& children);
+  Node newExpression(Kind kind, const std::vector<Node>& children);
 
   /**
    * Creates a new expression based on the given string of expressions and kinds.
    * The expression is created so that it respects the kinds precedence table.
    */
-  Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds);
+  Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds);
 
   /**
    * Creates a new predicated over the given sorts.
@@ -193,16 +193,16 @@ private:
    * Creates a new expression based on the given string of expressions and kinds.
    * The expression is created so that it respects the kinds precedence table.
    */
-  Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
+  Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
 
   /** The status of the benchmark */
   BenchmarkStatus d_benchmark_status;
 
   /** The expression manager */
-  ExprManager* d_expr_manager;
+  NodeManager* d_expr_manager;
 
   /** The symbol table lookup */
-  SymbolTable<Expr> d_var_symbol_table;
+  SymbolTable<Node> d_var_symbol_table;
 };
 
 std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp
index adeb5761d..2bb01007a 100644
--- a/src/parser/cvc/cvc_parser.cpp
+++ b/src/parser/cvc/cvc_parser.cpp
@@ -44,8 +44,8 @@ Command* CvcParser::parseNextCommand() throw(ParserException) {
   return cmd;
 }
 
-Expr CvcParser::parseNextExpression() throw(ParserException) {
-  Expr result;
+Node CvcParser::parseNextExpression() throw(ParserException) {
+  Node result;
   if(!done()) {
     try {
       result = d_antlr_parser->formula();
@@ -62,7 +62,7 @@ CvcParser::~CvcParser() {
   delete d_antlr_lexer;
 }
 
-CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
+CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) :
   Parser(em), d_input(input) {
   if(!d_input) {
     throw ParserException(string("Read error") +
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 625f2c381..812925b0b 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -34,7 +34,7 @@ options {
  */
 command returns [CVC4::Command* cmd = 0]
 {
-  Expr f;
+  Node f;
   vector<string> ids;
 }
   : ASSERT   f = formula  { cmd = new AssertCommand(f);   }
@@ -60,15 +60,15 @@ type
   : BOOLEAN
   ;
 
-formula returns [CVC4::Expr formula]
+formula returns [CVC4::Node formula]
   :  formula = bool_formula
   ;
 
-bool_formula returns [CVC4::Expr formula] 
+bool_formula returns [CVC4::Node formula] 
 {
-  vector<Expr> formulas;
+  vector<Node> formulas;
   vector<Kind> kinds;
-  Expr f1, f2;
+  Node f1, f2;
   Kind k;
 }
   : f1 = primary_bool_formula { formulas.push_back(f1); } 
@@ -79,7 +79,7 @@ bool_formula returns [CVC4::Expr formula]
     }
   ;
   
-primary_bool_formula returns [CVC4::Expr formula]
+primary_bool_formula returns [CVC4::Node formula]
   : formula = bool_atom
   | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
   | LPAREN formula = bool_formula RPAREN
@@ -93,7 +93,7 @@ bool_operator returns [CVC4::Kind kind]
   | IFF      { kind = CVC4::IFF;     }
   ;
     
-bool_atom returns [CVC4::Expr atom]
+bool_atom returns [CVC4::Node atom]
 {
   string p;
 }
diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h
index 9cb6b7594..07699916f 100644
--- a/src/parser/cvc/cvc_parser.h
+++ b/src/parser/cvc/cvc_parser.h
@@ -37,7 +37,7 @@ public:
    * @param input the input stream to parse
    * @param file_name the name of the file (for diagnostic output)
    */
-  CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
+  CvcParser(NodeManager* em, std::istream& input, const char* file_name = "");
 
   /**
    * Destructor.
@@ -57,7 +57,7 @@ public:
    * Parses the next complete expression of the stream.
    * @return the expression parsed
    */
-  Expr parseNextExpression() throw(ParserException);
+  Node parseNextExpression() throw(ParserException);
 
 protected:
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 8d4af5ba1..c6d5bcb5c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -28,7 +28,7 @@ using namespace std;
 namespace CVC4 {
 namespace parser {
 
-Parser::Parser(ExprManager* em) :
+Parser::Parser(NodeManager* em) :
   d_expr_manager(em), d_done(false) {
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7755d65f0..7f63261c7 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -22,9 +22,9 @@
 namespace CVC4 {
 
 // Forward declarations
-class Expr;
+class Node;
 class Command;
-class ExprManager;
+class NodeManager;
 
 namespace parser {
 
@@ -44,7 +44,7 @@ public:
    * Construct the parser that uses the given expression manager.
    * @param em the expression manager.
    */
-  Parser(ExprManager* em);
+  Parser(NodeManager* em);
 
   /**
    * Destructor.
@@ -60,7 +60,7 @@ public:
   /**
    * Parse the next expression of the stream
    */
-  virtual Expr parseNextExpression() throw (ParserException) = 0;
+  virtual Node parseNextExpression() throw (ParserException) = 0;
 
   /**
    * Check if we are done -- either the end of input has been reached.
@@ -73,7 +73,7 @@ protected:
   void setDone(bool done = true);
 
   /** Expression manager the parser will be using */
-  ExprManager* d_expr_manager;
+  NodeManager* d_expr_manager;
 
   /** Are we done */
   bool d_done;
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp
index 65d36690c..411866540 100644
--- a/src/parser/smt/smt_parser.cpp
+++ b/src/parser/smt/smt_parser.cpp
@@ -41,8 +41,8 @@ Command* SmtParser::parseNextCommand() throw(ParserException) {
   return cmd;
 }
 
-Expr SmtParser::parseNextExpression() throw(ParserException) {
-  Expr result;
+Node SmtParser::parseNextExpression() throw(ParserException) {
+  Node result;
   if(!done()) {
     try {
       result = d_antlr_parser->an_formula();
@@ -59,7 +59,7 @@ SmtParser::~SmtParser() {
   delete d_antlr_lexer;
 }
 
-SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
+SmtParser::SmtParser(NodeManager* em, istream& input, const char* file_name) :
   Parser(em), d_input(input) {
   if(!d_input) {
     throw ParserException(string("Read error") +
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index f68d783bc..c2f5c145b 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -60,7 +60,7 @@ pred_symb returns [std::string p]
 /**
  * Matches a propositional atom from the input. 
  */
-prop_atom returns [CVC4::Expr atom]
+prop_atom returns [CVC4::Node atom]
 {
   std::string p;
 } 
@@ -78,7 +78,7 @@ prop_atom returns [CVC4::Expr atom]
  * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
  * here in order to get rid of the ugly antlr non-determinism warrnings. 
  */
-an_atom returns [CVC4::Expr atom] 
+an_atom returns [CVC4::Node atom] 
   : atom = prop_atom  
   ;
   
@@ -97,18 +97,18 @@ connective returns [CVC4::Kind kind]
 /** 
  * Matches an annotated formula. 
  */
-an_formula returns [CVC4::Expr formula] 
+an_formula returns [CVC4::Node formula] 
 { 
   Kind kind; 
-  vector<Expr> children;
+  vector<Node> children;
 }
   :  formula = an_atom 
   |  LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children);  }    
   ;
   
-an_formulas[std::vector<Expr>& formulas]
+an_formulas[std::vector<Node>& formulas]
 {
-  Expr f;
+  Node f;
 }
   : ( f = an_formula { formulas.push_back(f); } )+
   ;
@@ -149,7 +149,7 @@ status returns [ AntlrParser::BenchmarkStatus status ]
 bench_attribute returns [ Command* smt_command = 0]
 {
   BenchmarkStatus b_status = SMT_UNKNOWN;
-  Expr formula;  
+  Node formula;  
   vector<string> sorts;
 }
   : C_LOGIC       IDENTIFIER      
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
index a68f0e783..7dedcd5b4 100644
--- a/src/parser/smt/smt_parser.h
+++ b/src/parser/smt/smt_parser.h
@@ -37,7 +37,7 @@ public:
    * @param input the input stream to parse
    * @param file_name the name of the file (for diagnostic output)
    */
-  SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
+  SmtParser(NodeManager* em, std::istream& input, const char* file_name = "");
 
   /**
    * Destructor.
@@ -57,7 +57,7 @@ public:
    * Parses the next complete expression of the stream.
    * @return the expression parsed
    */
-  Expr parseNextExpression() throw(ParserException);
+  Node parseNextExpression() throw(ParserException);
 
 protected:
 
diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index 32532c734..2c4f0e8b7 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -16,8 +16,6 @@
 #include <stack>
 #include <ext/hash_map>
 
-#include "expr/expr.h"
-
 namespace __gnu_cxx {
 template<>
   struct hash<std::string> {
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 2fb73cbed..166546a2c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -30,9 +30,9 @@ PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
   d_de(de), d_te(te), d_sat() {
 }
 
-void PropEngine::addVars(Expr e) {
+void PropEngine::addVars(Node e) {
   Debug("prop") << "adding vars to " << e << endl;
-  for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+  for(Node::iterator i = e.begin(); i != e.end(); ++i) {
     Debug("prop") << "expr " << *i << endl;
     if(i->getKind() == VARIABLE) {
       if(d_vars.find(*i) == d_vars.end()) {
@@ -45,18 +45,18 @@ void PropEngine::addVars(Expr e) {
   }
 }
 
-static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) {
+static void doAtom(SimpSolver* minisat, map<Node, Var>* vars, Node e, vec<Lit>* c) {
   if(e.getKind() == VARIABLE) {
-    map<Expr, Var>::iterator v = vars->find(e);
+    map<Node, Var>::iterator v = vars->find(e);
     Assert(v != vars->end());
     c->push(Lit(v->second, false));
     return;
   }
   if(e.getKind() == NOT) {
     Assert(e.numChildren() == 1);
-    Expr child = *e.begin();
+    Node child = *e.begin();
     Assert(child.getKind() == VARIABLE);
-    map<Expr, Var>::iterator v = vars->find(child);
+    map<Node, Var>::iterator v = vars->find(child);
     Assert(v != vars->end());
     c->push(Lit(v->second, true));
     return;
@@ -64,14 +64,14 @@ static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>*
   Unhandled();
 }
 
-static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) {
+static void doClause(SimpSolver* minisat, map<Node, Var>* vars, map<Var, Node>* varsReverse, Node e) {
   vec<Lit> c;
   Debug("prop") << "  " << e << endl;
   if(e.getKind() == VARIABLE || e.getKind() == NOT) {
     doAtom(minisat, vars, e, &c);
   } else {
     Assert(e.getKind() == OR);
-    for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
+    for(Node::iterator i = e.begin(); i != e.end(); ++i) {
       Debug("prop") << "    " << *i << endl;
       doAtom(minisat, vars, *i, &c);
     }
@@ -86,12 +86,12 @@ static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>*
   minisat->addClause(c);
 }
 
-void PropEngine::solve(Expr e) {
+void PropEngine::solve(Node e) {
   Debug("prop") << "SOLVING " << e << endl;
   addVars(e);
   if(e.getKind() == AND) {
     Debug("prop") << "AND" << endl;
-    for(Expr::iterator i = e.begin(); i != e.end(); ++i)
+    for(Node::iterator i = e.begin(); i != e.end(); ++i)
       doClause(&d_sat, &d_vars, &d_varsReverse, *i);
   } else doClause(&d_sat, &d_vars, &d_varsReverse, e);
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a3355bf89..21a6669d7 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -13,7 +13,7 @@
 #define __CVC4__PROP_ENGINE_H
 
 #include "cvc4_config.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "util/decision_engine.h"
 #include "theory/theory_engine.h"
 #include "prop/minisat/simp/SimpSolver.h"
@@ -31,10 +31,10 @@ class PropEngine {
   DecisionEngine &d_de;
   TheoryEngine &d_te;
   CVC4::prop::minisat::SimpSolver d_sat;
-  std::map<Expr, CVC4::prop::minisat::Var> d_vars;
-  std::map<CVC4::prop::minisat::Var, Expr> d_varsReverse;
+  std::map<Node, CVC4::prop::minisat::Var> d_vars;
+  std::map<CVC4::prop::minisat::Var, Node> d_varsReverse;
 
-  void addVars(Expr);
+  void addVars(Node);
 
 public:
   /**
@@ -45,7 +45,7 @@ public:
   /**
    * Converts to CNF if necessary.
    */
-  void solve(Expr);
+  void solve(Node);
 
 };/* class PropEngine */
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2e895cdc0..4ccdd07d0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -19,12 +19,12 @@ void SmtEngine::doCommand(Command* c) {
   c->invoke(this);
 }
 
-Expr SmtEngine::preprocess(Expr e) {
+Node SmtEngine::preprocess(Node e) {
   return e;
 }
 
 void SmtEngine::processAssertionList() {
-  for(std::vector<Expr>::iterator i = d_assertions.begin();
+  for(std::vector<Node>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
     d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i);
@@ -41,23 +41,23 @@ Result SmtEngine::quickCheck() {
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
-void SmtEngine::addFormula(Expr e) {
+void SmtEngine::addFormula(Node e) {
   d_assertions.push_back(e);
 }
 
-Result SmtEngine::checkSat(Expr e) {
+Result SmtEngine::checkSat(Node e) {
   e = preprocess(e);
   addFormula(e);
   return check();
 }
 
-Result SmtEngine::query(Expr e) {
+Result SmtEngine::query(Node e) {
   e = preprocess(e);
   addFormula(e);
   return check();
 }
 
-Result SmtEngine::assertFormula(Expr e) {
+Result SmtEngine::assertFormula(Node e) {
   e = preprocess(e);
   addFormula(e);
   return quickCheck();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 30786511e..c4addc7dd 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -15,8 +15,8 @@
 #include <vector>
 
 #include "cvc4_config.h"
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
@@ -45,16 +45,16 @@ class Command;
 class SmtEngine {
   /** Current set of assertions. */
   // TODO: make context-aware to handle user-level push/pop.
-  std::vector<Expr> d_assertions;
+  std::vector<Node> d_assertions;
 
   /** Our expression manager */
-  ExprManager *d_em;
+  NodeManager *d_em;
 
   /** User-level options */
   Options *d_opts;
 
   /** Expression built-up for handing off to the propagation engine */
-  Expr d_expr;
+  Node d_expr;
 
   /** The decision engine */
   DecisionEngine d_de;
@@ -66,17 +66,17 @@ class SmtEngine {
   PropEngine d_prop;
 
   /**
-   * Pre-process an Expr.  This is expected to be highly-variable,
+   * Pre-process an Node.  This is expected to be highly-variable,
    * with a lot of "source-level configurability" to add multiple
-   * passes over the Expr.  TODO: may need to specify a LEVEL of
+   * passes over the Node.  TODO: may need to specify a LEVEL of
    * preprocessing (certain contexts need more/less ?).
    */
-  Expr preprocess(Expr);
+  Node preprocess(Node);
 
   /**
    * Adds a formula to the current context.
    */
-  void addFormula(Expr);
+  void addFormula(Node);
 
   /**
    * Full check of consistency in current context.  Returns true iff
@@ -101,10 +101,10 @@ public:
   /*
    * Construct an SmtEngine with the given expression manager and user options.
    */
-  SmtEngine(ExprManager* em, Options* opts) throw() :
+  SmtEngine(NodeManager* em, Options* opts) throw() :
     d_em(em),
     d_opts(opts),
-    d_expr(Expr::null()),
+    d_expr(Node::null()),
     d_de(),
     d_te(),
     d_prop(d_de, d_te) {
@@ -121,25 +121,25 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(Expr);
+  Result assertFormula(Node);
 
   /**
    * Add a formula to the current context and call check().  Returns
    * true iff consistent.
    */
-  Result query(Expr);
+  Result query(Node);
 
   /**
    * Add a formula to the current context and call check().  Returns
    * true iff consistent.
    */
-  Result checkSat(Expr);
+  Result checkSat(Node);
 
   /**
    * Simplify a formula without doing "much" work.  Requires assist
    * from the SAT Engine.
    */
-  Expr simplify(Expr);
+  Node simplify(Node);
 
   /**
    * Get a (counter)model (only if preceded by a SAT or INVALID query.
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5e5f053a6..21124375a 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4__THEORY__THEORY_H
 #define __CVC4__THEORY__THEORY_H
 
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "util/literal.h"
 
 namespace CVC4 {
@@ -46,9 +46,9 @@ public:
   static bool fullEffort(Effort e)           { return e >= FULL_EFFORT; }
 
   /**
-   * Prepare for an Expr.
+   * Prepare for an Node.
    */
-  virtual void setup(Expr) = 0;
+  virtual void setup(Node) = 0;
 
   /**
    * Assert a literal in the current context.
@@ -75,7 +75,7 @@ public:
   /**
    * Return an explanation for the literal (which was previously propagated by this theory)..
    */
-  virtual Expr explain(Literal) = 0;
+  virtual Node explain(Literal) = 0;
 
 };/* class Theory */
 
diff --git a/src/util/command.cpp b/src/util/command.cpp
index ed6b61703..0953a2ba2 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -7,7 +7,7 @@
 
 #include "util/command.h"
 #include "smt/smt_engine.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "util/result.h"
 
 using namespace std;
@@ -26,7 +26,7 @@ EmptyCommand::EmptyCommand(string name) :
 void EmptyCommand::invoke(SmtEngine* smt_engine) {
 }
 
-AssertCommand::AssertCommand(const Expr& e) :
+AssertCommand::AssertCommand(const Node& e) :
   d_expr(e) {
 }
 
@@ -37,7 +37,7 @@ void AssertCommand::invoke(SmtEngine* smt_engine) {
 CheckSatCommand::CheckSatCommand() {
 }
 
-CheckSatCommand::CheckSatCommand(const Expr& e) :
+CheckSatCommand::CheckSatCommand(const Node& e) :
   d_expr(e) {
 }
 
@@ -45,7 +45,7 @@ void CheckSatCommand::invoke(SmtEngine* smt_engine) {
   smt_engine->checkSat(d_expr);
 }
 
-QueryCommand::QueryCommand(const Expr& e) :
+QueryCommand::QueryCommand(const Node& e) :
   d_expr(e) {
 }
 
diff --git a/src/util/command.h b/src/util/command.h
index 31acbc43b..189872220 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -15,12 +15,12 @@
 #include <iostream>
 
 #include "cvc4_config.h"
-#include "expr/expr.h"
+#include "expr/node.h"
 
 namespace CVC4 {
   class SmtEngine;
   class Command;
-  class Expr;
+  class Node;
 }/* CVC4 namespace */
 
 namespace CVC4 {
@@ -46,9 +46,9 @@ private:
 
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
-  Expr d_expr;
+  Node d_expr;
 public:
-  AssertCommand(const Expr& e);
+  AssertCommand(const Node& e);
   void invoke(CVC4::SmtEngine* smt_engine);
   void toString(std::ostream& out) const;
 };/* class AssertCommand */
@@ -57,21 +57,21 @@ public:
 class CVC4_PUBLIC CheckSatCommand : public Command {
 public:
   CheckSatCommand();
-  CheckSatCommand(const Expr& e);
+  CheckSatCommand(const Node& e);
   void invoke(SmtEngine* smt);
   void toString(std::ostream& out) const;
 protected:
-  Expr d_expr;
+  Node d_expr;
 };/* class CheckSatCommand */
 
 
 class CVC4_PUBLIC QueryCommand : public Command {
 public:
-  QueryCommand(const Expr& e);
+  QueryCommand(const Node& e);
   void invoke(SmtEngine* smt);
   void toString(std::ostream& out) const;
 protected:
-  Expr d_expr;
+  Node d_expr;
 };/* class QueryCommand */
 
 
diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h
index 5f1deee8a..ad70bec91 100644
--- a/test/unit/expr/expr_black.h
+++ b/test/unit/expr/expr_black.h
@@ -1,4 +1,4 @@
-/* Black box testing of CVC4::Expr. */
+/* Black box testing of CVC4::Node. */
 
 #include <cxxtest/TestSuite.h>
 
@@ -10,10 +10,10 @@ class ExprBlack : public CxxTest::TestSuite {
 public:
 
   void testNull() {
-    Expr::s_null;
+    Node::s_null;
   }
 
   void testCopyCtor() {
-    Expr e(Expr::s_null);
+    Node e(Node::s_null);
   }
 };
diff --git a/test/unit/expr/expr_white.h b/test/unit/expr/expr_white.h
index 3da360126..6b48d66e6 100644
--- a/test/unit/expr/expr_white.h
+++ b/test/unit/expr/expr_white.h
@@ -1,4 +1,4 @@
-/* White box testing of CVC4::Expr. */
+/* White box testing of CVC4::Node. */
 
 #include <cxxtest/TestSuite.h>
 
@@ -10,10 +10,10 @@ class ExprWhite : public CxxTest::TestSuite {
 public:
 
   void testNull() {
-    Expr::s_null;
+    Node::s_null;
   }
 
   void testCopyCtor() {
-    Expr e(Expr::s_null);
+    Node e(Node::s_null);
   }
 };