From: Gereon Kremer <nafur42@gmail.com>
Date: Tue, 8 Jun 2021 13:43:13 +0000 (+0200)
Subject: Make env hold a pointer to the original options to properly initialize subsolvers... 
X-Git-Tag: cvc5-1.0.0~1629
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=52f02c087ca45a65c1e483faab32ac2078106aa0;p=cvc5.git

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.
---

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 */