From 52f02c087ca45a65c1e483faab32ac2078106aa0 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 8 Jun 2021 15:43:13 +0200 Subject: 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. --- src/smt/env.cpp | 3 +++ src/smt/env.h | 9 +++++++++ 2 files changed, 12 insertions(+) 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()), 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 d_resourceManager; }; /* class Env */ -- cgit v1.2.3