Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

1 files changed, 6 insertions, 5 deletions

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index b150b186a..44035e7d9 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -19,6 +19,8 @@
 #pragma once
 
 #include "expr/node.h"
+#include "util/unsafe_interrupt_exception.h"
+
 //#include "expr/attribute.h"
 
 namespace CVC4 {
@@ -56,7 +58,7 @@ class RewriterInitializer;
 class Rewriter {
 
   friend class RewriterInitializer;
-
+  static unsigned long d_iterationCount;
   /** Returns the appropriate cache for a node */
   static Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
 
@@ -100,20 +102,19 @@ class Rewriter {
    * Should be called to clean up any state.
    */
   static void shutdown();
-
+  static void clearCachesInternal();
 public:
 
   /**
    * Rewrites the node using theoryOf() to determine which rewriter to
    * use on the node.
    */
-  static Node rewrite(TNode node);
+  static Node rewrite(TNode node) throw (UnsafeInterruptException);
 
   /**
    * Garbage collects the rewrite caches.
    */
-  static void garbageCollect();
-
+  static void clearCaches();
 };/* class Rewriter */
 
 }/* CVC4::theory namespace */