Fix a memory issue in ResourceManager on 32-bit (resolves bug #606).

3 files changed, 38 insertions, 37 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d039377a1..ee09359ad 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -303,6 +303,7 @@ struct SmtEngineStatistics {
  */
 class SmtEnginePrivate : public NodeManagerListener {
   SmtEngine& d_smt;
+
   /**
    * Manager for limiting time and abstract resource usage.
    */
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 7aeb2fc0f..6d32120d9 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -23,7 +23,7 @@
 using namespace CVC4;
 using namespace std;
 
-void Timer::set(unsigned long millis, bool wallTime) {
+void Timer::set(uint64_t millis, bool wallTime) {
   d_ms = millis;
   Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl;
   // keep track of when it was set, even if it's disabled (i.e. == 0)
@@ -47,7 +47,7 @@ void Timer::set(unsigned long millis, bool wallTime) {
 }
 
 /** Return the milliseconds elapsed since last set(). */
-unsigned long Timer::elapsedWall() const {
+uint64_t Timer::elapsedWall() const {
   Assert (d_wall_time);
   timeval tv;
   gettimeofday(&tv, NULL);
@@ -58,14 +58,14 @@ unsigned long Timer::elapsedWall() const {
   return tv.tv_sec * 1000 + tv.tv_usec / 1000;
 }
 
-unsigned long Timer::elapsedCPU() const {
+uint64_t Timer::elapsedCPU() const {
   Assert (!d_wall_time);
   clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time;
   Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <<std::endl;
   return elapsed;
 }
 
-unsigned long Timer::elapsed() const {
+uint64_t Timer::elapsed() const {
   if (d_wall_time)
     return elapsedWall();
   return elapsedCPU();
@@ -99,7 +99,7 @@ bool Timer::expired() const {
   return false;
 }
 
-const unsigned long ResourceManager::s_resourceCount = 1000;
+const uint64_t ResourceManager::s_resourceCount = 1000;
 
 ResourceManager::ResourceManager()
   : d_cumulativeTimer()
@@ -120,7 +120,7 @@ ResourceManager::ResourceManager()
 {}
 
 
-void ResourceManager::setResourceLimit(unsigned long units, bool cumulative) {
+void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) {
   d_on = true;
   if(cumulative) {
     Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl;
@@ -132,7 +132,7 @@ void ResourceManager::setResourceLimit(unsigned long units, bool cumulative) {
   }
 }
 
-void ResourceManager::setTimeLimit(unsigned long millis, bool cumulative) {
+void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) {
   d_on = true;
   if(cumulative) {
     Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl;
@@ -146,25 +146,25 @@ void ResourceManager::setTimeLimit(unsigned long millis, bool cumulative) {
 
 }
 
-unsigned long ResourceManager::getResourceUsage() const {
+uint64_t ResourceManager::getResourceUsage() const {
   return d_cumulativeResourceUsed;
 }
 
-unsigned long ResourceManager::getTimeUsage() const {
+uint64_t ResourceManager::getTimeUsage() const {
   if (d_timeBudgetCumulative) {
     return d_cumulativeTimer.elapsed();
   }
   return d_cumulativeTimeUsed;
 }
 
-unsigned long ResourceManager::getResourceRemaining() const {
+uint64_t ResourceManager::getResourceRemaining() const {
   if (d_thisCallResourceBudget <= d_thisCallResourceUsed)
     return 0;
   return d_thisCallResourceBudget - d_thisCallResourceUsed;
 }
 
-unsigned long ResourceManager::getTimeRemaining() const {
-  unsigned long time_passed = d_cumulativeTimer.elapsed();
+uint64_t ResourceManager::getTimeRemaining() const {
+  uint64_t time_passed = d_cumulativeTimer.elapsed();
   if (time_passed >= d_thisCallTimeBudget)
     return 0;
   return d_thisCallTimeBudget - time_passed;
@@ -239,7 +239,7 @@ void ResourceManager::beginCall() {
 }
 
 void ResourceManager::endCall() {
-  unsigned long usedInCall = d_perCallTimer.elapsed();
+  uint64_t usedInCall = d_perCallTimer.elapsed();
   d_perCallTimer.set(0);
   d_cumulativeTimeUsed += usedInCall;
 }
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 94e7dbba2..d1ec0456a 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -33,7 +33,7 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC Timer {
 
-  unsigned long d_ms;
+  uint64_t d_ms;
   timeval d_wall_limit;
   clock_t d_cpu_start_time;
   clock_t d_cpu_limit;
@@ -41,9 +41,9 @@ class CVC4_PUBLIC Timer {
   bool d_wall_time;
 
   /** Return the milliseconds elapsed since last set() cpu time. */
-  unsigned long elapsedCPU() const;
+  uint64_t elapsedCPU() const;
   /** Return the milliseconds elapsed since last set() wall time. */
-  unsigned long elapsedWall() const;
+  uint64_t elapsedWall() const;
 
 public:
 
@@ -61,10 +61,10 @@ public:
   }
 
   /** Set a millisecond timer (0==off). */
-  void set(unsigned long millis, bool wall_time = true);
+  void set(uint64_t millis, bool wall_time = true);
   /** Return the milliseconds elapsed since last set() wall/cpu time
    depending on d_wall_time*/
-  unsigned long elapsed() const;
+  uint64_t elapsed() const;
   bool expired() const;
 
 };/* class Timer */
@@ -76,36 +76,36 @@ class CVC4_PUBLIC ResourceManager {
   Timer d_perCallTimer;
 
   /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
-  unsigned long d_timeBudgetCumulative;
+  uint64_t d_timeBudgetCumulative;
   /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
-  unsigned long d_timeBudgetPerCall;
+  uint64_t d_timeBudgetPerCall;
   /** A user-imposed cumulative resource budget. 0 = no limit. */
-  unsigned long d_resourceBudgetCumulative;
+  uint64_t d_resourceBudgetCumulative;
   /** A user-imposed per-call resource budget. 0 = no limit. */
-  unsigned long d_resourceBudgetPerCall;
+  uint64_t d_resourceBudgetPerCall;
 
   /** The number of milliseconds used. */
-  unsigned long d_cumulativeTimeUsed;
+  uint64_t d_cumulativeTimeUsed;
   /** The amount of resource used. */
-  unsigned long d_cumulativeResourceUsed;
+  uint64_t d_cumulativeResourceUsed;
 
   /** The ammount of resource used during this call. */
-  unsigned long d_thisCallResourceUsed;
+  uint64_t d_thisCallResourceUsed;
 
   /**
    * The ammount of resource budget for this call (min between per call
    * budget and left-over cumulative budget.
    */
-  unsigned long d_thisCallTimeBudget;
-  unsigned long d_thisCallResourceBudget;
+  uint64_t d_thisCallTimeBudget;
+  uint64_t d_thisCallResourceBudget;
 
   bool d_isHardLimit;
   bool d_on;
   bool d_cpuTime;
-  unsigned long d_spendResourceCalls;
+  uint64_t d_spendResourceCalls;
 
   /** Counter indicating how often to check resource manager in loops */
-  static const unsigned long s_resourceCount;
+  static const uint64_t s_resourceCount;
 
 public:
 
@@ -119,20 +119,20 @@ public:
   bool outOfTime() const;
   bool out() const { return d_on && (outOfResources() || outOfTime()); }
 
-  unsigned long getResourceUsage() const;
-  unsigned long getTimeUsage() const;
-  unsigned long getResourceRemaining() const;
-  unsigned long getTimeRemaining() const;
+  uint64_t getResourceUsage() const;
+  uint64_t getTimeUsage() const;
+  uint64_t getResourceRemaining() const;
+  uint64_t getTimeRemaining() const;
 
-  unsigned long getResourceBudgetForThisCall() {
+  uint64_t getResourceBudgetForThisCall() {
     return d_thisCallResourceBudget;
   }
 
   void spendResource() throw(UnsafeInterruptException);
 
   void setHardLimit(bool value);
-  void setResourceLimit(unsigned long units, bool cumulative = false);
-  void setTimeLimit(unsigned long millis, bool cumulative = false);
+  void setResourceLimit(uint64_t units, bool cumulative = false);
+  void setTimeLimit(uint64_t millis, bool cumulative = false);
   void useCPUTime(bool cpu);
 
   void enable(bool on);
@@ -149,7 +149,7 @@ public:
    */
   void endCall();
 
-  static unsigned long getFrequencyCount() { return s_resourceCount; }
+  static uint64_t getFrequencyCount() { return s_resourceCount; }
   friend class SmtEngine;
 };/* class ResourceManager */