1 files changed, 13 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 51ed1f94d..32c492003 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -46,6 +46,7 @@ class StatisticsRegistry;
 
 namespace expr {
   namespace attr {
+    class AttributeUniqueId;
     class AttributeManager;
   }/* CVC4::expr::attr namespace */
 
@@ -859,6 +860,18 @@ public:
    */
   static inline TypeNode fromType(Type t);
 
+  /** Deletes a list of attributes from the NM's AttributeManager.*/
+  void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
+
+  /**
+   * This function gives developers a hook into the NodeManager.
+   * This can be changed in node_manager.cpp without recompiling most of cvc4.
+   *
+   * debugHook is a debugging only function, and should not be present in
+   * any published code!
+   */
+  void debugHook(int debugFlag);
+
 };/* class NodeManager */
 
 /**