Avoid options listener for resource manager. (#6366)

This PR simplifies how the resource manager interacts with the options. Instead of using some notification mechanism, the resource manager simply retrieves the options via options::xyz(). This simplifies the options handler, the resource manager interface and the options.
When instructed to do so by the API, the SmtEngine now overwrites the respective option instead of calling out to the resource manager.

4 files changed, 16 insertions, 26 deletions

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 68ee629dc..c84854992 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -28,8 +28,7 @@
 namespace cvc5 {
 namespace smt {
 
-OptionsManager::OptionsManager(Options* opts, ResourceManager* rm)
-    : d_options(opts), d_resourceManager(rm)
+OptionsManager::OptionsManager(Options* opts) : d_options(opts)
 {
   // set options that must take effect immediately
   if (opts->wasSetByUser(options::defaultExprDepth))
@@ -125,20 +124,6 @@ void OptionsManager::notifySetOption(const std::string& key)
 
 void OptionsManager::finishInit(LogicInfo& logic, bool isInternalSubsolver)
 {
-  // set up the timeouts and resource limits
-  if ((*d_options)[options::perCallResourceLimit] != 0)
-  {
-    d_resourceManager->setResourceLimit(options::perCallResourceLimit(), false);
-  }
-  if ((*d_options)[options::cumulativeResourceLimit] != 0)
-  {
-    d_resourceManager->setResourceLimit(options::cumulativeResourceLimit(),
-                                        true);
-  }
-  if ((*d_options)[options::perCallMillisecondLimit] != 0)
-  {
-    d_resourceManager->setTimeLimit(options::perCallMillisecondLimit());
-  }
   // ensure that our heuristics are properly set up
   setDefaults(logic, isInternalSubsolver);
 }
diff --git a/src/smt/options_manager.h b/src/smt/options_manager.h
index 4705b4273..2201ceb40 100644
--- a/src/smt/options_manager.h
+++ b/src/smt/options_manager.h
@@ -42,7 +42,7 @@ namespace smt {
 class OptionsManager : public OptionsListener
 {
  public:
-  OptionsManager(Options* opts, ResourceManager* rm = nullptr);
+  OptionsManager(Options* opts);
   ~OptionsManager();
   /**
    * Called when a set option call is made on the options object associated
@@ -65,8 +65,6 @@ class OptionsManager : public OptionsListener
  private:
   /** Reference to the options object */
   Options* d_options;
-  /** Pointer to the resource manager */
-  ResourceManager* d_resourceManager;
   /** Manager for the memory of regular-output-channel. */
   ManagedRegularOutputChannel d_managedRegularChannel;
   /** Manager for the memory of diagnostic-output-channel. */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c877b7ce3..88cb078ae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -123,7 +123,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
   // non-null. This may throw an options exception.
   d_env->setOptions(optr);
   // set the options manager
-  d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager()));
+  d_optm.reset(new smt::OptionsManager(&getOptions()));
   // listen to node manager events
   getNodeManager()->subscribeEvents(d_snmListener.get());
   // listen to resource out
@@ -1841,13 +1841,20 @@ void SmtEngine::interrupt()
   d_smtSolver->interrupt();
 }
 
-void SmtEngine::setResourceLimit(unsigned long units, bool cumulative)
+void SmtEngine::setResourceLimit(uint64_t units, bool cumulative)
 {
-  getResourceManager()->setResourceLimit(units, cumulative);
+  if (cumulative)
+  {
+    d_env->d_options.set(options::cumulativeResourceLimit__option_t(), units);
+  }
+  else
+  {
+    d_env->d_options.set(options::perCallResourceLimit__option_t(), units);
+  }
 }
-void SmtEngine::setTimeLimit(unsigned long milis)
+void SmtEngine::setTimeLimit(uint64_t millis)
 {
-  getResourceManager()->setTimeLimit(milis);
+  d_env->d_options.set(options::perCallMillisecondLimit__option_t(), millis);
 }
 
 unsigned long SmtEngine::getResourceUsage() const
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 151b6106b..ff1a955ee 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -776,7 +776,7 @@ class CVC4_EXPORT SmtEngine
    * resource limit for all remaining calls into the SmtEngine (true), or
    * whether it's a per-call resource limit (false); the default is false
    */
-  void setResourceLimit(unsigned long units, bool cumulative = false);
+  void setResourceLimit(uint64_t units, bool cumulative = false);
 
   /**
    * Set a per-call time limit for SmtEngine operations.
@@ -801,7 +801,7 @@ class CVC4_EXPORT SmtEngine
    *
    * @param millis the time limit in milliseconds, or 0 for no limit
    */
-  void setTimeLimit(unsigned long millis);
+  void setTimeLimit(uint64_t millis);
 
   /**
    * Get the current resource usage count for this SmtEngine.  This