Resource-limiting work.

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

17 files changed, 121 insertions, 55 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 0ff12da95..e13587323 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -28,6 +28,7 @@
 #include "prop/sat_solver.h"
 #include "theory/valuation.h"
 #include "theory/theory_registrar.h"
+#include "util/resource_manager.h"
 
 class Abc_Obj_t_;
 typedef Abc_Obj_t_ Abc_Obj_t;
@@ -134,6 +135,7 @@ class TLazyBitblaster :  public TBitblaster<Node> {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
+    void spendResource();
     void safePoint();
   };
   
@@ -228,7 +230,8 @@ private:
     Statistics(const std::string& name);
     ~Statistics();
   };
-  std::string d_name; 
+  std::string d_name;
+public:
   Statistics d_statistics;
 };
 
@@ -237,6 +240,9 @@ public:
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) { return true; }
   void notify(prop::SatClause& clause) { }
+  void spendResource() {
+    NodeManager::currentResourceManager()->spendResource();
+  }
   void safePoint() {}
 };
 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index f9f8ff581..57a635c20 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -67,6 +67,7 @@ bool EagerBitblastSolver::isInitialized() {
 }
 
 void EagerBitblastSolver::assertFormula(TNode formula) {
+  d_bv->spendResource();
   Assert (isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; 
   d_assertionSet.insert(formula);
diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index e8acf268f..5b139e327 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -557,6 +557,7 @@ bool AlgebraicSolver::isSubstitutableIn(TNode node, TNode in) {
 void AlgebraicSolver::processAssertions(std::vector<WorklistElement>& worklist, SubstitutionEx& subst) {
   bool changed = true;
   while(changed) {
+    // d_bv->spendResource();
     changed = false;
     for (unsigned i = 0; i < worklist.size(); ++i) {
       // apply current substitutions
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index d0b99f869..c86572ead 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -103,8 +103,11 @@ void BitblastSolver::bitblastQueue() {
       // don't bit-blast lemma atoms
       continue;
     }
-    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; 
-    d_bitblaster->bbAtom(atom);
+    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
+    {
+      TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
+      d_bitblaster->bbAtom(atom);
+    }
   }
 }
 
@@ -149,6 +152,7 @@ bool BitblastSolver::check(Theory::Effort e) {
 
   // We need to ensure we are fully propagated, so propagate now
   if (d_useSatPropagation) {
+    d_bv->spendResource();
     bool ok = d_bitblaster->propagate();
     if (!ok) {
       std::vector<TNode> conflictAtoms;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index d2c79fec2..938a93b85 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -166,6 +166,9 @@ bool CoreSolver::decomposeFact(TNode fact) {
 
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
+
+  d_bv->spendResource();
+
   d_checkCalled = true; 
   Assert (!d_bv->inConflict());
   ++(d_statistics.d_numCallstoCheck);
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 917b10c33..660551fe2 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -29,6 +29,7 @@ using namespace CVC4::theory::bv::utils;
 bool InequalitySolver::check(Theory::Effort e) {
   Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
   ++(d_statistics.d_numCallstoCheck);
+  d_bv->spendResource();
 
   bool ok = true;
   while (!done() && ok) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 877baec4e..065d5d5ef 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -103,6 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
+  d_bv->spendResource();
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
 
   d_termBBStrategies[node.getKind()] (node, bits, this);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index b74506e4d..e5b5ed664 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -170,6 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
+  d_bv->spendResource();
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -355,6 +356,10 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
+void TLazyBitblaster::MinisatNotify::spendResource() {
+  d_bv->spendResource();
+}
+
 void TLazyBitblaster::MinisatNotify::safePoint() {
   d_bv->d_out->safePoint();
 }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 99bc764dd..eddd5017c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -107,6 +107,10 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
+void TheoryBV::spendResource() throw(UnsafeInterruptException) {
+  getOutputChannel().spendResource();
+}
+
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
@@ -362,6 +366,7 @@ void TheoryBV::check(Effort e)
     return;
   }
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
+  TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
   // we may be getting new assertions so the model cache may not be sound
   d_invalidateModelCache.set(true); 
   // if we are using the eager solver
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index a37a4019e..11d8cb895 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,6 +103,7 @@ private:
 
   Statistics d_statistics;
 
+  void spendResource() throw(UnsafeInterruptException);
 
   /**
    * Return the uninterpreted function symbol corresponding to division-by-zero
@@ -218,6 +219,7 @@ private:
   friend class CoreSolver;
   friend class InequalitySolver;
   friend class AlgebraicSolver;
+  friend class EagerBitblastSolver;
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 40eba6ff5..fdf253d3f 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -21,6 +21,7 @@
 
 #include "util/cvc4_assert.h"
 #include "theory/interrupted.h"
+#include "util/resource_manager.h"
 
 namespace CVC4 {
 namespace theory {
@@ -84,7 +85,7 @@ public:
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
-  virtual void safePoint() throw(Interrupted, AssertionException) {
+  virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) {
   }
 
   /**
@@ -97,7 +98,7 @@ public:
    * unit conflict) which is assigned TRUE (and T-conflicting) in the
    * current assignment.
    */
-  virtual void conflict(TNode n) throw(AssertionException) = 0;
+  virtual void conflict(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Propagate a theory literal.
@@ -105,7 +106,7 @@ public:
    * @param n - a theory consequence at the current decision level
    * @return false if an immediate conflict was encountered
    */
-  virtual bool propagate(TNode n) throw(AssertionException) = 0;
+  virtual bool propagate(TNode n) throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Tell the core that a valid theory lemma at decision level 0 has
@@ -119,7 +120,7 @@ public:
    */
   virtual LemmaStatus lemma(TNode n, bool removable = false,
                             bool preprocess = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Request a split on a new theory atom.  This is equivalent to
@@ -128,12 +129,12 @@ public:
    * @param n - a theory atom; must be of Boolean type
    */
   LemmaStatus split(TNode n)
-    throw(TypeCheckingExceptionPrivate, AssertionException) {
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
     return splitLemma(n.orNode(n.notNode()));
   }
 
   virtual LemmaStatus splitLemma(TNode n, bool removable = false)
-    throw(TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * If a decision is made on n, it must be in the phase specified.
@@ -148,7 +149,7 @@ public:
    * @param phase - the phase to decide on n
    */
   virtual void requirePhase(TNode n, bool phase)
-    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Flips the most recent unflipped decision to the other phase and
@@ -191,14 +192,14 @@ public:
    * could be flipped, or if the root decision was re-flipped
    */
   virtual bool flipDecision()
-    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException) = 0;
+    throw(Interrupted, TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * Notification from a theory that it realizes it is incomplete at
    * this context level.  If SAT is later determined by the
    * TheoryEngine, it should actually return an UNKNOWN result.
    */
-  virtual void setIncomplete() throw(AssertionException) = 0;
+  virtual void setIncomplete() throw(AssertionException, UnsafeInterruptException) = 0;
 
   /**
    * "Spend" a "resource."  The meaning is specific to the context in
@@ -211,7 +212,7 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource() throw() {}
+  virtual void spendResource() throw(UnsafeInterruptException) {}
 
   /**
    * Handle user attribute.
@@ -226,7 +227,7 @@ public:
    * Using this leads to non-termination issues.
    * It is appropriate for prototyping for theories.
    */
-  virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {}
+  virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {}
 
 };/* class OutputChannel */
 
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 960602846..a940bcc3d 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -18,12 +18,16 @@
 #include "theory/theory.h"
 #include "theory/rewriter.h"
 #include "theory/rewriter_tables.h"
+#include "smt/smt_engine_scope.h"
+#include "util/resource_manager.h"
 
 using namespace std;
 
 namespace CVC4 {
 namespace theory {
 
+unsigned long Rewriter::d_iterationCount = 0;
+
 static TheoryId theoryOf(TNode node) {
   return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
 }
@@ -76,7 +80,7 @@ struct RewriteStackElement {
   }
 };
 
-Node Rewriter::rewrite(TNode node) {
+Node Rewriter::rewrite(TNode node) throw (UnsafeInterruptException){
   return rewriteTo(theoryOf(node), node);
 }
 
@@ -102,9 +106,20 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   vector<RewriteStackElement> rewriteStack;
   rewriteStack.push_back(RewriteStackElement(node, theoryId));
 
+  ResourceManager* rm = NULL;
+  bool hasSmtEngine = smt::smtEngineInScope();
+  if (hasSmtEngine) {
+    rm = NodeManager::currentResourceManager();
+  }
   // Rewrite until the stack is empty
   for (;;){
 
+    if (hasSmtEngine &&
+		d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
+      rm->spendResource();
+      d_iterationCount = 0;
+    }
+
     // Get the top of the recursion stack
     RewriteStackElement& rewriteStackTop = rewriteStack.back();
 
@@ -139,7 +154,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
         rewriteStackTop.theoryId = theoryOf(cached);
       }
     }
-    
+
     rewriteStackTop.original =rewriteStackTop.node;
     // Now it's time to rewrite the children, check if this has already been done
     Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
@@ -233,5 +248,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
   return Node::null();
 }/* Rewriter::rewriteTo() */
 
+void Rewriter::clearCaches() {
+#ifdef CVC4_ASSERTIONS
+  if(s_rewriteStack != NULL) {
+    delete s_rewriteStack;
+    s_rewriteStack = NULL;
+  }
+#endif
+  Rewriter::clearCachesInternal();
+}
+
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
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 */
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 9b51d2b32..d79f464b5 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -85,7 +85,7 @@ void Rewriter::shutdown() {
 ${rewrite_shutdown}
 }
 
-void Rewriter::garbageCollect() {
+void Rewriter::clearCachesInternal() {
   typedef CVC4::expr::attr::AttributeUniqueId AttributeUniqueId;
   std::vector<AttributeUniqueId> preids;
   ${pre_rewrite_attribute_ids}
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 12a169e09..d83626a6b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -26,6 +26,7 @@
 #include "expr/node_builder.h"
 #include "options/options.h"
 #include "util/lemma_output_channel.h"
+#include "util/resource_manager.h"
 
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
@@ -142,6 +143,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true(),
   d_false(),
   d_interrupted(false),
+  d_resourceManager(NodeManager::currentResourceManager()),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
@@ -334,8 +336,7 @@ void TheoryEngine::dumpAssertions(const char* tag) {
  * @param effort the effort level to use
  */
 void TheoryEngine::check(Theory::Effort effort) {
-
-  d_propEngine->checkTime();
+  // spendResource();
 
   // Reset the interrupt flag
   d_interrupted = false;
@@ -846,6 +847,7 @@ struct preprocess_stack_element {
 Node TheoryEngine::preprocess(TNode assertion) {
 
   Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
+  // spendResource();
 
   // Do a topological sort of the subexpressions and substitute them
   vector<preprocess_stack_element> toVisit;
@@ -1082,7 +1084,7 @@ void TheoryEngine::assertFact(TNode literal)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
 
-  d_propEngine->checkTime();
+  // spendResource();
 
   // If we're in conflict, nothing to do
   if (d_inConflict) {
@@ -1145,7 +1147,7 @@ bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
   Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
 
-  d_propEngine->checkTime();
+  // spendResource();
 
   if(Dump.isOn("t-propagations")) {
     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
@@ -1368,7 +1370,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 
 theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) {
   // For resource-limiting (also does a time check).
-  spendResource();
+  // spendResource();
 
   // Do we need to check atoms
   if (atomsTo != theory::THEORY_LAST) {
@@ -1553,7 +1555,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
         Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
         Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
         d_iteUtilities->clear();
-        Rewriter::garbageCollect();
+        Rewriter::clearCaches();
         d_iteRemover.garbageCollect();
         nm->reclaimZombiesUntil(options::zombieHuntThreshold());
         Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
@@ -1742,3 +1744,7 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T
 
   return th->entailmentCheck(lit, params, seffects);
 }
+
+void TheoryEngine::spendResource() {
+  d_resourceManager->spendResource();
+}
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 136c0409f..6360ea5fb 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -39,6 +39,7 @@
 #include "util/statistics_registry.h"
 #include "util/cvc4_assert.h"
 #include "util/sort_inference.h"
+#include "util/unsafe_interrupt_exception.h"
 #include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/bv/bv_to_bool.h"
@@ -46,6 +47,8 @@
 
 namespace CVC4 {
 
+class ResourceManager;
+  
 /**
  * A pair of a theory and a node. This is used to mark the flow of
  * propagations between theories.
@@ -279,42 +282,42 @@ class TheoryEngine {
     {
     }
 
-    void safePoint() throw(theory::Interrupted, AssertionException) {
+      void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
       spendResource();
       if (d_engine->d_interrupted) {
         throw theory::Interrupted();
       }
     }
 
-    void conflict(TNode conflictNode) throw(AssertionException) {
+    void conflict(TNode conflictNode) throw(AssertionException, UnsafeInterruptException) {
       Trace("theory::conflict") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl;
       ++ d_statistics.conflicts;
       d_engine->d_outputChannelUsed = true;
       d_engine->conflict(conflictNode, d_theory);
     }
 
-    bool propagate(TNode literal) throw(AssertionException) {
+    bool propagate(TNode literal) throw(AssertionException, UnsafeInterruptException) {
       Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
       ++ d_statistics.propagations;
       d_engine->d_outputChannelUsed = true;
       return d_engine->propagate(literal, d_theory);
     }
 
-    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+    theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
       return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST);
     }
 
-    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) {
+    theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl;
       ++ d_statistics.lemmas;
       d_engine->d_outputChannelUsed = true;
       return d_engine->lemma(lemma, false, removable, false, d_theory);
     }
 
-    void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {
+    void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
       NodeManager* curr = NodeManager::currentNM();
       Node restartVar =  curr->mkSkolem("restartVar",
                                         curr->booleanType(),
@@ -325,7 +328,7 @@ class TheoryEngine {
     }
 
     void requirePhase(TNode n, bool phase)
-      throw(theory::Interrupted, AssertionException) {
+      throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
       Debug("theory") << "EngineOutputChannel::requirePhase("
                       << n << ", " << phase << ")" << std::endl;
       ++ d_statistics.requirePhase;
@@ -333,18 +336,18 @@ class TheoryEngine {
     }
 
     bool flipDecision()
-      throw(theory::Interrupted, AssertionException) {
+      throw(theory::Interrupted, AssertionException, UnsafeInterruptException) {
       Debug("theory") << "EngineOutputChannel::flipDecision()" << std::endl;
       ++ d_statistics.flipDecision;
       return d_engine->d_propEngine->flipDecision();
     }
 
-    void setIncomplete() throw(AssertionException) {
+    void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
       Trace("theory") << "TheoryEngine::setIncomplete()" << std::endl;
       d_engine->setIncomplete(d_theory);
     }
 
-    void spendResource() throw() {
+    void spendResource() throw(UnsafeInterruptException) {
       d_engine->spendResource();
     }
 
@@ -387,12 +390,6 @@ class TheoryEngine {
     d_incomplete = true;
   }
 
-  /**
-   * "Spend" a resource during a search or preprocessing.
-   */
-  void spendResource() throw() {
-    d_propEngine->spendResource();
-  }
 
   /**
    * Mapping of propagations from recievers to senders.
@@ -477,6 +474,7 @@ class TheoryEngine {
 
   /** Whether we were just interrupted (or not) */
   bool d_interrupted;
+  ResourceManager* d_resourceManager;
 
 public:
 
@@ -487,6 +485,10 @@ public:
   ~TheoryEngine();
 
   void interrupt() throw(ModalException);
+  /**
+   * "Spend" a resource during a search or preprocessing.
+   */
+  void spendResource();
 
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 6d1275c20..46a717cc5 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -23,13 +23,13 @@
 #include "expr/node.h"
 #include "theory/output_channel.h"
 #include "theory/interrupted.h"
+#include "util/unsafe_interrupt_exception.h"
 
 #include <vector>
 #include <utility>
 #include <iostream>
 
 namespace CVC4 {
-
 namespace theory {
 
 /**
@@ -72,42 +72,44 @@ public:
   void safePoint()  throw(Interrupted, AssertionException) {}
 
   void conflict(TNode n)
-    throw(AssertionException) {
+    throw(AssertionException, UnsafeInterruptException) {
     push(CONFLICT, n);
   }
 
   bool propagate(TNode n)
-    throw(AssertionException) {
+    throw(AssertionException, UnsafeInterruptException) {
     push(PROPAGATE, n);
     return true;
   }
 
   void propagateAsDecision(TNode n)
-    throw(AssertionException) {
+    throw(AssertionException, UnsafeInterruptException) {
     push(PROPAGATE_AS_DECISION, n);
   }
 
-  LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException) {
+  LemmaStatus lemma(TNode n, bool removable, bool preprocess) throw(AssertionException, UnsafeInterruptException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
 
-  void requirePhase(TNode, bool) throw(Interrupted, AssertionException) {
+  void requirePhase(TNode, bool) throw(Interrupted, AssertionException, UnsafeInterruptException) {
   }
 
-  bool flipDecision() throw(Interrupted, AssertionException) {
+  bool flipDecision() throw(Interrupted, AssertionException, UnsafeInterruptException) {
     return true;
   }
 
-  void setIncomplete() throw(AssertionException) {}
+  void setIncomplete() throw(AssertionException, UnsafeInterruptException) {
+  }
 
-  void handleUserAttribute( const char* attr, theory::Theory* t ){}
+  void handleUserAttribute( const char* attr, theory::Theory* t ) {
+  }
 
   void clear() {
     d_callHistory.clear();
   }
 
-  LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException){
+  LemmaStatus splitLemma(TNode n, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException, UnsafeInterruptException) {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
@@ -125,7 +127,7 @@ public:
     return d_callHistory.size();
   }
 
-  void printIth(std::ostream& os, int i){
+  void printIth(std::ostream& os, int i) {
     os << "[TestOutputChannel " << i;
     os << " " << getIthCallType(i);
     os << " " << getIthNode(i) << "]";