Make env hold a pointer to the original options to properly initialize subsolvers...

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.

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 1381ef87c05348312f596f19c5aad8c61fe4058c..b6cdfb67b12757eac6e3ad237e87afec06ddc013 100644 (file)
--- 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 29a3602091a7f941ca3d3d1ea6d4f3446538fdc6..57b5ad9c73a2b72ef8addd7b3be8caebe955ff3d 100644 (file)
--- 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 */