Fixes to the build system:

Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors

54 files changed, 946 insertions, 641 deletions

diff --git a/src/Makefile b/src/Makefile
new file mode 100644
index 000000000..e119c83d7
--- /dev/null
+++ b/src/Makefile
@@ -0,0 +1,5 @@
+topdir = ..
+srcdir = src
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/Makefile.am b/src/Makefile.am
index 1db9d9ecf..f429e8b2a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -15,9 +15,10 @@
 LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
 LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
 
-INCLUDES = -I@srcdir@/include -I@srcdir@
+AM_CPPFLAGS =
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/include -I@srcdir@
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 SUBDIRS = util expr context prop smt theory . parser main
 
diff --git a/src/Makefile.in b/src/Makefile.in
index 8f33fd330..38d59d02a 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -159,6 +159,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -287,9 +288,8 @@ top_srcdir = @top_srcdir@
 #
 LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
 LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
-INCLUDES = -I@srcdir@/include -I@srcdir@
+AM_CPPFLAGS = 
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 SUBDIRS = util expr context prop smt theory . parser main
 lib_LTLIBRARIES = libcvc4.la
 libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE)
@@ -700,6 +700,8 @@ uninstall-am: uninstall-libLTLIBRARIES
 	tags tags-recursive uninstall uninstall-am \
 	uninstall-libLTLIBRARIES
 
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/include -I@srcdir@
 
 install-data-local: $(publicheaders)
 	$(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4
diff --git a/src/context/Makefile b/src/context/Makefile
new file mode 100644
index 000000000..5286dd3ac
--- /dev/null
+++ b/src/context/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/context
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index e38f7f4eb..b36d5e69c 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libcontext.la
 
diff --git a/src/context/Makefile.in b/src/context/Makefile.in
index 0e5281ca6..51069583d 100644
--- a/src/context/Makefile.in
+++ b/src/context/Makefile.in
@@ -52,7 +52,7 @@ CONFIG_CLEAN_FILES =
 CONFIG_CLEAN_VPATH_FILES =
 LTLIBRARIES = $(noinst_LTLIBRARIES)
 libcontext_la_LIBADD =
-am_libcontext_la_OBJECTS = context.lo
+am_libcontext_la_OBJECTS = context.lo context_mm.lo
 libcontext_la_OBJECTS = $(am_libcontext_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -104,6 +104,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -215,13 +216,17 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libcontext.la
 libcontext_la_SOURCES = \
 	context.cpp \
-	context.h
+	context.h \
+	context_mm.cpp \
+	context_mm.h
 
 all: all-am
 
@@ -276,6 +281,7 @@ distclean-compile:
 	-rm -f *.tab.c
 
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/context.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/context_mm.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index 51f192f2a..3b4089b25 100644
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -14,14 +14,13 @@
 #include <cstdlib>
 #include <vector>
 #include <deque>
+#include <new>
 #include "context/context_mm.h"
 #include "util/Assert.h"
 
-
 namespace CVC4 {
 namespace context {
 
-
 void ContextMemoryManager::newChunk() {
 
   // Increment index to chunk list
@@ -30,16 +29,16 @@ void ContextMemoryManager::newChunk() {
          "Index should be at the end of the list");
 
   // Create new chunk if no free chunk available
-  if (d_freePages.empty()) {
+  if (d_freeChunks.empty()) {
     d_chunkList.push_back((char*)malloc(chunkSizeBytes));
     if (d_chunkList.back() == NULL) {
-      throw bad_alloc();
+      throw std::bad_alloc();
     }
   }
   // If there is a free chunk, use that
   else {
-    d_chunkList.push_back(d_freePages.back());
-    d_freePages.pop_back();
+    d_chunkList.push_back(d_freeChunks.back());
+    d_freeChunks.pop_back();
   }
   // Set up the current chunk pointers
   d_nextFree = d_chunkList.back();
@@ -47,30 +46,30 @@ void ContextMemoryManager::newChunk() {
 }
 
 
-ContextMemoryManager() : d_indexChunkList(0) {
+ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) {
   // Create initial chunk
   d_chunkList.push_back((char*)malloc(chunkSizeBytes));
   d_nextFree = d_chunkList.back();
   if (d_nextFree == NULL) {
-    throw bad_alloc;
+    throw std::bad_alloc();
   }
   d_endChunk = d_nextFree + chunkSizeBytes;
 }
 
 
-~ContextMemoryManager() {
+ContextMemoryManager::~ContextMemoryManager() {
   // Delete all chunks
   while (!d_chunkList.empty()) {
     free(d_chunkList.back());
     d_chunkList.pop_back();
   }
-  while (!d_freePages.empty()) {
-    free(d_freePages.back());
-    d_freePages.pop_back();
+  while (!d_freeChunks.empty()) {
+    free(d_freeChunks.back());
+    d_freeChunks.pop_back();
   }
 }
 
-void* newData(size_t size) {
+void* ContextMemoryManager::newData(size_t size) {
   // Use next available free location in current chunk
   void* res = (void*)d_nextFree;
   d_nextFree += size;
@@ -86,7 +85,7 @@ void* newData(size_t size) {
 }
 
 
-void push() {
+void ContextMemoryManager::push() {
   // Store current state on the stack
   d_nextFreeStack.push_back(d_nextFree);
   d_endChunkStack.push_back(d_endChunk);
@@ -94,7 +93,7 @@ void push() {
 }
 
 
-void pop() {
+void ContextMemoryManager::pop() {
   // Restore state from stack
   d_nextFree = d_nextFreeStack.back();
   d_nextFreeStack.pop_back();
@@ -103,7 +102,7 @@ void pop() {
 
   // Free all the new chunks since the last push
   while (d_indexChunkList > d_indexChunkListStack.back()) {
-    d_freePages.push_back(d_chunkList.back());
+    d_freeChunks.push_back(d_chunkList.back());
     d_chunkList.pop_back();
     --d_indexChunkList;
   }
@@ -111,12 +110,11 @@ void pop() {
 
   // Delete excess free chunks
   while (d_freeChunks.size() > maxFreeChunks) {
-    free(d_freePages.front());
-    d_freePages.pop_front();
+    free(d_freeChunks.front());
+    d_freeChunks.pop_front();
   }
 }
 
 
 }/* CVC4::context namespace */
-
 }/* CVC4 namespace */
diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index 6b442d4a0..d48cbedc0 100644
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -33,13 +33,13 @@ class ContextMemoryManager {
   /**
    * Memory in regions is allocated in chunks.  This is the minimum chunk size
    */
-  const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
+  static const unsigned chunkSizeBytes = 16384; // #bytes in each chunk
 
   /**
    * A list of free chunks is maintained.  This is the maximum number of
    * free chunks.
    */
-  const unsigned maxFreeChunks = 100;
+  static const unsigned maxFreeChunks = 100;
 
   /**
    * List of all chunks that are currently active
diff --git a/src/expr/Makefile b/src/expr/Makefile
new file mode 100644
index 000000000..b661835a5
--- /dev/null
+++ b/src/expr/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/expr
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index b8606e051..046281702 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libexpr.la
 
@@ -10,7 +11,7 @@ libexpr_la_SOURCES = \
 	node.h \
 	node_builder.h \
 	expr.h \
-	expr_value.h \
+	node_value.h \
 	node_manager.h \
 	expr_manager.h \
 	node_attribute.h \
@@ -19,6 +20,6 @@ libexpr_la_SOURCES = \
 	node_builder.cpp \
 	node_manager.cpp \
 	expr_manager.cpp \
-	expr_value.cpp \
+	node_value.cpp \
 	expr.cpp
 
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index 6b1555e6c..c7d99dc84 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -53,7 +53,7 @@ CONFIG_CLEAN_VPATH_FILES =
 LTLIBRARIES = $(noinst_LTLIBRARIES)
 libexpr_la_LIBADD =
 am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \
-	expr_manager.lo expr_value.lo expr.lo
+	expr_manager.lo node_value.lo expr.lo
 libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -105,6 +105,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -216,9 +217,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libexpr.la
 libexpr_la_SOURCES = \
 	attr_type.h \
@@ -226,7 +229,7 @@ libexpr_la_SOURCES = \
 	node.h \
 	node_builder.h \
 	expr.h \
-	expr_value.h \
+	node_value.h \
 	node_manager.h \
 	expr_manager.h \
 	node_attribute.h \
@@ -235,7 +238,7 @@ libexpr_la_SOURCES = \
 	node_builder.cpp \
 	node_manager.cpp \
 	expr_manager.cpp \
-	expr_value.cpp \
+	node_value.cpp \
 	expr.cpp
 
 all: all-am
@@ -292,10 +295,10 @@ distclean-compile:
 
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.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@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_value.Plo@am__quote@
 
 .cpp.o:
 @am__fastdepCXX_TRUE@	$(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $<
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
deleted file mode 100644
index af064f43d..000000000
--- a/src/expr/expr_value.cpp
+++ /dev/null
@@ -1,103 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** expr_value.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.
- **
- ** An expression node.
- **
- ** Instances of this class are generally referenced through
- ** cvc4::Node rather than by pointer; cvc4::Node maintains the
- ** reference count on ExprValue instances and
- **/
-
-#include "expr_value.h"
-#include <sstream>
-
-using namespace std;
-
-namespace CVC4 {
-
-size_t ExprValue::next_id = 1;
-
-ExprValue::ExprValue() :
-  d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
-}
-
-uint64_t ExprValue::hash() const {
-  return computeHash<const_iterator>(d_kind, begin(), end());
-}
-
-ExprValue* ExprValue::inc() {
-  // FIXME multithreading
-  if(d_rc < MAX_RC)
-    ++d_rc;
-  return this;
-}
-
-ExprValue* ExprValue::dec() {
-  // FIXME multithreading
-  if(d_rc < MAX_RC)
-    if(--d_rc == 0) {
-      // FIXME gc
-      return 0;
-    }
-  return this;
-}
-
-ExprValue::iterator ExprValue::begin() {
-  return d_children;
-}
-
-ExprValue::iterator ExprValue::end() {
-  return d_children + d_nchildren;
-}
-
-ExprValue::iterator ExprValue::rbegin() {
-  return d_children + d_nchildren - 1;
-}
-
-ExprValue::iterator ExprValue::rend() {
-  return d_children - 1;
-}
-
-ExprValue::const_iterator ExprValue::begin() const {
-  return d_children;
-}
-
-ExprValue::const_iterator ExprValue::end() const {
-  return d_children + d_nchildren;
-}
-
-ExprValue::const_iterator ExprValue::rbegin() const {
-  return d_children + d_nchildren - 1;
-}
-
-ExprValue::const_iterator ExprValue::rend() const {
-  return d_children - 1;
-}
-
-string ExprValue::toString() const {
-  stringstream ss;
-  toStream(ss);
-  return ss.str();
-}
-
-void ExprValue::toStream(std::ostream& out) const {
-  out << "(" << Kind(d_kind);
-  if(d_kind == VARIABLE) {
-    out << ":" << this;
-  } else {
-    for(const_iterator i = begin(); i != end(); ++i) {
-      if(i != end())
-        out << " ";
-      out << *i;
-    }
-  }
-  out << ")";
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 5ac02ca7c..624ab7337 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -12,6 +12,7 @@
 #ifndef __CVC4__KIND_H
 #define __CVC4__KIND_H
 
+#include "cvc4_config.h"
 #include <iostream>
 
 namespace CVC4 {
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index be9ac995c..1a549973f 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr.cpp
+/** node.cpp
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,7 +11,7 @@
  **/
 
 #include "expr/node.h"
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
 #include "expr/node_builder.h"
 #include "util/Assert.h"
 
@@ -22,26 +22,29 @@ using namespace std;
 
 namespace CVC4 {
 
-ExprValue ExprValue::s_null;
+NodeValue NodeValue::s_null;
 
-Node Node::s_null(&ExprValue::s_null);
+Node Node::s_null(&NodeValue::s_null);
 
 Node Node::null() {
   return s_null;
 }
 
-
 bool Node::isNull() const {
-  return d_ev == &ExprValue::s_null;
+  return d_ev == &NodeValue::s_null;
 }
 
 Node::Node() :
-  d_ev(&ExprValue::s_null) {
+  d_ev(&NodeValue::s_null) {
   // No refcount needed
 }
 
-Node::Node(ExprValue* ev)
-  : d_ev(ev) {
+// 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.
+Node::Node(const NodeValue* ev)
+  : d_ev(const_cast<NodeValue*>(ev)) {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
   d_ev->inc();
 }
@@ -57,7 +60,7 @@ Node::~Node() {
   d_ev->dec();
 }
 
-void Node::assignExprValue(ExprValue* ev) {
+void Node::assignNodeValue(NodeValue* ev) {
   d_ev = ev;
   d_ev->inc();
 }
@@ -72,7 +75,7 @@ Node& Node::operator=(const Node& e) {
   return *this;
 }
 
-ExprValue const* Node::operator->() const {
+NodeValue const* Node::operator->() const {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
   return d_ev;
 }
@@ -83,35 +86,35 @@ uint64_t Node::hash() const {
 }
 
 Node Node::eqExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
+  return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
 }
 
 Node Node::notExpr() const {
-  return NodeManager::currentEM()->mkExpr(NOT, *this);
+  return NodeManager::currentNM()->mkExpr(NOT, *this);
 }
 
 Node Node::andExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(AND, *this, right);
+  return NodeManager::currentNM()->mkExpr(AND, *this, right);
 }
 
 Node Node::orExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(OR, *this, right);
+  return NodeManager::currentNM()->mkExpr(OR, *this, right);
 }
 
 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
-  return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
+  return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
 }
 
 Node Node::iffExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(IFF, *this, right);
+  return NodeManager::currentNM()->mkExpr(IFF, *this, right);
 }
 
 Node Node::impExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
+  return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
 }
 
 Node Node::xorExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(XOR, *this, right);
+  return NodeManager::currentNM()->mkExpr(XOR, *this, right);
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node.h b/src/expr/node.h
index 17d1c0111..5415a5b3c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -10,6 +10,8 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
+#include "expr/node_value.h"
+
 #ifndef __CVC4__NODE_H
 #define __CVC4__NODE_H
 
@@ -32,38 +34,44 @@ inline std::ostream& operator<<(std::ostream&, const Node&);
 class NodeManager;
 
 namespace expr {
-  class ExprValue;
+  class NodeValue;
 }/* CVC4::expr namespace */
 
-using CVC4::expr::ExprValue;
+using CVC4::expr::NodeValue;
 
 /**
- * Encapsulation of an ExprValue pointer.  The reference count is
- * maintained in the ExprValue.
+ * Encapsulation of an NodeValue pointer.  The reference count is
+ * maintained in the NodeValue.
  */
 class Node {
 
-  friend class ExprValue;
+  friend class NodeValue;
 
   /** A convenient null-valued encapsulated pointer */
   static Node s_null;
 
-  /** The referenced ExprValue */
-  ExprValue* d_ev;
+  /** The referenced NodeValue */
+  NodeValue* d_ev;
 
   /** This constructor is reserved for use by the Node package; one
    *  must construct an Node using one of the build mechanisms of the
    *  Node package.
    *
-   *  Increments the reference count. */
-  explicit Node(ExprValue*);
-
-  friend class NodeBuilder;
+   *  Increments the reference count.
+   *
+   *  FIXME: there's a type-system escape here to cast away the const,
+   *  since the refcount needs to be updated.  But conceptually Nodes
+   *  don't change their arguments, and it's nice to have
+   *  const_iterators over them.  See notes in .cpp file for
+   *  details. */
+  explicit Node(const NodeValue*);
+
+  template <unsigned> friend class NodeBuilder;
   friend class NodeManager;
 
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
-  ExprValue const* operator->() const;
+  NodeValue const* operator->() const;
 
   /**
    * Assigns the expression value and does reference counting. No assumptions are
@@ -72,7 +80,15 @@ class Node {
    *
    * @param ev the expression value to assign
    */
-  void assignExprValue(ExprValue* ev);
+  void assignNodeValue(NodeValue* ev);
+
+  typedef NodeValue::iterator ev_iterator;
+  typedef NodeValue::const_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:
 
@@ -82,7 +98,7 @@ public:
   Node(const Node&);
 
   /** Destructor.  Decrements the reference count and, if zero,
-   *  collects the ExprValue. */
+   *  collects the NodeValue. */
   ~Node();
 
   bool operator==(const Node& e) const { return d_ev == e.d_ev; }
@@ -117,8 +133,8 @@ public:
 
   static Node null();
 
-  typedef Node* iterator;
-  typedef Node const* const_iterator;
+  typedef NodeValue::node_iterator iterator;
+  typedef NodeValue::node_iterator const_iterator;
 
   inline iterator begin();
   inline iterator end();
@@ -134,7 +150,7 @@ public:
 
 }/* CVC4 namespace */
 
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
 
 namespace CVC4 {
 
@@ -159,6 +175,22 @@ inline void Node::toStream(std::ostream& out) const {
   d_ev->toStream(out);
 }
 
+inline Node::ev_iterator Node::ev_begin() {
+  return d_ev->ev_begin();
+}
+
+inline Node::ev_iterator Node::ev_end() {
+  return d_ev->ev_end();
+}
+
+inline Node::const_ev_iterator Node::ev_begin() const {
+  return d_ev->ev_begin();
+}
+
+inline Node::const_ev_iterator Node::ev_end() const {
+  return d_ev->ev_end();
+}
+
 inline Node::iterator Node::begin() {
   return d_ev->begin();
 }
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
index 7d30ff4e3..0a36421f2 100644
--- a/src/expr/node_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_builder.cpp
+/** node_builder.cpp
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,214 +11,7 @@
 
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
 #include "util/output.h"
 
 using namespace std;
-
-namespace CVC4 {
-
-NodeBuilder::NodeBuilder() :
-  d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false),
-      d_nchildren(0) {
-}
-
-NodeBuilder::NodeBuilder(Kind k) :
-  d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {
-}
-
-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();;
-}
-
-NodeBuilder& NodeBuilder::reset(const ExprValue* ev) {
-  this->~NodeBuilder();
-  d_kind = Kind(ev->d_kind);
-  d_used = false;
-  d_nchildren = ev->d_nchildren;
-  for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i)
-    addChild(i->d_ev);
-  return *this;
-}
-
-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<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));
-  } else {
-    ev_iterator j = d_children.u_arr;
-    ExprValue* const * i = eb.d_children.u_arr;
-    ExprValue* const * i_end = i + eb.d_nchildren;
-    for(; i != i_end; ++i, ++j)
-      *j = (*i)->inc();
-  }
-}
-
-NodeBuilder::NodeBuilder(NodeManager* em) :
-  d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
-}
-
-NodeBuilder::NodeBuilder(NodeManager* em, Kind k) :
-  d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
-}
-
-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();
-}
-
-NodeBuilder::~NodeBuilder() {
-  if(d_nchildren > nchild_thresh) {
-    delete d_children.u_vec;
-  } else {
-    ev_iterator i = d_children.u_arr;
-    ev_iterator i_end = d_children.u_arr + d_nchildren;
-    for(; i != i_end ; ++i) {
-      (*i)->dec();
-    }
-  }
-}
-
-// Compound expression constructors
-NodeBuilder& NodeBuilder::eqExpr(const Node& right) {
-  Assert( d_kind != UNDEFINED_KIND );
-  if(EXPECT_TRUE( d_kind != EQUAL )) {
-    collapse();
-    d_kind = EQUAL;
-  }
-  addChild(right);
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::notExpr() {
-  Assert( d_kind != UNDEFINED_KIND );
-  collapse();
-  d_kind = NOT;
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::andExpr(const Node& right) {
-  Assert( d_kind != UNDEFINED_KIND );
-  if(d_kind != AND) {
-    collapse();
-    d_kind = AND;
-  }
-  addChild(right);
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::orExpr(const Node& right) {
-  Assert( d_kind != UNDEFINED_KIND );
-  if(EXPECT_TRUE( d_kind != OR )) {
-    collapse();
-    d_kind = OR;
-  }
-  addChild(right);
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) {
-  Assert( d_kind != UNDEFINED_KIND );
-  collapse();
-  d_kind = ITE;
-  addChild(thenpart);
-  addChild(elsepart);
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::iffExpr(const Node& right) {
-  Assert( d_kind != UNDEFINED_KIND );
-  if(EXPECT_TRUE( d_kind != IFF )) {
-    collapse();
-    d_kind = IFF;
-  }
-  addChild(right);
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::impExpr(const Node& right) {
-  Assert( d_kind != UNDEFINED_KIND );
-  collapse();
-  d_kind = IMPLIES;
-  addChild(right);
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::xorExpr(const Node& right) {
-  Assert( d_kind != UNDEFINED_KIND );
-  if(EXPECT_TRUE( d_kind != XOR )) {
-    collapse();
-    d_kind = XOR;
-  }
-  addChild(right);
-  return *this;
-}
-
-// "Stream" expression constructor syntax
-NodeBuilder& NodeBuilder::operator<<(const Kind& op) {
-  d_kind = op;
-  return *this;
-}
-
-NodeBuilder& NodeBuilder::operator<<(const Node& child) {
-  addChild(child);
-  return *this;
-}
-
-/**
- * We keep the children either:
- * (a) In the array of expression values if the number of children is less than
- *     nchild_thresh. Hence (last else) we increase the reference count.
- * (b) If the number of children reaches the nchild_thresh, we allocate a vector
- *     for the children. Children are now expressions, so we also decrement the
- *     reference count for each child.
- * (c) Otherwise we just add to the end of the vector.
- */
-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<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(Node(*i));
-      (*i)->dec();
-    }
-    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(Node(ev));
-    // ++d_nchildren; no need for this
-  } else {
-    Debug("expr") << "under thresh " << d_nchildren
-                  << " < " << nchild_thresh << endl;
-    d_children.u_arr[d_nchildren ++] = ev->inc();
-  }
-}
-
-NodeBuilder& NodeBuilder::collapse() {
-  if(d_nchildren == nchild_thresh) {
-    vector<Node>* v = new vector<Node> ();
-    v->reserve(nchild_thresh + 5);
-    //
-    Unreachable();// unimplemented
-  }
-  return *this;
-}
-
-}/* CVC4 namespace */
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 5be3c284d..63048c1ac 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_builder.h
+/** node_builder.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -14,68 +14,90 @@
 
 #include <vector>
 #include <cstdlib>
+#include <stdint.h>
+
+namespace CVC4 {
+  static const unsigned default_nchild_thresh = 10;
+
+  template <unsigned nchild_thresh = default_nchild_thresh>
+  class NodeBuilder;
+
+  class NodeManager;
+}/* CVC4 namespace */
 
-#include "expr/node_manager.h"
 #include "expr/kind.h"
 #include "util/Assert.h"
+#include "expr/node_value.h"
 
 namespace CVC4 {
 
-class AndExprBuilder;
-class OrExprBuilder;
-class PlusExprBuilder;
-class MinusExprBuilder;
-class MultExprBuilder;
+class AndNodeBuilder;
+class OrNodeBuilder;
+class PlusNodeBuilder;
+class MinusNodeBuilder;
+class MultNodeBuilder;
 
+template <unsigned nchild_thresh>
 class NodeBuilder {
-  NodeManager* d_em;
+  unsigned d_size;
 
-  Kind d_kind;
+  uint64_t d_hash;
+
+  NodeManager* d_nm;
 
   // initially false, when you extract the Node this is set and you can't
   // extract another
   bool d_used;
 
-  static const unsigned nchild_thresh = 10;
-
-  unsigned d_nchildren;
-  union {
-    ExprValue*         u_arr[nchild_thresh];
-    std::vector<Node>* u_vec;
-  } d_children;
-
-  void addChild(const Node& e) { addChild(e.d_ev); }
-  void addChild(ExprValue*);
-  NodeBuilder& collapse();
+  NodeValue *d_ev;
+  NodeValue d_inlineEv;
+  NodeValue *d_childrenStorage[nchild_thresh];
 
-  typedef ExprValue** ev_iterator;
-  typedef ExprValue const** const_ev_iterator;
+  bool evIsAllocated() {
+    return d_ev->d_nchildren > nchild_thresh;
+  }
 
-  ev_iterator ev_begin() {
-    return d_children.u_arr;
+  template <unsigned N>
+  bool evIsAllocated(const NodeBuilder<N>& nb) {
+    return nb.d_ev->d_nchildren > N;
   }
 
-  ev_iterator ev_end() {
-    return d_children.u_arr + d_nchildren;
+  bool evNeedsToBeAllocated() {
+    return d_ev->d_nchildren == d_size;
   }
 
-  NodeBuilder& reset(const ExprValue*);
+  // realloc in the default way
+  void realloc();
+
+  // realloc to a specific size
+  void realloc(size_t toSize, bool copy = true);
+
+  void allocateEvIfNecessaryForAppend() {
+    if(EXPECT_FALSE( evNeedsToBeAllocated() )) {
+      realloc();
+    }
+  }
 
 public:
 
-  NodeBuilder();
-  NodeBuilder(Kind k);
-  NodeBuilder(const Node&);
-  NodeBuilder(const NodeBuilder&);
+  inline NodeBuilder();
+  inline NodeBuilder(Kind k);
+  inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb);
+  template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
+  inline NodeBuilder(NodeManager* nm);
+  inline NodeBuilder(NodeManager* nm, Kind k);
+  inline ~NodeBuilder();
 
-  NodeBuilder(NodeManager*);
-  NodeBuilder(NodeManager*, Kind k);
-  NodeBuilder(NodeManager*, const Node&);
-  NodeBuilder(NodeManager*, const NodeBuilder&);
+  typedef NodeValue::ev_iterator iterator;
+  typedef NodeValue::const_ev_iterator const_iterator;
 
-  ~NodeBuilder();
+  iterator begin() { return d_ev->ev_begin(); }
+  iterator end() { return d_ev->ev_end(); }
+  const_iterator begin() const { return d_ev->ev_begin(); }
+  const_iterator end() const { return d_ev->ev_end(); }
 
   // Compound expression constructors
+  /*
   NodeBuilder& eqExpr(const Node& right);
   NodeBuilder& notExpr();
   NodeBuilder& andExpr(const Node& right);
@@ -84,230 +106,413 @@ public:
   NodeBuilder& iffExpr(const Node& right);
   NodeBuilder& impExpr(const Node& right);
   NodeBuilder& xorExpr(const Node& right);
+  */
 
-  /* TODO design: these modify NodeBuilder */
+  /* 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);  }
+  */
+
+  /*
+  NodeBuilder& operator&&=(const Node& right) { return andExpr(right); }
+  NodeBuilder& operator||=(const Node& right) { return orExpr(right);  }
+  */
 
   // "Stream" expression constructor syntax
-  NodeBuilder& operator<<(const Kind& op);
-  NodeBuilder& operator<<(const Node& child);
+
+  NodeBuilder& operator<<(const Kind& k) {
+    Assert(d_ev->d_kind == UNDEFINED_KIND);
+    d_ev->d_kind = k;
+    return *this;
+  }
+
+  NodeBuilder& operator<<(const Node& n) {
+    return append(n);
+  }
 
   // For pushing sequences of children
-  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 Node();// not const
-
-  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;
+  NodeBuilder& append(const std::vector<Node>& children) {
+    return append(children.begin(), children.end());
+  }
+
+  NodeBuilder& append(const Node& n) {
+    allocateEvIfNecessaryForAppend();
+    NodeValue* ev = n.d_ev;
+    d_hash = NodeValue::computeHash(d_hash, ev);
+    ev->inc();
+    d_ev->d_children[d_ev->d_nchildren++] = ev;
+    return *this;
+  }
+
+  template <class Iterator>
+  NodeBuilder& append(const Iterator& begin, const Iterator& end) {
+    for(Iterator i = begin; i != end; ++i) {
+      append(*i);
+    }
+    return *this;
+  }
+
+  void crop() {
+    if(EXPECT_FALSE( evIsAllocated() ) && d_size > d_ev->d_nchildren) {
+      d_ev = (NodeValue*)
+        std::realloc(d_ev, sizeof(NodeValue) +
+                     ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) ));
+    }
+  }
+
+  // not const
+  operator Node();
+
+  /*
+  AndNodeBuilder   operator&&(Node);
+  OrNodeBuilder    operator||(Node);
+  PlusNodeBuilder  operator+ (Node);
+  PlusNodeBuilder  operator- (Node);
+  MultNodeBuilder  operator* (Node);
+
+  friend class AndNodeBuilder;
+  friend class OrNodeBuilder;
+  friend class PlusNodeBuilder;
+  friend class MultNodeBuilder;
+  */
 };/* class NodeBuilder */
 
-class AndExprBuilder {
+#if 0
+class AndNodeBuilder {
   NodeBuilder d_eb;
 
 public:
 
-  AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+  AndNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != AND) {
       d_eb.collapse();
       d_eb.d_kind = AND;
     }
   }
 
-  AndExprBuilder&   operator&&(Node);
-  OrExprBuilder     operator||(Node);
+  AndNodeBuilder&   operator&&(Node);
+  OrNodeBuilder     operator||(Node);
 
   operator NodeBuilder() { return d_eb; }
 
-};/* class AndExprBuilder */
+};/* class AndNodeBuilder */
 
-class OrExprBuilder {
+class OrNodeBuilder {
   NodeBuilder d_eb;
 
 public:
 
-  OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+  OrNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != OR) {
       d_eb.collapse();
       d_eb.d_kind = OR;
     }
   }
 
-  AndExprBuilder    operator&&(Node);
-  OrExprBuilder&    operator||(Node);
+  AndNodeBuilder    operator&&(Node);
+  OrNodeBuilder&    operator||(Node);
 
   operator NodeBuilder() { return d_eb; }
 
-};/* class OrExprBuilder */
+};/* class OrNodeBuilder */
 
-class PlusExprBuilder {
+class PlusNodeBuilder {
   NodeBuilder d_eb;
 
 public:
 
-  PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+  PlusNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != PLUS) {
       d_eb.collapse();
       d_eb.d_kind = PLUS;
     }
   }
 
-  PlusExprBuilder&  operator+(Node);
-  PlusExprBuilder&  operator-(Node);
-  MultExprBuilder   operator*(Node);
+  PlusNodeBuilder&  operator+(Node);
+  PlusNodeBuilder&  operator-(Node);
+  MultNodeBuilder   operator*(Node);
 
   operator NodeBuilder() { return d_eb; }
 
-};/* class PlusExprBuilder */
+};/* class PlusNodeBuilder */
 
-class MultExprBuilder {
+class MultNodeBuilder {
   NodeBuilder d_eb;
 
 public:
 
-  MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) {
+  MultNodeBuilder(const NodeBuilder& eb) : d_eb(eb) {
     if(d_eb.d_kind != MULT) {
       d_eb.collapse();
       d_eb.d_kind = MULT;
     }
   }
 
-  PlusExprBuilder   operator+(Node);
-  PlusExprBuilder   operator-(Node);
-  MultExprBuilder&  operator*(Node);
+  PlusNodeBuilder   operator+(Node);
+  PlusNodeBuilder   operator-(Node);
+  MultNodeBuilder&  operator*(Node);
 
   operator NodeBuilder() { return d_eb; }
 
-};/* class MultExprBuilder */
-
-template <class Iterator>
-inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) {
-  for(Iterator i = begin; i != end; ++i)
-    addChild(*i);
-  return *this;
-}
-
-// not const
-inline NodeBuilder::operator Node() {
-  ExprValue *ev;
-  uint64_t hash;
-
-  Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!");
+};/* class MultNodeBuilder */
 
-  // variables are permitted to be duplicates (from POV of the expression manager)
-  if(d_kind == VARIABLE) {
-    ev = new ExprValue;
-    ev->d_kind = d_kind;
-    ev->d_id = ExprValue::next_id++;// FIXME multithreading
-    return Node(ev);
-  } 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(Node));
-      ev = new (space) ExprValue;
-      size_t nc = 0;
-      ev_iterator i = ev_begin();
-      ev_iterator i_end = ev_end();
-      for(; i != i_end; ++i) {
-        // The expressions in the allocated children are all 0, so we must
-        // construct it without using an assignment operator
-        ev->d_children[nc++].assignExprValue(*i);
-      }
-    } else {
-      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<Node>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
-        ev->d_children[nc++] = Node(*i);
-    }
-  }
-
-  ev->d_nchildren = d_nchildren;
-  ev->d_kind = d_kind;
-  ev->d_id = ExprValue::next_id++;// FIXME multithreading
-  ev->d_rc = 0;
-  Node e(ev);
-
-  return d_em->lookup(hash, e);
-}
-
-inline AndExprBuilder   NodeBuilder::operator&&(Node e) {
-  return AndExprBuilder(*this) && e;
+inline AndNodeBuilder   NodeBuilder::operator&&(Node e) {
+  return AndNodeBuilder(*this) && e;
 }
 
-inline OrExprBuilder    NodeBuilder::operator||(Node e) {
-  return OrExprBuilder(*this) || e;
+inline OrNodeBuilder    NodeBuilder::operator||(Node e) {
+  return OrNodeBuilder(*this) || e;
 }
 
-inline PlusExprBuilder  NodeBuilder::operator+ (Node e) {
-  return PlusExprBuilder(*this) + e;
+inline PlusNodeBuilder  NodeBuilder::operator+ (Node e) {
+  return PlusNodeBuilder(*this) + e;
 }
 
-inline PlusExprBuilder  NodeBuilder::operator- (Node e) {
-  return PlusExprBuilder(*this) - e;
+inline PlusNodeBuilder  NodeBuilder::operator- (Node e) {
+  return PlusNodeBuilder(*this) - e;
 }
 
-inline MultExprBuilder  NodeBuilder::operator* (Node e) {
-  return MultExprBuilder(*this) * e;
+inline MultNodeBuilder  NodeBuilder::operator* (Node e) {
+  return MultNodeBuilder(*this) * e;
 }
 
-inline AndExprBuilder&  AndExprBuilder::operator&&(Node e) {
+inline AndNodeBuilder&  AndNodeBuilder::operator&&(Node e) {
   d_eb.append(e);
   return *this;
 }
 
-inline OrExprBuilder    AndExprBuilder::operator||(Node e) {
-  return OrExprBuilder(d_eb.collapse()) || e;
+inline OrNodeBuilder    AndNodeBuilder::operator||(Node e) {
+  return OrNodeBuilder(d_eb.collapse()) || e;
 }
 
-inline AndExprBuilder   OrExprBuilder::operator&&(Node e) {
-  return AndExprBuilder(d_eb.collapse()) && e;
+inline AndNodeBuilder   OrNodeBuilder::operator&&(Node e) {
+  return AndNodeBuilder(d_eb.collapse()) && e;
 }
 
-inline OrExprBuilder&   OrExprBuilder::operator||(Node e) {
+inline OrNodeBuilder&   OrNodeBuilder::operator||(Node e) {
   d_eb.append(e);
   return *this;
 }
 
-inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) {
+inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) {
   d_eb.append(e);
   return *this;
 }
 
-inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) {
+inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) {
   d_eb.append(e.uMinusExpr());
   return *this;
 }
 
-inline MultExprBuilder  PlusExprBuilder::operator*(Node e) {
-  return MultExprBuilder(d_eb.collapse()) * e;
+inline MultNodeBuilder  PlusNodeBuilder::operator*(Node e) {
+  return MultNodeBuilder(d_eb.collapse()) * e;
 }
 
-inline PlusExprBuilder  MultExprBuilder::operator+(Node e) {
-  return MultExprBuilder(d_eb.collapse()) + e;
+inline PlusNodeBuilder  MultNodeBuilder::operator+(Node e) {
+  return MultNodeBuilder(d_eb.collapse()) + e;
 }
 
-inline PlusExprBuilder  MultExprBuilder::operator-(Node e) {
-  return MultExprBuilder(d_eb.collapse()) - e;
+inline PlusNodeBuilder  MultNodeBuilder::operator-(Node e) {
+  return MultNodeBuilder(d_eb.collapse()) - e;
 }
 
-inline MultExprBuilder& MultExprBuilder::operator*(Node e) {
+inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) {
   d_eb.append(e);
   return *this;
 }
 
+#endif /* 0 */
+
+}/* CVC4 namespace */
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+
+// template implementations
+
+namespace CVC4 {
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder() :
+  d_size(nchild_thresh),
+  d_nm(NodeManager::currentNM()),
+  d_used(false),
+  d_ev(&d_inlineEv),
+  d_inlineEv(0),
+  d_childrenStorage(0) {}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) :
+  d_size(nchild_thresh),
+  d_nm(NodeManager::currentNM()),
+  d_used(false),
+  d_ev(&d_inlineEv),
+  d_inlineEv(0),
+  d_childrenStorage(0) {
+
+  d_inlineEv.d_kind = k;
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) :
+  d_size(nchild_thresh),
+  d_nm(nb.d_nm),
+  d_used(nb.d_used),
+  d_ev(&d_inlineEv),
+  d_inlineEv(0),
+  d_childrenStorage(0) {
+
+  if(evIsAllocated(nb)) {
+    realloc(nb->d_size, false);
+    std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+  } else {
+    std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+  }
+}
+
+template <unsigned nchild_thresh>
+template <unsigned N>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) :
+  d_size(nchild_thresh),
+  d_nm(NodeManager::currentNM()),
+  d_used(nb.d_used),
+  d_ev(&d_inlineEv),
+  d_inlineEv(0),
+  d_childrenStorage(0) {
+
+  if(nb.d_ev->d_nchildren > nchild_thresh) {
+    realloc(nb.d_size, false);
+    std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end());
+  } else {
+    std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end());
+  }
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) :
+  d_size(nchild_thresh),
+  d_nm(nm),
+  d_used(false),
+  d_ev(&d_inlineEv),
+  d_inlineEv(0),
+  d_childrenStorage(0) {}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) :
+  d_size(nchild_thresh),
+  d_nm(nm),
+  d_used(false),
+  d_ev(&d_inlineEv),
+  d_inlineEv(0),
+  d_childrenStorage() {
+
+  d_inlineEv.d_kind = k;
+}
+
+template <unsigned nchild_thresh>
+inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
+  for(iterator i = begin();
+      i != end();
+      ++i) {
+    (*i)->dec();
+  }
+  if(evIsAllocated()) {
+    free(d_ev);
+  }
+}
+
+template <unsigned nchild_thresh>
+void NodeBuilder<nchild_thresh>::realloc() {
+  if(EXPECT_FALSE( evIsAllocated() )) {
+    d_ev = (NodeValue*)
+      std::realloc(d_ev,
+                   sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) ));
+  } else {
+    d_ev = (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_ev->d_children,
+              d_inlineEv.d_children,
+              d_inlineEv.d_children + nchild_thresh);
+  }
+}
+
+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) +
+                   ( sizeof(NodeValue*) * (d_size = toSize) ));
+  } else {
+    d_ev = (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;
+    if(copy) {
+      std::copy(d_ev->d_children,
+                d_inlineEv.d_children,
+                d_inlineEv.d_children + nchild_thresh);
+    }
+  }
+}
+
+template <unsigned nchild_thresh>
+NodeBuilder<nchild_thresh>::operator Node() {// not const
+  Assert(d_ev->d_kind != UNDEFINED_KIND,
+         "Can't make an expression of an undefined kind!");
+  Assert(! d_used, "This NodeBuilder has already been used!");
+
+  // implementation differs depending on whether the expression value
+  // was malloc'ed or not
+
+  if(EXPECT_FALSE( evIsAllocated() )) {
+    NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev);
+    if(ev != d_ev) {
+      // expression already exists in node manager
+      return Node(ev);
+    }
+
+    // otherwise create the canonical expression value for this node
+    crop();
+    d_used = true;
+    ev = d_ev;
+    d_ev = NULL;
+    // this inserts into the NodeManager;
+    // return the result of lookup() in case another thread beat us to it
+    return d_nm->lookup(d_hash, ev);
+  }
+
+  NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv);
+  if(ev != &d_inlineEv) {
+    // expression already exists in node manager
+    return Node(ev);
+  }
+
+  // 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_ev->d_nchildren;
+  ev->d_kind = d_ev->d_kind;
+  ev->d_id = NodeValue::next_id++;// FIXME multithreading
+  ev->d_rc = 0;
+  d_used = true;
+  d_ev = NULL;
+
+  // this inserts into the NodeManager;
+  // return the result of lookup() in case another thread beat us to it
+  return d_nm->lookup(d_hash, ev);
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8da87c9eb..ab52b9f40 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_manager.cpp
+/** node_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
@@ -18,76 +18,116 @@ 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!");
+Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
+  Assert(this != NULL, "Whoops, we have a bad expression manager!");
   hash_t::iterator i = d_hash.find(hash);
   if(i == d_hash.end()) {
     // insert
     std::vector<Node> v;
+    Node e(ev);
     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())
+      if(ev->getKind() != j->getKind()) {
         continue;
+      }
 
-      if(e.numChildren() != j->numChildren())
+      if(ev->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)
+      NodeValue::const_iterator c1 = ev->ev_begin();
+      NodeValue::iterator c2 = j->d_ev->ev_begin();
+      for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
+        if((*c1).d_ev != (*c2).d_ev) {
           break;
+        }
       }
 
-      if(c1 != e.end() || c2 != j->end())
+      if(c1 != ev->ev_end() || c2 != j->end()) {
         continue;
+      }
 
       return *j;
     }
     // didn't find it, insert
     std::vector<Node> v;
+    Node e(ev);
     v.push_back(e);
     d_hash.insert(std::make_pair(hash, v));
     return e;
   }
 }
 
+NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
+  Assert(this != NULL, "Whoops, we have a bad expression manager!");
+  hash_t::iterator i = d_hash.find(hash);
+  if(i == d_hash.end()) {
+    return NULL;
+  } else {
+    for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
+      if(ev->getKind() != j->getKind()) {
+        continue;
+      }
+
+      if(ev->numChildren() != j->numChildren()) {
+        continue;
+      }
+
+      NodeValue::const_iterator c1 = ev->ev_begin();
+      NodeValue::iterator c2 = j->d_ev->ev_begin();
+      for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
+        if((*c1).d_ev != (*c2).d_ev) {
+          break;
+        }
+      }
+
+      if(c1 != ev->ev_end() || c2 != j->end()) {
+        continue;
+      }
+
+      return j->d_ev;
+    }
+    // didn't find it
+    return 0;
+  }
+}
+
 // general expression-builders
 
 Node NodeManager::mkExpr(Kind kind) {
-  return NodeBuilder(this, kind);
+  return NodeBuilder<>(this, kind);
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1) {
-  return NodeBuilder(this, kind) << child1;
+  return NodeBuilder<>(this, kind) << child1;
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
-  return NodeBuilder(this, kind) << child1 << 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;
+  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;
+  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;
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
 }
 
 // N-ary version
 Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
-  return NodeBuilder(this, kind).append(children);
+  return NodeBuilder<>(this, kind).append(children);
 }
 
 Node NodeManager::mkVar() {
-  return NodeBuilder(this, VARIABLE);
+  return NodeBuilder<>(this, VARIABLE);
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6c20b29e8..3a28a22ff 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -20,22 +20,20 @@
 
 namespace CVC4 {
 
-namespace expr {
-  class ExprBuilder;
-}/* CVC4::expr namespace */
-
 class NodeManager {
   static __thread NodeManager* s_current;
 
-  friend class CVC4::NodeBuilder;
+  template <unsigned> friend class CVC4::NodeBuilder;
 
   typedef std::map<uint64_t, std::vector<Node> > hash_t;
   hash_t d_hash;
 
-  Node lookup(uint64_t hash, const Node& e);
+  Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); }
+  Node lookup(uint64_t hash, NodeValue* e);
+  NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e);
 
 public:
-  static NodeManager* currentEM() { return s_current; }
+  static NodeManager* currentNM() { return s_current; }
 
   // general expression-builders
   Node mkExpr(Kind kind);
@@ -50,20 +48,20 @@ public:
   // variables are special, because duplicates are permitted
   Node mkVar();
 
-  // TODO: these use the current EM (but must be renamed)
+  // TODO: these use the current NM (but must be renamed)
   /*
   static Node mkExpr(Kind kind)
-  { currentEM()->mkExpr(kind); }
+  { currentNM()->mkExpr(kind); }
   static Node mkExpr(Kind kind, Node child1);
-  { currentEM()->mkExpr(kind, child1); }
+  { currentNM()->mkExpr(kind, child1); }
   static Node mkExpr(Kind kind, Node child1, Node child2);
-  { currentEM()->mkExpr(kind, child1, child2); }
+  { currentNM()->mkExpr(kind, child1, child2); }
   static Node mkExpr(Kind kind, Node child1, Node child2, Node child3);
-  { currentEM()->mkExpr(kind, child1, child2, child3); }
+  { currentNM()->mkExpr(kind, child1, child2, child3); }
   static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4);
-  { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
+  { currentNM()->mkExpr(kind, child1, child2, child3, child4); }
   static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5);
-  { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
+  { currentNM()->mkExpr(kind, child1, child2, child3, child4, child5); }
   */
 
   // do we want a varargs one?  perhaps not..
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
new file mode 100644
index 000000000..7af2cd2b5
--- /dev/null
+++ b/src/expr/node_value.cpp
@@ -0,0 +1,147 @@
+/*********************                                           -*- C++ -*-  */
+/** node_value.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.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Node rather than by pointer; cvc4::Node maintains the
+ ** reference count on NodeValue instances and
+ **/
+
+#include "node_value.h"
+#include <sstream>
+
+using namespace std;
+
+namespace CVC4 {
+
+size_t NodeValue::next_id = 1;
+
+NodeValue::NodeValue() :
+  d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) {
+}
+
+NodeValue::NodeValue(int) :
+  d_id(0), d_rc(0), d_kind(unsigned(UNDEFINED_KIND)), d_nchildren(0) {
+}
+
+NodeValue::~NodeValue() {
+  for(ev_iterator i = ev_begin(); i != ev_end(); ++i) {
+    (*i)->dec();
+  }
+}
+
+uint64_t NodeValue::hash() const {
+  return computeHash(d_kind, ev_begin(), ev_end());
+}
+
+NodeValue* NodeValue::inc() {
+  // FIXME multithreading
+  if(d_rc < MAX_RC)
+    ++d_rc;
+  return this;
+}
+
+NodeValue* NodeValue::dec() {
+  // FIXME multithreading
+  if(d_rc < MAX_RC) {
+    if(--d_rc == 0) {
+      // FIXME gc
+      return 0;
+    }
+  }
+  return this;
+}
+
+NodeValue::iterator NodeValue::begin() {
+  return node_iterator(d_children);
+}
+
+NodeValue::iterator NodeValue::end() {
+  return node_iterator(d_children + d_nchildren);
+}
+
+NodeValue::iterator NodeValue::rbegin() {
+  return node_iterator(d_children + d_nchildren - 1);
+}
+
+NodeValue::iterator NodeValue::rend() {
+  return node_iterator(d_children - 1);
+}
+
+NodeValue::const_iterator NodeValue::begin() const {
+  return const_node_iterator(d_children);
+}
+
+NodeValue::const_iterator NodeValue::end() const {
+  return const_node_iterator(d_children + d_nchildren);
+}
+
+NodeValue::const_iterator NodeValue::rbegin() const {
+  return const_node_iterator(d_children + d_nchildren - 1);
+}
+
+NodeValue::const_iterator NodeValue::rend() const {
+  return const_node_iterator(d_children - 1);
+}
+
+NodeValue::ev_iterator NodeValue::ev_begin() {
+  return d_children;
+}
+
+NodeValue::ev_iterator NodeValue::ev_end() {
+  return d_children + d_nchildren;
+}
+
+NodeValue::ev_iterator NodeValue::ev_rbegin() {
+  return d_children + d_nchildren - 1;
+}
+
+NodeValue::ev_iterator NodeValue::ev_rend() {
+  return d_children - 1;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_begin() const {
+  return d_children;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_end() const {
+  return d_children + d_nchildren;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_rbegin() const {
+  return d_children + d_nchildren - 1;
+}
+
+NodeValue::const_ev_iterator NodeValue::ev_rend() const {
+  return d_children - 1;
+}
+
+string NodeValue::toString() const {
+  stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
+void NodeValue::toStream(std::ostream& out) const {
+  out << "(" << Kind(d_kind);
+  if(d_kind == VARIABLE) {
+    out << ":" << this;
+  } else {
+    for(const_iterator i = begin(); i != end(); ++i) {
+      if(i != end()) {
+        out << " ";
+      }
+      out << *i;
+    }
+  }
+  out << ")";
+}
+
+}/* CVC4 namespace */
diff --git a/src/expr/expr_value.h b/src/expr/node_value.h
index 25fada4af..9bdbb7f8c 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/node_value.h
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_value.h
+/** node_value.h
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,15 +11,15 @@
  **
  ** Instances of this class are generally referenced through
  ** cvc4::Node rather than by pointer; cvc4::Node maintains the
- ** reference count on ExprValue instances and
+ ** reference count on NodeValue instances and
  **/
 
-/* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */
+/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */
 /* to resolve a circular dependency */
-#include "expr/node.h"
+//#include "expr/node.h"
 
-#ifndef __CVC4__EXPR__EXPR_VALUE_H
-#define __CVC4__EXPR__EXPR_VALUE_H
+#ifndef __CVC4__EXPR__NODE_VALUE_H
+#define __CVC4__EXPR__NODE_VALUE_H
 
 #include "cvc4_config.h"
 #include <stdint.h>
@@ -30,17 +30,18 @@
 namespace CVC4 {
 
 class Node;
-class NodeBuilder;
+template <unsigned> class NodeBuilder;
+class NodeManager;
 
 namespace expr {
 
 /**
- * This is an ExprValue.
+ * This is an NodeValue.
  */
-class ExprValue {
+class NodeValue {
 
   /** A convenient null-valued expression value */
-  static ExprValue s_null;
+  static NodeValue s_null;
 
   /** Maximum reference count possible.  Used for sticky
    *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
@@ -61,25 +62,32 @@ class ExprValue {
   unsigned d_nchildren : 16;
 
   /** Variable number of child nodes */
-  Node     d_children[0];
+  NodeValue *d_children[0];
 
   // todo add exprMgr ref in debug case
 
   friend class CVC4::Node;
-  friend class CVC4::NodeBuilder;
+  template <unsigned> friend class CVC4::NodeBuilder;
+  friend class CVC4::NodeManager;
 
-  ExprValue* inc();
-  ExprValue* dec();
+  NodeValue* inc();
+  NodeValue* dec();
 
   static size_t next_id;
 
   /** Private default constructor for the null value. */
-  ExprValue();
+  NodeValue();
+
+  /** Private default constructor for the NodeBuilder. */
+  NodeValue(int);
+
+  /** Destructor decrements the ref counts of its children */
+  ~NodeValue();
 
   /**
    * Computes the hash over the given iterator span of children, and the
    * root hash. The iterator should be either over a range of Node or pointers
-   * to ExprValue.
+   * to NodeValue.
    * @param hash the initial value for the hash
    * @param begin the begining of the range
    * @param end the end of the range
@@ -87,11 +95,55 @@ class ExprValue {
    */
   template<typename const_iterator_type>
   static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
-    for(const_iterator_type i = begin; i != end; ++i)
-      hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->getId();
+    for(const_iterator_type i = begin; i != end; ++i) {
+      hash = computeHash(hash, *i);
+    }
     return hash;
   }
 
+  static uint64_t computeHash(uint64_t hash, const NodeValue* ev) {
+    return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId();
+  }
+
+  typedef NodeValue** ev_iterator;
+  typedef NodeValue const* const* const_ev_iterator;
+
+  ev_iterator ev_begin();
+  ev_iterator ev_end();
+  ev_iterator ev_rbegin();
+  ev_iterator ev_rend();
+
+  const_ev_iterator ev_begin() const;
+  const_ev_iterator ev_end() const;
+  const_ev_iterator ev_rbegin() const;
+  const_ev_iterator ev_rend() const;
+
+  class node_iterator {
+    const_ev_iterator d_i;
+  public:
+    node_iterator(const_ev_iterator i) : d_i(i) {}
+
+    inline Node operator*();
+
+    bool operator==(const node_iterator& i) {
+      return d_i == i.d_i;
+    }
+
+    bool operator!=(const node_iterator& i) {
+      return d_i != i.d_i;
+    }
+
+    node_iterator& operator++() {
+      ++d_i;
+      return *this;
+    }
+
+    node_iterator operator++(int) {
+      return node_iterator(d_i++);
+    }
+  };
+  typedef node_iterator const_node_iterator;
+
 public:
   /** Hash this expression.
    *  @return the hash value of this expression. */
@@ -99,8 +151,8 @@ public:
 
   // Iterator support
 
-  typedef Node* iterator;
-  typedef Node const* const_iterator;
+  typedef node_iterator iterator;
+  typedef node_iterator const_iterator;
 
   iterator begin();
   iterator end();
@@ -113,7 +165,8 @@ public:
   const_iterator rend() const;
 
   unsigned getId() const { return d_id; }
-  unsigned getKind() const { return (Kind) d_kind; }
+  Kind getKind() const { return (Kind) d_kind; }
+  unsigned numChildren() const { return d_nchildren; }
   std::string toString() const;
   void toStream(std::ostream& out) const;
 };
@@ -121,4 +174,16 @@ public:
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__EXPR__EXPR_VALUE_H */
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+inline Node NodeValue::node_iterator::operator*() {
+  return Node(*d_i);
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__NODE_VALUE_H */
diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h
index a42ae28fb..f1877781f 100644
--- a/src/include/cvc4_config.h
+++ b/src/include/cvc4_config.h
@@ -10,6 +10,9 @@
  ** [[ Add file-specific comments here ]]
  **/
 
+#ifndef __CVC4_CONFIG_H
+#define __CVC4_CONFIG_H
+
 #if defined _WIN32 || defined __CYGWIN__
 #  ifdef BUILDING_DLL
 #    ifdef __GNUC__
@@ -35,3 +38,9 @@
 #define EXPECT_TRUE(x) __builtin_expect( (x), true)
 #define EXPECT_FALSE(x) __builtin_expect( (x), false)
 #define NORETURN __attribute__ ((noreturn))
+
+#ifndef NULL
+#  define NULL ((void*) 0)
+#endif
+
+#endif /* __CVC4_CONFIG_H */
diff --git a/src/main/Makefile b/src/main/Makefile
new file mode 100644
index 000000000..686674906
--- /dev/null
+++ b/src/main/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/main
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 6b8ea928c..f5b76fcfb 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -1,6 +1,6 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS =
 
 bin_PROGRAMS = cvc4
 
diff --git a/src/main/Makefile.in b/src/main/Makefile.in
index ba924109e..26ea81859 100644
--- a/src/main/Makefile.in
+++ b/src/main/Makefile.in
@@ -106,6 +106,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -217,9 +218,10 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = 
 cvc4_SOURCES = \
 	main.cpp \
 	getopt.cpp \
diff --git a/src/parser/Makefile b/src/parser/Makefile
new file mode 100644
index 000000000..1ea7edf5d
--- /dev/null
+++ b/src/parser/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/parser
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index e54d4aa2d..7f1ddce1f 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -15,9 +15,10 @@
 LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
 LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
 
-INCLUDES = -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 SUBDIRS = smt cvc
 
diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in
index b2e066f8d..859329834 100644
--- a/src/parser/Makefile.in
+++ b/src/parser/Makefile.in
@@ -168,6 +168,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -296,9 +297,11 @@ top_srcdir = @top_srcdir@
 #
 LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@
 LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES)
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 SUBDIRS = smt cvc
 nobase_lib_LTLIBRARIES = libcvc4parser.la
 libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS)
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 2d3033a59..1baaf2139 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -133,10 +133,10 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
                                  LT(0).get()->getColumn());
 }
 
-Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
-    Kind>& kinds) {
+Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs,
+                                       const vector<Kind>& kinds) {
   Assert( exprs.size() > 0, "Expected non-empty vector expr");
-  Assert( vectors.size() + 1 == exprs.size(), "Expected kinds to match exprs");
+  Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs");
   return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
 }
 
diff --git a/src/parser/cvc/Makefile b/src/parser/cvc/Makefile
new file mode 100644
index 000000000..c91554a47
--- /dev/null
+++ b/src/parser/cvc/Makefile
@@ -0,0 +1,5 @@
+topdir = ../../..
+srcdir = src/parser/cvc
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index 6fb9689de..666c408cf 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 noinst_LTLIBRARIES = libparsercvc.la
 
diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in
index cbab2fd5c..57db98f0b 100644
--- a/src/parser/cvc/Makefile.in
+++ b/src/parser/cvc/Makefile.in
@@ -108,6 +108,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -219,9 +220,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 noinst_LTLIBRARIES = libparsercvc.la
 ANTLR_TOKEN_STUFF = \
 	@srcdir@/generated/CvcVocabularyTokenTypes.hpp \
diff --git a/src/parser/smt/Makefile b/src/parser/smt/Makefile
new file mode 100644
index 000000000..aa3e74236
--- /dev/null
+++ b/src/parser/smt/Makefile
@@ -0,0 +1,5 @@
+topdir = ../../..
+srcdir = src/parser/smt
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index c3273f501..6f5f1bfd4 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 
 noinst_LTLIBRARIES = libparsersmt.la
 
diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in
index 281d2152b..2e9350486 100644
--- a/src/parser/smt/Makefile.in
+++ b/src/parser/smt/Makefile.in
@@ -108,6 +108,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -219,9 +220,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4PARSERLIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB
 noinst_LTLIBRARIES = libparsersmt.la
 ANTLR_TOKEN_STUFF = \
 	@srcdir@/generated/SmtVocabularyTokenTypes.hpp \
diff --git a/src/prop/Makefile b/src/prop/Makefile
new file mode 100644
index 000000000..79fe1084b
--- /dev/null
+++ b/src/prop/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/prop
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 715e79d16..3473de30f 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libprop.la
 
diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in
index 6d4e7f0b5..311d3f8c7 100644
--- a/src/prop/Makefile.in
+++ b/src/prop/Makefile.in
@@ -142,6 +142,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -253,9 +254,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libprop.la
 libprop_la_SOURCES = \
 	prop_engine.cpp \
diff --git a/src/prop/minisat/Makefile b/src/prop/minisat/Makefile
new file mode 100644
index 000000000..49512a1cd
--- /dev/null
+++ b/src/prop/minisat/Makefile
@@ -0,0 +1,5 @@
+topdir = ../../..
+srcdir = src/prop/minisat
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am
index f066f8669..609c25dd7 100644
--- a/src/prop/minisat/Makefile.am
+++ b/src/prop/minisat/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in
index a2cc36300..a54518c74 100644
--- a/src/prop/minisat/Makefile.in
+++ b/src/prop/minisat/Makefile.in
@@ -104,6 +104,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -215,9 +216,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libminisat.la
 libminisat_la_SOURCES = \
 	core/Solver.C \
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 166546a2c..caf87428b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -34,7 +34,7 @@ void PropEngine::addVars(Node e) {
   Debug("prop") << "adding vars to " << e << endl;
   for(Node::iterator i = e.begin(); i != e.end(); ++i) {
     Debug("prop") << "expr " << *i << endl;
-    if(i->getKind() == VARIABLE) {
+    if((*i).getKind() == VARIABLE) {
       if(d_vars.find(*i) == d_vars.end()) {
         Var v = d_sat.newVar();
         Debug("prop") << "adding var " << *i << " <--> " << v << endl;
diff --git a/src/smt/Makefile b/src/smt/Makefile
new file mode 100644
index 000000000..84a43ff39
--- /dev/null
+++ b/src/smt/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/smt
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index b3637b6d9..bd75bacab 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libsmt.la
 
diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in
index 7c60db89b..9647e51b9 100644
--- a/src/smt/Makefile.in
+++ b/src/smt/Makefile.in
@@ -104,6 +104,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -215,9 +216,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libsmt.la
 libsmt_la_SOURCES = \
 	smt_engine.cpp \
diff --git a/src/theory/Makefile b/src/theory/Makefile
new file mode 100644
index 000000000..2a4a03491
--- /dev/null
+++ b/src/theory/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/theory
+builddir = $(topdir)/$(builds)/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index f8e9908c9..4eba7811c 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libtheory.la
 
diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in
index 7af3f957c..d37387741 100644
--- a/src/theory/Makefile.in
+++ b/src/theory/Makefile.in
@@ -142,6 +142,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -253,9 +254,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libtheory.la
 libtheory_la_SOURCES = \
 	theory_engine.h \
diff --git a/src/theory/uf/Makefile b/src/theory/uf/Makefile
new file mode 100644
index 000000000..524ff2009
--- /dev/null
+++ b/src/theory/uf/Makefile
@@ -0,0 +1,5 @@
+topdir = ../../..
+srcdir = src/theory/uf
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 11c9f536e..4b36d2fe8 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libuf.la
 
diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in
index 4920e7a0c..dfb8ea932 100644
--- a/src/theory/uf/Makefile.in
+++ b/src/theory/uf/Makefile.in
@@ -90,6 +90,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -201,9 +202,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../../include -I@srcdir@/../..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../../include -I@srcdir@/../..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libuf.la
 libuf_la_SOURCES = 
 all: all-am
diff --git a/src/util/Makefile b/src/util/Makefile
new file mode 100644
index 000000000..0bd2f197b
--- /dev/null
+++ b/src/util/Makefile
@@ -0,0 +1,5 @@
+topdir = ../..
+srcdir = src/util
+builddir = $(topdir)/builds/$(srcdir)
+
+include $(topdir)/Makefile.subdir
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b6c116a6d..316c747de 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -1,6 +1,7 @@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
 noinst_LTLIBRARIES = libutil.la
 
diff --git a/src/util/Makefile.in b/src/util/Makefile.in
index 61768f933..5627e01a9 100644
--- a/src/util/Makefile.in
+++ b/src/util/Makefile.in
@@ -105,6 +105,7 @@ CXX = @CXX@
 CXXCPP = @CXXCPP@
 CXXDEPMODE = @CXXDEPMODE@
 CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
 CXXTESTGEN = @CXXTESTGEN@
 CYGPATH_W = @CYGPATH_W@
 DEFS = @DEFS@
@@ -216,9 +217,11 @@ target_vendor = @target_vendor@
 top_build_prefix = @top_build_prefix@
 top_builddir = @top_builddir@
 top_srcdir = @top_srcdir@
-INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@srcdir@/../include -I@srcdir@/..
+
 AM_CXXFLAGS = -Wall -fvisibility=hidden
-AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 noinst_LTLIBRARIES = libutil.la
 libutil_la_SOURCES = \
 	Assert.h \