diff options
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/options/options.h | 2 | ||||
-rw-r--r-- | src/options/options_public_functions.cpp | 7 | ||||
-rw-r--r-- | src/options/resource_manager_options.toml | 56 | ||||
-rw-r--r-- | src/options/smt_options.toml | 55 |
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" |