Remove cumulative time limits and cpu time limits (#4711)

This PR removes two things from the resource manager:

cumulative time limits
cpu time limits
Cumulative time limiting has been moved to the binary and is (as before) accessible via --tlimit. As per discussion among the devs, we no longer support time limits based on CPU time and thus everything related to that is removed as well.
Note that this includes the option --cpu-time, removes an argument from SmtEngine::setTimeLimit() and the method SmtEngine::getTimeRemaining() .

1 files changed, 122 insertions, 148 deletions

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index eddf9e5c9..7080d5040 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -25,79 +25,59 @@ using namespace std;
 
 namespace CVC4 {
 
-void Timer::set(uint64_t millis, bool wallTime) {
+void Timer::set(uint64_t millis)
+{
   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)
-  d_wall_time = wallTime;
-  if (d_wall_time) {
-    // 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) {
-      ++d_wall_limit.tv_sec;
-      d_wall_limit.tv_usec -= 1000000;
-    }
-    Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
-  } else {
-    // CPU time
-    d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001);
-    d_cpu_limit = d_cpu_start_time + d_ms;
+  // 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)
+  {
+    ++d_wall_limit.tv_sec;
+    d_wall_limit.tv_usec -= 1000000;
   }
+  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::elapsedWall() const {
-  Assert(d_wall_time);
+uint64_t Timer::elapsed() const
+{
   timeval tv;
   gettimeofday(&tv, NULL);
-  Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+  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;
+  Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec
+                 << "," << tv.tv_usec << std::endl;
   return tv.tv_sec * 1000 + tv.tv_usec / 1000;
 }
 
-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;
-}
-
-uint64_t Timer::elapsed() const {
-  if (d_wall_time)
-    return elapsedWall();
-  return elapsedCPU();
-}
-
-bool Timer::expired() const {
+bool Timer::expired() const
+{
   if (!on()) return false;
 
-  if (d_wall_time) {
-    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;
-  }
-
-  // cpu time
-  double current = ((double)clock())/(CLOCKS_PER_SEC*0.001);
-  Debug("limit") << "Timer::expired(): current cpu time is " << current <<  std::endl;
-  Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit <<  std::endl;
-  if (current >= d_cpu_limit) {
-    Debug("limit") << "Timer::expired(): OVER LIMIT!" << current <<  std::endl;
+  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;
 }
 
@@ -182,9 +162,7 @@ ResourceManager::Statistics::~Statistics()
 const uint64_t ResourceManager::s_resourceCount = 1000;
 
 ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
-    : d_cumulativeTimer(),
-      d_perCallTimer(),
-      d_timeBudgetCumulative(0),
+    : d_perCallTimer(),
       d_timeBudgetPerCall(0),
       d_resourceBudgetCumulative(0),
       d_resourceBudgetPerCall(0),
@@ -195,65 +173,56 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
       d_thisCallResourceBudget(0),
       d_isHardLimit(),
       d_on(false),
-      d_cpuTime(false),
       d_spendResourceCalls(0),
       d_hardListeners(),
       d_softListeners(),
       d_statistics(new ResourceManager::Statistics(stats)),
       d_options(options)
 
-{}
+{
+}
 
 ResourceManager::~ResourceManager() {}
 
-void ResourceManager::setResourceLimit(uint64_t 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;
-    d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
+  if (cumulative)
+  {
+    Trace("limit") << "ResourceManager: setting cumulative resource limit to "
+                   << units << endl;
+    d_resourceBudgetCumulative =
+        (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
     d_thisCallResourceBudget = d_resourceBudgetCumulative;
-  } else {
-    Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl;
+  }
+  else
+  {
+    Trace("limit") << "ResourceManager: setting per-call resource limit to "
+                   << units << endl;
     d_resourceBudgetPerCall = units;
   }
 }
 
-void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) {
+void ResourceManager::setTimeLimit(uint64_t millis)
+{
   d_on = true;
-  if(cumulative) {
-    Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl;
-    d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
-    d_cumulativeTimer.set(millis, !d_cpuTime);
-  } else {
-    Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl;
-    d_timeBudgetPerCall = millis;
-    // perCall timer will be set in beginCall
-  }
-
+  Trace("limit") << "ResourceManager: setting per-call time limit to " << millis
+                 << " ms" << endl;
+  d_timeBudgetPerCall = millis;
+  // perCall timer will be set in beginCall
 }
 
-const uint64_t& ResourceManager::getResourceUsage() const {
+const uint64_t& ResourceManager::getResourceUsage() const
+{
   return d_cumulativeResourceUsed;
 }
 
-uint64_t ResourceManager::getTimeUsage() const {
-  if (d_timeBudgetCumulative) {
-    return d_cumulativeTimer.elapsed();
-  }
-  return d_cumulativeTimeUsed;
-}
+uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
 
-uint64_t ResourceManager::getResourceRemaining() const {
-  if (d_thisCallResourceBudget <= d_thisCallResourceUsed)
-    return 0;
-  return d_thisCallResourceBudget - d_thisCallResourceUsed;
-}
-
-uint64_t ResourceManager::getTimeRemaining() const {
-  uint64_t time_passed = d_cumulativeTimer.elapsed();
-  if (time_passed >= d_thisCallTimeBudget)
-    return 0;
-  return d_thisCallTimeBudget - time_passed;
+uint64_t ResourceManager::getResourceRemaining() const
+{
+  if (d_resourceBudgetCumulative <= d_cumulativeResourceUsed) return 0;
+  return d_resourceBudgetCumulative - d_cumulativeResourceUsed;
 }
 
 void ResourceManager::spendResource(unsigned amount)
@@ -264,21 +233,25 @@ void ResourceManager::spendResource(unsigned amount)
 
   Debug("limit") << "ResourceManager::spendResource()" << std::endl;
   d_thisCallResourceUsed += amount;
-  if(out()) {
+  if (out())
+  {
     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
     Trace("limit") << "          on call " << d_spendResourceCalls << std::endl;
-    if (outOfTime()) {
+    if (outOfTime())
+    {
       Trace("limit") << "ResourceManager::spendResource: elapsed time"
-                     << d_cumulativeTimer.elapsed() << std::endl;
+                     << d_perCallTimer.elapsed() << std::endl;
     }
 
-    if (d_isHardLimit) {
+    if (d_isHardLimit)
+    {
       d_hardListeners.notify();
       throw UnsafeInterruptException();
-    } else {
+    }
+    else
+    {
       d_softListeners.notify();
     }
-
   }
 }
 
@@ -348,88 +321,89 @@ void ResourceManager::spendResource(Resource r)
   spendResource(amount);
 }
 
-void ResourceManager::beginCall() {
-
-  d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime);
+void ResourceManager::beginCall()
+{
+  d_perCallTimer.set(d_timeBudgetPerCall);
   d_thisCallResourceUsed = 0;
   if (!d_on) return;
 
-  if (cumulativeLimitOn()) {
-    if (d_resourceBudgetCumulative) {
-      d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
-                                 d_resourceBudgetCumulative - d_cumulativeResourceUsed;
-    }
-
-    if (d_timeBudgetCumulative) {
-      AlwaysAssert(d_cumulativeTimer.on());
-      // timer was on since the option was set
-      d_cumulativeTimeUsed = d_cumulativeTimer.elapsed();
-      d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 :
-                             d_timeBudgetCumulative - d_cumulativeTimeUsed;
-      d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime);
+  if (cumulativeLimitOn())
+  {
+    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;
+    if (d_thisCallTimeBudget == 0 || d_thisCallResourceUsed == 0) return;
   }
 
-  if (perCallLimitOn()) {
+  if (perCallLimitOn())
+  {
     // 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_resourceBudgetPerCall)
+    {
+      d_thisCallResourceBudget =
+          d_thisCallResourceBudget < d_resourceBudgetPerCall
+                  && d_thisCallResourceBudget != 0
+              ? d_thisCallResourceBudget
+              : d_resourceBudgetPerCall;
     }
 
-    if (d_timeBudgetPerCall) {
-      d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall;
+    if (d_timeBudgetPerCall)
+    {
+      d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall
+                                     && d_thisCallTimeBudget != 0
+                                 ? d_thisCallTimeBudget
+                                 : d_timeBudgetPerCall;
     }
   }
 }
 
-void ResourceManager::endCall() {
-  uint64_t usedInCall = d_perCallTimer.elapsed();
+void ResourceManager::endCall()
+{
+  d_cumulativeTimeUsed += d_perCallTimer.elapsed();
   d_perCallTimer.set(0);
-  d_cumulativeTimeUsed += usedInCall;
 }
 
-bool ResourceManager::cumulativeLimitOn() const {
-  return d_timeBudgetCumulative || d_resourceBudgetCumulative;
+bool ResourceManager::cumulativeLimitOn() const
+{
+  return d_resourceBudgetCumulative;
 }
 
-bool ResourceManager::perCallLimitOn() const {
+bool ResourceManager::perCallLimitOn() const
+{
   return d_timeBudgetPerCall || d_resourceBudgetPerCall;
 }
 
-bool ResourceManager::outOfResources() const {
+bool ResourceManager::outOfResources() const
+{
   // resource limiting not enabled
-  if (d_resourceBudgetPerCall == 0 &&
-      d_resourceBudgetCumulative == 0)
+  if (d_resourceBudgetPerCall == 0 && d_resourceBudgetCumulative == 0)
     return false;
 
   return getResourceRemaining() == 0;
 }
 
-bool ResourceManager::outOfTime() const {
-  if (d_timeBudgetPerCall == 0 &&
-      d_timeBudgetCumulative == 0)
-    return false;
-
-  return d_cumulativeTimer.expired() || d_perCallTimer.expired();
-}
+bool ResourceManager::outOfTime() const
+{
+  if (d_timeBudgetPerCall == 0) return false;
 
-void ResourceManager::useCPUTime(bool cpu) {
-  Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n";
-  d_cpuTime = cpu;
+  return d_perCallTimer.expired();
 }
 
-void ResourceManager::setHardLimit(bool value) {
-  Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n";
+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";
+void ResourceManager::enable(bool on)
+{
+  Trace("limit") << "ResourceManager::enable(" << on << ")\n";
   d_on = on;
 }