Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing...

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 21e30cef6e9f3f8b0c6605a73d34b85f95358713..575bde1202a1ce2ab30be52a83ff243ce1042a15 100644 (file)
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -60,14 +60,7 @@
  **     itself from the map completely and put itself on a "trash
  **     list" for its scope.
  **
- **     Third, you might obliterate() the key.  This calls the CDOhash_map
- **     destructor, which calls destroy(), which does a successive
- **     restore() until level 0.  If the key was in the map since
- **     level 0, the restore() won't remove it, so in that case
- **     obliterate() removes it from the map and frees the CDOhash_map's
- **     memory.
- **
- **     Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
+ **     Third, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
  **     This first calls destroy(), as per ContextObj contract, but
  **     cdhashmapdoesn't save/restore itself, so that does nothing at the
  **     CDHashMap-level. Then, for each element in the map, it marks it as being
@@ -75,7 +68,7 @@
  **     CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
  **     it.
  **
- **     Fifth, you might clear() the CDHashMap.  This does exactly the
+ **     Fourth, you might clear() the CDHashMap.  This does exactly the
  **     same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
  **     on itself.
  **
@@ -403,43 +396,6 @@ public:
 
   // FIXME: no erase(), too much hassle to implement efficiently...
 
-  /**
-   * "Obliterating" is kind of like erasing, except it's not
-   * backtrackable; the key is permanently removed from the map.
-   * (Naturally, it can be re-added as a new element.)
-   */
-  void obliterate(const Key& k) {
-    typename table_type::iterator i = d_map.find(k);
-    if(i != d_map.end()) {
-      Debug("gc") << "key " << k << " obliterated" << std::endl;
-      // Restore this object to level 0.  If it was inserted after level 0,
-      // nothing else to do as restore will put it in the trash.
-      (*i).second->destroy();
-
-      // Check if object was inserted at level 0: in that case, still have
-      // to do some work.
-      typename table_type::iterator j = d_map.find(k);
-      if(j != d_map.end()) {
-        Element* elt = (*j).second;
-        if(d_first == elt) {
-          if(elt->d_next == elt) {
-            Assert(elt->d_prev == elt);
-            d_first = NULL;
-          } else {
-            d_first = elt->d_next;
-          }
-        }
-        elt->d_prev->d_next = elt->d_next;
-        elt->d_next->d_prev = elt->d_prev;
-        d_map.erase(j);//FIXME multithreading
-        Debug("gc") << "key " << k << " obliterated zero-scope: " << elt << std::endl;
-        if(!elt->d_noTrash) {
-          elt->deleteSelf();
-        }
-      }
-    }
-  }
-
   class iterator {
     const Element* d_it;
 

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 2f938736e5ad0a8bf89dd2153a6ff7d60297dcf7..f221c7c7e67633ceef9645c035d62dfcf3b168d0 100644 (file)
--- 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 b5897ac51ace9259c7422cd39b3c7d307b167afb..5aea4a4d1bd7e081bf5d7d3c24c14fd87a49c337 100644 (file)
--- 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);
 }
 
@@ -605,17 +476,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 861739932983256b8782788cec9cfc79bac92c12..28c618cb06234df0044c062fe4afb69e1245eebc 100644 (file)
--- 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 =================================================
@@ -852,17 +639,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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 327f978e4ddaf2bb4548fdd22f70c030f79841b1..837968aa2a87ca3709def001e3dd68b0f986c353 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -794,9 +794,7 @@ public:
     }
   }
 
-  void nmNotifyDeleteNode(TNode n) {
-    d_smt.d_smtAttributes->deleteAllAttributes(n);
-  }
+  void nmNotifyDeleteNode(TNode n) {}
 
   Node applySubstitutions(TNode node) const {
     return Rewriter::rewrite(d_topLevelSubstitutions.apply(node));
@@ -981,14 +979,12 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_status(),
   d_replayStream(NULL),
   d_private(NULL),
-  d_smtAttributes(NULL),
   d_statisticsRegistry(NULL),
   d_stats(NULL),
   d_channels(new LemmaChannels())
 {
   SmtScope smts(this);
   d_originalOptions.copyValues(em->getOptions());
-  d_smtAttributes = new expr::attr::SmtAttributes(d_context);
   d_private = new smt::SmtEnginePrivate(*this);
   d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
@@ -1204,9 +1200,6 @@ SmtEngine::~SmtEngine() throw() {
     delete d_private;
     d_private = NULL;
 
-    delete d_smtAttributes;
-    d_smtAttributes = NULL;
-
     delete d_userContext;
     d_userContext = NULL;
     delete d_context;

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3df1dbea8c3fdc999787cd9f16b8c4519ab178f8..ed265e2b8e7e75a48a38ec239db0eb3a1c5c7fdb 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -74,13 +74,6 @@ namespace prop {
   class PropEngine;
 }/* CVC4::prop namespace */
 
-namespace expr {
-  namespace attr {
-    class AttributeManager;
-    struct SmtAttributes;
-  }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
 namespace smt {
   /**
    * Representation of a defined function.  We keep these around in
@@ -357,20 +350,9 @@ class CVC4_PUBLIC SmtEngine {
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
-  // to access SmtAttributes
-  friend class expr::attr::AttributeManager;
   // to access getModel(), which is private (for now)
   friend class GetModelCommand;
 
-  /**
-   * There's something of a handshake between the expr package's
-   * AttributeManager and the SmtEngine because the expr package
-   * doesn't have a Context on its own (that's owned by the
-   * SmtEngine).  Thus all context-dependent attributes are stored
-   * here.
-   */
-  expr::attr::SmtAttributes* d_smtAttributes;
-
   StatisticsRegistry* d_statisticsRegistry;
 
   smt::SmtEngineStatistics* d_stats;

diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h
index 1b9e1fa7b1c1f80098c10e82024d9115debe97bd..d0db0cc0f28cd7c96a391640605d6336efd6c475 100644 (file)
--- a/test/unit/context/cdmap_black.h
+++ b/test/unit/context/cdmap_black.h
@@ -16,178 +16,97 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include <map>
+
+#include "base/cvc4_assert.h"
+#include "context/context.h"
 #include "context/cdhashmap.h"
 #include "context/cdlist.h"
 
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::context;
+using CVC4::AssertionException;
+using CVC4::context::Context;
+using CVC4::context::CDHashMap;
 
 class CDMapBlack : public CxxTest::TestSuite {
-
   Context* d_context;
 
-public:
-
+ public:
   void setUp() {
     d_context = new Context;
-    //Debug.on("context");
-    //Debug.on("gc");
-    //Debug.on("pushpop");
+    // Debug.on("context");
+    // Debug.on("gc");
+    // Debug.on("pushpop");
   }
 
-  void tearDown() {
-    delete d_context;
+  void tearDown() { delete d_context; }
+
+  // Returns the elements in a CDHashMap.
+  static std::map<int, int> GetElements(const CDHashMap<int, int>& map) {
+    return std::map<int, int>{map.begin(), map.end()};
+  }
+
+  // Returns true if the elements in map are the same as expected.
+  // NOTE: This is mostly to help the type checker for matching expected within
+  // a TS_ASSERT.
+  static bool ElementsAre(const CDHashMap<int, int>& map,
+                          const std::map<int, int>& expected) {
+    return GetElements(map) == expected;
   }
 
   void testSimpleSequence() {
     CDHashMap<int, int> map(d_context);
-
-    TS_ASSERT(map.find(3) == map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
+    TS_ASSERT(ElementsAre(map, {}));
 
     map.insert(3, 4);
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
-    TS_ASSERT(map[3] == 4);
+    TS_ASSERT(ElementsAre(map, {{3, 4}}));
 
     {
       d_context->push();
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) == map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(ElementsAre(map, {{3, 4}}));
 
       map.insert(5, 6);
       map.insert(9, 8);
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
 
       {
         d_context->push();
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
 
         map.insert(1, 2);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
 
         {
           d_context->push();
-
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) == map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
+          TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
 
           map.insertAtContextLevelZero(23, 317);
           map.insert(1, 45);
 
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 45);
-          TS_ASSERT(map[23] == 317);
-
+          TS_ASSERT(
+              ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
           map.insert(23, 324);
 
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 45);
-          TS_ASSERT(map[23] == 324);
-
+          TS_ASSERT(
+              ElementsAre(map, {{1, 45}, {3, 4}, {5, 6}, {9, 8}, {23, 324}}));
           d_context->pop();
         }
 
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 317);
-
+        TS_ASSERT(
+            ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
         d_context->pop();
       }
 
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) != map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-      TS_ASSERT(map[23] == 317);
-
+      TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
       d_context->pop();
     }
 
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) != map.end());
-    TS_ASSERT(map[3] == 4);
-    TS_ASSERT(map[23] == 317);
+    TS_ASSERT(ElementsAre(map, {{3, 4}, {23, 317}}));
   }
 
   // no intervening find() in this one
   // (under the theory that this could trigger a bug)
   void testSimpleSequenceFewerFinds() {
     CDHashMap<int, int> map(d_context);
-
     map.insert(3, 4);
 
     {
@@ -201,18 +120,9 @@ public:
 
         map.insert(1, 2);
 
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(7) == map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[5] == 6);
-
+        TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
         {
           d_context->push();
-
           d_context->pop();
         }
 
@@ -223,416 +133,34 @@ public:
     }
   }
 
-  void testObliterate() {
-    CDHashMap<int, int> map(d_context);
-
-    map.insert(3, 4);
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
-    TS_ASSERT(map[3] == 4);
-
-    {
-      d_context->push();
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) == map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-
-      map.insert(5, 6);
-      map.insert(9, 8);
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      {
-        d_context->push();
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-
-        map.insertAtContextLevelZero(23, 317);
-        map.insert(1, 2);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 317);
-
-        map.obliterate(5);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) == map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 317);
-
-        {
-          d_context->push();
-
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) == map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
-          TS_ASSERT(map[23] == 317);
-
-          d_context->pop();
-        }
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) == map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 317);
-
-        map.obliterate(23);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) == map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-
-        d_context->pop();
-      }
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[9] == 8);
-
-      d_context->pop();
-    }
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
-    TS_ASSERT(map[3] == 4);
-  }
-
-  void testObliteratePrimordial() {
-    CDHashMap<int, int> map(d_context);
-
-    map.insert(3, 4);
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map[3] == 4);
-
-    {
-      d_context->push();
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) == map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map[3] == 4);
-
-      map.insert(5, 6);
-      map.insert(9, 8);
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      {
-        d_context->push();
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        map.insert(1, 2);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-
-        map.obliterate(3);
-
-        TS_ASSERT(map.find(3) == map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-
-        {
-          d_context->push();
-
-          TS_ASSERT(map.find(3) == map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
-
-          d_context->pop();
-        }
-
-        TS_ASSERT(map.find(3) == map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-
-        d_context->pop();
-      }
-
-      TS_ASSERT(map.find(3) == map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      d_context->pop();
-    }
-
-    TS_ASSERT(map.find(3) == map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-  }
-
-  void testObliterateCurrent() {
-    CDHashMap<int, int> map(d_context);
-
-    map.insert(3, 4);
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map[3] == 4);
-
-    {
-      d_context->push();
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) == map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map[3] == 4);
-
-      map.insert(5, 6);
-      map.insert(9, 8);
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      {
-        d_context->push();
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-
-        map.insert(1, 2);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-
-        map.obliterate(1);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-
-        {
-          d_context->push();
-
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) == map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-
-          d_context->pop();
-        }
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-
-        d_context->pop();
-      }
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      d_context->pop();
-    }
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map[3] == 4);
-  }
-
   void testInsertAtContextLevelZero() {
     CDHashMap<int, int> map(d_context);
 
     map.insert(3, 4);
 
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
-    TS_ASSERT(map[3] == 4);
-
+    TS_ASSERT(ElementsAre(map, {{3, 4}}));
     {
       d_context->push();
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) == map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
+      TS_ASSERT(ElementsAre(map, {{3, 4}}));
 
       map.insert(5, 6);
       map.insert(9, 8);
 
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
+      TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
 
       {
         d_context->push();
 
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
+        TS_ASSERT(ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}}));
 
         map.insert(1, 2);
 
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
+        TS_ASSERT(ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}}));
 
         map.insertAtContextLevelZero(23, 317);
 
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 317);
+        TS_ASSERT(
+            ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 317}}));
 
         TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
                          AssertionException);
@@ -640,278 +168,42 @@ public:
                          AssertionException);
         map.insert(23, 472);
 
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 472);
-
+        TS_ASSERT(
+            ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
         {
           d_context->push();
 
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
-          TS_ASSERT(map[23] == 472);
+          TS_ASSERT(
+            ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
 
           TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
                            AssertionException);
           map.insert(23, 1024);
 
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
-          TS_ASSERT(map[23] == 1024);
-
+          TS_ASSERT(
+            ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 1024}}));
           d_context->pop();
         }
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 472);
-
+        TS_ASSERT(
+            ElementsAre(map, {{1, 2}, {3, 4}, {5, 6}, {9, 8}, {23, 472}}));
         d_context->pop();
       }
 
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) != map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-      TS_ASSERT(map[23] == 317);
-
-      TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
-                       AssertionException);
-      map.insert(23, 477);
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) != map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-      TS_ASSERT(map[23] == 477);
-
-      d_context->pop();
-    }
-
-    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
-                     AssertionException);
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) != map.end());
-    TS_ASSERT(map[3] == 4);
-    TS_ASSERT(map[23] == 317);
-  }
-
-  void testObliterateInsertedAtContextLevelZero() {
-    CDHashMap<int, int> map(d_context);
-
-    map.insert(3, 4);
-
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
-    TS_ASSERT(map[3] == 4);
-
-    {
-      d_context->push();
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) == map.end());
-      TS_ASSERT(map.find(9) == map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-
-      map.insert(5, 6);
-      map.insert(9, 8);
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      {
-        d_context->push();
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) == map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-
-        map.insert(1, 2);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-
-        map.insertAtContextLevelZero(23, 317);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 317);
-
-        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 317),
-                         AssertionException);
-        TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 472),
-                         AssertionException);
-        map.insert(23, 472);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 472);
-
-        {
-          d_context->push();
-
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
-          TS_ASSERT(map[23] == 472);
-
-          TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0),
-                           AssertionException);
-          map.insert(23, 1024);
-
-          TS_ASSERT(map.find(3) != map.end());
-          TS_ASSERT(map.find(5) != map.end());
-          TS_ASSERT(map.find(9) != map.end());
-          TS_ASSERT(map.find(1) != map.end());
-          TS_ASSERT(map.find(23) != map.end());
-          TS_ASSERT(map[3] == 4);
-          TS_ASSERT(map[5] == 6);
-          TS_ASSERT(map[9] == 8);
-          TS_ASSERT(map[1] == 2);
-          TS_ASSERT(map[23] == 1024);
-
-          d_context->pop();
-        }
 
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) != map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
-        TS_ASSERT(map[23] == 472);
-
-        map.obliterate(23);
-
-        TS_ASSERT(map.find(3) != map.end());
-        TS_ASSERT(map.find(5) != map.end());
-        TS_ASSERT(map.find(9) != map.end());
-        TS_ASSERT(map.find(1) != map.end());
-        TS_ASSERT(map.find(23) == map.end());
-        TS_ASSERT(map[3] == 4);
-        TS_ASSERT(map[5] == 6);
-        TS_ASSERT(map[9] == 8);
-        TS_ASSERT(map[1] == 2);
+      TS_ASSERT(
+          ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 317}}));
 
-        d_context->pop();
-      }
-
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) == map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-
-      // reinsert as a normal map entry
+      TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException);
       map.insert(23, 477);
 
-      TS_ASSERT(map.find(3) != map.end());
-      TS_ASSERT(map.find(5) != map.end());
-      TS_ASSERT(map.find(9) != map.end());
-      TS_ASSERT(map.find(1) == map.end());
-      TS_ASSERT(map.find(23) != map.end());
-      TS_ASSERT(map[3] == 4);
-      TS_ASSERT(map[5] == 6);
-      TS_ASSERT(map[9] == 8);
-      TS_ASSERT(map[23] == 477);
-
+      TS_ASSERT(
+          ElementsAre(map, {{3, 4}, {5, 6}, {9, 8}, {23, 477}}));
       d_context->pop();
     }
 
-    TS_ASSERT(map.find(3) != map.end());
-    TS_ASSERT(map.find(5) == map.end());
-    TS_ASSERT(map.find(9) == map.end());
-    TS_ASSERT(map.find(1) == map.end());
-    TS_ASSERT(map.find(23) == map.end());
-    TS_ASSERT(map[3] == 4);
+    TS_ASSERT_THROWS(map.insertAtContextLevelZero(23, 0), AssertionException);
+
+    TS_ASSERT(
+        ElementsAre(map, {{3, 4}, {23, 317}}));
   }
 };

diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index d919bcbe30a87c815205218dfa300f57c8c530ae..d3f043f36ea6e969cee5989dd18b869fca93a2df 100644 (file)
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -88,10 +88,7 @@ public:
   }
 
   struct PrimitiveIntAttributeId {};
-  struct CDPrimitiveIntAttributeId {};
-
   typedef expr::Attribute<PrimitiveIntAttributeId,uint64_t> PrimitiveIntAttribute;
-  typedef expr::CDAttribute<CDPrimitiveIntAttributeId,uint64_t> CDPrimitiveIntAttribute;
   void testInts(){
     TypeNode booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -105,21 +102,12 @@ public:
     TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT_EQUALS(data1, val);
 
-    uint64_t data2 = 0;
-    uint64_t data3 = 0;
-    CDPrimitiveIntAttribute cdattr;
-    TS_ASSERT(!node->getAttribute(cdattr, data2));
-    node->setAttribute(cdattr, val);
-    TS_ASSERT(node->getAttribute(cdattr, data3));
-    TS_ASSERT_EQUALS(data3, val);
     delete node;
   }
 
   struct TNodeAttributeId {};
-  struct CDTNodeAttributeId {};
 
   typedef expr::Attribute<TNodeAttributeId, TNode> TNodeAttribute;
-  typedef expr::CDAttribute<CDTNodeAttributeId, TNode> CDTNodeAttribute;
   void testTNodes(){
     TypeNode booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -134,13 +122,6 @@ public:
     TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT_EQUALS(data1, val);
 
-    TNode data2;
-    TNode data3;
-    CDTNodeAttribute cdattr;
-    TS_ASSERT(!node->getAttribute(cdattr, data2));
-    node->setAttribute(cdattr, val);
-    TS_ASSERT(node->getAttribute(cdattr, data3));
-    TS_ASSERT_EQUALS(data3, val);
     delete node;
   }
 
@@ -152,10 +133,8 @@ public:
   };
 
   struct PtrAttributeId {};
-  struct CDPtrAttributeId {};
 
   typedef expr::Attribute<PtrAttributeId, Foo*> PtrAttribute;
-  typedef expr::CDAttribute<CDPtrAttributeId, Foo*> CDPtrAttribute;
   void testPtrs(){
     TypeNode booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -170,25 +149,14 @@ public:
     TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT_EQUALS(data1, val);
 
-    Foo* data2 = NULL;
-    Foo* data3 = NULL;
-    CDPtrAttribute cdattr;
-    TS_ASSERT(!node->getAttribute(cdattr, data2));
-    node->setAttribute(cdattr, val);
-    TS_ASSERT(node->getAttribute(cdattr, data3));
-    TS_ASSERT(data3 != NULL);
-    TS_ASSERT_EQUALS(63489, data3->getBar());
-    TS_ASSERT_EQUALS(data3, val);
     delete node;
     delete val;
   }
 
 
   struct ConstPtrAttributeId {};
-  struct CDConstPtrAttributeId {};
 
   typedef expr::Attribute<ConstPtrAttributeId, const Foo*> ConstPtrAttribute;
-  typedef expr::CDAttribute<CDConstPtrAttributeId, const Foo*> CDConstPtrAttribute;
   void testConstPtrs(){
     TypeNode booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -203,22 +171,12 @@ public:
     TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT_EQUALS(data1, val);
 
-    const Foo* data2 = NULL;
-    const Foo* data3 = NULL;
-    CDConstPtrAttribute cdattr;
-    TS_ASSERT(!node->getAttribute(cdattr, data2));
-    node->setAttribute(cdattr, val);
-    TS_ASSERT(node->getAttribute(cdattr, data3));
-    TS_ASSERT_EQUALS(data3, val);
     delete node;
     delete val;
   }
 
   struct StringAttributeId {};
-  struct CDStringAttributeId {};
-
   typedef expr::Attribute<StringAttributeId, std::string> StringAttribute;
-  typedef expr::CDAttribute<CDStringAttributeId, std::string> CDStringAttribute;
   void testStrings(){
     TypeNode booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -233,21 +191,11 @@ public:
     TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT_EQUALS(data1, val);
 
-    std::string data2;
-    std::string data3;
-    CDStringAttribute cdattr;
-    TS_ASSERT(!node->getAttribute(cdattr, data2));
-    node->setAttribute(cdattr, val);
-    TS_ASSERT(node->getAttribute(cdattr, data3));
-    TS_ASSERT_EQUALS(data3, val);
     delete node;
   }
 
   struct BoolAttributeId {};
-  struct CDBoolAttributeId {};
-
   typedef expr::Attribute<BoolAttributeId, bool> BoolAttribute;
-  typedef expr::CDAttribute<CDBoolAttributeId, bool> CDBoolAttribute;
   void testBools(){
     TypeNode booleanType = d_nodeManager->booleanType();
     Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
@@ -263,14 +211,6 @@ public:
     TS_ASSERT(node->getAttribute(attr, data1));
     TS_ASSERT_EQUALS(data1, val);
 
-    bool data2 = false;
-    bool data3 = false;
-    CDBoolAttribute cdattr;
-    TS_ASSERT(node->getAttribute(cdattr, data2));
-    TS_ASSERT_EQUALS(false, data2);
-    node->setAttribute(cdattr, val);
-    TS_ASSERT(node->getAttribute(cdattr, data3));
-    TS_ASSERT_EQUALS(data3, val);
     delete node;
   }
 

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index e4786b8e3e2130dcc2ed83b29f03eaa2adfe350d..60a83b5c798b09099d5ec3cb5eb07fc1461b02be 100644 (file)
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -47,18 +47,12 @@ struct Test5;
 typedef Attribute<Test1, std::string> TestStringAttr1;
 typedef Attribute<Test2, std::string> TestStringAttr2;
 
-// it would be nice to have CDAttribute<> for context-dependence
-typedef CDAttribute<Test1, bool> TestCDFlag;
-
 typedef Attribute<Test1, bool> TestFlag1;
 typedef Attribute<Test2, bool> TestFlag2;
 typedef Attribute<Test3, bool> TestFlag3;
 typedef Attribute<Test4, bool> TestFlag4;
 typedef Attribute<Test5, bool> TestFlag5;
 
-typedef CDAttribute<Test1, bool> TestFlag1cd;
-typedef CDAttribute<Test2, bool> TestFlag2cd;
-
 class AttributeWhite : public CxxTest::TestSuite {
 
   ExprManager* d_em;
@@ -127,11 +121,6 @@ public:
     TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id);
 
     lastId = attr::LastAttributeId<bool, true>::getId();
-    TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId);
-    TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId);
-    TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
-    cout << "1: " << TestFlag1cd::s_id << endl;
-    cout << "2: " << TestFlag2cd::s_id << endl;
 
     lastId = attr::LastAttributeId<Node, false>::getId();
 //    TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId);
@@ -149,132 +138,6 @@ public:
     TS_ASSERT_LESS_THAN(TypeAttr::s_id, lastId);
   }
 
-  void testCDAttributes() {
-    //Debug.on("cdboolattr");
-
-    Node a = d_nm->mkVar(*d_booleanType);
-    Node b = d_nm->mkVar(*d_booleanType);
-    Node c = d_nm->mkVar(*d_booleanType);
-
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    d_smtEngine->push(); // level 1
-
-    // test that all boolean flags are FALSE to start
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    // test that they all HAVE the boolean attributes
-    TS_ASSERT(a.hasAttribute(TestFlag1cd()));
-    TS_ASSERT(b.hasAttribute(TestFlag1cd()));
-    TS_ASSERT(c.hasAttribute(TestFlag1cd()));
-
-    // test two-arg version of hasAttribute()
-    bool bb = false;
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(a.getAttribute(TestFlag1cd(), bb));
-    TS_ASSERT(! bb);
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(b.getAttribute(TestFlag1cd(), bb));
-    TS_ASSERT(! bb);
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(c.getAttribute(TestFlag1cd(), bb));
-    TS_ASSERT(! bb);
-
-    // setting boolean flags
-    Debug("cdboolattr") << "set flag 1 on a to T\n";
-    a.setAttribute(TestFlag1cd(), true);
-    Debug("cdboolattr") << "set flag 1 on b to F\n";
-    b.setAttribute(TestFlag1cd(), false);
-    Debug("cdboolattr") << "set flag 1 on c to F\n";
-    c.setAttribute(TestFlag1cd(), false);
-
-    Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
-    TS_ASSERT(a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    d_smtEngine->push(); // level 2
-
-    Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
-    TS_ASSERT(a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    Debug("cdboolattr") << "set flag 1 on a to F\n";
-    a.setAttribute(TestFlag1cd(), false);
-    Debug("cdboolattr") << "set flag 1 on b to T\n";
-    b.setAttribute(TestFlag1cd(), true);
-
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
-    TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    d_smtEngine->push(); // level 3
-
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
-    TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    Debug("cdboolattr") << "set flag 1 on c to T\n";
-    c.setAttribute(TestFlag1cd(), true);
-
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
-    TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be T)\n";
-    TS_ASSERT(c.getAttribute(TestFlag1cd()));
-
-    d_smtEngine->pop(); // level 2
-
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be T)\n";
-    TS_ASSERT(b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    d_smtEngine->pop(); // level 1
-
-    Debug("cdboolattr") << "get flag 1 on a (should be T)\n";
-    TS_ASSERT(a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    d_smtEngine->pop(); // level 0
-
-    Debug("cdboolattr") << "get flag 1 on a (should be F)\n";
-    TS_ASSERT(! a.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on b (should be F)\n";
-    TS_ASSERT(! b.getAttribute(TestFlag1cd()));
-    Debug("cdboolattr") << "get flag 1 on c (should be F)\n";
-    TS_ASSERT(! c.getAttribute(TestFlag1cd()));
-
-    TS_ASSERT_THROWS( d_smtEngine->pop(), ModalException );
-  }
-
   void testAttributes() {
     //Debug.on("boolattr");