Adding the changes needed to delete rewriter attributes. This includes being able to list attributes. Additionally, added debugging hooks to node manager and attribute manager.

1 files changed, 63 insertions, 0 deletions

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 20d52e3cc..92a21546c 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -26,6 +26,15 @@ namespace CVC4 {
 namespace expr {
 namespace attr {
 
+
+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
+   * the AttributeManager without recompiling all of CVC4.
+   * Formally this is a nop.
+   */
+}
+
 void AttributeManager::deleteAllAttributes(NodeValue* nv) {
   d_bools.erase(nv);
   deleteFromTable(d_ints, nv);
@@ -60,6 +69,60 @@ void AttributeManager::deleteAllAttributes() {
   d_cdptrs.clear();
 }
 
+void AttributeManager::deleteAttributes(const AttrIdVec& atids){
+  typedef std::map<uint64_t, std::vector< uint64_t> > AttrToVecMap;
+  AttrToVecMap perTableIds;
+
+  for(AttrIdVec::const_iterator it = atids.begin(), it_end = atids.end(); it != it_end; ++it){
+    const AttributeUniqueId& pair = *(*it);
+    std::vector< uint64_t>& inTable = perTableIds[pair.getTableId()];
+    inTable.push_back(pair.getWithinTypeId());
+  }
+  AttrToVecMap::iterator it = perTableIds.begin(), it_end = perTableIds.end();
+  for(; it != it_end; ++it){
+    Assert(((*it).first) <= LastAttrTable);
+    AttrTableId tableId = (AttrTableId) ((*it).first);
+    std::vector< uint64_t>& ids = (*it).second;
+    std::sort(ids.begin(), ids.end());
+
+    switch(tableId){
+    case AttrTableBool:
+      Unimplemented("delete attributes is unimplemented for bools");
+      break;
+    case AttrTableUInt64:
+      deleteAttributesFromTable(d_ints, ids);
+      break;
+    case AttrTableTNode:
+      deleteAttributesFromTable(d_tnodes, ids);
+      break;
+    case AttrTableNode:
+      deleteAttributesFromTable(d_nodes, ids);
+      break;
+    case AttrTableTypeNode:
+      deleteAttributesFromTable(d_types, ids);
+      break;
+    case AttrTableString:
+      deleteAttributesFromTable(d_strings, ids);
+      break;
+    case AttrTablePointer:
+      deleteAttributesFromTable(d_ptrs, ids);
+      break;
+
+    case AttrTableCDBool:
+    case AttrTableCDUInt64:
+    case AttrTableCDTNode:
+    case AttrTableCDNode:
+    case AttrTableCDString:
+    case AttrTableCDPointer:
+      Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behaviour is desired.");
+      break;
+    case LastAttrTable:
+    default:
+      Unreachable();
+    }
+  }
+}
+
 }/* CVC4::expr::attr namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */