Refactor resource manager options (#6446)

This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index df632224ceffb4617e22040e9991578df4026508..38f68461b3e254e099256bc7067ebbeafb257fff 100644 (file)
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -55,6 +55,7 @@ set(options_toml_files
   proof_options.toml
   prop_options.toml
   quantifiers_options.toml
+  resource_manager_options.toml
   sep_options.toml
   sets_options.toml
   smt_options.toml

diff --git a/src/options/options.h b/src/options/options.h
index 4d8a979c653769890604f94e041aec0e9406cd77..324850c43f58b7c9a263eb70f0cb09ec52bf74ab 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -192,7 +192,7 @@ public:
   bool getStatsEveryQuery() const;
   bool getStrictParsing() const;
   int getTearDownIncremental() const;
-  unsigned long getCumulativeTimeLimit() const;
+  uint64_t getCumulativeTimeLimit() const;
   bool getVersion() const;
   const std::string& getForceLogicString() const;
   int getVerbosity() const;

diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 6ad537240c755f037483f05f5d89db30fcfeab1e..8c55a19eb18f5271c1beda6d3225c5bd0b05af8d 100644 (file)
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -16,8 +16,6 @@
  * Options::wasSetByUser<T> for different option types T.
  */
 
-#include "options.h"
-
 #include <fstream>
 #include <ostream>
 #include <string>
@@ -25,6 +23,7 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
+#include "options.h"
 #include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
@@ -33,6 +32,7 @@
 #include "options/printer_modes.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
+#include "options/resource_manager_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
 
@@ -141,7 +141,8 @@ int Options::getTearDownIncremental() const{
   return (*this)[options::tearDownIncremental];
 }
 
-unsigned long Options::getCumulativeTimeLimit() const {
+uint64_t Options::getCumulativeTimeLimit() const
+{
   return (*this)[options::cumulativeMillisecondLimit];
 }
 

diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
new file mode 100644 (file)
index 0000000..05dd613
--- /dev/null
+++ b/src/options/resource_manager_options.toml
@@ -0,0 +1,56 @@
+id     = "resource_manager"
+name   = "Resource Manager options"
+header = "options/resource_manager_options.h"
+
+[[option]]
+  name       = "cumulativeMillisecondLimit"
+  smt_name   = "tlimit"
+  category   = "common"
+  long       = "tlimit=MS"
+  type       = "uint64_t"
+  help       = "set time limit in milliseconds of wall clock time"
+
+[[option]]
+  name       = "perCallMillisecondLimit"
+  smt_name   = "tlimit-per"
+  category   = "common"
+  long       = "tlimit-per=MS"
+  type       = "uint64_t"
+  help       = "set time limit per query in milliseconds"
+
+[[option]]
+  name       = "cumulativeResourceLimit"
+  smt_name   = "rlimit"
+  category   = "common"
+  long       = "rlimit=N"
+  type       = "uint64_t"
+  help       = "set resource limit"
+
+[[option]]
+  name       = "perCallResourceLimit"
+  smt_name   = "reproducible-resource-limit"
+  category   = "common"
+  long       = "rlimit-per=N"
+  type       = "uint64_t"
+  help       = "set resource limit per query"
+
+# --rweight is used to override the default of one particular resource weight.
+# It can be given multiple times to override multiple weights. When options are
+# parsed, the resource manager might now be created yet, and it is not clear
+# how an option handler would access it in a reasonable way. The option handler
+# thus merely puts the data in another option that holds a vector of strings.
+# This other option "resourceWeightHolder" has the sole purpose of storing
+# this data in a way so that the resource manager can access it in its
+# constructor.
+[[option]]
+  category   = "expert"
+  long       = "rweight=VAL=N"
+  type       = "std::string"
+  handler    = "setResourceWeight"
+  read_only  = true
+  help       = "set a single resource weight"
+
+[[option]]
+  name       = "resourceWeightHolder"
+  category   = "undocumented"
+  type       = "std::vector<std::string>"

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index bb5cc1abea5234d00cd499eae0c6361dca271249..24ae162dadffddec787901d5bd76adfce6606944 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -444,60 +444,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "set the diagnostic output channel of the solver"
 
-[[option]]
-  name       = "cumulativeMillisecondLimit"
-  smt_name   = "tlimit"
-  category   = "common"
-  long       = "tlimit=MS"
-  type       = "uint64_t"
-  help       = "set time limit in milliseconds of wall clock time"
-
-[[option]]
-  name       = "perCallMillisecondLimit"
-  smt_name   = "tlimit-per"
-  category   = "common"
-  long       = "tlimit-per=MS"
-  type       = "uint64_t"
-  help       = "set time limit per query in milliseconds"
-
-[[option]]
-  name       = "cumulativeResourceLimit"
-  smt_name   = "rlimit"
-  category   = "common"
-  long       = "rlimit=N"
-  type       = "uint64_t"
-  help       = "set resource limit"
-
-[[option]]
-  name       = "perCallResourceLimit"
-  smt_name   = "reproducible-resource-limit"
-  category   = "common"
-  long       = "rlimit-per=N"
-  type       = "uint64_t"
-  help       = "set resource limit per query"
-
-# --rweight is used to override the default of one particular resource weight.
-# It can be given multiple times to override multiple weights. When options are
-# parsed, the resource manager might now be created yet, and it is not clear
-# how an option handler would access it in a reasonable way. The option handler
-# thus merely puts the data in another option that holds a vector of strings.
-# This other option "resourceWeightHolder" has the sole purpose of storing
-# this data in a way so that the resource manager can access it in its
-# constructor.
-[[option]]
-  smt_name   = "resourceWeight"
-  category   = "expert"
-  long       = "rweight=VAL=N"
-  type       = "std::string"
-  handler    = "setResourceWeight"
-  read_only  = true
-  help       = "set a single resource weight"
-
-[[option]]
-  name       = "resourceWeightHolder"
-  category   = "undocumented"
-  type       = "std::vector<std::string>"
-
 [[option]]
   name       = "forceNoLimitCpuWhileDump"
   category   = "regular"
@@ -516,7 +462,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "Cross-theory rewrites"
 
-
 [[option]]
   name       = "solveBVAsInt"
   category   = "undocumented"

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 46e11af205fa26987dabb15800be1057b1cb43e6..ef338fdfecf7200bf6290156eba3ef4eed44bc2e 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -29,6 +29,7 @@
 #include "options/option_exception.h"
 #include "options/printer_options.h"
 #include "options/proof_options.h"
+#include "options/resource_manager_options.h"
 #include "options/smt_options.h"
 #include "options/theory_options.h"
 #include "printer/printer.h"

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 872b23ac4140c945c8bf3720f943403e368e735b..de9a322487fa9a2a6c6a612f6af59d820bb28ee1 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -24,7 +24,7 @@
 #include "base/output.h"
 #include "options/option_exception.h"
 #include "options/options.h"
-#include "options/smt_options.h"
+#include "options/resource_manager_options.h"
 #include "util/statistics_registry.h"
 
 using namespace std;
@@ -151,8 +151,10 @@ bool setWeight(const std::string& name, uint64_t weight, Weights& weights)
 
 /*---------------------------------------------------------------------------*/
 
-ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
-    : d_perCallTimer(),
+ResourceManager::ResourceManager(StatisticsRegistry& stats,
+                                 const Options& options)
+    : d_options(options),
+      d_perCallTimer(),
       d_cumulativeTimeUsed(0),
       d_cumulativeResourceUsed(0),
       d_thisCallResourceUsed(0),
@@ -162,8 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats, Options& options)
 
   d_infidWeights.fill(1);
   d_resourceWeights.fill(1);
-  for (const auto& opt :
-       options[cvc5::options::resourceWeightHolder__option_t()])
+  for (const auto& opt : d_options[options::resourceWeightHolder])
   {
     std::string name;
     uint64_t weight;
@@ -188,8 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
 
 uint64_t ResourceManager::getResourceRemaining() const
 {
-  if (options::cumulativeResourceLimit() <= d_cumulativeResourceUsed) return 0;
-  return options::cumulativeResourceLimit() - d_cumulativeResourceUsed;
+  if (d_options[options::cumulativeResourceLimit] <= d_cumulativeResourceUsed)
+    return 0;
+  return d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed;
 }
 
 void ResourceManager::spendResource(uint64_t amount)
@@ -235,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid)
 
 void ResourceManager::beginCall()
 {
-  d_perCallTimer.set(options::perCallMillisecondLimit());
+  d_perCallTimer.set(d_options[options::perCallMillisecondLimit]);
   d_thisCallResourceUsed = 0;
 
-  if (options::cumulativeResourceLimit() > 0)
+  if (d_options[options::cumulativeResourceLimit] > 0)
   {
     // Compute remaining cumulative resource budget
     d_thisCallResourceBudget =
-        options::cumulativeResourceLimit() - d_cumulativeResourceUsed;
+        d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed;
   }
-  if (options::perCallResourceLimit() > 0)
+  if (d_options[options::perCallResourceLimit] > 0)
   {
     // Check if per-call resource budget is even smaller
-    if (options::perCallResourceLimit() < d_thisCallResourceBudget)
+    if (d_options[options::perCallResourceLimit] < d_thisCallResourceBudget)
     {
-      d_thisCallResourceBudget = options::perCallResourceLimit();
+      d_thisCallResourceBudget = d_options[options::perCallResourceLimit];
     }
   }
 }
@@ -263,25 +265,25 @@ void ResourceManager::endCall()
 
 bool ResourceManager::limitOn() const
 {
-  return (options::cumulativeResourceLimit() > 0)
-         || (options::perCallMillisecondLimit() > 0)
-         || (options::perCallResourceLimit() > 0);
+  return (d_options[options::cumulativeResourceLimit] > 0)
+         || (d_options[options::perCallMillisecondLimit] > 0)
+         || (d_options[options::perCallResourceLimit] > 0);
 }
 
 bool ResourceManager::outOfResources() const
 {
-  if (options::perCallResourceLimit() > 0)
+  if (d_options[options::perCallResourceLimit] > 0)
   {
     // Check if per-call resources are exhausted
-    if (d_thisCallResourceUsed >= options::perCallResourceLimit())
+    if (d_thisCallResourceUsed >= d_options[options::perCallResourceLimit])
     {
       return true;
     }
   }
-  if (options::cumulativeResourceLimit() > 0)
+  if (d_options[options::cumulativeResourceLimit] > 0)
   {
     // Check if cumulative resources are exhausted
-    if (d_cumulativeResourceUsed >= options::cumulativeResourceLimit())
+    if (d_cumulativeResourceUsed >= d_options[options::cumulativeResourceLimit])
     {
       return true;
     }
@@ -291,7 +293,7 @@ bool ResourceManager::outOfResources() const
 
 bool ResourceManager::outOfTime() const
 {
-  if (options::perCallMillisecondLimit() == 0) return false;
+  if (d_options[options::perCallMillisecondLimit] == 0) return false;
   return d_perCallTimer.expired();
 }
 

diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 2590799fcd80cfeb74e6d275fc20cca9fcadf1be..3dd3370584c3cb39deee0a21db0a3f28174605cf 100644 (file)
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -114,7 +114,8 @@ class ResourceManager
 {
  public:
   /** Construct a resource manager. */
-  ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
+  ResourceManager(StatisticsRegistry& statistics_registry,
+                  const Options& options);
   /** Default destructor. */
   ~ResourceManager();
   /** Can not be copied. */
@@ -173,6 +174,7 @@ class ResourceManager
   void registerListener(Listener* listener);
 
  private:
+  const Options& d_options;
   /** The per-call wall clock timer. */
   WallClockTimer d_perCallTimer;