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()

2 files changed, 142 insertions, 175 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 */
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 822f17713..57a227d7b 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -23,6 +23,7 @@
 
 #include <sys/time.h>
 
+#include <chrono>
 #include <cstddef>
 #include <memory>
 
@@ -36,36 +37,48 @@ namespace CVC4 {
 class StatisticsRegistry;
 
 /**
- * A helper class to keep track of a time budget and signal
- * the PropEngine when the budget expires.
+ * This class implements a easy to use wall clock timer based on std::chrono.
  */
-class CVC4_PUBLIC Timer
+class CVC4_PUBLIC WallClockTimer
 {
- public:
-  /** Construct a Timer. */
-  Timer() : d_ms(0)
-  {
-    d_wall_limit.tv_sec = 0;
-    d_wall_limit.tv_usec = 0;
-  }
-
-  /** Is the timer currently active? */
-  bool on() const { return d_ms != 0; }
+  /**
+   * The underlying clock that is used.
+   * std::chrono::system_clock represents wall clock time.
+   */
+  using clock = std::chrono::system_clock;
+  /** A time point of the clock we use. */
+  using time_point = std::chrono::time_point<clock>;
 
-  /** Set a millisecond timer (0==off). */
+ public:
+  /** Checks whether this timer is active. */
+  bool on() const;
+  /**
+   * Activates this timer with a timeout in milliseconds.
+   * If millis is zero, the timer is deactivated.
+   */
   void set(uint64_t millis);
-  /** Return the milliseconds elapsed since last set() wall time. */
+  /** Returns the number of elapsed milliseconds since the last call to set().
+   */
   uint64_t elapsed() const;
+  /** Checks whether the current timeout has expired. */
   bool expired() const;
 
  private:
-  uint64_t d_ms;
-  timeval d_wall_limit;
-}; /* class Timer */
+  /** The start of this timer. */
+  time_point d_start;
+  /** The point in time when this timer expires. */
+  time_point d_limit;
+};
 
+/**
+ * This class manages resource limits (cumulative or per call) and (per call)
+ * time limits. The available resources are listed in ResourceManager::Resource
+ * and their individual costs are configured via command line options.
+ */
 class CVC4_PUBLIC ResourceManager
 {
  public:
+  /** Types of resources. */
   enum class Resource
   {
     BitblastStep,
@@ -84,32 +97,54 @@ class CVC4_PUBLIC ResourceManager
     TheoryCheckStep,
   };
 
+  /** Construst a resource manager. */
   ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
+  /** Default destructor. */
   ~ResourceManager();
+  /** Can not be copied. */
+  ResourceManager(const ResourceManager&) = delete;
+  /** Can not be moved. */
+  ResourceManager(ResourceManager&&) = delete;
+  /** Can not be copied. */
+  ResourceManager& operator=(const ResourceManager&) = delete;
+  /** Can not be moved. */
+  ResourceManager& operator=(ResourceManager&&) = delete;
 
+  /** Checks whether any limit is active. */
   bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+  /** Checks whether any cumulative limit is active. */
   bool cumulativeLimitOn() const;
+  /** Checks whether any per-call limit is active. */
   bool perCallLimitOn() const;
 
+  /** Checks whether resources have been exhausted. */
   bool outOfResources() const;
+  /** Checks whether time has been exhausted. */
   bool outOfTime() const;
+  /** Checks whether any limit has been exhausted. */
   bool out() const { return d_on && (outOfResources() || outOfTime()); }
 
-  /**
-   * This returns a const uint64_t& to support being used as a ReferenceStat.
-   */
-  const uint64_t& getResourceUsage() const;
+  /** Retrieves amount of resources used overall. */
+  uint64_t getResourceUsage() const;
+  /** Retrieves time used over all calls. */
   uint64_t getTimeUsage() const;
+  /** Retrieves the remaining number of cumulative resources. */
   uint64_t getResourceRemaining() const;
 
+  /** Retrieves resource budget for this call. */
   uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
-  // Throws an UnsafeInterruptException if there are no remaining resources.
+
+  /**
+   * Spends a given resources. Throws an UnsafeInterruptException if there are
+   * no remaining resources.
+   */
   void spendResource(Resource r);
 
-  void setHardLimit(bool value);
+  /** Sets the resource limit. */
   void setResourceLimit(uint64_t units, bool cumulative = false);
+  /** Sets the time limit. */
   void setTimeLimit(uint64_t millis);
-
+  /** Sets whether resource limitation is enabled. */
   void enable(bool on);
 
   /**
@@ -127,23 +162,16 @@ class CVC4_PUBLIC ResourceManager
   static uint64_t getFrequencyCount() { return s_resourceCount; }
 
   /**
-   * Registers a listener that is notified on a hard resource out.
+   * Registers a listener that is notified on a resource out.
    *
    * This Registration must be destroyed by the user before this
    * ResourceManager.
    */
-  ListenerCollection::Registration* registerHardListener(Listener* listener);
-
-  /**
-   * Registers a listener that is notified on a soft resource out.
-   *
-   * This Registration must be destroyed by the user before this
-   * ResourceManager.
-   */
-  ListenerCollection::Registration* registerSoftListener(Listener* listener);
+  ListenerCollection::Registration* registerListener(Listener* listener);
 
  private:
-  Timer d_perCallTimer;
+  /** The per-call wall clock timer. */
+  WallClockTimer d_perCallTimer;
 
   /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
   uint64_t d_timeBudgetPerCall;
@@ -152,45 +180,28 @@ class CVC4_PUBLIC ResourceManager
   /** A user-imposed per-call resource budget. 0 = no limit. */
   uint64_t d_resourceBudgetPerCall;
 
-  /** The number of milliseconds used. */
+  /** The total number of milliseconds used. */
   uint64_t d_cumulativeTimeUsed;
-  /** The amount of resource used. */
+  /** The total amount of resources used. */
   uint64_t d_cumulativeResourceUsed;
 
-  /** The amount of resource used during this call. */
+  /** The amount of resources used during this call. */
   uint64_t d_thisCallResourceUsed;
 
   /**
-   * The amount of resource budget for this call (min between per call
-   * budget and left-over cumulative budget.
+   * The resource budget for this call (min between per call
+   * budget and left-over cumulative budget.)
    */
-  uint64_t d_thisCallTimeBudget;
   uint64_t d_thisCallResourceBudget;
 
-  bool d_isHardLimit;
+  /** A flag indicating whether resource limitation is active. */
   bool d_on;
-  uint64_t d_spendResourceCalls;
 
   /** Counter indicating how often to check resource manager in loops */
   static const uint64_t s_resourceCount;
 
-  /** Receives a notification on reaching a hard limit. */
-  ListenerCollection d_hardListeners;
-
-  /** Receives a notification on reaching a hard limit. */
-  ListenerCollection d_softListeners;
-
-  /**
-   * ResourceManagers cannot be copied as they are given an explicit
-   * list of Listeners to respond to.
-   */
-  ResourceManager(const ResourceManager&) = delete;
-
-  /**
-   * ResourceManagers cannot be assigned as they are given an explicit
-   * list of Listeners to respond to.
-   */
-  ResourceManager& operator=(const ResourceManager&) = delete;
+  /** Receives a notification on reaching a limit. */
+  ListenerCollection d_listeners;
 
   void spendResource(unsigned amount);