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.

5 files changed, 62 insertions, 59 deletions

diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index df632224c..38f68461b 100644
--- 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 4d8a979c6..324850c43 100644
--- 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 6ad537240..8c55a19eb 100644
--- 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
index 000000000..05dd613f1
--- /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 bb5cc1abe..24ae162da 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -445,60 +445,6 @@ header = "options/smt_options.h"
   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"
   long       = "force-no-limit-cpu-while-dump"
@@ -516,7 +462,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "Cross-theory rewrites"
 
-
 [[option]]
   name       = "solveBVAsInt"
   category   = "undocumented"