changed resource step options to unsigned

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 2c966265591a484fadbab5290fb92e8923c8e39d..0bf4edf6a8cb1bde36259639f34baf34e5a6aebe 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -46,10 +46,10 @@ private:
       d_notify->notify(satClause);
     }
 
-    void spendResource(uint64_t ammount) {
+    void spendResource(unsigned ammount) {
       d_notify->spendResource(ammount);
     }
-    void safePoint(uint64_t ammount) {
+    void safePoint(unsigned ammount) {
       d_notify->safePoint(ammount);
     }
   };

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 7d2a978b9de90788e5c32187d3fbfc4fbf0a2375..016a0c22558e68f87a112723a25fd11ce97c0136 100644 (file)
--- 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(uint64_t ammount) = 0;
-  virtual void safePoint(uint64_t ammount) = 0;
+  virtual void spendResource(unsigned ammount) = 0;
+  virtual void safePoint(unsigned ammount) = 0;
 };
 
 //=================================================================================================

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e6d965f8f174044c495dab75d90785d41ae7a666..794e36e2c4997a3cf7b8df2318456047f6873103 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -281,7 +281,7 @@ void PropEngine::interrupt() throw(ModalException) {
   Debug("prop") << "interrupt()" << endl;
 }
 
-void PropEngine::spendResource(uint64_t ammount) throw (UnsafeInterruptException) {
+void PropEngine::spendResource(unsigned ammount) throw (UnsafeInterruptException) {
   d_resourceManager->spendResource(ammount);
 }
 

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 17ac394c369217c4d65d2e31c3476d52239b4c88..768f07108334125dcb5d7abff42682f653e21d43 100644 (file)
--- 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(uint64_t ammount) throw (UnsafeInterruptException);
+  void spendResource(unsigned 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 79758a425fe2182466c100d711f51d13d2d1014a..50d3085412f6b6ccf17bc89dd51efd2cf8bcfc89 100644 (file)
--- 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(uint64_t ammount) = 0;
-    virtual void safePoint(uint64_t ammount) = 0;
+    virtual void spendResource(unsigned ammount) = 0;
+    virtual void safePoint(unsigned ammount) = 0;
     
   };/* class BVSatSolverInterface::Notify */
 

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 5b80b7596949bdd44bd80cf18de5d13705a47733..9c6da703a563ff396b8f97362489043607d9c23e 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -179,7 +179,7 @@ void TheoryProxy::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
-void TheoryProxy::spendResource(uint64_t ammount) {
+void TheoryProxy::spendResource(unsigned ammount) {
   d_theoryEngine->spendResource(ammount);
 }
 

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index d978edefd99b5a7aa38b6f19122059a3460210ea..90ad558f5c917cb4d0297d76226152d4e4eb3c8e 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -111,7 +111,7 @@ public:
 
   void logDecision(SatLiteral lit);
 
-  void spendResource(uint64_t ammount);
+  void spendResource(unsigned ammount);
 
   bool isDecisionEngineDone();
 

diff --git a/src/smt/options b/src/smt/options
index dbee33f5aea32104335c5936777d2b5fd684e0e2..077acc6e9f63911f44f3fdf7b827d0e4daa752f2 100644 (file)
--- a/src/smt/options
+++ b/src/smt/options
@@ -105,40 +105,40 @@ 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
+expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
  ammount of resources spent for each rewrite step
 
-expert-option theoryCheckStep theory-check-step --theory-check-step uint64_t :default 1
+expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
  ammount of resources spent for each theory check call
 
-expert-option decisionStep decision-step --decision-step uint64_t :default 1
+expert-option decisionStep decision-step --decision-step unsigned :default 1
  ammount of getNext decision calls in the decision engine
  
-expert-option bitblastStep bitblast-step --bitblast-step uint64_t :default 1
+expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
  ammount of resources spent for each bitblast step
  
-expert-option parseStep parse-step --parse-step uint64_t :default 1
+expert-option parseStep parse-step --parse-step unsigned :default 1
  ammount of resources spent for each command/expression parsing
  
-expert-option lemmaStep lemma-step --lemma-step uint64_t :default 1
+expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
  ammount of resources spent when adding lemmas
  
-expert-option restartStep restart-step --restart-step uint64_t :default 1
+expert-option restartStep restart-step --restart-step unsigned :default 1
  ammount of resources spent for each theory restart
  
-expert-option cnfStep cnf-step --cnf-step uint64_t :default 1
+expert-option cnfStep cnf-step --cnf-step unsigned :default 1
  ammount of resources spent for each call to cnf conversion
  
-expert-option preprocessStep preprocess-step --preprocess-step uint64_t :default 1
+expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
  ammount of resources spent for each preprocessing step in SmtEngine
  
-expert-option quantifierStep quantifier-step --quantifier-step uint64_t :default 1
+expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
  ammount of resources spent for quantifier instantiations
  
-expert-option satConflictStep sat-conflict-step --sat-conflict-step uint64_t :default 1
+expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :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
+expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
  ammount of resources spent for each sat conflict (bitvectors)
  
  

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c7c0bc71a854899772c4735cf3ba2a471b65ec0e..11a412c7529a6a5755f77b23d61a6665a463d02d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -492,7 +492,7 @@ public:
   }
 
   ResourceManager* getResourceManager() { return d_resourceManager; }
-  void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+  void spendResource(unsigned ammount) throw(UnsafeInterruptException) {
     d_resourceManager->spendResource(ammount);
   }
 

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 4d953b03c0d37242985b7682c18574fa7ffa1764..d42c4a8c9c39c180b02440946ceaad425b2f020d 100644 (file)
--- 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(uint64_t ammount);
-    void safePoint(uint64_t ammount);
+    void spendResource(unsigned ammount);
+    void safePoint(unsigned ammount);
   };
   
   TheoryBV *d_bv;
@@ -240,10 +240,10 @@ public:
   MinisatEmptyNotify() {}
   bool notify(prop::SatLiteral lit) { return true; }
   void notify(prop::SatClause& clause) { }
-  void spendResource(uint64_t ammount) {
+  void spendResource(unsigned ammount) {
     NodeManager::currentResourceManager()->spendResource(ammount);
   }
-  void safePoint(uint64_t ammount) {}
+  void safePoint(unsigned ammount) {}
 };
 
 

diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 61472fd79bf8c65e0e9a0ae0e87ffa7ab0a23895..59ecc738556822874bd95220f24917b7c3b7059f 100644 (file)
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -356,11 +356,11 @@ void TLazyBitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 }
 
-void TLazyBitblaster::MinisatNotify::spendResource(uint64_t ammount) {
+void TLazyBitblaster::MinisatNotify::spendResource(unsigned ammount) {
   d_bv->spendResource(ammount);
 }
 
-void TLazyBitblaster::MinisatNotify::safePoint(uint64_t ammount) {
+void TLazyBitblaster::MinisatNotify::safePoint(unsigned ammount) {
   d_bv->d_out->safePoint(ammount);
 }
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 6f399cb7aa074cbd721adf1a4afab4cd64be7eba..95a483d34e3da615133842cac77828e4241af815 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -107,7 +107,7 @@ void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
   }
 }
 
-void TheoryBV::spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+void TheoryBV::spendResource(unsigned ammount) throw(UnsafeInterruptException) {
   getOutputChannel().spendResource(ammount);
 }
 

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 3317d1b010d2ac5ef9bb30f7e9ef81c909188140..193de55db7c9b9dad017ed78ee893d09245a6ed0 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -103,7 +103,7 @@ private:
 
   Statistics d_statistics;
 
-  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
+  void spendResource(unsigned 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 f340c994cc2c2e9a46425e8388dc56f1de6f1cbb..2da0f04670a80137a55b91c9959f7d5b9409acbf 100644 (file)
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -213,7 +213,7 @@ public:
    * long-running operations, they cannot rely on resource() to break
    * out of infinite or intractable computations.
    */
-  virtual void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {}
+  virtual void spendResource(unsigned ammount) throw(UnsafeInterruptException) {}
 
   /**
    * Handle user attribute.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 75dafb7f61a740df9ba690a3eeefa6238578f382..9b4815fd4c5d7824c29beb250c8cd60f0090bc9c 100644 (file)
--- 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(uint64_t ammount) {
+void TheoryEngine::spendResource(unsigned ammount) {
   d_resourceManager->spendResource(ammount);
 }

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bb4d4c16d7a967b8147aab868af12ff3f988ce55..0c1a7c0811bdcb29260f2b58cac6d5b84b685b1b 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -347,7 +347,7 @@ class TheoryEngine {
       d_engine->setIncomplete(d_theory);
     }
 
-    void spendResource(uint64_t ammount) throw(UnsafeInterruptException) {
+    void spendResource(unsigned ammount) throw(UnsafeInterruptException) {
       d_engine->spendResource(ammount);
     }
 
@@ -488,7 +488,7 @@ public:
   /**
    * "Spend" a resource during a search or preprocessing.
    */
-  void spendResource(uint64_t ammount);
+  void spendResource(unsigned ammount);
 
   /**
    * Adds a theory. Only one theory per TheoryId can be present, so if

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 37fea2c67f6082952fa1a8a1eb5d03daa7c1313d..22496a4337ef84c8b73761dd145573853a7dcc27 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -170,7 +170,7 @@ uint64_t ResourceManager::getTimeRemaining() const {
   return d_thisCallTimeBudget - time_passed;
 }
 
-void ResourceManager::spendResource(uint64_t ammount) throw (UnsafeInterruptException) {
+void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) {
   ++d_spendResourceCalls;
   d_cumulativeResourceUsed += ammount;
   if (!d_on) return;

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 9c2812f0f13363d5bfdd043d0b813dda27c6a879..e84917db032f05015cc0aeec859c5de13ce65c7d 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -128,7 +128,7 @@ public:
     return d_thisCallResourceBudget;
   }
 
-  void spendResource(uint64_t ammount) throw(UnsafeInterruptException);
+  void spendResource(unsigned ammount) throw(UnsafeInterruptException);
 
   void setHardLimit(bool value);
   void setResourceLimit(uint64_t units, bool cumulative = false);