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

3 files changed, 8 insertions, 32 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a3313a733..16e4e916a 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -148,9 +148,9 @@ void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
   commands.clear();
 }
 
-class SoftResourceOutListener : public Listener {
+class ResourceOutListener : public Listener {
  public:
-  SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
+  ResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
   void notify() override
   {
     SmtScope scope(d_smt);
@@ -159,20 +159,7 @@ class SoftResourceOutListener : public Listener {
   }
  private:
   SmtEngine* d_smt;
-}; /* class SoftResourceOutListener */
-
-
-class HardResourceOutListener : public Listener {
- public:
-  HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {}
-  void notify() override
-  {
-    SmtScope scope(d_smt);
-    theory::Rewriter::clearCaches();
-  }
- private:
-  SmtEngine* d_smt;
-}; /* class HardResourceOutListener */
+}; /* class ResourceOutListener */
 
 class BeforeSearchListener : public Listener {
  public:
@@ -364,10 +351,7 @@ class SmtEnginePrivate : public NodeManagerListener {
     ResourceManager* rm = d_smt.getResourceManager();
 
     d_listenerRegistrations->add(
-        rm->registerSoftListener(new SoftResourceOutListener(d_smt)));
-
-    d_listenerRegistrations->add(
-        rm->registerHardListener(new HardResourceOutListener(d_smt)));
+        rm->registerListener(new ResourceOutListener(d_smt)));
 
     try
     {
@@ -638,8 +622,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       new ResourceManager(*d_statisticsRegistry.get(), d_options));
   d_private.reset(new smt::SmtEnginePrivate(*this));
   d_stats.reset(new SmtEngineStatistics());
-  d_stats->d_resourceUnitsUsed.setData(d_resourceManager->getResourceUsage());
-
+  
   // The ProofManager is constructed before any other proof objects such as
   // SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
   // initialized in TheoryEngine and PropEngine respectively.
@@ -663,7 +646,6 @@ void SmtEngine::finishInit()
   // of SMT-LIB 2.6 standard.
 
   // Inialize the resource manager based on the options.
-  d_resourceManager->setHardLimit(options::hardLimit());
   if (options::perCallResourceLimit() != 0)
   {
     d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
@@ -1371,16 +1353,15 @@ Result SmtEngine::check() {
 
   Trace("smt") << "SmtEngine::check()" << endl;
 
-  d_resourceManager->beginCall();
 
-  // Only way we can be out of resource is if cumulative budget is on
-  if (d_resourceManager->cumulativeLimitOn() && d_resourceManager->out())
+  if (d_resourceManager->out())
   {
     Result::UnknownExplanation why = d_resourceManager->outOfResources()
                                          ? Result::RESOURCEOUT
                                          : Result::TIMEOUT;
     return Result(Result::ENTAILMENT_UNKNOWN, why, d_filename);
   }
+  d_resourceManager->beginCall();
 
   // Make sure the prop layer has all of the assertions
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
diff --git a/src/smt/smt_engine_stats.cpp b/src/smt/smt_engine_stats.cpp
index 964237499..9b25580d2 100644
--- a/src/smt/smt_engine_stats.cpp
+++ b/src/smt/smt_engine_stats.cpp
@@ -32,8 +32,7 @@ SmtEngineStatistics::SmtEngineStatistics()
       d_solveTime("smt::SmtEngine::solveTime"),
       d_pushPopTime("smt::SmtEngine::pushPopTime"),
       d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
-      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0),
-      d_resourceUnitsUsed("smt::SmtEngine::resourceUnitsUsed")
+      d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_definitionExpansionTime);
   smtStatisticsRegistry()->registerStat(&d_numConstantProps);
@@ -48,7 +47,6 @@ SmtEngineStatistics::SmtEngineStatistics()
   smtStatisticsRegistry()->registerStat(&d_pushPopTime);
   smtStatisticsRegistry()->registerStat(&d_processAssertionsTime);
   smtStatisticsRegistry()->registerStat(&d_simplifiedToFalse);
-  smtStatisticsRegistry()->registerStat(&d_resourceUnitsUsed);
 }
 
 SmtEngineStatistics::~SmtEngineStatistics()
@@ -66,7 +64,6 @@ SmtEngineStatistics::~SmtEngineStatistics()
   smtStatisticsRegistry()->unregisterStat(&d_pushPopTime);
   smtStatisticsRegistry()->unregisterStat(&d_processAssertionsTime);
   smtStatisticsRegistry()->unregisterStat(&d_simplifiedToFalse);
-  smtStatisticsRegistry()->unregisterStat(&d_resourceUnitsUsed);
 }
 
 }  // namespace smt
diff --git a/src/smt/smt_engine_stats.h b/src/smt/smt_engine_stats.h
index 3ea46eaa4..3463a0371 100644
--- a/src/smt/smt_engine_stats.h
+++ b/src/smt/smt_engine_stats.h
@@ -53,8 +53,6 @@ struct SmtEngineStatistics
 
   /** Has something simplified to false? */
   IntStat d_simplifiedToFalse;
-  /** Number of resource units spent. */
-  ReferenceStat<uint64_t> d_resourceUnitsUsed;
 }; /* struct SmtEngineStatistics */
 
 }  // namespace smt