Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing it as well.

3 files changed, 23 insertions, 416 deletions

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 2f938736e..f221c7c7e 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -13,12 +13,12 @@
  **
  ** AttributeManager implementation.
  **/
+#include "expr/attribute.h"
+
 #include <utility>
 
 #include "base/output.h"
-#include "expr/attribute.h"
 #include "expr/node_value.h"
-#include "smt/smt_engine.h"
 
 using namespace std;
 
@@ -26,15 +26,6 @@ namespace CVC4 {
 namespace expr {
 namespace attr {
 
-SmtAttributes::SmtAttributes(context::Context* ctxt) :
-  d_cdbools(ctxt),
-  d_cdints(ctxt),
-  d_cdtnodes(ctxt),
-  d_cdnodes(ctxt),
-  d_cdstrings(ctxt),
-  d_cdptrs(ctxt) {
-}
-
 AttributeManager::AttributeManager() :
   d_inGarbageCollection(false)
 {}
@@ -43,15 +34,6 @@ bool AttributeManager::inGarbageCollection() const {
   return d_inGarbageCollection;
 }
 
-SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) {
-  Assert(smt != NULL);
-  return *smt->d_smtAttributes;
-}
-
-const SmtAttributes& AttributeManager::getSmtAttributes(SmtEngine* smt) const {
-  return *smt->d_smtAttributes;
-}
-
 void AttributeManager::debugHook(int debugFlag) {
   /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
    * debugHook() is an empty function for the purpose of debugging
@@ -71,17 +53,6 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   deleteFromTable(d_ptrs, nv);
 }
 
-void SmtAttributes::deleteAllAttributes(TNode n) {
-  NodeValue* nv = n.d_nv;
-
-  d_cdbools.erase(nv);
-  deleteFromTable(d_cdints, nv);
-  deleteFromTable(d_cdtnodes, nv);
-  deleteFromTable(d_cdnodes, nv);
-  deleteFromTable(d_cdstrings, nv);
-  deleteFromTable(d_cdptrs, nv);
-}
-
 void AttributeManager::deleteAllAttributes() {
   d_bools.clear();
   deleteAllFromTable(d_ints);
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index b5897ac51..5aea4a4d1 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -20,7 +20,6 @@
  * attributes and nodes due to template use */
 #include "expr/node.h"
 #include "expr/type_node.h"
-#include "context/context.h"
 
 #ifndef __CVC4__EXPR__ATTRIBUTE_H
 #define __CVC4__EXPR__ATTRIBUTE_H
@@ -35,45 +34,11 @@
 #undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 
 namespace CVC4 {
-
-class SmtEngine;
-
-namespace smt {
-  extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
-}/* CVC4::smt namespace */
-
 namespace expr {
 namespace attr {
 
 // ATTRIBUTE MANAGER ===========================================================
 
-struct SmtAttributes {
-  SmtAttributes(context::Context*);
-
-  // IF YOU ADD ANY TABLES, don't forget to add them also to the
-  // implementation of deleteAllAttributes().
-
-  /** Underlying hash table for context-dependent boolean-valued attributes */
-  CDAttrHash<bool> d_cdbools;
-  /** Underlying hash table for context-dependent integral-valued attributes */
-  CDAttrHash<uint64_t> d_cdints;
-  /** Underlying hash table for context-dependent node-valued attributes */
-  CDAttrHash<TNode> d_cdtnodes;
-  /** Underlying hash table for context-dependent node-valued attributes */
-  CDAttrHash<Node> d_cdnodes;
-  /** Underlying hash table for context-dependent string-valued attributes */
-  CDAttrHash<std::string> d_cdstrings;
-  /** Underlying hash table for context-dependent pointer-valued attributes */
-  CDAttrHash<void*> d_cdptrs;
-
-  /** Delete all attributes of given node */
-  void deleteAllAttributes(TNode n);
-
-  template <class T>
-  void deleteFromTable(CDAttrHash<T>& table, NodeValue* nv);
-
-};/* struct SmtAttributes */
-
 /**
  * A container for the main attribute tables of the system.  There's a
  * one-to-one NodeManager : AttributeManager correspondence.
@@ -103,9 +68,6 @@ class AttributeManager {
 
   void clearDeleteAllAttributesBuffer();
 
-  SmtAttributes& getSmtAttributes(SmtEngine*);
-  const SmtAttributes& getSmtAttributes(SmtEngine*) const;
-
 public:
 
   /** Construct an attribute manager. */
@@ -239,10 +201,10 @@ template <>
 struct getTable<bool, false> {
   static const AttrTableId id = AttrTableBool;
   typedef AttrHash<bool> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_bools;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_bools;
   }
 };
@@ -252,10 +214,10 @@ template <>
 struct getTable<uint64_t, false> {
   static const AttrTableId id = AttrTableUInt64;
   typedef AttrHash<uint64_t> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_ints;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_ints;
   }
 };
@@ -265,10 +227,10 @@ template <>
 struct getTable<TNode, false> {
   static const AttrTableId id = AttrTableTNode;
   typedef AttrHash<TNode> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_tnodes;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_tnodes;
   }
 };
@@ -278,10 +240,10 @@ template <>
 struct getTable<Node, false> {
   static const AttrTableId id = AttrTableNode;
   typedef AttrHash<Node> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_nodes;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_nodes;
   }
 };
@@ -291,10 +253,10 @@ template <>
 struct getTable<TypeNode, false> {
   static const AttrTableId id = AttrTableTypeNode;
   typedef AttrHash<TypeNode> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_types;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_types;
   }
 };
@@ -304,10 +266,10 @@ template <>
 struct getTable<std::string, false> {
   static const AttrTableId id = AttrTableString;
   typedef AttrHash<std::string> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_strings;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_strings;
   }
 };
@@ -317,10 +279,10 @@ template <class T>
 struct getTable<T*, false> {
   static const AttrTableId id = AttrTablePointer;
   typedef AttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_ptrs;
   }
 };
@@ -330,105 +292,14 @@ template <class T>
 struct getTable<const T*, false> {
   static const AttrTableId id = AttrTablePointer;
   typedef AttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
+  static inline table_type& get(AttributeManager& am) {
     return am.d_ptrs;
   }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
+  static inline const table_type& get(const AttributeManager& am) {
     return am.d_ptrs;
   }
 };
 
-/** Access the "d_cdbools" member of AttributeManager. */
-template <>
-struct getTable<bool, true> {
-  static const AttrTableId id = AttrTableCDBool;
-  typedef CDAttrHash<bool> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdbools;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdbools;
-  }
-};
-
-/** Access the "d_cdints" member of AttributeManager. */
-template <>
-struct getTable<uint64_t, true> {
-  static const AttrTableId id = AttrTableCDUInt64;
-  typedef CDAttrHash<uint64_t> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdints;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdints;
-  }
-};
-
-/** Access the "d_tnodes" member of AttributeManager. */
-template <>
-struct getTable<TNode, true> {
-  static const AttrTableId id = AttrTableCDTNode;
-  typedef CDAttrHash<TNode> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdtnodes;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdtnodes;
-  }
-};
-
-/** Access the "d_cdnodes" member of AttributeManager. */
-template <>
-struct getTable<Node, true> {
-  static const AttrTableId id = AttrTableCDNode;
-  typedef CDAttrHash<Node> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdnodes;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdnodes;
-  }
-};
-
-/** Access the "d_cdstrings" member of AttributeManager. */
-template <>
-struct getTable<std::string, true> {
-  static const AttrTableId id = AttrTableCDString;
-  typedef CDAttrHash<std::string> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdstrings;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdstrings;
-  }
-};
-
-/** Access the "d_cdptrs" member of AttributeManager. */
-template <class T>
-struct getTable<T*, true> {
-  static const AttrTableId id = AttrTableCDPointer;
-  typedef CDAttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-};
-
-/** Access the "d_cdptrs" member of AttributeManager. */
-template <class T>
-struct getTable<const T*, true> {
-  static const AttrTableId id = AttrTableCDPointer;
-  typedef CDAttrHash<void*> table_type;
-  static inline table_type& get(AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-  static inline const table_type& get(const AttributeManager& am, SmtEngine* smt) {
-    return am.getSmtAttributes(smt).d_cdptrs;
-  }
-};
-
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE MANAGER IMPLEMENTATIONS ===========================================
@@ -445,7 +316,7 @@ AttributeManager::getAttribute(NodeValue* nv, const AttrKind&) const {
             table_type table_type;
 
   const table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
+    getTable<value_type, AttrKind::context_dependent>::get(*this);
   typename table_type::const_iterator i =
     ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -488,7 +359,7 @@ struct HasAttribute<true, AttrKind> {
       table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -516,7 +387,7 @@ struct HasAttribute<false, AttrKind> {
               table_type table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -536,7 +407,7 @@ struct HasAttribute<false, AttrKind> {
               table_type table_type;
 
     const table_type& ah =
-      getTable<value_type, AttrKind::context_dependent>::get(*am, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*am);
     typename table_type::const_iterator i =
       ah.find(std::make_pair(AttrKind::getId(), nv));
 
@@ -576,7 +447,7 @@ AttributeManager::setAttribute(NodeValue* nv,
             table_type table_type;
 
   table_type& ah =
-    getTable<value_type, AttrKind::context_dependent>::get(*this, smt::s_smtEngine_current);
+      getTable<value_type, AttrKind::context_dependent>::get(*this);
   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
@@ -606,17 +477,6 @@ inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
 }
 
 /**
- * Obliterate a NodeValue from a (context-dependent) attribute table.
- */
-template <class T>
-inline void SmtAttributes::deleteFromTable(CDAttrHash<T>& table,
-                                           NodeValue* nv) {
-  for(unsigned id = 0; id < attr::LastAttributeId<T, true>::getId(); ++id) {
-    table.obliterate(std::make_pair(id, nv));
-  }
-}
-
-/**
  * Remove all attributes from the table calling the cleanup function
  * if one is defined.
  */
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 861739932..28c618cb0 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -25,8 +25,6 @@
 
 #include <ext/hash_map>
 
-#include "context/cdhashmap.h"
-
 namespace CVC4 {
 namespace expr {
 
@@ -368,217 +366,6 @@ public:
   }
 };/* 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::CDHashMap<std::pair<uint64_t, NodeValue*>,
-                          value_type,
-                          AttrHashFunction> {
-public:
-  CDAttrHash(context::Context* ctxt) :
-    context::CDHashMap<std::pair<uint64_t, NodeValue*>,
-                   value_type,
-                   AttrHashFunction>(ctxt) {
-  }
-};/* class CDAttrHash<> */
-
-/**
- * In the case of Boolean-valued attributes we have a special
- * "CDAttrHash<bool>" to pack bits together in words.
- */
-template <>
-class CDAttrHash<bool> :
-    protected context::CDHashMap<NodeValue*,
-                             uint64_t,
-                             AttrBoolHashFunction> {
-
-  /** A "super" type, like in Java, for easy reference below. */
-  typedef context::CDHashMap<NodeValue*, uint64_t, AttrBoolHashFunction> 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 {
-
-    super& d_map;
-
-    NodeValue* d_key;
-
-    uint64_t d_word;
-
-    unsigned d_bit;
-
-  public:
-
-    BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) :
-      d_map(map),
-      d_key(key),
-      d_word(word),
-      d_bit(bit) {
-      /*
-      Debug.printf("cdboolattr",
-                   "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n",
-                   &map, key, (unsigned long long) word, bit);
-      */
-    }
-
-    BitAccessor& operator=(bool b) {
-      if(b) {
-        // set the bit
-        d_word |= (1 << d_bit);
-        d_map.insert(d_key, d_word);
-        /*
-        Debug.printf("cdboolattr",
-                     "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n",
-                     &d_map, d_key, (unsigned long long) d_word, d_bit);
-        */
-      } else {
-        // clear the bit
-        d_word &= ~(1 << d_bit);
-        d_map.insert(d_key, d_word);
-        /*
-        Debug.printf("cdboolattr",
-                     "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n",
-                     &d_map, d_key, (unsigned long long) d_word, d_bit);
-        */
-      }
-
-      return *this;
-    }
-
-    operator bool() const {
-      /*
-      Debug.printf("cdboolattr",
-                   "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n",
-                   &d_map, d_key, (unsigned long long) d_word, d_bit);
-      */
-      return (d_word & (1 << d_bit)) ? true : false;
-    }
-  };/* class CDAttrHash<bool>::BitAccessor */
-
-  /**
-   * 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(),
-      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;
-    }
-  };/* class CDAttrHash<bool>::ConstBitIterator */
-
-  /* remove non-permitted operations */
-  CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED;
-  CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED;
-
-public:
-
-  CDAttrHash(context::Context* context) : super(context) { }
-
-  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 ConstBitIterator 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.
-   */
-  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("cdboolattr",
-                 "underlying word at address looks like 0x%016llx, bit is %u\n",
-                 (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(*this, k.second, word, k.first);
-  }
-
-  /**
-   * Delete all flags from the given node.  Simply calls superclass's
-   * obliterate().  Note this removes all attributes at all context
-   * levels for this NodeValue!  This is important when the NodeValue
-   * is no longer referenced and is being collected, but otherwise
-   * it probably isn't useful to do this.
-   */
-  void erase(NodeValue* nv) {
-    super::obliterate(nv);
-  }
-
-  /**
-   * Clear the hash table.  This simply exposes the protected superclass
-   * version of clear() to clients.
-   */
-  void clear() {
-    super::clear();
-  }
-
-  /** Is the hash table empty? */
-  bool empty() const {
-    return super::empty();
-  }
-
-  /** This is currently very misleading! */
-  size_t size() const {
-    return super::size();
-  }
-
-};/* class CDAttrHash<bool> */
-
 }/* CVC4::expr::attr namespace */
 
 // ATTRIBUTE CLEANUP FUNCTIONS =================================================
@@ -853,17 +640,6 @@ public:
 };/* 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).