summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2013-11-14 11:56:34 -0500
committerTim King <taking@cs.nyu.edu>2013-11-21 10:43:44 -0500
commit91424455840a7365a328cbcc3d02ec453fe9d0ea (patch)
treee8072eb0c7dda81feafb1c5f9a4ca2f0fcbc0399 /src/expr/node_manager.h
parentbd8e9319aab69db90692f72bc52288329879eefc (diff)
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.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h13
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 */
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback