diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-06-08 15:43:13 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-08 13:43:13 +0000 |
commit | 52f02c087ca45a65c1e483faab32ac2078106aa0 (patch) | |
tree | 2034cc1cc8365da5a03422477e259dc6ec6abf8d | |
parent | 57b632c70aa01c95216fd5f43338cf2d76374b4e (diff) |
Make env hold a pointer to the original options to properly initialize subsolvers (#6705)
This PR extends the Env class to hold a pointer to the original options that are owned by the api::Solver. These original options will be used to properly initialize subsolvers as using the current options leads to subtle issues as setDefaults is not (in general) idempotent.
-rw-r--r-- | src/smt/env.cpp | 3 | ||||
-rw-r--r-- | src/smt/env.h | 9 |
2 files changed, 12 insertions, 0 deletions
diff --git a/src/smt/env.cpp b/src/smt/env.cpp index 1381ef87c..b6cdfb67b 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -43,6 +43,7 @@ Env::Env(NodeManager* nm, Options* opts) d_logic(), d_statisticsRegistry(std::make_unique<StatisticsRegistry>()), d_options(), + d_originalOptions(opts), d_resourceManager() { if (opts != nullptr) @@ -97,6 +98,8 @@ StatisticsRegistry& Env::getStatisticsRegistry() const Options& Env::getOptions() const { return d_options; } +const Options& Env::getOriginalOptions() const { return *d_originalOptions; } + ResourceManager* Env::getResourceManager() const { return d_resourceManager.get(); diff --git a/src/smt/env.h b/src/smt/env.h index 29a360209..57b5ad9c7 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -94,6 +94,9 @@ class Env /** Get the options object (const version only) owned by this Env. */ const Options& getOptions() const; + /** Get the original options object (const version only). */ + const Options& getOriginalOptions() const; + /** Get the resource manager owned by this Env. */ ResourceManager* getResourceManager() const; @@ -180,6 +183,12 @@ class Env * consider during solving and initialization. */ Options d_options; + /** + * A pointer to the original options object as stored in the api::Solver. + * The referenced objects holds the options as initially parsed before being + * changed, e.g., by setDefaults(). + */ + const Options* d_originalOptions; /** Manager for limiting time and abstract resource usage. */ std::unique_ptr<ResourceManager> d_resourceManager; }; /* class Env */ |