Resource manager cleanup (#4732)

This PR performs some general cleanup in and around the ResourceManager class. In detail, it does

remove --hard-limit (we decided to always leave the solver in a usable state, i.e. always do a soft limit),
remove --cpu-time (we decided to always use wall-clock time for time limiting)
replace old gettimeofday-based Timer by new std::chrono-based WallClockTimer
clean up the logic around beginCall() and endCall()

1 files changed, 70 insertions, 114 deletions

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 7080d5040..ac1d57324 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -25,66 +25,47 @@ using namespace std;
 
 namespace CVC4 {
 
-void Timer::set(uint64_t millis)
+bool WallClockTimer::on() const
 {
-  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)
-  // Wall time
-  gettimeofday(&d_wall_limit, NULL);
-  Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << ","
-                 << d_wall_limit.tv_usec << std::endl;
-  d_wall_limit.tv_sec += millis / 1000;
-  d_wall_limit.tv_usec += (millis % 1000) * 1000;
-  if (d_wall_limit.tv_usec > 1000000)
+  // default-constructed time points are at the respective epoch
+  return d_limit.time_since_epoch().count() != 0;
+}
+void WallClockTimer::set(uint64_t millis)
+{
+  if (millis == 0)
+  {
+    // reset / deactivate
+    d_start = time_point();
+    d_limit = time_point();
+  }
+  else
   {
-    ++d_wall_limit.tv_sec;
-    d_wall_limit.tv_usec -= 1000000;
+    // set to now() + millis
+    d_start = clock::now();
+    d_limit = d_start + std::chrono::milliseconds(millis);
   }
-  Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << ","
-                 << d_wall_limit.tv_usec << std::endl;
 }
-
-/** Return the milliseconds elapsed since last set(). */
-uint64_t Timer::elapsed() const
+uint64_t WallClockTimer::elapsed() const
 {
-  timeval tv;
-  gettimeofday(&tv, NULL);
-  Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << ","
-                 << tv.tv_usec << std::endl;
-  tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000;
-  tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000;
-  Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec
-                 << "," << tv.tv_usec << std::endl;
-  return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+  if (!on()) return 0;
+  // now() - d_start casted to milliseconds
+  return std::chrono::duration_cast<std::chrono::milliseconds>(clock::now()
+                                                               - d_start)
+      .count();
 }
-
-bool Timer::expired() const
+bool WallClockTimer::expired() const
 {
+  // whether d_limit is in the past
   if (!on()) return false;
-
-  timeval tv;
-  gettimeofday(&tv, NULL);
-  Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec
-                 << "," << tv.tv_usec << std::endl;
-  Debug("limit") << "Timer::expired(): limit wall time is "
-                 << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec
-                 << std::endl;
-  if (d_wall_limit.tv_sec < tv.tv_sec
-      || (d_wall_limit.tv_sec == tv.tv_sec
-          && d_wall_limit.tv_usec <= tv.tv_usec))
-  {
-    Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl;
-    return true;
-  }
-  Debug("limit") << "Timer::expired(): within limit" << std::endl;
-  return false;
+  return d_limit <= clock::now();
 }
 
 /*---------------------------------------------------------------------------*/
 
 struct ResourceManager::Statistics
 {
+  ReferenceStat<std::uint64_t> d_resourceUnitsUsed;
+  IntStat d_spendResourceCalls;
   IntStat d_numBitblastStep;
   IntStat d_numBvEagerAssertStep;
   IntStat d_numBvPropagationStep;
@@ -107,7 +88,9 @@ struct ResourceManager::Statistics
 };
 
 ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
-    : d_numBitblastStep("resource::BitblastStep", 0),
+    : d_resourceUnitsUsed("resource::resourceUnitsUsed"),
+      d_spendResourceCalls("resource::spendResourceCalls", 0),
+      d_numBitblastStep("resource::BitblastStep", 0),
       d_numBvEagerAssertStep("resource::BvEagerAssertStep", 0),
       d_numBvPropagationStep("resource::BvPropagationStep", 0),
       d_numBvSatConflictsStep("resource::BvSatConflictsStep", 0),
@@ -123,6 +106,8 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
       d_numTheoryCheckStep("resource::TheoryCheckStep", 0),
       d_statisticsRegistry(stats)
 {
+  d_statisticsRegistry.registerStat(&d_resourceUnitsUsed);
+  d_statisticsRegistry.registerStat(&d_spendResourceCalls);
   d_statisticsRegistry.registerStat(&d_numBitblastStep);
   d_statisticsRegistry.registerStat(&d_numBvEagerAssertStep);
   d_statisticsRegistry.registerStat(&d_numBvPropagationStep);
@@ -141,6 +126,8 @@ ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
 
 ResourceManager::Statistics::~Statistics()
 {
+  d_statisticsRegistry.unregisterStat(&d_resourceUnitsUsed);
+  d_statisticsRegistry.unregisterStat(&d_spendResourceCalls);
   d_statisticsRegistry.unregisterStat(&d_numBitblastStep);
   d_statisticsRegistry.unregisterStat(&d_numBvEagerAssertStep);
   d_statisticsRegistry.unregisterStat(&d_numBvPropagationStep);
@@ -169,17 +156,14 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
       d_cumulativeTimeUsed(0),
       d_cumulativeResourceUsed(0),
       d_thisCallResourceUsed(0),
-      d_thisCallTimeBudget(0),
       d_thisCallResourceBudget(0),
-      d_isHardLimit(),
       d_on(false),
-      d_spendResourceCalls(0),
-      d_hardListeners(),
-      d_softListeners(),
+      d_listeners(),
       d_statistics(new ResourceManager::Statistics(stats)),
       d_options(options)
 
 {
+  d_statistics->d_resourceUnitsUsed.setData(d_cumulativeResourceUsed);
 }
 
 ResourceManager::~ResourceManager() {}
@@ -212,7 +196,7 @@ void ResourceManager::setTimeLimit(uint64_t millis)
   // perCall timer will be set in beginCall
 }
 
-const uint64_t& ResourceManager::getResourceUsage() const
+uint64_t ResourceManager::getResourceUsage() const
 {
   return d_cumulativeResourceUsed;
 }
@@ -227,7 +211,7 @@ uint64_t ResourceManager::getResourceRemaining() const
 
 void ResourceManager::spendResource(unsigned amount)
 {
-  ++d_spendResourceCalls;
+  ++d_statistics->d_spendResourceCalls;
   d_cumulativeResourceUsed += amount;
   if (!d_on) return;
 
@@ -236,22 +220,14 @@ void ResourceManager::spendResource(unsigned amount)
   if (out())
   {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
-    Trace("limit") << "          on call " << d_spendResourceCalls << std::endl;
+    Trace("limit") << "          on call " << d_statistics->d_spendResourceCalls.getData() << std::endl;
     if (outOfTime())
     {
       Trace("limit") << "ResourceManager::spendResource: elapsed time"
                      << d_perCallTimer.elapsed() << std::endl;
     }
 
-    if (d_isHardLimit)
-    {
-      d_hardListeners.notify();
-      throw UnsafeInterruptException();
-    }
-    else
-    {
-      d_softListeners.notify();
-    }
+    d_listeners.notify();
   }
 }
 
@@ -327,38 +303,18 @@ void ResourceManager::beginCall()
   d_thisCallResourceUsed = 0;
   if (!d_on) return;
 
-  if (cumulativeLimitOn())
+  if (d_resourceBudgetCumulative > 0)
   {
-    if (d_resourceBudgetCumulative)
-    {
-      d_thisCallResourceBudget =
-          d_resourceBudgetCumulative <= d_cumulativeResourceUsed
-              ? 0
-              : d_resourceBudgetCumulative - d_cumulativeResourceUsed;
-    }
-    // we are out of resources so we shouldn't update the
-    // budget for this call to the per call budget
-    if (d_thisCallTimeBudget == 0 || d_thisCallResourceUsed == 0) return;
+    // Compute remaining cumulative resource budget
+    d_thisCallResourceBudget =
+        d_resourceBudgetCumulative - d_cumulativeResourceUsed;
   }
-
-  if (perCallLimitOn())
+  if (d_resourceBudgetPerCall > 0)
   {
-    // take min of what's left and per-call budget
-    if (d_resourceBudgetPerCall)
-    {
-      d_thisCallResourceBudget =
-          d_thisCallResourceBudget < d_resourceBudgetPerCall
-                  && d_thisCallResourceBudget != 0
-              ? d_thisCallResourceBudget
-              : d_resourceBudgetPerCall;
-    }
-
-    if (d_timeBudgetPerCall)
+    // Check if per-call resource budget is even smaller
+    if (d_resourceBudgetPerCall < d_thisCallResourceBudget)
     {
-      d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall
-                                     && d_thisCallTimeBudget != 0
-                                 ? d_thisCallTimeBudget
-                                 : d_timeBudgetPerCall;
+      d_thisCallResourceBudget = d_resourceBudgetPerCall;
     }
   }
 }
@@ -367,56 +323,56 @@ void ResourceManager::endCall()
 {
   d_cumulativeTimeUsed += d_perCallTimer.elapsed();
   d_perCallTimer.set(0);
+  d_thisCallResourceUsed = 0;
 }
 
 bool ResourceManager::cumulativeLimitOn() const
 {
-  return d_resourceBudgetCumulative;
+  return d_resourceBudgetCumulative > 0;
 }
 
 bool ResourceManager::perCallLimitOn() const
 {
-  return d_timeBudgetPerCall || d_resourceBudgetPerCall;
+  return (d_timeBudgetPerCall > 0) || (d_resourceBudgetPerCall > 0);
 }
 
 bool ResourceManager::outOfResources() const
 {
-  // resource limiting not enabled
-  if (d_resourceBudgetPerCall == 0 && d_resourceBudgetCumulative == 0)
-    return false;
-
-  return getResourceRemaining() == 0;
+  if (d_resourceBudgetPerCall > 0)
+  {
+    // Check if per-call resources are exhausted
+    if (d_thisCallResourceUsed >= d_resourceBudgetPerCall)
+    {
+      return true;
+    }
+  }
+  if (d_resourceBudgetCumulative > 0)
+  {
+    // Check if cumulative resources are exhausted
+    if (d_cumulativeResourceUsed >= d_resourceBudgetCumulative)
+    {
+      return true;
+    }
+  }
+  return false;
 }
 
 bool ResourceManager::outOfTime() const
 {
   if (d_timeBudgetPerCall == 0) return false;
-
   return d_perCallTimer.expired();
 }
 
-void ResourceManager::setHardLimit(bool value)
-{
-  Trace("limit") << "ResourceManager::setHardLimit(" << value << ")\n";
-  d_isHardLimit = value;
-}
-
 void ResourceManager::enable(bool on)
 {
   Trace("limit") << "ResourceManager::enable(" << on << ")\n";
   d_on = on;
 }
 
-ListenerCollection::Registration* ResourceManager::registerHardListener(
-    Listener* listener)
-{
-  return d_hardListeners.registerListener(listener);
-}
-
-ListenerCollection::Registration* ResourceManager::registerSoftListener(
+ListenerCollection::Registration* ResourceManager::registerListener(
     Listener* listener)
 {
-  return d_softListeners.registerListener(listener);
+  return d_listeners.registerListener(listener);
 }
 
 } /* namespace CVC4 */