added options for controlling resource step-count for various solving stages

35 files changed, 133 insertions, 83 deletions

diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 61900e59d..ffcf2db63 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -118,7 +118,7 @@ public:
 
   /** Gets the next decision based on strategies that are enabled */
   SatLiteral getNext(bool &stopSearch) {
-    NodeManager::currentResourceManager()->spendResource();
+    NodeManager::currentResourceManager()->spendResource(options::decisionStep());
     Assert(d_cnfStream != NULL,
            "Forgot to set cnfStream for decision engine?");
     Assert(d_satSolver != NULL,
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 10a729420..d17d5d141 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -31,6 +31,7 @@
 #include "util/output.h"
 #include "util/resource_manager.h"
 #include "options/options.h"
+#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -499,14 +500,14 @@ Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException)
       dynamic_cast<QuitCommand*>(cmd) == NULL) {
     // don't count set-option commands as to not get stuck in an infinite
     // loop of resourcing out
-    d_resourceManager->spendResource();
+    d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]);
   }
   return cmd;
 }
 
 Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
   Debug("parser") << "nextExpression()" << std::endl;
-  d_resourceManager->spendResource();
+  d_resourceManager->spendResource(d_exprManager->getOptions()[options::parseStep]);
   Expr result;
   if(!done()) {
     try {
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 6246e6885..2c9662655 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -46,11 +46,11 @@ private:
       d_notify->notify(satClause);
     }
 
-    void spendResource() {
-      d_notify->spendResource();
+    void spendResource(uint64_t ammount) {
+      d_notify->spendResource(ammount);
     }
-    void safePoint() {
-      d_notify->safePoint();
+    void safePoint(uint64_t ammount) {
+      d_notify->safePoint(ammount);
     }
   };
 
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index b6238460b..1267561fb 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -29,6 +29,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "util/utility.h"
 #include "util/exception.h"
 #include "theory/bv/options.h"
+#include "smt/options.h"
 #include "theory/interrupted.h"
 using namespace BVMinisat;
 
@@ -871,7 +872,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             // NO CONFLICT
             bool isWithinBudget;
             try {
-              isWithinBudget = withinBudget(); 
+              isWithinBudget = withinBudget(CVC4::options::bvSatConflictStep()); 
             }
             catch (const CVC4::theory::Interrupted& e) {
               // do some clean-up and rethrow 
@@ -1021,7 +1022,7 @@ lbool Solver::solve_()
     while (status == l_Undef){
         double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
         status = search(rest_base * restart_first);
-        if (!withinBudget()) break;
+        if (!withinBudget(CVC4::options::bvSatConflictStep())) break;
         curr_restarts++;
     }
 
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 3fcf34185..7d2a978b9 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -52,8 +52,8 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
-  virtual void spendResource() = 0;
-  virtual void safePoint() = 0;
+  virtual void spendResource(uint64_t ammount) = 0;
+  virtual void safePoint(uint64_t ammount) = 0;
 };
 
 //=================================================================================================
@@ -324,7 +324,7 @@ protected:
     CRef     reason           (Var x) const;
     int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
-    bool     withinBudget     ()      const;
+    bool     withinBudget     (uint64_t ammount)      const;
 
     // Static helpers:
     //
@@ -412,10 +412,10 @@ inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagati
 inline void     Solver::interrupt(){ asynch_interrupt = true; }
 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
-inline bool     Solver::withinBudget() const {
+inline bool     Solver::withinBudget(uint64_t ammount) const {
     Assert (notify);
-    notify->spendResource();
-    notify->safePoint();
+    notify->spendResource(ammount);
+    notify->safePoint(0);
 
     return !asynch_interrupt &&
            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index c8d86c73d..f03cc9944 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -679,7 +679,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
-    NodeManager::currentResourceManager()->spendResource();
+    NodeManager::currentResourceManager()->spendResource(options::cnfStep());
     d_convertAndAssertCounter = 0;
   }
   ++d_convertAndAssertCounter;
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 56316ca0b..2c94401fb 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -1205,7 +1205,8 @@ lbool Solver::search(int nof_conflicts)
               check_type = CHECK_WITH_THEORY;
             }
 
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) {
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts ||
+                !withinBudget(options::satConflictStep())) {
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
                 cancelUntil(0);
@@ -1343,11 +1344,11 @@ lbool Solver::solve_()
     while (status == l_Undef){
         double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
         status = search(rest_base * restart_first);
-        if (!withinBudget()) break;
+        if (!withinBudget(options::satConflictStep())) break; // FIXME add restart option?
         curr_restarts++;
     }
 
-    if(!withinBudget())
+    if(!withinBudget(options::satConflictStep()))
         status = l_Undef;
 
     if (verbosity >= 1)
@@ -1599,7 +1600,7 @@ CRef Solver::updateLemmas() {
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
   // Avoid adding lemmas indefinitely without resource-out
-  proxy->spendResource();
+  proxy->spendResource(options::lemmaStep());
 
   CRef conflict = CRef_Undef;
 
@@ -1717,11 +1718,11 @@ CRef Solver::updateLemmas() {
   return conflict;
 }
 
-inline bool Solver::withinBudget() const {
+inline bool Solver::withinBudget(uint64_t ammount) const {
   Assert (proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
   // depending on whether hard-limit is enabled
-  proxy->spendResource();
+  proxy->spendResource(ammount);
 
   bool within_budget =  !asynch_interrupt &&
     (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 9243a2b35..1508e3e35 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -424,7 +424,7 @@ protected:
     int      trail_index      (Var x) const; // Index in the trail
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 public:
-    bool     withinBudget     ()      const;
+    bool     withinBudget     (uint64_t amount)      const;
 protected:
 
     // Static helpers:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c7dae533e..e6d965f8f 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -281,8 +281,8 @@ void PropEngine::interrupt() throw(ModalException) {
   Debug("prop") << "interrupt()" << endl;
 }
 
-void PropEngine::spendResource() throw (UnsafeInterruptException) {
-  d_resourceManager->spendResource();
+void PropEngine::spendResource(uint64_t ammount) throw (UnsafeInterruptException) {
+  d_resourceManager->spendResource(ammount);
 }
 
 bool PropEngine::properExplanation(TNode node, TNode expl) const {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 2750319e6..17ac394c3 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -228,7 +228,7 @@ public:
    * Informs the ResourceManager that a resource has been spent.  If out of
    * resources, can throw an UnsafeInterruptException exception.
    */
-  void spendResource() throw (UnsafeInterruptException);
+  void spendResource(uint64_t ammount) throw (UnsafeInterruptException);
 
   /**
    * For debugging.  Return true if "expl" is a well-formed
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 8effa8189..79758a425 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -97,8 +97,8 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
-    virtual void spendResource() = 0;
-    virtual void safePoint() = 0;
+    virtual void spendResource(uint64_t ammount) = 0;
+    virtual void safePoint(uint64_t ammount) = 0;
     
   };/* class BVSatSolverInterface::Notify */
 
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 59e87dd33..5b80b7596 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -103,7 +103,7 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
 }
 
 void TheoryProxy::notifyRestart() {
-  d_propEngine->spendResource();
+  d_propEngine->spendResource(options::restartStep());
   d_theoryEngine->notifyRestart();
 
   static uint32_t lemmaCount = 0;
@@ -179,8 +179,8 @@ void TheoryProxy::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
-void TheoryProxy::spendResource() {
-  d_theoryEngine->spendResource();
+void TheoryProxy::spendResource(uint64_t ammount) {
+  d_theoryEngine->spendResource(ammount);
 }
 
 bool TheoryProxy::isDecisionRelevant(SatVariable var) {
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 3565aa501..d978edefd 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -111,7 +111,7 @@ public:
 
   void logDecision(SatLiteral lit);
 
-  void spendResource();
+  void spendResource(uint64_t ammount);
 
   bool isDecisionEngineDone();
 
diff --git a/src/smt/options b/src/smt/options
index b23d73943..dbee33f5a 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -104,6 +104,44 @@ common-option hardLimit hard-limit --hard-limit bool :default false
 common-option cpuTime cpu-time --cpu-time bool :default false
  measures CPU time if set to true and wall time if false (default false)
 
+# Resource spending options for SPARK
+expert-option rewriteStep rewrite-step --rewrite-step uint64_t :default 1
+ ammount of resources spent for each rewrite step
+
+expert-option theoryCheckStep theory-check-step --theory-check-step uint64_t :default 1
+ ammount of resources spent for each theory check call
+
+expert-option decisionStep decision-step --decision-step uint64_t :default 1
+ ammount of getNext decision calls in the decision engine
+ 
+expert-option bitblastStep bitblast-step --bitblast-step uint64_t :default 1
+ ammount of resources spent for each bitblast step
+ 
+expert-option parseStep parse-step --parse-step uint64_t :default 1
+ ammount of resources spent for each command/expression parsing
+ 
+expert-option lemmaStep lemma-step --lemma-step uint64_t :default 1
+ ammount of resources spent when adding lemmas
+ 
+expert-option restartStep restart-step --restart-step uint64_t :default 1
+ ammount of resources spent for each theory restart
+ 
+expert-option cnfStep cnf-step --cnf-step uint64_t :default 1
+ ammount of resources spent for each call to cnf conversion
+ 
+expert-option preprocessStep preprocess-step --preprocess-step uint64_t :default 1
+ ammount of resources spent for each preprocessing step in SmtEngine
+ 
+expert-option quantifierStep quantifier-step --quantifier-step uint64_t :default 1
+ ammount of resources spent for quantifier instantiations
+ 
+expert-option satConflictStep sat-conflict-step --sat-conflict-step uint64_t :default 1
+ ammount of resources spent for each sat conflict (main sat solver)
+ 
+expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step uint64_t :default 1
+ ammount of resources spent for each sat conflict (bitvectors)
+ 
+ 
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
  eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index bc594a47e..c7c0bc71a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -492,8 +492,8 @@ public:
   }
 
   ResourceManager* getResourceManager() { return d_resourceManager; }
-  void spendResource() throw(UnsafeInterruptException) {
-    d_resourceManager->spendResource();
+  void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+    d_resourceManager->spendResource(ammount);
   }
 
   void nmNotifyNewSort(TypeNode tn, uint32_t flags) {
@@ -1776,7 +1776,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   // or upward pass).
 
   do {
-    spendResource();
+    spendResource(options::preprocessStep());
     n = worklist.top().first;                      // n is the input / original
     Node node = worklist.top().second;             // node is the output / result
     bool childrenPushed = worklist.top().third;
@@ -1912,7 +1912,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
 void SmtEnginePrivate::removeITEs() {
   d_smt.finalOptionsAreSet();
-  spendResource();
+  spendResource(options::preprocessStep());
   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 
   // Remove all of the ITE occurrences and normalize
@@ -1924,7 +1924,7 @@ void SmtEnginePrivate::removeITEs() {
 
 void SmtEnginePrivate::staticLearning() {
   d_smt.finalOptionsAreSet();
-  spendResource();
+  spendResource(options::preprocessStep());
 
   TimerStat::CodeTimer staticLearningTimer(d_smt.d_stats->d_staticLearningTime);
 
@@ -1957,7 +1957,7 @@ static void dumpAssertions(const char* key, const AssertionPipeline& assertionLi
 
 // returns false if it learns a conflict
 bool SmtEnginePrivate::nonClausalSimplify() {
-  spendResource();
+  spendResource(options::preprocessStep());
   d_smt.finalOptionsAreSet();
 
   if(options::unsatCores()) {
@@ -2286,7 +2286,7 @@ void SmtEnginePrivate::bvAbstraction() {
 
 void SmtEnginePrivate::bvToBool() {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
-  spendResource();
+  spendResource(options::preprocessStep());
   std::vector<Node> new_assertions;
   d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
@@ -2297,13 +2297,13 @@ void SmtEnginePrivate::bvToBool() {
 bool SmtEnginePrivate::simpITE() {
   TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
 
-  spendResource();
+  spendResource(options::preprocessStep());
 
   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
 
   unsigned numAssertionOnEntry = d_assertions.size();
   for (unsigned i = 0; i < d_assertions.size(); ++i) {
-    spendResource();
+    spendResource(options::preprocessStep());
     Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
     d_assertions.replace(i, result);
     if(result.isConst() && !result.getConst<bool>()){
@@ -2350,7 +2350,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
 
 void SmtEnginePrivate::unconstrainedSimp() {
   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
-  spendResource();
+  spendResource(options::preprocessStep());
   Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
   d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
 }
@@ -2799,7 +2799,7 @@ void SmtEnginePrivate::doMiplibTrick() {
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
-  spendResource();
+  spendResource(options::preprocessStep());
   Assert(d_smt.d_pendingPops == 0);
   try {
     ScopeCounter depth(d_simplifyAssertionsDepth);
@@ -3042,7 +3042,7 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node,
 Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
   TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
 
-  spendResource();
+  spendResource(options::preprocessStep());
 
   if(d_booleanTermConverter == NULL) {
     // This needs to be initialized _after_ the whole SMT framework is in place, subscribed
@@ -3077,7 +3077,7 @@ Node SmtEnginePrivate::rewriteBooleanTerms(TNode n) {
 
 void SmtEnginePrivate::processAssertions() {
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
-  spendResource();
+  spendResource(options::preprocessStep());
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
 
@@ -3199,7 +3199,7 @@ void SmtEnginePrivate::processAssertions() {
                         << "applying substitutions" << endl;
       for (unsigned i = 0; i < d_assertions.size(); ++ i) {
         Trace("simplify") << "applying to " << d_assertions[i] << endl;
-         spendResource();
+         spendResource(options::preprocessStep());
         d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
         Trace("simplify") << "  got " << d_assertions[i] << endl;
       }
@@ -3759,7 +3759,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
 }
 
 Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
-  d_private->spendResource();
+  d_private->spendResource(options::preprocessStep());
 
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7b5b40c8b..565c69514 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/theory_arith.h"
 #include "theory/arith/theory_arith_private.h"
 #include "theory/arith/infer_bounds.h"
+#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -70,6 +71,7 @@ void TheoryArith::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 }
 
 void TheoryArith::check(Effort effortLevel){
+  getOutputChannel().spendResource(options::theoryCheckStep());
   d_internal->check(effortLevel);
 }
 
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index c770fb7ae..8bdf38ca3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,6 +23,7 @@
 #include "expr/command.h"
 #include "theory/theory_model.h"
 #include "theory/arrays/options.h"
+#include "smt/options.h"
 #include "smt/logic_exception.h"
 
 
@@ -1031,6 +1032,9 @@ void TheoryArrays::check(Effort e) {
   if (done() && !fullEffort(e)) {
     return;
   }
+  
+  getOutputChannel().spendResource(options::theoryCheckStep());
+
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
   while (!done() && !d_conflict)
@@ -1209,7 +1213,7 @@ void TheoryArrays::checkModel(Effort e)
   int numrestarts = 0;
   while (true || numrestarts < 1 || fullEffort(e) || combination(e)) {
     ++numrestarts;
-    d_out->safePoint();
+    d_out->safePoint(1);
     int level = getSatContext()->getLevel();
     d_getModelValCache.clear();
     for (constraintIdx = 0; constraintIdx < d_modelConstraints.size(); ++constraintIdx) {
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index d4d7bc04c..4d953b03c 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -135,8 +135,8 @@ class TLazyBitblaster :  public TBitblaster<Node> {
     {}
     bool notify(prop::SatLiteral lit);
     void notify(prop::SatClause& clause);
-    void spendResource();
-    void safePoint();
+    void spendResource(uint64_t ammount);
+    void safePoint(uint64_t ammount);
   };
   
   TheoryBV *d_bv;
@@ -240,10 +240,10 @@ public:
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) { return true; }
   void notify(prop::SatClause& clause) { }
-  void spendResource() {
-    NodeManager::currentResourceManager()->spendResource();
+  void spendResource(uint64_t ammount) {
+    NodeManager::currentResourceManager()->spendResource(ammount);
   }
-  void safePoint() {}
+  void safePoint(uint64_t ammount) {}
 };
 
 
diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index 57a635c20..0c087ddb9 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -67,7 +67,7 @@ bool EagerBitblastSolver::isInitialized() {
 }
 
 void EagerBitblastSolver::assertFormula(TNode formula) {
-  d_bv->spendResource();
+  d_bv->spendResource(1);
   Assert (isInitialized());
   Debug("bitvector-eager") << "EagerBitblastSolver::assertFormula "<< formula <<"\n"; 
   d_assertionSet.insert(formula);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index c86572ead..7e3ed46c8 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -152,7 +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();
+    d_bv->spendResource(1);
     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 9481b9894..13c31463b 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -21,6 +21,7 @@
 #include "theory/bv/slicer.h"
 #include "theory/theory_model.h"
 #include "theory/bv/options.h"
+#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -167,7 +168,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
 
-  d_bv->spendResource();
+  d_bv->spendResource(options::theoryCheckStep());
 
   d_checkCalled = true; 
   Assert (!d_bv->inConflict());
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 660551fe2..55dcbb03a 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -18,6 +18,7 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory_model.h"
+#include "smt/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -29,7 +30,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();
+  d_bv->spendResource(options::theoryCheckStep());
 
   bool ok = true;
   while (!done() && ok) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 065d5d5ef..eca9f12ab 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -103,7 +103,7 @@ void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  d_bv->spendResource();
+  d_bv->spendResource(options::bitblastStep());
   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 080f23143..61472fd79 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -170,7 +170,7 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  d_bv->spendResource();
+  d_bv->spendResource(options::bitblastStep());
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numTerms;
 
@@ -356,12 +356,12 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
-void TLazyBitblaster::MinisatNotify::spendResource() {
-  d_bv->spendResource();
+void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) {
+  d_bv->spendResource(ammount);
 }
 
-void TLazyBitblaster::MinisatNotify::safePoint() {
-  d_bv->d_out->safePoint();
+void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) {
+  d_bv->d_out->safePoint(ammount);
 }
 
 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 9dcd5ac62..6f399cb7a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -107,8 +107,8 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
-void TheoryBV::spendResource() throw(UnsafeInterruptException) {
-  getOutputChannel().spendResource();
+void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+  getOutputChannel().spendResource(ammount);
 }
 
 TheoryBV::Statistics::Statistics():
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 11d8cb895..3317d1b01 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,7 +103,7 @@ private:
 
   Statistics d_statistics;
 
-  void spendResource() throw(UnsafeInterruptException);
+  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
 
   /**
    * Return the uninterpreted function symbol corresponding to division-by-zero
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index bef39f536..f340c994c 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -86,7 +86,7 @@ public:
    * With safePoint(), the theory signals that it is at a safe point
    * and can be interrupted.
    */
-  virtual void safePoint() throw(Interrupted, UnsafeInterruptException, AssertionException) {
+  virtual void safePoint(uint64_t ammount) throw(Interrupted, UnsafeInterruptException, AssertionException) {
   }
 
   /**
@@ -213,7 +213,7 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource() throw(UnsafeInterruptException) {}
+  virtual void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {}
 
   /**
    * Handle user attribute.
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index afc607470..2177ebc32 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -767,7 +767,7 @@ bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool
 
 bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& terms, bool mkRep, bool modEq, bool modInst ) {
   // For resource-limiting (also does a time check).
-  getOutputChannel().safePoint();
+  getOutputChannel().safePoint(options::quantifierStep());
 
   Assert( terms.size()==f[0].getNumChildren() );
   Trace("inst-add-debug") << "Add instantiation: ";
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index a940bcc3d..842df69c5 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -116,7 +116,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
     if (hasSmtEngine &&
 		d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
-      rm->spendResource();
+      rm->spendResource(options::rewriteStep());
       d_iterationCount = 0;
     }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bbeec5125..75dafb7f6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1756,6 +1756,6 @@ std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, T
   return th->entailmentCheck(lit, params, seffects);
 }
 
-void TheoryEngine::spendResource() {
-  d_resourceManager->spendResource();
+void TheoryEngine::spendResource(uint64_t ammount) {
+  d_resourceManager->spendResource(ammount);
 }
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8aedc65f0..bb4d4c16d 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -282,8 +282,8 @@ class TheoryEngine {
     {
     }
 
-      void safePoint() throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
-      spendResource();
+      void safePoint(uint64_t ammount) throw(theory::Interrupted, UnsafeInterruptException, AssertionException) {
+      spendResource(ammount);
       if (d_engine->d_interrupted) {
         throw theory::Interrupted();
       }
@@ -347,8 +347,8 @@ class TheoryEngine {
       d_engine->setIncomplete(d_theory);
     }
 
-    void spendResource() throw(UnsafeInterruptException) {
-      d_engine->spendResource();
+    void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+      d_engine->spendResource(ammount);
     }
 
     void handleUserAttribute( const char* attr, theory::Theory* t ){
@@ -488,7 +488,7 @@ public:
   /**
    * "Spend" a resource during a search or preprocessing.
    */
-  void spendResource();
+  void spendResource(uint64_t ammount);
 
   /**
    * 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 46a717cc5..6fe92eb6e 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -69,7 +69,7 @@ public:
 
   ~TestOutputChannel() {}
 
-  void safePoint()  throw(Interrupted, AssertionException) {}
+  void safePoint(uint64_t ammount)  throw(Interrupted, AssertionException) {}
 
   void conflict(TNode n)
     throw(AssertionException, UnsafeInterruptException) {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index b00fdd6ee..073399894 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -17,6 +17,7 @@
 
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/options.h"
+#include "smt/options.h"
 #include "theory/quantifiers/options.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 #include "theory/theory_model.h"
@@ -92,7 +93,7 @@ void TheoryUF::check(Effort level) {
   if (done() && !fullEffort(level)) {
     return;
   }
-
+  getOutputChannel().spendResource(options::theoryCheckStep());
   TimerStat::CodeTimer checkTimer(d_checkTime);
 
   while (!done() && !d_conflict)
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 6d32120d9..37fea2c67 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -170,13 +170,13 @@ uint64_t ResourceManager::getTimeRemaining() const {
   return d_thisCallTimeBudget - time_passed;
 }
 
-void ResourceManager::spendResource() throw (UnsafeInterruptException) {
+void ResourceManager::spendResource(uint64_t ammount) throw (UnsafeInterruptException) {
   ++d_spendResourceCalls;
-  ++d_cumulativeResourceUsed;
+  d_cumulativeResourceUsed += ammount;
   if (!d_on) return;
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
-  ++d_thisCallResourceUsed;
+  d_thisCallResourceUsed += ammount;
   if(out()) {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
 	Trace("limit") << "                 on call " << d_spendResourceCalls << std::endl;
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index d1ec0456a..9c2812f0f 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -128,7 +128,7 @@ public:
     return d_thisCallResourceBudget;
   }
 
-  void spendResource() throw(UnsafeInterruptException);
+  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
 
   void setHardLimit(bool value);
   void setResourceLimit(uint64_t units, bool cumulative = false);