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

6 files changed, 287 insertions, 373 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index e4847716a..96fccdcdb 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -492,15 +492,6 @@ header = "options/smt_options.h"
   help       = "the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)"
 
 [[option]]
-  name       = "cpuTime"
-  category   = "common"
-  long       = "cpu-time"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "measures CPU time if set to true and wall time if false (default false)"
-
-[[option]]
   name       = "rewriteStep"
   category   = "expert"
   long       = "rewrite-step=N"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ff5cff5b6..d80c01035 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -727,16 +727,7 @@ void SmtEngine::finishInit()
   }
   if (options::perCallMillisecondLimit() != 0)
   {
-    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit(), false);
-  }
-  if (options::cumulativeMillisecondLimit() != 0)
-  {
-    d_resourceManager->setTimeLimit(options::cumulativeMillisecondLimit(),
-                                    true);
-  }
-  if (options::cpuTime())
-  {
-    d_resourceManager->useCPUTime(true);
+    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
   }
 
   // set the random seed
@@ -3430,8 +3421,9 @@ void SmtEngine::interrupt()
 void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
   d_resourceManager->setResourceLimit(units, cumulative);
 }
-void SmtEngine::setTimeLimit(unsigned long milis, bool cumulative) {
-  d_resourceManager->setTimeLimit(milis, cumulative);
+void SmtEngine::setTimeLimit(unsigned long milis)
+{
+  d_resourceManager->setTimeLimit(milis);
 }
 
 unsigned long SmtEngine::getResourceUsage() const {
@@ -3447,11 +3439,6 @@ unsigned long SmtEngine::getResourceRemaining() const
   return d_resourceManager->getResourceRemaining();
 }
 
-unsigned long SmtEngine::getTimeRemaining() const
-{
-  return d_resourceManager->getTimeRemaining();
-}
-
 NodeManager* SmtEngine::getNodeManager() const
 {
   return d_exprManager->getNodeManager();
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3ed2b987c..738a6c22a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -775,18 +775,14 @@ class CVC4_PUBLIC SmtEngine
   void setResourceLimit(unsigned long units, bool cumulative = false);
 
   /**
-   * Set a time limit for SmtEngine operations.
+   * Set a per-call time limit for SmtEngine operations.
    *
-   * A cumulative and non-cumulative (per-call) time limit can be
-   * set at the same time.  A call to setTimeLimit() with
-   * cumulative==true replaces any cumulative time limit currently
-   * in effect; a call with cumulative==false replaces any per-call
-   * time limit currently in effect.  Resource limits can be set in
-   * addition to time limits; the SmtEngine obeys both.  That means
-   * that up to four independent limits can control the SmtEngine
-   * at the same time.
+   * A per-call time limit can be set at the same time and replaces
+   * any per-call time limit currently in effect.
+   * Resource limits (either per-call or cumulative) can be set in
+   * addition to a time limit; the SmtEngine obeys all three of them.
    *
-   * Note that the cumulative timer only ticks away when one of the
+   * Note that the per-call timer only ticks away when one of the
    * SmtEngine's workhorse functions (things like assertFormula(),
    * checkEntailed(), checkSat(), and simplify()) are running.
    * Between calls, the timer is still.
@@ -800,11 +796,8 @@ class CVC4_PUBLIC SmtEngine
    * We reserve the right to change this in the future.
    *
    * @param millis the time limit in milliseconds, or 0 for no limit
-   * @param cumulative whether this time limit is to be a cumulative
-   * time limit for all remaining calls into the SmtEngine (true), or
-   * whether it's a per-call time limit (false); the default is false
    */
-  void setTimeLimit(unsigned long millis, bool cumulative = false);
+  void setTimeLimit(unsigned long millis);
 
   /**
    * Get the current resource usage count for this SmtEngine.  This
@@ -826,16 +819,6 @@ class CVC4_PUBLIC SmtEngine
    */
   unsigned long getResourceRemaining() const;
 
-  /**
-   * Get the remaining number of milliseconds that can be consumed by
-   * this SmtEngine according to the currently-set cumulative time limit.
-   * If there is not a cumulative resource limit set, this function
-   * throws a ModalException.
-   *
-   * @throw ModalException
-   */
-  unsigned long getTimeRemaining() const;
-
   /** Permit access to the underlying ExprManager. */
   ExprManager* getExprManager() const { return d_exprManager; }
 
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 41526c30d..2419962aa 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -53,7 +53,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte,
   smte->setLogic(smtCurr->getLogicInfo());
   if (needsTimeout)
   {
-    smte->setTimeLimit(timeout, true);
+    smte->setTimeLimit(timeout);
   }
   smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
 }
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;
 }
 
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 39fceb7ec..822f17713 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -9,11 +9,12 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** [[ Add lengthier description here ]]
-
- ** \todo document this file
-
-**/
+ ** \brief Provides mechanisms to limit resources.
+  **
+ ** This file provides the ResourceManager class. It can be used to impose
+ ** (cumulative and per-call) resource limits on the solver, as well as per-call
+ ** time limits.
+ **/
 
 #include "cvc4_public.h"
 
@@ -38,190 +39,168 @@ class StatisticsRegistry;
  * A helper class to keep track of a time budget and signal
  * the PropEngine when the budget expires.
  */
-class CVC4_PUBLIC Timer {
+class CVC4_PUBLIC Timer
+{
  public:
   /** Construct a Timer. */
-  Timer()
-      : d_ms(0),
-        d_cpu_start_time(0),
-        d_cpu_limit(0),
-        d_wall_time(true)
+  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;
-  }
+  bool on() const { return d_ms != 0; }
 
   /** Set a millisecond timer (0==off). */
-  void set(uint64_t millis, bool wall_time = true);
-  /** Return the milliseconds elapsed since last set() wall/cpu time
-   depending on d_wall_time*/
+  void set(uint64_t millis);
+  /** Return the milliseconds elapsed since last set() wall time. */
   uint64_t elapsed() const;
   bool expired() const;
 
  private:
-
-  /** Return the milliseconds elapsed since last set() cpu time. */
-  uint64_t elapsedCPU() const;
-  /** Return the milliseconds elapsed since last set() wall time. */
-  uint64_t elapsedWall() const;
-
   uint64_t d_ms;
-  clock_t d_cpu_start_time;
-  clock_t d_cpu_limit;
-  bool d_wall_time;
   timeval d_wall_limit;
-};/* class Timer */
-
-
-class CVC4_PUBLIC ResourceManager {
-public:
- enum class Resource
- {
-   BitblastStep,
-   BvEagerAssertStep,
-   BvPropagationStep,
-   BvSatConflictsStep,
-   CnfStep,
-   DecisionStep,
-   LemmaStep,
-   ParseStep,
-   PreprocessStep,
-   QuantifierStep,
-   RestartStep,
-   RewriteStep,
-   SatConflictStep,
-   TheoryCheckStep,
- };
-
- ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
- ~ResourceManager();
-
- bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
- bool cumulativeLimitOn() const;
- bool perCallLimitOn() const;
-
- bool outOfResources() const;
- bool outOfTime() const;
- 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;
- uint64_t getTimeUsage() const;
- uint64_t getResourceRemaining() const;
- uint64_t getTimeRemaining() const;
-
- uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
- // Throws an UnsafeInterruptException if there are no remaining resources.
- void spendResource(Resource r);
-
- void setHardLimit(bool value);
- void setResourceLimit(uint64_t units, bool cumulative = false);
- void setTimeLimit(uint64_t millis, bool cumulative = false);
- void useCPUTime(bool cpu);
-
- void enable(bool on);
-
- /**
-  * Resets perCall limits to mark the start of a new call,
-  * updates budget for current call and starts the timer
-  */
- void beginCall();
-
- /**
-  * Marks the end of a SmtEngine check call, stops the per
-  * call timer, updates cumulative time used.
-  */
- void endCall();
-
- static uint64_t getFrequencyCount() { return s_resourceCount; }
-
- /**
-  * Registers a listener that is notified on a hard 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);
-
-private:
- Timer d_cumulativeTimer;
- Timer d_perCallTimer;
-
- /** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
- uint64_t d_timeBudgetCumulative;
- /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
- uint64_t d_timeBudgetPerCall;
- /** A user-imposed cumulative resource budget. 0 = no limit. */
- uint64_t d_resourceBudgetCumulative;
- /** A user-imposed per-call resource budget. 0 = no limit. */
- uint64_t d_resourceBudgetPerCall;
-
- /** The number of milliseconds used. */
- uint64_t d_cumulativeTimeUsed;
- /** The amount of resource used. */
- uint64_t d_cumulativeResourceUsed;
-
- /** The amount of resource 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.
-  */
- uint64_t d_thisCallTimeBudget;
- uint64_t d_thisCallResourceBudget;
-
- bool d_isHardLimit;
- bool d_on;
- bool d_cpuTime;
- 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;
-
- void spendResource(unsigned amount);
-
- struct Statistics;
- std::unique_ptr<Statistics> d_statistics;
-
- Options& d_options;
-
-};/* class ResourceManager */
-
-
-}/* CVC4 namespace */
+}; /* class Timer */
+
+class CVC4_PUBLIC ResourceManager
+{
+ public:
+  enum class Resource
+  {
+    BitblastStep,
+    BvEagerAssertStep,
+    BvPropagationStep,
+    BvSatConflictsStep,
+    CnfStep,
+    DecisionStep,
+    LemmaStep,
+    ParseStep,
+    PreprocessStep,
+    QuantifierStep,
+    RestartStep,
+    RewriteStep,
+    SatConflictStep,
+    TheoryCheckStep,
+  };
+
+  ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
+  ~ResourceManager();
+
+  bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
+  bool cumulativeLimitOn() const;
+  bool perCallLimitOn() const;
+
+  bool outOfResources() const;
+  bool outOfTime() const;
+  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;
+  uint64_t getTimeUsage() const;
+  uint64_t getResourceRemaining() const;
+
+  uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
+  // Throws an UnsafeInterruptException if there are no remaining resources.
+  void spendResource(Resource r);
+
+  void setHardLimit(bool value);
+  void setResourceLimit(uint64_t units, bool cumulative = false);
+  void setTimeLimit(uint64_t millis);
+
+  void enable(bool on);
+
+  /**
+   * Resets perCall limits to mark the start of a new call,
+   * updates budget for current call and starts the timer
+   */
+  void beginCall();
+
+  /**
+   * Marks the end of a SmtEngine check call, stops the per
+   * call timer.
+   */
+  void endCall();
+
+  static uint64_t getFrequencyCount() { return s_resourceCount; }
+
+  /**
+   * Registers a listener that is notified on a hard 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);
+
+ private:
+  Timer d_perCallTimer;
+
+  /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
+  uint64_t d_timeBudgetPerCall;
+  /** A user-imposed cumulative resource budget. 0 = no limit. */
+  uint64_t d_resourceBudgetCumulative;
+  /** A user-imposed per-call resource budget. 0 = no limit. */
+  uint64_t d_resourceBudgetPerCall;
+
+  /** The number of milliseconds used. */
+  uint64_t d_cumulativeTimeUsed;
+  /** The amount of resource used. */
+  uint64_t d_cumulativeResourceUsed;
+
+  /** The amount of resource 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.
+   */
+  uint64_t d_thisCallTimeBudget;
+  uint64_t d_thisCallResourceBudget;
+
+  bool d_isHardLimit;
+  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;
+
+  void spendResource(unsigned amount);
+
+  struct Statistics;
+  std::unique_ptr<Statistics> d_statistics;
+
+  Options& d_options;
+
+}; /* class ResourceManager */
+
+}  // namespace CVC4
 
 #endif /* CVC4__RESOURCE_MANAGER_H */