From: lianah <lianahady@gmail.com>
Date: Fri, 29 May 2015 14:18:36 +0000 (-0400)
Subject: changed resource step options to unsigned
X-Git-Tag: cvc5-1.0.0~6320
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=331f8cccb1f5fc8806774652deb71f23c7572772;p=cvc5.git

changed resource step options to unsigned
---

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 2c9662655..0bf4edf6a 100644
--- 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 7d2a978b9..016a0c225 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(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 e6d965f8f..794e36e2c 100644
--- 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 17ac394c3..768f07108 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(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 79758a425..50d308541 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(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 5b80b7596..9c6da703a 100644
--- 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 d978edefd..90ad558f5 100644
--- 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 dbee33f5a..077acc6e9 100644
--- 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 c7c0bc71a..11a412c75 100644
--- 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 4d953b03c..d42c4a8c9 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(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 61472fd79..59ecc7385 100644
--- 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 6f399cb7a..95a483d34 100644
--- 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 3317d1b01..193de55db 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(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 f340c994c..2da0f0467 100644
--- 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 75dafb7f6..9b4815fd4 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(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 bb4d4c16d..0c1a7c081 100644
--- 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 37fea2c67..22496a433 100644
--- 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 9c2812f0f..e84917db0 100644
--- 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);