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.

1 files changed, 69 insertions, 686 deletions

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 */