PARSER STUFF:

* Other minor changes to the new parser to match coding guidelines,
  add documentation, ....

* Add CFLAGS stuff to configure.ac parser Makefile.ams.  This ensures
  that profiling, coverage, optimization, debugging, and warning
  level options will apply to the new parser as well (which is in C,
  not C++).  This fixes the deprecated warning we were seeing this
  evening.

* Now, if you have ANTLR_HOME set in your environment, you don't need
  to specify --with-antlr-dir to ./configure or have libantlr3c
  installed in standard places.  --with-antlr-dir still overrides
  $ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or
  doesn't work, the standard places are still tried.

* Extend "silent make" to new parser stuff.

* Added src/parser/bounded_token_buffer.{h,cpp} to the list of
  exclusions in contrib/update-copyright.pl and mention them as
  excluded from CVC4 copyright in COPYING.  They are antlr3-derived
  works, covered under a BSD license.

OTHER STUFF:

* expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now
  auto-generated by a "mkexpr" script.  This provides the correct
  instantiations of mkConst() for public use, e.g., by the parser.

* Fix doxygen documentation in expr, expr_manager.. closes bug #35

* Node::isAtomic() implemented in a better way, based on theory kinds
  files.  Fixes bug #40.  To support this, a "nonatomic_operator"
  command has been added.  All other "parameterized" or "operator"
  kinds are atomic.

* Added expr_black test

* Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind
  that takes a "bool" payload; for example, to make "true" you now do
  nodeManager->mkConst(true).

* Make new "cvc4_public.h" and "cvc4parser_public.h" headers.  Private
  headers should include "cvc4_private.h"
  (resp. "cvc4parser_private.h"), which existed previously.  Public
  headers should include the others.  **No one** should include the
  autoheader #include (which has been renamed "cvc4autoconfig.h")
  directly, and public CVC4 headers can't access its #defines.  This
  is to avoid us having the same distribution problem as libantlr3c.

* Preliminary fixes based on Tim's code review of attributes (bug #61).
  This includes splitting hairy template internals into
  attribute_internals.h, for which another code review ticket will be
  opened.  Bug is still outstanding, but pending further
  refactoring/documentation.

* Some *HashFcns renamed to *HashStrategy to match refactoring done
  elsewhere (done by Chris?) earlier this week.

* Simplified creation of make rules for generated files (expr.cpp,
  expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h,
  metakind.h).

* CVC4::Configuration interface and implementation split (so private
  stuff doesn't leak into public headers).

* Some documentation/code formatting fixes.

* Add required versions of autotools to autogen.sh.

* src/expr/mkmetakind: fix a nonportable thing in invocation of "expr"
  that was causing warnings on Red Hat.

* src/context/cdmap.h: add workaround to what appears to be a g++ 4.1
  parsing bug.

19 files changed, 1428 insertions, 934 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 7b34fe431..76f6ef1a4 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -9,19 +9,19 @@ libexpr_la_SOURCES = \
 	node.h \
 	node.cpp \
 	node_builder.h \
-	expr.h \
+	@srcdir@/expr.h \
 	type.h \
 	node_value.h \
 	node_manager.h \
-	expr_manager.h \
+	@srcdir@/expr_manager.h \
 	attribute.h \
 	attribute.cpp \
 	@srcdir@/kind.h \
 	@srcdir@/metakind.h \
 	node_manager.cpp \
-	expr_manager.cpp \
+	@srcdir@/expr_manager.cpp \
 	node_value.cpp \
-	expr.cpp \
+	@srcdir@/expr.cpp \
 	type.cpp \
 	command.h \
 	command.cpp
@@ -29,25 +29,91 @@ libexpr_la_SOURCES = \
 EXTRA_DIST = \
 	@srcdir@/kind.h \
 	@srcdir@/metakind.h \
+	@srcdir@/expr_manager.h \
+	@srcdir@/expr.h \
+	@srcdir@/expr_manager.cpp \
+	@srcdir@/expr.cpp \
 	kind_template.h \
-	metakind_template.h
+	metakind_template.h \
+	expr_manager_template.h \
+	expr_manager_template.cpp \
+	expr_template.h \
+	expr_template.cpp
 
-@srcdir@/kind.h: mkkind kind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/kind.h: kind_template.h mkkind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkkind
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkkind \
-		@srcdir@/kind_template.h \
+		$< \
 		@srcdir@/builtin_kinds \
 		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
-	> @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
+	> $@) || (rm -f $@ && exit 1)
 
-@srcdir@/metakind.h: mkmetakind metakind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/metakind.h: metakind_template.h mkmetakind builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkmetakind
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkmetakind \
-		@srcdir@/metakind_template.h \
+		$< \
 		@srcdir@/builtin_kinds \
 		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
-	> @srcdir@/metakind.h) || (rm -f @srcdir@/metakind.h && exit 1)
+	> $@) || (rm -f $@ && exit 1)
 
-BUILT_SOURCES = @srcdir@/kind.h @srcdir@/metakind.h
-dist-hook: @srcdir@/kind.h @srcdir@/metakind.h
-MAINTAINERCLEANFILES = @srcdir@/kind.h @srcdir@/metakind.h
+@srcdir@/expr.h: expr_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkexpr
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkexpr \
+		$< \
+		@srcdir@/builtin_kinds \
+		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+	> $@) || (rm -f $@ && exit 1)
+
+@srcdir@/expr.cpp: expr_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkexpr
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkexpr \
+		$< \
+		@srcdir@/builtin_kinds \
+		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+	> $@) || (rm -f $@ && exit 1)
+
+@srcdir@/expr_manager.h: expr_manager_template.h mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkexpr
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkexpr \
+		$< \
+		@srcdir@/builtin_kinds \
+		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+	> $@) || (rm -f $@ && exit 1)
+
+@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+	$(AM_V_at)chmod +x @srcdir@/mkexpr
+	$(AM_V_at)mv -f $@ $@~ 2>/dev/null || true
+	$(AM_V_GEN)(@srcdir@/mkexpr \
+		$< \
+		@srcdir@/builtin_kinds \
+		`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+	> $@) || (rm -f $@ && exit 1)
+
+BUILT_SOURCES = \
+	@srcdir@/kind.h \
+	@srcdir@/metakind.h \
+	@srcdir@/expr.h \
+	@srcdir@/expr.cpp \
+	@srcdir@/expr_manager.h \
+	@srcdir@/expr_manager.cpp
+
+dist-hook: \
+	@srcdir@/kind.h \
+	@srcdir@/metakind.h \
+	@srcdir@/expr.h \
+	@srcdir@/expr.cpp \
+	@srcdir@/expr_manager.h \
+	@srcdir@/expr_manager.cpp
+
+MAINTAINERCLEANFILES = \
+	@srcdir@/kind.h \
+	@srcdir@/metakind.h \
+	@srcdir@/expr.h \
+	@srcdir@/expr.cpp \
+	@srcdir@/expr_manager.h \
+	@srcdir@/expr_manager.cpp
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 26cb96646..5e8918133 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -25,29 +25,6 @@ namespace CVC4 {
 namespace expr {
 namespace attr {
 
-/**
- * Search for the NodeValue in all attribute tables and remove it,
- * calling the cleanup function if one is defined.
- */
-template <class T>
-inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
-                                              NodeValue* nv) {
-  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
-    typedef AttributeTraits<T, false> traits_t;
-    typedef AttrHash<T> hash_t;
-    pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
-    if(traits_t::cleanup[id] != NULL) {
-      typename hash_t::iterator i = table.find(pr);
-      if(i != table.end()) {
-        traits_t::cleanup[id]((*i).second);
-        table.erase(pr);
-      }
-    } else {
-      table.erase(pr);
-    }
-  }
-}
-
 void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   d_bools.erase(nv);
   deleteFromTable(d_ints, nv);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index efd33d83b..358755192 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -27,678 +27,22 @@
 #include <string>
 #include <ext/hash_map>
 
-#include "config.h"
 #include "context/cdmap.h"
 #include "expr/node.h"
 #include "expr/type.h"
-
 #include "util/output.h"
 
+// include supporting templates
+#define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+#include "expr/attribute_internals.h"
+#undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+
 namespace CVC4 {
 namespace expr {
-
-// ATTRIBUTE HASH FUNCTIONS ====================================================
-
-namespace attr {
-
-/**
- * A hash function for attribute table keys.  Attribute table keys are
- * pairs, (unique-attribute-id, Node).
- */
-struct AttrHashStrategy {
-  enum { LARGE_PRIME = 32452843ul };
-  std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
-    return p.first * LARGE_PRIME + p.second->getId();
-  }
-};
-
-/**
- * A hash function for boolean-valued attribute table keys; here we
- * don't have to store a pair as the key, because we use a known bit
- * in [0..63] for each attribute
- */
-struct AttrHashBoolStrategy {
-  std::size_t operator()(NodeValue* nv) const {
-    return (size_t)nv->getId();
-  }
-};
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE TYPE MAPPINGS =====================================================
-
-namespace attr {
-
-/**
- * KindValueToTableValueMapping is a compile-time-only mechanism to
- * convert "attribute value types" into "table value types" and back
- * again.
- *
- * Each instantiation <T> is expected to have three members:
- *
- *   typename table_value_type
- *
- *      A type representing the underlying table's value_type for
- *      attribute value type (T).  It may be different from T, e.g. T
- *      could be a pointer-to-Foo, but the underlying table value_type
- *      might be pointer-to-void.
- *
- *   static [convertible-to-table_value_type] convert([convertible-from-T])
- *
- *      Converts a T into a table_value_type.  Used to convert an
- *      attribute value on setting it (and assigning it into the
- *      underlying table).  See notes on specializations of
- *      KindValueToTableValueMapping, below.
- *
- *   static [convertible-to-T] convertBack([convertible-from-table_value_type])
- *
- *      Converts a table_value_type back into a T.  Used to convert an
- *      underlying table value back into the attribute's expected type
- *      when retrieving it from the table.  See notes on
- *      specializations of KindValueToTableValueMapping, below.
- *
- * This general (non-specialized) implementation of the template does
- * nothing.
- */
-template <class T>
-struct KindValueToTableValueMapping {
-  /** Simple case: T == table_value_type */
-  typedef T table_value_type;
-  /** No conversion necessary */
-  inline static T convert(const T& t) { return t; }
-  /** No conversion necessary */
-  inline static T convertBack(const T& t) { return t; }
-};
-
-/**
- * Specialization of KindValueToTableValueMapping<> for pointer-valued
- * attributes.
- */
-template <class T>
-struct KindValueToTableValueMapping<T*> {
-  /** Table's value type is void* */
-  typedef void* table_value_type;
-  /** A simple reinterpret_cast<>() conversion from T* to void* */
-  inline static void* convert(const T* const& t) {
-    return reinterpret_cast<void*>(const_cast<T*>(t));
-  }
-  /** A simple reinterpret_cast<>() conversion from void* to T* */
-  inline static T* convertBack(void* const& t) {
-    return reinterpret_cast<T*>(t);
-  }
-};
-
-/**
- * Specialization of KindValueToTableValueMapping<> for const
- * pointer-valued attributes.
- */
-template <class T>
-struct KindValueToTableValueMapping<const T*> {
-  /** Table's value type is void* */
-  typedef void* table_value_type;
-  /** A simple reinterpret_cast<>() conversion from const T* const to void* */
-  inline static void* convert(const T* const& t) {
-    return reinterpret_cast<void*>(const_cast<T*>(t));
-  }
-  /** A simple reinterpret_cast<>() conversion from const void* const to T* */
-  inline static const T* convertBack(const void* const& t) {
-    return reinterpret_cast<const T*>(t);
-  }
-};
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE HASH TABLES =======================================================
-
-namespace attr {
-
-/**
- * An "AttrHash<value_type>"---the hash table underlying
- * attributes---is simply a mapping of pair<unique-attribute-id, Node>
- * to value_type using our specialized hash function for these pairs.
- */
-template <class value_type>
-struct AttrHash :
-    public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
-                               value_type,
-                               AttrHashStrategy> {
-};
-
-/**
- * In the case of Boolean-valued attributes we have a special
- * "AttrHash<bool>" to pack bits together in words.
- */
-template <>
-class AttrHash<bool> :
-    protected __gnu_cxx::hash_map<NodeValue*,
-                                  uint64_t,
-                                  AttrHashBoolStrategy> {
-
-  /** A "super" type, like in Java, for easy reference below. */
-  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
-
-  /**
-   * BitAccessor allows us to return a bit "by reference."  Of course,
-   * we don't require bit-addressibility supported by the system, we
-   * do it with a complex type.
-   */
-  class BitAccessor {
-
-    uint64_t& d_word;
-
-    unsigned d_bit;
-
-  public:
-
-    BitAccessor(uint64_t& word, unsigned bit) :
-      d_word(word),
-      d_bit(bit) {
-    }
-
-    BitAccessor& operator=(bool b) {
-      if(b) {
-        // set the bit
-        d_word |= (1 << d_bit);
-      } else {
-        // clear the bit
-        d_word &= ~(1 << d_bit);
-      }
-
-      return *this;
-    }
-
-    operator bool() const {
-      return (d_word & (1 << d_bit)) ? true : false;
-    }
-  };
-
-  /**
-   * A (somewhat degenerate) iterator over boolean-valued attributes.
-   * This iterator doesn't support anything except comparison and
-   * dereference.  It's intended just for the result of find() on the
-   * table.
-   */
-  class BitIterator {
-
-    std::pair<NodeValue* const, uint64_t>* d_entry;
-
-    unsigned d_bit;
-
-  public:
-
-    BitIterator() :
-      d_entry(NULL),
-      d_bit(0) {
-    }
-
-    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
-      d_entry(&entry),
-      d_bit(bit) {
-    }
-
-    std::pair<NodeValue* const, BitAccessor> operator*() {
-      return std::make_pair(d_entry->first, BitAccessor(d_entry->second, d_bit));
-    }
-
-    bool operator==(const BitIterator& b) {
-      return d_entry == b.d_entry && d_bit == b.d_bit;
-    }
-  };
-
-  /**
-   * A (somewhat degenerate) const_iterator over boolean-valued
-   * attributes.  This const_iterator doesn't support anything except
-   * comparison and dereference.  It's intended just for the result of
-   * find() on the table.
-   */
-  class ConstBitIterator {
-
-    const std::pair<NodeValue* const, uint64_t>* d_entry;
-
-    unsigned d_bit;
-
-  public:
-
-    ConstBitIterator() :
-      d_entry(NULL),
-      d_bit(0) {
-    }
-
-    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
-      d_entry(&entry),
-      d_bit(bit) {
-    }
-
-    std::pair<NodeValue* const, bool> operator*() {
-      return std::make_pair(d_entry->first, (d_entry->second & (1 << d_bit)) ? true : false);
-    }
-
-    bool operator==(const ConstBitIterator& b) {
-      return d_entry == b.d_entry && d_bit == b.d_bit;
-    }
-  };
-
-public:
-
-  typedef std::pair<uint64_t, NodeValue*> key_type;
-  typedef bool data_type;
-  typedef std::pair<const key_type, data_type> value_type;
-
-  /** an iterator type; see above for limitations */
-  typedef BitIterator iterator;
-  /** a const_iterator type; see above for limitations */
-  typedef ConstBitIterator const_iterator;
-
-  /**
-   * Find the boolean value in the hash table.  Returns something ==
-   * end() if not found.
-   */
-  BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
-    super::iterator i = super::find(k.second);
-    if(i == super::end()) {
-      return BitIterator();
-    }
-    Debug.printf("boolattr",
-                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
-                 &(*i).second,
-                 (unsigned long long)((*i).second),
-                 unsigned(k.first));
-    return BitIterator(*i, k.first);
-  }
-
-  /** The "off the end" iterator */
-  BitIterator end() {
-    return BitIterator();
-  }
-
-  /**
-   * Find the boolean value in the hash table.  Returns something ==
-   * end() if not found.
-   */
-  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
-    super::const_iterator i = super::find(k.second);
-    if(i == super::end()) {
-      return ConstBitIterator();
-    }
-    Debug.printf("boolattr",
-                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
-                 &(*i).second,
-                 (unsigned long long)((*i).second),
-                 unsigned(k.first));
-    return ConstBitIterator(*i, k.first);
-  }
-
-  /** The "off the end" const_iterator */
-  ConstBitIterator end() const {
-    return ConstBitIterator();
-  }
-
-  /**
-   * Access the hash table using the underlying operator[].  Inserts
-   * the key into the table (associated to default value) if it's not
-   * already there.
-   */
-  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
-    uint64_t& word = super::operator[](k.second);
-    return BitAccessor(word, k.first);
-  }
-
-  /**
-   * Delete all flags from the given node.
-   */
-  void erase(NodeValue* nv) {
-    super::erase(nv);
-  }
-
-};/* class AttrHash<bool> */
-
-/**
- * A "CDAttrHash<value_type>"---the hash table underlying
- * attributes---is simply a context-dependent mapping of
- * pair<unique-attribute-id, Node> to value_type using our specialized
- * hash function for these pairs.
- */
-template <class value_type>
-class CDAttrHash :
-    public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>,
-                                value_type,
-                                AttrHashStrategy> {
-public:
-  CDAttrHash(context::Context* ctxt) :
-    context::CDMap<std::pair<uint64_t, NodeValue*>,
-                   value_type,
-                   AttrHashStrategy>(ctxt) {
-  }
-};
-
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-/// FIXME ------ need optimized (packed) specialization of CDAttrHash<bool> ------- FIXME
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE CLEANUP FUNCTIONS =================================================
-
 namespace attr {
 
-/** Default cleanup for unmanaged Attribute<> */
-struct NullCleanupStrategy {
-};/* struct NullCleanupStrategy */
-
-/** Default cleanup for ManagedAttribute<> */
-template <class T>
-struct ManagedAttributeCleanupStrategy {
-};/* struct ManagedAttributeCleanupStrategy<> */
-
-/** Specialization for T* */
-template <class T>
-struct ManagedAttributeCleanupStrategy<T*> {
-  static inline void cleanup(T* p) { delete p; }
-};/* struct ManagedAttributeCleanupStrategy<T*> */
-
-/** Specialization for const T* */
-template <class T>
-struct ManagedAttributeCleanupStrategy<const T*> {
-  static inline void cleanup(const T* p) { delete p; }
-};/* struct ManagedAttributeCleanupStrategy<const T*> */
-
-/**
- * Helper for Attribute<> class below to determine whether a cleanup
- * is defined or not.
- */
-template <class T, class C>
-struct getCleanupStrategy {
-  typedef T value_type;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void fn(typename mapping::table_value_type t) {
-    C::cleanup(mapping::convertBack(t));
-  }
-};/* struct getCleanupStrategy<> */
-
-/**
- * Specialization for NullCleanupStrategy.
- */
-template <class T>
-struct getCleanupStrategy<T, NullCleanupStrategy> {
-  typedef T value_type;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
-
-// out-of-class initialization required (because it's a non-integral type)
-template <class T>
-void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)(typename getCleanupStrategy<T, NullCleanupStrategy>::mapping::table_value_type) = NULL;
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<T>.
- */
-template <class T>
-struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
-  typedef T value_type;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
-
-// out-of-class initialization required (because it's a non-integral type)
-template <class T>
-void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)(typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::mapping::table_value_type) = NULL;
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<T*>.
- */
-template <class T>
-struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
-  typedef T* value_type;
-  typedef ManagedAttributeCleanupStrategy<value_type> C;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void fn(typename mapping::table_value_type t) {
-    C::cleanup(mapping::convertBack(t));
-  }
-};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
-
-/**
- * Specialization for ManagedAttributeCleanupStrategy<const T*>.
- */
-template <class T>
-struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > {
-  typedef const T* value_type;
-  typedef ManagedAttributeCleanupStrategy<value_type> C;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void fn(typename mapping::table_value_type t) {
-    C::cleanup(mapping::convertBack(t));
-  }
-};/* struct getCleanupStrategy<const T*, ManagedAttributeCleanupStrategy<const T*> > */
-
-/**
- * Cause compile-time error for improperly-instantiated
- * getCleanupStrategy<>.
- */
-template <class T, class U>
-struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
-
-namespace attr {
-
-/**
- * This is the last-attribute-assigner.  IDs are not globally
- * unique; rather, they are unique for each table_value_type.
- */
-template <class T, bool context_dep>
-struct LastAttributeId {
-  static uint64_t s_id;
-};
-
-/** Initially zero. */
-template <class T, bool context_dep>
-uint64_t LastAttributeId<T, context_dep>::s_id = 0;
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE TRAITS ============================================================
-
-namespace attr {
-
-/**
- * This is the last-attribute-assigner.  IDs are not globally
- * unique; rather, they are unique for each table_value_type.
- */
-template <class T, bool context_dep>
-struct AttributeTraits {
-  typedef void (*cleanup_t)(T);
-  static std::vector<cleanup_t> cleanup;
-};
-
-template <class T, bool context_dep>
-std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
-  AttributeTraits<T, context_dep>::cleanup;
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE DEFINITION ========================================================
-
-/**
- * An "attribute type" structure.
- *
- * @param T the tag for the attribute kind.
- *
- * @param value_t the underlying value_type for the attribute kind
- *
- * @param CleanupStrategy Clean-up routine for associated values when the
- * Node goes away.  Useful, e.g., for pointer-valued attributes when
- * the values are "owned" by the table.
- *
- * @param context_dep whether this attribute kind is
- * context-dependent
- */
-template <class T,
-          class value_t,
-          class CleanupStrategy = attr::NullCleanupStrategy,
-          bool context_dep = false>
-class Attribute {
-  /**
-   * The unique ID associated to this attribute.  Assigned statically,
-   * at load time.
-   */
-  static const uint64_t s_id;
-
-public:
-
-  /** The value type for this attribute. */
-  typedef value_t value_type;
-
-  /** Get the unique ID associated to this attribute. */
-  static inline uint64_t getId() { return s_id; }
-
-  /**
-   * This attribute does not have a default value: calling
-   * hasAttribute() for a Node that hasn't had this attribute set will
-   * return false, and getAttribute() for the Node will return a
-   * default-constructed value_type.
-   */
-  static const bool has_default_value = false;
-
-  /**
-   * Expose this setting to the users of this Attribute kind.
-   */
-  static const bool context_dependent = context_dep;
-
-  /**
-   * Register this attribute kind and check that the ID is a valid ID
-   * for bool-valued attributes.  Fail an assert if not.  Otherwise
-   * return the id.
-   */
-  static inline uint64_t registerAttribute() {
-    typedef typename attr::KindValueToTableValueMapping<value_t>::table_value_type table_value_type;
-    typedef attr::AttributeTraits<table_value_type, context_dep> traits;
-    uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
-    Assert(traits::cleanup.size() == id);// sanity check
-    traits::cleanup.push_back(attr::getCleanupStrategy<value_t, CleanupStrategy>::fn);
-    return id;
-  }
-};/* class Attribute<> */
-
-/**
- * An "attribute type" structure for boolean flags (special).  The
- * full one is below; the existence of this one disallows for boolean
- * flag attributes with a specialized cleanup function.
- */
-/* -- doesn't work; other specialization is "more specific" ??
-template <class T, class CleanupStrategy, bool context_dep>
-class Attribute<T, bool, CleanupStrategy, context_dep> {
-  template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
-  ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
-};
-*/
-
-/**
- * An "attribute type" structure for boolean flags (special).
- */
-template <class T, bool context_dep>
-class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
-  /** IDs for bool-valued attributes are actually bit assignments. */
-  static const uint64_t s_id;
-
-public:
-
-  /** The value type for this attribute; here, bool. */
-  typedef bool value_type;
-
-  /** Get the unique ID associated to this attribute. */
-  static inline uint64_t getId() { return s_id; }
-
-  /**
-   * Such bool-valued attributes ("flags") have a default value: they
-   * are false for all nodes on entry.  Calling hasAttribute() for a
-   * Node that hasn't had this attribute set will return true, and
-   * getAttribute() for the Node will return the default_value below.
-   */
-  static const bool has_default_value = true;
-
-  /**
-   * Default value of the attribute for Nodes without one explicitly
-   * set.
-   */
-  static const bool default_value = false;
-
-  /**
-   * Expose this setting to the users of this Attribute kind.
-   */
-  static const bool context_dependent = context_dep;
-
-  /**
-   * Register this attribute kind and check that the ID is a valid ID
-   * for bool-valued attributes.  Fail an assert if not.  Otherwise
-   * return the id.
-   */
-  static inline uint64_t registerAttribute() {
-    uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
-    AlwaysAssert( id <= 63,
-                  "Too many boolean node attributes registered "
-                  "during initialization !" );
-    return id;
-  }
-};/* class Attribute<..., bool, ...> */
-
-/**
- * This is a context-dependent attribute kind (the only difference
- * between CDAttribute<> and Attribute<> (with the fourth argument
- * "true") is that you cannot supply a cleanup function (a no-op one
- * is used).
- */
-template <class T,
-          class value_type>
-struct CDAttribute :
-    public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
-
-/**
- * This is a managed attribute kind (the only difference between
- * ManagedAttribute<> and Attribute<> is the default cleanup function
- * and the fact that ManagedAttributes cannot be context-dependent).
- * In the default ManagedAttribute cleanup function, the value is
- * destroyed with the delete operator.  If the value is allocated with
- * the array version of new[], an alternate cleanup function should be
- * provided that uses array delete[].  It is an error to create a
- * ManagedAttribute<> kind with a non-pointer value_type if you don't
- * also supply a custom cleanup function.
- */
-template <class T,
-          class value_type,
-          class CleanupStrategy = attr::ManagedAttributeCleanupStrategy<value_type> >
-struct ManagedAttribute :
-    public Attribute<T, value_type, CleanupStrategy, false> {};
-
-// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
-
-/** Assign unique IDs to attributes at load time. */
-// Use of the comma-operator here forces instantiation (and
-// initialization) of the AttributeTraits<> structure and its
-// "cleanup" vector before registerAttribute() is called.  This is
-// important because otherwise the vector is initialized later,
-// clearing the first-pushed cleanup function.
-template <class T, class value_t, class CleanupStrategy, bool context_dep>
-const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
-  ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
-    Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
-
-/** Assign unique IDs to attributes at load time. */
-template <class T, bool context_dep>
-const uint64_t Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::s_id =
-  Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::registerAttribute();
-
 // ATTRIBUTE MANAGER ===========================================================
 
-namespace attr {
-
 /**
  * A container for the main attribute tables of the system.  There's a
  * one-to-one NodeManager : AttributeManager correspondence.
@@ -868,7 +212,7 @@ struct getTable<uint64_t, false> {
 
 /** Access the "d_exprs" member of AttributeManager. */
 template <>
-struct getTable<Node, false> {
+struct getTable<TNode, false> {
   typedef AttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_exprs;
@@ -940,7 +284,7 @@ struct getTable<uint64_t, true> {
 
 /** Access the "d_cdexprs" member of AttributeManager. */
 template <>
-struct getTable<Node, true> {
+struct getTable<TNode, true> {
   typedef CDAttrHash<TNode> table_type;
   static inline table_type& get(AttributeManager& am) {
     return am.d_cdexprs;
@@ -994,15 +338,17 @@ namespace attr {
 
 // implementation for AttributeManager::getAttribute()
 template <class AttrKind>
-typename AttrKind::value_type AttributeManager::getAttribute(NodeValue* nv,
-                                                             const AttrKind&) const {
-
+typename AttrKind::value_type
+AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
   typedef typename AttrKind::value_type value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
-  typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+  typedef typename getTable<value_type, AttrKind::context_dependent>::
+            table_type table_type;
 
-  const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
-  typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+  const table_type& ah =
+    getTable<value_type, AttrKind::context_dependent>::get(*this);
+  typename table_type::const_iterator i =
+    ah.find(std::make_pair(AttrKind::getId(), nv));
 
   if(i == ah.end()) {
     return typename AttrKind::value_type();
@@ -1038,10 +384,14 @@ struct HasAttribute<true, AttrKind> {
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
-    typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+    typedef typename getTable<value_type,
+                              AttrKind::context_dependent>::table_type
+      table_type;
 
-    const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
-    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+    const table_type& ah =
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
+    typename table_type::const_iterator i =
+      ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
       ret = AttrKind::default_value;
@@ -1063,10 +413,13 @@ struct HasAttribute<false, AttrKind> {
                                   NodeValue* nv) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
-    typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+    typedef typename getTable<value_type, AttrKind::context_dependent>::
+              table_type table_type;
 
-    const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
-    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+    const table_type& ah =
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
+    typename table_type::const_iterator i =
+      ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
       return false;
@@ -1080,10 +433,13 @@ struct HasAttribute<false, AttrKind> {
                                   typename AttrKind::value_type& ret) {
     typedef typename AttrKind::value_type value_type;
     typedef KindValueToTableValueMapping<value_type> mapping;
-    typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+    typedef typename getTable<value_type, AttrKind::context_dependent>::
+              table_type table_type;
 
-    const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
-    typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
+    const table_type& ah =
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
+    typename table_type::const_iterator i =
+      ah.find(std::make_pair(AttrKind::getId(), nv));
 
     if(i == ah.end()) {
       return false;
@@ -1098,29 +454,56 @@ struct HasAttribute<false, AttrKind> {
 template <class AttrKind>
 bool AttributeManager::hasAttribute(NodeValue* nv,
                                     const AttrKind&) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::hasAttribute(this, nv);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::
+           hasAttribute(this, nv);
 }
 
 template <class AttrKind>
 bool AttributeManager::getAttribute(NodeValue* nv,
                                     const AttrKind&,
                                     typename AttrKind::value_type& ret) const {
-  return HasAttribute<AttrKind::has_default_value, AttrKind>::getAttribute(this, nv, ret);
+  return HasAttribute<AttrKind::has_default_value, AttrKind>::
+           getAttribute(this, nv, ret);
 }
 
 template <class AttrKind>
-inline void AttributeManager::setAttribute(NodeValue* nv,
-                                           const AttrKind&,
-                                           const typename AttrKind::value_type& value) {
-
+inline void
+AttributeManager::setAttribute(NodeValue* nv,
+                               const AttrKind&,
+                               const typename AttrKind::value_type& value) {
   typedef typename AttrKind::value_type value_type;
   typedef KindValueToTableValueMapping<value_type> mapping;
-  typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
+  typedef typename getTable<value_type, AttrKind::context_dependent>::
+            table_type table_type;
 
-  table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
+  table_type& ah =
+    getTable<value_type, AttrKind::context_dependent>::get(*this);
   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
+/**
+ * Search for the NodeValue in all attribute tables and remove it,
+ * calling the cleanup function if one is defined.
+ */
+template <class T>
+inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
+                                              NodeValue* nv) {
+  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+    typedef AttributeTraits<T, false> traits_t;
+    typedef AttrHash<T> hash_t;
+    std::pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
+    if(traits_t::cleanup[id] != NULL) {
+      typename hash_t::iterator i = table.find(pr);
+      if(i != table.end()) {
+        traits_t::cleanup[id]((*i).second);
+        table.erase(pr);
+      }
+    } else {
+      table.erase(pr);
+    }
+  }
+}
+
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
new file mode 100644
index 000000000..d50c2284d
--- /dev/null
+++ b/src/expr/attribute_internals.h
@@ -0,0 +1,695 @@
+/*********************                                                        */
+/** attribute_internals.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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.
+ **
+ ** Node attributes' internals.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+#  error expr/attribute_internals.h should only be included by expr/attribute.h
+#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
+
+#ifndef __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+#define __CVC4__EXPR__ATTRIBUTE_INTERNALS_H
+
+namespace CVC4 {
+namespace expr {
+
+// ATTRIBUTE HASH FUNCTIONS ====================================================
+
+namespace attr {
+
+/**
+ * A hash function for attribute table keys.  Attribute table keys are
+ * pairs, (unique-attribute-id, Node).
+ */
+struct AttrHashStrategy {
+  enum { LARGE_PRIME = 32452843ul };
+  std::size_t operator()(const std::pair<uint64_t, NodeValue*>& p) const {
+    return p.first * LARGE_PRIME + p.second->getId();
+  }
+};
+
+/**
+ * A hash function for boolean-valued attribute table keys; here we
+ * don't have to store a pair as the key, because we use a known bit
+ * in [0..63] for each attribute
+ */
+struct AttrHashBoolStrategy {
+  std::size_t operator()(NodeValue* nv) const {
+    return (size_t)nv->getId();
+  }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TYPE MAPPINGS =====================================================
+
+namespace attr {
+
+/**
+ * KindValueToTableValueMapping is a compile-time-only mechanism to
+ * convert "attribute value types" into "table value types" and back
+ * again.
+ *
+ * Each instantiation <T> is expected to have three members:
+ *
+ *   typename table_value_type
+ *
+ *      A type representing the underlying table's value_type for
+ *      attribute value type (T).  It may be different from T, e.g. T
+ *      could be a pointer-to-Foo, but the underlying table value_type
+ *      might be pointer-to-void.
+ *
+ *   static [convertible-to-table_value_type] convert([convertible-from-T])
+ *
+ *      Converts a T into a table_value_type.  Used to convert an
+ *      attribute value on setting it (and assigning it into the
+ *      underlying table).  See notes on specializations of
+ *      KindValueToTableValueMapping, below.
+ *
+ *   static [convertible-to-T] convertBack([convertible-from-table_value_type])
+ *
+ *      Converts a table_value_type back into a T.  Used to convert an
+ *      underlying table value back into the attribute's expected type
+ *      when retrieving it from the table.  See notes on
+ *      specializations of KindValueToTableValueMapping, below.
+ *
+ * This general (non-specialized) implementation of the template does
+ * nothing.
+ */
+template <class T>
+struct KindValueToTableValueMapping {
+  /** Simple case: T == table_value_type */
+  typedef T table_value_type;
+  /** No conversion necessary */
+  inline static T convert(const T& t) { return t; }
+  /** No conversion necessary */
+  inline static T convertBack(const T& t) { return t; }
+};
+
+/**
+ * Specialization of KindValueToTableValueMapping<> for pointer-valued
+ * attributes.
+ */
+template <class T>
+struct KindValueToTableValueMapping<T*> {
+  /** Table's value type is void* */
+  typedef void* table_value_type;
+  /** A simple reinterpret_cast<>() conversion from T* to void* */
+  inline static void* convert(const T* const& t) {
+    return reinterpret_cast<void*>(const_cast<T*>(t));
+  }
+  /** A simple reinterpret_cast<>() conversion from void* to T* */
+  inline static T* convertBack(void* const& t) {
+    return reinterpret_cast<T*>(t);
+  }
+};
+
+/**
+ * Specialization of KindValueToTableValueMapping<> for const
+ * pointer-valued attributes.
+ */
+template <class T>
+struct KindValueToTableValueMapping<const T*> {
+  /** Table's value type is void* */
+  typedef void* table_value_type;
+  /** A simple reinterpret_cast<>() conversion from const T* const to void* */
+  inline static void* convert(const T* const& t) {
+    return reinterpret_cast<void*>(const_cast<T*>(t));
+  }
+  /** A simple reinterpret_cast<>() conversion from const void* const to T* */
+  inline static const T* convertBack(const void* const& t) {
+    return reinterpret_cast<const T*>(t);
+  }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE HASH TABLES =======================================================
+
+namespace attr {
+
+/**
+ * An "AttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a mapping of pair<unique-attribute-id, Node>
+ * to value_type using our specialized hash function for these pairs.
+ */
+template <class value_type>
+struct AttrHash :
+    public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>,
+                               value_type,
+                               AttrHashStrategy> {
+};
+
+/**
+ * In the case of Boolean-valued attributes we have a special
+ * "AttrHash<bool>" to pack bits together in words.
+ */
+template <>
+class AttrHash<bool> :
+    protected __gnu_cxx::hash_map<NodeValue*,
+                                  uint64_t,
+                                  AttrHashBoolStrategy> {
+
+  /** A "super" type, like in Java, for easy reference below. */
+  typedef __gnu_cxx::hash_map<NodeValue*, uint64_t, AttrHashBoolStrategy> super;
+
+  /**
+   * BitAccessor allows us to return a bit "by reference."  Of course,
+   * we don't require bit-addressibility supported by the system, we
+   * do it with a complex type.
+   */
+  class BitAccessor {
+
+    uint64_t& d_word;
+
+    unsigned d_bit;
+
+  public:
+
+    BitAccessor(uint64_t& word, unsigned bit) :
+      d_word(word),
+      d_bit(bit) {
+    }
+
+    BitAccessor& operator=(bool b) {
+      if(b) {
+        // set the bit
+        d_word |= (1 << d_bit);
+      } else {
+        // clear the bit
+        d_word &= ~(1 << d_bit);
+      }
+
+      return *this;
+    }
+
+    operator bool() const {
+      return (d_word & (1 << d_bit)) ? true : false;
+    }
+  };
+
+  /**
+   * A (somewhat degenerate) iterator over boolean-valued attributes.
+   * This iterator doesn't support anything except comparison and
+   * dereference.  It's intended just for the result of find() on the
+   * table.
+   */
+  class BitIterator {
+
+    std::pair<NodeValue* const, uint64_t>* d_entry;
+
+    unsigned d_bit;
+
+  public:
+
+    BitIterator() :
+      d_entry(NULL),
+      d_bit(0) {
+    }
+
+    BitIterator(std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) :
+      d_entry(&entry),
+      d_bit(bit) {
+    }
+
+    std::pair<NodeValue* const, BitAccessor> operator*() {
+      return std::make_pair(d_entry->first,
+                            BitAccessor(d_entry->second, d_bit));
+    }
+
+    bool operator==(const BitIterator& b) {
+      return d_entry == b.d_entry && d_bit == b.d_bit;
+    }
+  };
+
+  /**
+   * A (somewhat degenerate) const_iterator over boolean-valued
+   * attributes.  This const_iterator doesn't support anything except
+   * comparison and dereference.  It's intended just for the result of
+   * find() on the table.
+   */
+  class ConstBitIterator {
+
+    const std::pair<NodeValue* const, uint64_t>* d_entry;
+
+    unsigned d_bit;
+
+  public:
+
+    ConstBitIterator() :
+      d_entry(NULL),
+      d_bit(0) {
+    }
+
+    ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry,
+                     unsigned bit) :
+      d_entry(&entry),
+      d_bit(bit) {
+    }
+
+    std::pair<NodeValue* const, bool> operator*() {
+      return std::make_pair(d_entry->first,
+                            (d_entry->second & (1 << d_bit)) ? true : false);
+    }
+
+    bool operator==(const ConstBitIterator& b) {
+      return d_entry == b.d_entry && d_bit == b.d_bit;
+    }
+  };
+
+public:
+
+  typedef std::pair<uint64_t, NodeValue*> key_type;
+  typedef bool data_type;
+  typedef std::pair<const key_type, data_type> value_type;
+
+  /** an iterator type; see above for limitations */
+  typedef BitIterator iterator;
+  /** a const_iterator type; see above for limitations */
+  typedef ConstBitIterator const_iterator;
+
+  /**
+   * Find the boolean value in the hash table.  Returns something ==
+   * end() if not found.
+   */
+  BitIterator find(const std::pair<uint64_t, NodeValue*>& k) {
+    super::iterator i = super::find(k.second);
+    if(i == super::end()) {
+      return BitIterator();
+    }
+    Debug.printf("boolattr",
+                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+                 &(*i).second,
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
+    return BitIterator(*i, k.first);
+  }
+
+  /** The "off the end" iterator */
+  BitIterator end() {
+    return BitIterator();
+  }
+
+  /**
+   * Find the boolean value in the hash table.  Returns something ==
+   * end() if not found.
+   */
+  ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const {
+    super::const_iterator i = super::find(k.second);
+    if(i == super::end()) {
+      return ConstBitIterator();
+    }
+    Debug.printf("boolattr",
+                 "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+                 &(*i).second,
+                 (unsigned long long)((*i).second),
+                 unsigned(k.first));
+    return ConstBitIterator(*i, k.first);
+  }
+
+  /** The "off the end" const_iterator */
+  ConstBitIterator end() const {
+    return ConstBitIterator();
+  }
+
+  /**
+   * Access the hash table using the underlying operator[].  Inserts
+   * the key into the table (associated to default value) if it's not
+   * already there.
+   */
+  BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) {
+    uint64_t& word = super::operator[](k.second);
+    return BitAccessor(word, k.first);
+  }
+
+  /**
+   * Delete all flags from the given node.
+   */
+  void erase(NodeValue* nv) {
+    super::erase(nv);
+  }
+
+};/* class AttrHash<bool> */
+
+/**
+ * A "CDAttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a context-dependent mapping of
+ * pair<unique-attribute-id, Node> to value_type using our specialized
+ * hash function for these pairs.
+ */
+template <class value_type>
+class CDAttrHash :
+    public context::CDMap<std::pair<uint64_t, NodeValue*>,
+                          value_type,
+                          AttrHashStrategy> {
+public:
+  CDAttrHash(context::Context* ctxt) :
+    context::CDMap<std::pair<uint64_t, NodeValue*>,
+                   value_type,
+                   AttrHashStrategy>(ctxt) {
+  }
+};
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE CLEANUP FUNCTIONS =================================================
+
+namespace attr {
+
+/** Default cleanup for unmanaged Attribute<> */
+struct NullCleanupStrategy {
+};/* struct NullCleanupStrategy */
+
+/** Default cleanup for ManagedAttribute<> */
+template <class T>
+struct ManagedAttributeCleanupStrategy {
+};/* struct ManagedAttributeCleanupStrategy<> */
+
+/** Specialization for T* */
+template <class T>
+struct ManagedAttributeCleanupStrategy<T*> {
+  static inline void cleanup(T* p) { delete p; }
+};/* struct ManagedAttributeCleanupStrategy<T*> */
+
+/** Specialization for const T* */
+template <class T>
+struct ManagedAttributeCleanupStrategy<const T*> {
+  static inline void cleanup(const T* p) { delete p; }
+};/* struct ManagedAttributeCleanupStrategy<const T*> */
+
+/**
+ * Helper for Attribute<> class below to determine whether a cleanup
+ * is defined or not.
+ */
+template <class T, class C>
+struct getCleanupStrategy {
+  typedef T value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void fn(typename mapping::table_value_type t) {
+    C::cleanup(mapping::convertBack(t));
+  }
+};/* struct getCleanupStrategy<> */
+
+/**
+ * Specialization for NullCleanupStrategy.
+ */
+template <class T>
+struct getCleanupStrategy<T, NullCleanupStrategy> {
+  typedef T value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)
+     (typename getCleanupStrategy<T, NullCleanupStrategy>::
+               mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupStrategy<T>.
+ */
+template <class T>
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > {
+  typedef T value_type;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> > */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::fn)
+     (typename getCleanupStrategy<T, ManagedAttributeCleanupStrategy<T> >::
+               mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupStrategy<T*>.
+ */
+template <class T>
+struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > {
+  typedef T* value_type;
+  typedef ManagedAttributeCleanupStrategy<value_type> C;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void fn(typename mapping::table_value_type t) {
+    C::cleanup(mapping::convertBack(t));
+  }
+};/* struct getCleanupStrategy<T*, ManagedAttributeCleanupStrategy<T*> > */
+
+/**
+ * Specialization for ManagedAttributeCleanupStrategy<const T*>.
+ */
+template <class T>
+struct getCleanupStrategy<const T*,
+                          ManagedAttributeCleanupStrategy<const T*> > {
+  typedef const T* value_type;
+  typedef ManagedAttributeCleanupStrategy<value_type> C;
+  typedef KindValueToTableValueMapping<value_type> mapping;
+  static void fn(typename mapping::table_value_type t) {
+    C::cleanup(mapping::convertBack(t));
+  }
+};/* struct getCleanupStrategy<const T*,
+                               ManagedAttributeCleanupStrategy<const T*> > */
+
+/**
+ * Cause compile-time error for improperly-instantiated
+ * getCleanupStrategy<>.
+ */
+template <class T, class U>
+struct getCleanupStrategy<T, ManagedAttributeCleanupStrategy<U> >;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner.  IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct LastAttributeId {
+  static uint64_t s_id;
+};
+
+/** Initially zero. */
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE TRAITS ============================================================
+
+namespace attr {
+
+/**
+ * This is the last-attribute-assigner.  IDs are not globally
+ * unique; rather, they are unique for each table_value_type.
+ */
+template <class T, bool context_dep>
+struct AttributeTraits {
+  typedef void (*cleanup_t)(T);
+  static std::vector<cleanup_t> cleanup;
+};
+
+template <class T, bool context_dep>
+std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
+  AttributeTraits<T, context_dep>::cleanup;
+
+}/* CVC4::expr::attr namespace */
+
+// ATTRIBUTE DEFINITION ========================================================
+
+/**
+ * An "attribute type" structure.
+ *
+ * @param T the tag for the attribute kind.
+ *
+ * @param value_t the underlying value_type for the attribute kind
+ *
+ * @param CleanupStrategy Clean-up routine for associated values when the
+ * Node goes away.  Useful, e.g., for pointer-valued attributes when
+ * the values are "owned" by the table.
+ *
+ * @param context_dep whether this attribute kind is
+ * context-dependent
+ */
+template <class T,
+          class value_t,
+          class CleanupStrategy = attr::NullCleanupStrategy,
+          bool context_dep = false>
+class Attribute {
+  /**
+   * The unique ID associated to this attribute.  Assigned statically,
+   * at load time.
+   */
+  static const uint64_t s_id;
+
+public:
+
+  /** The value type for this attribute. */
+  typedef value_t value_type;
+
+  /** Get the unique ID associated to this attribute. */
+  static inline uint64_t getId() { return s_id; }
+
+  /**
+   * This attribute does not have a default value: calling
+   * hasAttribute() for a Node that hasn't had this attribute set will
+   * return false, and getAttribute() for the Node will return a
+   * default-constructed value_type.
+   */
+  static const bool has_default_value = false;
+
+  /**
+   * Expose this setting to the users of this Attribute kind.
+   */
+  static const bool context_dependent = context_dep;
+
+  /**
+   * Register this attribute kind and check that the ID is a valid ID
+   * for bool-valued attributes.  Fail an assert if not.  Otherwise
+   * return the id.
+   */
+  static inline uint64_t registerAttribute() {
+    typedef typename attr::KindValueToTableValueMapping<value_t>::
+                     table_value_type table_value_type;
+    typedef attr::AttributeTraits<table_value_type, context_dep> traits;
+    uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
+    Assert(traits::cleanup.size() == id);// sanity check
+    traits::cleanup.push_back(attr::getCleanupStrategy<value_t,
+                                                       CleanupStrategy>::fn);
+    return id;
+  }
+};/* class Attribute<> */
+
+/**
+ * An "attribute type" structure for boolean flags (special).  The
+ * full one is below; the existence of this one disallows for boolean
+ * flag attributes with a specialized cleanup function.
+ */
+/* -- doesn't work; other specialization is "more specific" ??
+template <class T, class CleanupStrategy, bool context_dep>
+class Attribute<T, bool, CleanupStrategy, context_dep> {
+  template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
+  ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
+};
+*/
+
+/**
+ * An "attribute type" structure for boolean flags (special).
+ */
+template <class T, bool context_dep>
+class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
+  /** IDs for bool-valued attributes are actually bit assignments. */
+  static const uint64_t s_id;
+
+public:
+
+  /** The value type for this attribute; here, bool. */
+  typedef bool value_type;
+
+  /** Get the unique ID associated to this attribute. */
+  static inline uint64_t getId() { return s_id; }
+
+  /**
+   * Such bool-valued attributes ("flags") have a default value: they
+   * are false for all nodes on entry.  Calling hasAttribute() for a
+   * Node that hasn't had this attribute set will return true, and
+   * getAttribute() for the Node will return the default_value below.
+   */
+  static const bool has_default_value = true;
+
+  /**
+   * Default value of the attribute for Nodes without one explicitly
+   * set.
+   */
+  static const bool default_value = false;
+
+  /**
+   * Expose this setting to the users of this Attribute kind.
+   */
+  static const bool context_dependent = context_dep;
+
+  /**
+   * Register this attribute kind and check that the ID is a valid ID
+   * for bool-valued attributes.  Fail an assert if not.  Otherwise
+   * return the id.
+   */
+  static inline uint64_t registerAttribute() {
+    uint64_t id = attr::LastAttributeId<bool, context_dep>::s_id++;
+    AlwaysAssert( id <= 63,
+                  "Too many boolean node attributes registered "
+                  "during initialization !" );
+    return id;
+  }
+};/* class Attribute<..., bool, ...> */
+
+/**
+ * This is a context-dependent attribute kind (the only difference
+ * between CDAttribute<> and Attribute<> (with the fourth argument
+ * "true") is that you cannot supply a cleanup function (a no-op one
+ * is used).
+ */
+template <class T,
+          class value_type>
+struct CDAttribute :
+    public Attribute<T, value_type, attr::NullCleanupStrategy, true> {};
+
+/**
+ * This is a managed attribute kind (the only difference between
+ * ManagedAttribute<> and Attribute<> is the default cleanup function
+ * and the fact that ManagedAttributes cannot be context-dependent).
+ * In the default ManagedAttribute cleanup function, the value is
+ * destroyed with the delete operator.  If the value is allocated with
+ * the array version of new[], an alternate cleanup function should be
+ * provided that uses array delete[].  It is an error to create a
+ * ManagedAttribute<> kind with a non-pointer value_type if you don't
+ * also supply a custom cleanup function.
+ */
+template <class T,
+          class value_type,
+          class CleanupStrategy =
+                    attr::ManagedAttributeCleanupStrategy<value_type> >
+struct ManagedAttribute :
+    public Attribute<T, value_type, CleanupStrategy, false> {};
+
+// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
+
+/** Assign unique IDs to attributes at load time. */
+// Use of the comma-operator here forces instantiation (and
+// initialization) of the AttributeTraits<> structure and its
+// "cleanup" vector before registerAttribute() is called.  This is
+// important because otherwise the vector is initialized later,
+// clearing the first-pushed cleanup function.
+template <class T, class value_t, class CleanupStrategy, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
+  ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::
+                                   table_value_type,
+                          context_dep>::cleanup.size(),
+    Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
+
+/** Assign unique IDs to attributes at load time. */
+template <class T, bool context_dep>
+const uint64_t Attribute<T,
+                         bool,
+                         attr::NullCleanupStrategy, context_dep>::s_id =
+  Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::
+    registerAttribute();
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__ATTRIBUTE_INTERNALS_H */
diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index bb224aa91..c4eb3af1c 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -17,10 +17,13 @@
 #     SKOLEM.
 #
 #   operator K #children ["comment"]
+#   nonatomic_operator K #children ["comment"]
 #
 #     Declares a "built-in" operator kind K.  Really this is the same
 #     as "variable" except that it has an operator (automatically
-#     generated by NodeManager).
+#     generated by NodeManager).  These two commands are identical,
+#     except that kinds declared with nonatomic_operator answer false
+#     to Node::isAtomic().
 #
 #     You can specify an exact # of children required as the second
 #     argument to the operator command.  In debug mode, assertions are
@@ -109,12 +112,11 @@ theory builtin
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
 # not stored that way.  If you ask for the operator of (EQUAL a b),
 # you'll get a special, singleton (BUILTIN EQUAL) Node.
-constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \
+constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashStrategy \
     "expr/kind.h" "The kind of nodes representing built-in operators"
 
 operator EQUAL 2 "equality"
 operator DISTINCT 2: "disequality"
-operator ITE 3 "if-then-else"
 variable SKOLEM "skolem var"
 variable VARIABLE "variable"
 operator TUPLE 2: "a tuple"
diff --git a/src/expr/command.h b/src/expr/command.h
index e5994b3c7..6a4bb67ed 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -16,6 +16,8 @@
  ** client code.
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__COMMAND_H
 #define __CVC4__COMMAND_H
 
@@ -24,7 +26,6 @@
 #include <string>
 #include <vector>
 
-#include "cvc4_config.h"
 #include "expr/expr.h"
 #include "util/result.h"
 
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager_template.cpp
index 4eda9805a..2e25b4574 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** expr_manager.cpp
+/** expr_manager_template.cpp
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): none
@@ -10,23 +10,25 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Public-facing expression manager interface, implementation.
  **/
 
-/*
- * expr_manager.cpp
- *
- *  Created on: Dec 10, 2009
- *      Author: dejan
- */
-
-#include "context/context.h"
+#include "expr/node.h"
 #include "expr/expr.h"
-#include "expr/expr_manager.h"
 #include "expr/kind.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
+#include "expr/metakind.h"
 #include "expr/type.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+#include "context/context.h"
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one.  We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 32 "${template}"
 
 using namespace std;
 using namespace CVC4::context;
@@ -122,15 +124,13 @@ FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& argTypes,
   return d_nodeManager->mkFunctionType(argTypes, range);
 }
 
-FunctionType*
-ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
+FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& sorts) {
   Assert( sorts.size() >= 2 );
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkFunctionType(sorts);
 }
 
-FunctionType*
-ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
+FunctionType* ExprManager::mkPredicateType(const std::vector<Type*>& sorts) {
   Assert( sorts.size() >= 1 );
   NodeManagerScope nms(d_nodeManager);
   return d_nodeManager->mkPredicateType(sorts);
@@ -151,11 +151,12 @@ Expr ExprManager::mkVar(Type* type) {
   return Expr(this, new Node(d_nodeManager->mkVar(type)));
 }
 
-unsigned int ExprManager::minArity(Kind kind) {
+unsigned ExprManager::minArity(Kind kind) {
+  // FIXME: should be implemented this way, but parser depends on *parse*-level.
+  // See bug 75.
+  //return metakind::getLowerBoundForKind(kind);
   switch(kind) {
-  case FALSE:
   case SKOLEM:
-  case TRUE:
   case VARIABLE:
     return 0;
 
@@ -181,11 +182,12 @@ unsigned int ExprManager::minArity(Kind kind) {
   }
 }
 
-unsigned int ExprManager::maxArity(Kind kind) {
+unsigned ExprManager::maxArity(Kind kind) {
+  // FIXME: should be implemented this way, but parser depends on *parse*-level.
+  // See bug 75.
+  //return metakind::getUpperBoundForKind(kind);
   switch(kind) {
-  case FALSE:
   case SKOLEM:
-  case TRUE:
   case VARIABLE:
     return 0;
 
@@ -213,7 +215,6 @@ unsigned int ExprManager::maxArity(Kind kind) {
   }
 }
 
-
 NodeManager* ExprManager::getNodeManager() const {
   return d_nodeManager;
 }
@@ -222,4 +223,6 @@ Context* ExprManager::getContext() const {
   return d_ctxt;
 }
 
+${mkConst_implementations}
+
 }/* CVC4 namespace */
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager_template.h
index f2009ad80..523c12e3b 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** expr_manager.h
+/** expr_manager_template.h
  ** Original author: dejan
  ** Major contributors: cconway, mdeters
  ** Minor contributors (to current version): taking
@@ -13,20 +13,27 @@
  ** Public-facing expression manager interface.
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__EXPR_MANAGER_H
 #define __CVC4__EXPR_MANAGER_H
 
-#include "cvc4_config.h"
-#include "expr/kind.h"
 #include <vector>
 
+#include "expr/kind.h"
+#include "expr/type.h"
+
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one.  We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 33 "${template}"
+
 namespace CVC4 {
 
 class Expr;
-class Type;
-class BooleanType;
-class FunctionType;
-class KindType;
 class SmtEngine;
 class NodeManager;
 
@@ -35,6 +42,33 @@ namespace context {
 }/* CVC4::context namespace */
 
 class CVC4_PUBLIC ExprManager {
+private:
+  /** The context */
+  context::Context* d_ctxt;
+
+  /** The internal node manager */
+  NodeManager* d_nodeManager;
+
+  /**
+   * Returns the internal node manager.  This should only be used by
+   * internal users, i.e. the friend classes.
+   */
+  NodeManager* getNodeManager() const;
+
+  /**
+   * Returns the internal Context.  Used by internal users, i.e. the
+   * friend classes.
+   */
+  context::Context* getContext() const;
+
+  /**
+   * SmtEngine will use all the internals, so it will grab the
+   * NodeManager.
+   */
+  friend class SmtEngine;
+
+  /** ExprManagerScope reaches in to get the NodeManager */
+  friend class ExprManagerScope;
 
 public:
 
@@ -65,7 +99,7 @@ public:
 
   /**
    * Make a unary expression of a given kind (NOT, BVNOT, ...).
-   * @param kind the kind of expression
+   * @param child1 kind the kind of expression
    * @return the expression
    */
   Expr mkExpr(Kind kind, const Expr& child1);
@@ -79,10 +113,39 @@ public:
    */
   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
 
+  /**
+   * Make a 3-ary expression of a given kind (AND, PLUS, ...).
+   * @param kind the kind of expression
+   * @param child1 the first child of the new expression
+   * @param child2 the second child of the new expression
+   * @param child3 the third child of the new expression
+   * @return the expression
+   */
   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
               const Expr& child3);
+
+  /**
+   * Make a 4-ary expression of a given kind (AND, PLUS, ...).
+   * @param kind the kind of expression
+   * @param child1 the first child of the new expression
+   * @param child2 the second child of the new expression
+   * @param child3 the third child of the new expression
+   * @param child4 the fourth child of the new expression
+   * @return the expression
+   */
   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
               const Expr& child3, const Expr& child4);
+
+  /**
+   * Make a 5-ary expression of a given kind (AND, PLUS, ...).
+   * @param kind the kind of expression
+   * @param child1 the first child of the new expression
+   * @param child2 the second child of the new expression
+   * @param child3 the third child of the new expression
+   * @param child4 the fourth child of the new expression
+   * @param child5 the fifth child of the new expression
+   * @return the expression
+   */
   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
               const Expr& child3, const Expr& child4, const Expr& child5);
 
@@ -94,30 +157,36 @@ public:
    */
   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 
+  /** Create a constant of type T */
+  template <class T>
+  Expr mkConst(const T&);
+
   /** Make a function type from domain to range. */
-  FunctionType*
-    mkFunctionType(Type* domain,
-                   Type* range);
-
-  /** Make a function type with input types from argTypes. <code>argTypes</code>
-   * must have at least one element. */
-  FunctionType*
-    mkFunctionType(const std::vector<Type*>& argTypes,
-                   Type* range);
-
-  /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
-   * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
-   * least 2 elements.
+  FunctionType* mkFunctionType(Type* domain,
+                               Type* range);
+
+  /**
+   * Make a function type with input types from argTypes.
+   * <code>argTypes</code> must have at least one element.
    */
-  FunctionType*
-    mkFunctionType(const std::vector<Type*>& sorts);
+  FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
+                               Type* range);
 
-  /** Make a predicate type with input types from <code>sorts</code>. The result with
-   * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
-   * least one element.
+  /**
+   * Make a function type with input types from
+   * <code>sorts[0..sorts.size()-2]</code> and result type
+   * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
+   * at least 2 elements.
    */
-  FunctionType*
-    mkPredicateType(const std::vector<Type*>& sorts);
+  FunctionType* mkFunctionType(const std::vector<Type*>& sorts);
+
+  /**
+   * Make a predicate type with input types from
+   * <code>sorts</code>. The result with be a function type with range
+   * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+   * element.
+   */
+  FunctionType* mkPredicateType(const std::vector<Type*>& sorts);
 
   /** Make a new sort with the given name. */
   Type* mkSort(const std::string& name);
@@ -127,41 +196,14 @@ public:
   Expr mkVar(Type* type);
 
   /** Returns the minimum arity of the given kind. */
-  static unsigned int minArity(Kind kind);
+  static unsigned minArity(Kind kind);
 
   /** Returns the maximum arity of the given kind. */
-  static unsigned int maxArity(Kind kind);
-
-private:
-  /** The context */
-  context::Context* d_ctxt;
-
-  /** The internal node manager */
-  NodeManager* d_nodeManager;
-
-  /**
-   * Returns the internal node manager.  This should only be used by
-   * internal users, i.e. the friend classes.
-   */
-  NodeManager* getNodeManager() const;
-
-  /**
-   * Returns the internal Context.  Used by internal users, i.e. the
-   * friend classes.
-   */
-  context::Context* getContext() const;
-
-  /**
-   * SmtEngine will use all the internals, so it will grab the
-   * NodeManager.
-   */
-  friend class SmtEngine;
-
-  /** ExprManagerScope reaches in to get the NodeManager */
-  friend class ExprManagerScope;
+  static unsigned maxArity(Kind kind);
 };
 
+${mkConst_instantiations}
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_MANAGER_H */
-
diff --git a/src/expr/expr.cpp b/src/expr/expr_template.cpp
index 2bcd28422..d02272320 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr_template.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** expr.cpp
+/** expr_template.cpp
  ** Original author: dejan
  ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
@@ -10,7 +10,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.
  **
- ** [[ Add file-specific comments here ]]
+ ** Public-facing expression interface, implementation.
  **/
 
 #include "expr/expr.h"
@@ -19,6 +19,14 @@
 
 #include "util/output.h"
 
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one.  We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 29 "${template}"
+
 using namespace CVC4::kind;
 
 namespace CVC4 {
@@ -29,25 +37,25 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
 }
 
 Expr::Expr() :
-  d_node(new Node()), d_exprManager(NULL) {
+  d_node(new Node),
+  d_exprManager(NULL) {
 }
 
 Expr::Expr(ExprManager* em, Node* node) :
-  d_node(node), d_exprManager(em) {
+  d_node(node),
+  d_exprManager(em) {
 }
 
 Expr::Expr(const Expr& e) :
-  d_node(new Node(*e.d_node)), d_exprManager(e.d_exprManager) {
+  d_node(new Node(*e.d_node)),
+  d_exprManager(e.d_exprManager) {
 }
 
 Expr::Expr(uintptr_t n) :
-    d_node(new Node()),
-    d_exprManager(NULL) {
-  AlwaysAssert(n==0);
-}
+  d_node(new Node),
+  d_exprManager(NULL) {
 
-ExprManager* Expr::getExprManager() const {
-  return d_exprManager;
+  AlwaysAssert(n == 0);
 }
 
 Expr::~Expr() {
@@ -55,33 +63,37 @@ Expr::~Expr() {
   delete d_node;
 }
 
+ExprManager* Expr::getExprManager() const {
+  return d_exprManager;
+}
+
 Expr& Expr::operator=(const Expr& e) {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+
   ExprManagerScope ems(*this);
   *d_node = *e.d_node;
   d_exprManager = e.d_exprManager;
+
   return *this;
 }
 
 /* This should only ever be assigning NULL to a null Expr! */
 Expr& Expr::operator=(uintptr_t n) {
-  AlwaysAssert(n==0);
+  AlwaysAssert(n == 0);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  if( EXPECT_FALSE(!isNull()) ) {
+
+  if(EXPECT_FALSE( !isNull() )) {
     *d_node = Node::null();
   }
   return *this;
-/*
-  Assert(isNull());
-  return *this;
-*/
 }
 
 bool Expr::operator==(const Expr& e) const {
   if(d_exprManager != e.d_exprManager) {
     return false;
   }
+  ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
   return *d_node == *e.d_node;
@@ -94,22 +106,39 @@ bool Expr::operator!=(const Expr& e) const {
 bool Expr::operator<(const Expr& e) const {
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
-  if(d_exprManager != e.d_exprManager) {
-    return false;
+  if(isNull() && !e.isNull()) {
+    return true;
   }
+  ExprManagerScope ems(*this);
   return *d_node < *e.d_node;
 }
 
 Kind Expr::getKind() const {
+  ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->getKind();
 }
 
 size_t Expr::getNumChildren() const {
+  ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->getNumChildren();
 }
 
+bool Expr::hasOperator() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->hasOperator();
+}
+
+Expr Expr::getOperator() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  CheckArgument(d_node->hasOperator(),
+                "Expr::getOperator() called on an Expr with no operator");
+  return Expr(d_exprManager, new Node(d_node->getOperator()));
+}
+
 Type* Expr::getType() const {
   ExprManagerScope ems(*this);
   return d_node->getType();
@@ -122,6 +151,7 @@ std::string Expr::toString() const {
 }
 
 bool Expr::isNull() const {
+  ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");
   return d_node->isNull();
 }
@@ -130,6 +160,18 @@ Expr::operator bool() const {
   return !isNull();
 }
 
+bool Expr::isConst() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->isConst();
+}
+
+bool Expr::isAtomic() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->isAtomic();
+}
+
 void Expr::toStream(std::ostream& out) const {
   ExprManagerScope ems(*this);
   d_node->toStream(out);
@@ -207,5 +249,6 @@ void Expr::debugPrint() {
 #endif /* ! CVC4_MUZZLE */
 }
 
+${getConst_implementations}
 
-} // End namespace CVC4
+}/* CVC4 namespace */
diff --git a/src/expr/expr.h b/src/expr/expr_template.h
index 48b64fd17..12307e679 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/** expr.h
+/** expr_template.h
  ** Original author: dejan
  ** Major contributors: none
  ** Minor contributors (to current version): taking, mdeters
@@ -13,22 +13,30 @@
  ** Public-facing expression interface.
  **/
 
+#include "cvc4_public.h"
+
 // circular dependency: force expr_manager.h first
 #include "expr/expr_manager.h"
 
 #ifndef __CVC4__EXPR_H
 #define __CVC4__EXPR_H
 
-#include "cvc4_config.h"
-
 #include <string>
 #include <iostream>
 #include <stdint.h>
 
+${includes}
+
+// This is a hack, but an important one: if there's an error, the
+// compiler directs the user to the template file instead of the
+// generated one.  We don't want the user to modify the generated one,
+// since it'll get overwritten on a later build.
+#line 35 "${template}"
+
 namespace CVC4 {
 
 // The internal expression representation
-template <bool count_ref>
+template <bool ref_count>
 class NodeTemplate;
 
 /**
@@ -36,6 +44,20 @@ class NodeTemplate;
  * expressions.
  */
 class CVC4_PUBLIC Expr {
+protected:
+
+  /** The internal expression representation */
+  NodeTemplate<true>* d_node;
+
+  /** The responsible expression manager */
+  ExprManager* d_exprManager;
+
+  /**
+   * Constructor for internal purposes.
+   * @param em the expression manager that handles this expression
+   * @param node the actual expression node pointer
+   */
+  Expr(ExprManager* em, NodeTemplate<true>* node);
 
 public:
 
@@ -44,7 +66,7 @@ public:
 
   /**
    * Copy constructor, makes a copy of a given expression
-   * @param the expression to copy
+   * @param e the expression to copy
    */
   Expr(const Expr& e);
 
@@ -68,7 +90,7 @@ public:
    */
   Expr& operator=(const Expr& e);
 
-  /**
+  /*
    * Assignment from an integer. Fails if the integer is not 0.
    * NOTE: This is here purely to support the auto-initialization
    * behavior of the ANTLR3 C backend (i.e., a rule attribute
@@ -104,11 +126,6 @@ public:
   bool operator<(const Expr& e) const;
 
   /**
-   * Returns true if the expression is not the null expression.
-   */
-  operator bool() const;
-
-  /**
    * Returns the kind of the expression (AND, PLUS ...).
    * @return the kind of the expression
    */
@@ -120,6 +137,19 @@ public:
    */
   size_t getNumChildren() const;
 
+  /**
+   * Check if this is an expression that has an operator.
+   * @return true if this expression has an operator
+   */
+  bool hasOperator() const;
+
+  /**
+   * Get the operator of this expression.
+   * @throws IllegalArgumentException if it has no operator
+   * @return the operator of this expression
+   */
+  Expr getOperator() const;
+
   /** Returns the type of the expression, if it has been computed.
    * Returns NULL if the type of the expression is not known.
    */
@@ -133,7 +163,7 @@ public:
 
   /**
    * Outputs the string representation of the expression to the stream.
-   * @param the output stream
+   * @param out the output stream
    */
   void toStream(std::ostream& out) const;
 
@@ -144,6 +174,28 @@ public:
   bool isNull() const;
 
   /**
+   * Check if this is a null expression.
+   * @return true if NOT a null expression
+   */
+  operator bool() const;
+
+  /**
+   * Check if this is an expression representing a constant.
+   * @return true if a constant expression
+   */
+  bool isConst() const;
+
+  /**
+   * Check if this is an expression representing a constant.
+   * @return true if a constant expression
+   */
+  bool isAtomic() const;
+
+  /** Extract a constant of type T */
+  template <class T>
+  const T& getConst() const;
+
+  /**
    * Returns the expression reponsible for this expression.
    */
   ExprManager* getExprManager() const;
@@ -154,10 +206,10 @@ public:
    * @param out output stream to print to.
    * @param indent number of spaces to indent the formula by.
    */
-  void printAst(std::ostream & out, int indent = 0) const;
-  
+  void printAst(std::ostream& out, int indent = 0) const;
+
 private:
-  
+
   /**
    * Pretty printer for use within gdb
    * This is not intended to be used outside of gdb.
@@ -169,19 +221,6 @@ private:
 protected:
 
   /**
-   * Constructor for internal purposes.
-   * @param em the expression manager that handles this expression
-   * @param node the actual expression node pointer
-   */
-  Expr(ExprManager* em, NodeTemplate<true>* node);
-
-  /** The internal expression representation */
-  NodeTemplate<true>* d_node;
-
-  /** The responsible expression manager */
-  ExprManager* d_exprManager;
-
-  /**
    * Returns the actual internal node.
    * @return the internal node
    */
@@ -279,6 +318,8 @@ public:
   Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
 };
 
-}
+${getConst_instantiations}
+
+}/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_H */
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 2b675be0f..96c34a02a 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -13,10 +13,11 @@
  ** Template for the Node kind header.
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__KIND_H
 #define __CVC4__KIND_H
 
-#include "cvc4_config.h"
 #include <iostream>
 #include <sstream>
 
@@ -62,9 +63,9 @@ inline std::string kindToString(::CVC4::Kind k) {
   return ss.str();
 }
 
-struct KindHashFcn {
+struct KindHashStrategy {
   static inline size_t hash(::CVC4::Kind k) { return k; }
-};
+};/* struct KindHashStrategy */
 
 }/* CVC4::kind namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 95e107313..052458cbe 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -123,6 +123,16 @@ ${metakind_kinds}
   return metaKinds[k];
 }/* metaKindOf(k) */
 
+static inline bool kindIsAtomic(Kind k) {
+  static const bool isAtomic[] = {
+    false, /* NULL_EXPR */
+${metakind_isatomic}
+    false /* LAST_KIND */
+  };/* isAtomic[] */
+
+  return isAtomic[k];
+}/* kindIsAtomic(k) */
+
 }/* CVC4::kind namespace */
 
 namespace expr {
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
new file mode 100755
index 000000000..de6de014d
--- /dev/null
+++ b/src/expr/mkexpr
@@ -0,0 +1,177 @@
+#!/bin/bash
+#
+# mkexpr
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010  The CVC4 Project
+#
+# The purpose of this script is to create {expr,expr_manager}.{h,cpp}
+# from template files and a list of theory kinds.  Basically it just
+# sets up the public interface for access to constants.
+#
+# Invocation:
+#
+#   mkexpr template-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+copyright=2010
+
+filename=`basename "$1" | sed 's,_template,,'`
+
+cat <<EOF
+/*********************                                                        */
+/** $filename
+ **
+ ** Copyright $copyright  The AcSys Group, New York University, and as below.
+ **
+ ** This file automatically generated by:
+ **
+ **     $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+me=$(basename "$0")
+
+template=$1; shift
+
+includes=
+getConst_instantiations=
+getConst_implementations=
+mkConst_instantiations=
+mkConst_implementations=
+
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+  # theory T header
+
+  lineno=${BASH_LINENO[0]}
+
+  # this script doesn't care about the theory class information, but
+  # makes does make sure it's there
+  seen_theory=true
+  if [ "$1" = builtin ]; then
+    if $seen_theory_builtin; then
+      echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
+      exit 1
+    fi
+    seen_theory_builtin=true
+  elif [ -z "$1" -o -z "$2" ]; then
+    echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
+    exit 1
+  elif ! expr "$1" : '\(::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+  elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+    echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+  fi
+}
+
+function variable {
+  # variable K ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+}
+
+function operator {
+  # operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+}
+
+function nonatomic_operator {
+  # nonatomic_operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+}
+
+function parameterized {
+  # parameterized K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+}
+
+function constant {
+  # constant K T Hasher header ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+
+  includes="${includes}
+#include \"$4\""
+  mkConst_instantiations="${mkConst_instantiations}
+template <>
+Expr ExprManager::mkConst($2 const& val);
+"
+  mkConst_implementations="${mkConst_implementations}
+template <>
+Expr ExprManager::mkConst($2 const& val) {
+  return Expr(this, new Node(d_nodeManager->mkConst< $2 >(val)));
+}
+"
+  getConst_instantiations="${getConst_instantiations}
+template <>
+$2 const & Expr::getConst< $2 >() const;
+"
+  getConst_implementations="${getConst_implementations}
+template <>
+$2 const & Expr::getConst() const {
+  return d_node->getConst< $2 >();
+}
+"
+}
+
+function check_theory_seen {
+  if ! $seen_theory; then
+    echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
+    exit 1
+  fi
+}
+
+function check_builtin_theory_seen {
+  if ! $seen_theory_builtin; then
+    echo "$me: warning: no declaration for the builtin theory found" >&2
+  fi
+}
+
+while [ $# -gt 0 ]; do
+  kf=$1
+  seen_theory=false
+  b=$(basename $(dirname "$kf"))
+  source "$kf"
+  check_theory_seen
+  shift
+done
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in \
+    includes \
+    template \
+    getConst_instantiations \
+    getConst_implementations \
+    mkConst_instantiations \
+    mkConst_implementations; do
+  eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error=`expr "$text" : '.*\${\([^}]*\)}.*'`
+if [ -n "$error" ]; then
+  echo "$template:0: error: undefined replacement \${$error}" >&2
+  exit 1
+fi
+echo "$text"
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 6d75164d1..294dc5d7e 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -4,12 +4,12 @@
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
 # Copyright (c) 2010  The CVC4 Project
 #
-# The purpose of this script is to create kind.h from a prologue,
-# middle section, epilogue, and a list of theory kinds.
+# The purpose of this script is to create kind.h from a template and a
+# list of theory kinds.
 #
 # Invocation:
 #
-#   mkkind prologue-file middle-file epilogue-file theory-kind-files...
+#   mkkind template-file theory-kind-files...
 #
 # Output is to standard out.
 #
@@ -17,7 +17,7 @@
 copyright=2010
 
 cat <<EOF
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** kind.h
  **
  ** Copyright $copyright  The AcSys Group, New York University, and as below.
@@ -83,6 +83,15 @@ function operator {
   register_kind "$1" "$2" "$3"
 }
 
+function nonatomic_operator {
+  # nonatomic_operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_kind "$1" "$2" "$3"
+}
+
 function parameterized {
   # parameterized K #children ["comment"]
 
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 15551d54d..3884f636a 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -4,15 +4,15 @@
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
 # Copyright (c) 2010  The CVC4 Project
 #
-# The purpose of this script is to create metakind.h from a prologue,
-# two middle sections, epilogue, and a list of theory kinds.
+# The purpose of this script is to create metakind.h from a template
+# and a list of theory kinds.
 #
 # This is kept distinct from kind.h because kind.h is a public header
 # and metakind.h is intended for the expr package only.
 #
 # Invocation:
 #
-#   mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files...
+#   mkmetakind template-file theory-kind-files...
 #
 # Output is to standard out.
 #
@@ -20,7 +20,7 @@
 copyright=2010
 
 cat <<EOF
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** metakind.h
  **
  ** Copyright $copyright  The AcSys Group, New York University, and as below.
@@ -98,6 +98,15 @@ function operator {
   register_metakind OPERATOR "$1" "$2"
 }
 
+function nonatomic_operator {
+  # nonatomic_operator K #children ["comment"]
+
+  lineno=${BASH_LINENO[0]}
+
+  check_theory_seen
+  register_metakind NONATOMIC_OPERATOR "$1" "$2"
+}
+
 function parameterized {
   # parameterized K #children ["comment"]
 
@@ -115,7 +124,14 @@ function constant {
   check_theory_seen
 
   if ! expr "$2" : '\(::*\)' >/dev/null; then
-    echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+    if ! primitive_type "$2"; then
+      # if there's an embedded space, we're probably doing something
+      # tricky to specify the CONST payload, like "int const*"; in any
+      # case, this warning gives too many false positives, so disable it
+      if ! expr "$2" : '..* ..*' >/dev/null; then
+        echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+      fi
+    fi
   fi
   if ! expr "$3" : '\(::*\)' >/dev/null; then
     echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2
@@ -133,14 +149,15 @@ function constant {
 namespace expr {
 
 template <>
-inline const $2 & NodeValue::getConst< $2 >() const {
-  Assert(getKind() == ::CVC4::kind::$1);
+inline $2 const& NodeValue::getConst< $2 >() const {
+  AssertArgument(getKind() == ::CVC4::kind::$1, *this,
+                 \"Improper kind for getConst<$2>()\");
   // To support non-inlined CONSTANT-kinded NodeValues (those that are
   // \"constructed\" when initially checking them against the NodeManager
   // pool), we must check d_nchildren here.
   return d_nchildren == 0
-    ? *reinterpret_cast< const $2 * >(d_children)
-    : *reinterpret_cast< const $2 * >(d_children[0]);
+    ? *reinterpret_cast< $2 const* >(d_children)
+    : *reinterpret_cast< $2 const* >(d_children[0]);
 }
 
 }/* CVC4::expr namespace */
@@ -166,10 +183,12 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 "
   metakind_constHashes="${metakind_constHashes}
   case kind::$1:
+#line $lineno \"$kf\"
     return $3::hash(nv->getConst< $2 >());
 "
   metakind_constPrinters="${metakind_constPrinters}
   case kind::$1:
+#line $lineno \"$kf\"
     out << nv->getConst< $2 >();
     break;
 "
@@ -179,17 +198,27 @@ function register_metakind {
   mk=$1
   k=$2
   nc=$3
+
+  if [ $mk = NONATOMIC_OPERATOR ]; then
+    metakind_isatomic="${metakind_isatomic}    false, /* $k */
+";
+    mk=OPERATOR
+  else
+    metakind_isatomic="${metakind_isatomic}    true, /* $k */
+";
+  fi
+
   metakind_kinds="${metakind_kinds}    metakind::$mk, /* $k */
 ";
 
   # figure out the range given by $nc
-  if expr "$nc" : '^[0-9]\+$' >/dev/null; then
+  if expr "$nc" : '[0-9]\+$' >/dev/null; then
     lb=$nc
     ub=$nc
-  elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then
+  elif expr "$nc" : '[0-9]\+:$' >/dev/null; then
     let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
     ub=MAX_CHILDREN
-  elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then
+  elif expr "$nc" : '[0-9]\+:[0-9]\+$' >/dev/null; then
     let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
     if [ $ub -lt $lb ]; then
       echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2
@@ -200,12 +229,35 @@ function register_metakind {
     exit 1
   fi
 
+  if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then
+    if [ $lb = 0 ]; then
+      echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2
+      exit 1
+    fi
+  fi
+
   metakind_lbchildren="${metakind_lbchildren}
     $lb, /* $k */"
   metakind_ubchildren="${metakind_ubchildren}
     $ub, /* $k */"
 }
 
+# Returns 0 if arg is a primitive C++ type, or a pointer to same; 1
+# otherwise.  Really all this does is check whether we should issue a
+# "not fully qualified" warning or not.
+function primitive_type {
+  strip=`expr "$1" : ' *\(.*\)\* *'`
+  if [ -n "$strip" ]; then
+    primitive_type "$strip" >&2
+    return $?
+  fi
+
+  case "$1" in
+    bool|int|size_t|long|void|char|float|double) return 0;;
+    *) return 1;;
+  esac
+}
+
 function check_theory_seen {
   if ! $seen_theory; then
     echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
@@ -226,6 +278,9 @@ while [ $# -gt 0 ]; do
   metakind_kinds="${metakind_kinds}
     /* from $b */
 "
+  metakind_isatomic="${metakind_isatomic}
+    /* from $b */
+"
   source "$kf"
   check_theory_seen
   shift
@@ -235,9 +290,16 @@ check_builtin_theory_seen
 ## output
 
 text=$(cat "$template")
-for var in metakind_includes metakind_kinds metakind_constantMaps \
-           metakind_compares metakind_constHashes metakind_constPrinters \
-           metakind_ubchildren metakind_lbchildren; do
+for var in \
+    metakind_includes \
+    metakind_kinds \
+    metakind_isatomic \
+    metakind_constantMaps \
+    metakind_compares \
+    metakind_constHashes \
+    metakind_constPrinters \
+    metakind_ubchildren \
+    metakind_lbchildren; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
 error=`expr "$text" : '.*\${\([^}]*\)}.*'`
diff --git a/src/expr/node.h b/src/expr/node.h
index 343f03a1f..875760725 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -15,6 +15,7 @@
 
 #include "cvc4_private.h"
 
+// circular dependency
 #include "expr/node_value.h"
 
 #ifndef __CVC4__NODE_H
@@ -25,11 +26,10 @@
 #include <iostream>
 #include <stdint.h>
 
-#include "cvc4_config.h"
 #include "expr/kind.h"
+#include "expr/metakind.h"
 #include "expr/type.h"
 #include "util/Assert.h"
-
 #include "util/output.h"
 
 namespace CVC4 {
@@ -216,7 +216,15 @@ public:
    * Returns true if this node is atomic (has no more Boolean structure)
    * @return true if atomic
    */
-  bool isAtomic() const;
+  inline bool isAtomic() const;
+
+  /**
+   * Returns true if this node represents a constant
+   * @return true if const
+   */
+  inline bool isConst() const {
+    return getMetaKind() == kind::metakind::CONSTANT;
+  }
 
   /**
    * Returns the unique id of this node
@@ -578,23 +586,9 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
 template <bool ref_count>
 NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
 
-////FIXME: This function is a major hack! Should be changed ASAP
-////TODO: Should use positive definition, i.e. what kinds are atomic.
 template <bool ref_count>
 bool NodeTemplate<ref_count>::isAtomic() const {
-  using namespace kind;
-  switch(getKind()) {
-  case NOT:
-  case XOR:
-  case ITE:
-  case IFF:
-  case IMPLIES:
-  case OR:
-  case AND:
-    return false;
-  default:
-    return true;
-  }
+  return kind::kindIsAtomic(getKind());
 }
 
 // FIXME: escape from type system convenient but is there a better
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index f2718a06c..d17ec9497 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -293,24 +293,28 @@ public:
   /** Make a function type from domain to range. */
   inline FunctionType* mkFunctionType(Type* domain, Type* range) const;
 
-  /** Make a function type with input types from argTypes. <code>argTypes</code>
-   * must have at least one element. */
+  /**
+   * Make a function type with input types from
+   * argTypes. <code>argTypes</code> must have at least one element.
+   */
   inline FunctionType* mkFunctionType(const std::vector<Type*>& argTypes,
                                       Type* range) const;
 
-  /** Make a function type with input types from <code>sorts[0..sorts.size()-2]</code>
-   * and result type <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have at
-   * least 2 elements.
+  /**
+   * Make a function type with input types from
+   * <code>sorts[0..sorts.size()-2]</code> and result type
+   * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
+   * at least 2 elements.
    */
-  inline FunctionType*
-    mkFunctionType(const std::vector<Type*>& sorts);
+  inline FunctionType* mkFunctionType(const std::vector<Type*>& sorts) const;
 
-  /** Make a predicate type with input types from <code>sorts</code>. The result with
-   * be a function type with range <code>BOOLEAN</code>. <code>sorts</code> must have at
-   * least one element.
+  /**
+   * Make a predicate type with input types from
+   * <code>sorts</code>. The result with be a function type with range
+   * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
+   * element.
    */
-  inline FunctionType*
-    mkPredicateType(const std::vector<Type*>& sorts);
+  inline FunctionType* mkPredicateType(const std::vector<Type*>& sorts) const;
 
   /** Make a new sort with the given name. */
   inline Type* mkSort(const std::string& name) const;
@@ -453,7 +457,7 @@ NodeManager::mkFunctionType(const std::vector<Type*>& argTypes,
 }
 
 inline FunctionType*
-NodeManager::mkFunctionType(const std::vector<Type*>& sorts) {
+NodeManager::mkFunctionType(const std::vector<Type*>& sorts) const {
   Assert( sorts.size() >= 2 );
   std::vector<Type*> argTypes(sorts);
   Type* rangeType = argTypes.back();
@@ -462,10 +466,11 @@ NodeManager::mkFunctionType(const std::vector<Type*>& sorts) {
 }
 
 inline FunctionType*
-NodeManager::mkPredicateType(const std::vector<Type*>& sorts) {
+NodeManager::mkPredicateType(const std::vector<Type*>& sorts) const {
   Assert( sorts.size() >= 1 );
   return mkFunctionType(sorts,booleanType());
 }
+
 inline Type* NodeManager::mkSort(const std::string& name) const {
   return new SortType(name);
 }
@@ -577,23 +582,6 @@ template <class T>
 Node NodeManager::mkConst(const T& val) {
   // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
 
-  //
-  // TODO: construct a special NodeValue that points to this T but
-  // is == an inlined version (like exists in the hash_set).
-  //
-  // Something similar for (a, b) and (a, b, c) and (a, b, c, d)
-  // versions.
-  //
-  // ALSO TODO: make poolLookup() use hash_set<>::operator[] to auto-insert,
-  // and then set = value after to avoid double-hashing.  fix in all places
-  // where poolLookup is called.
-  //
-  // THEN ALSO TODO: CDMap<> destruction in attribute.cpp to make valgrind
-  // happy
-  //
-  // THEN: reconsider CVC3 tracing mechanism, experiments..
-  //
-
   NVStorage<1> nvStorage;
   expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
 
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 7dd90913f..6408ef01a 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -25,10 +25,9 @@
 #ifndef __CVC4__EXPR__NODE_VALUE_H
 #define __CVC4__EXPR__NODE_VALUE_H
 
-#include "cvc4_config.h"
 #include "expr/kind.h"
-#include <stdint.h>
 
+#include <stdint.h>
 #include <string>
 #include <iterator>
 
diff --git a/src/expr/type.h b/src/expr/type.h
index b406bfd76..9e6596e84 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -13,10 +13,11 @@
  ** Interface for expression types 
  **/
 
+#include "cvc4_public.h"
+
 #ifndef __CVC4__TYPE_H
 #define __CVC4__TYPE_H
 
-#include "cvc4_config.h"
 #include "util/output.h"
 #include "util/Assert.h"
 
@@ -262,7 +263,7 @@ struct TypeCleanupStrategy {
       delete t;
     }
   }
-};
+};/* struct TypeCleanupStrategy */
 
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */