Clean up option usage in command executor (#6844)

This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.

8 files changed, 59 insertions, 42 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 5a34f1453..4e14b8e34 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4742,7 +4742,7 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats)
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Solver::Solver(Options* opts)
+Solver::Solver(const Options* opts)
 {
   d_nodeMgr.reset(new NodeManager());
   d_originalOptions.reset(new Options());
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 161522654..0ee5990da 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -49,6 +49,10 @@ class Random;
 class Result;
 class StatisticsRegistry;
 
+namespace main {
+class CommandExecutor;
+}
+
 namespace api {
 
 class Solver;
@@ -2725,6 +2729,7 @@ class CVC5_EXPORT Solver
   friend class Grammar;
   friend class Op;
   friend class cvc5::Command;
+  friend class cvc5::main::CommandExecutor;
   friend class Sort;
   friend class Term;
 
@@ -2738,7 +2743,7 @@ class CVC5_EXPORT Solver
    * @param opts an optional pointer to a solver options object
    * @return the Solver
    */
-  Solver(Options* opts = nullptr);
+  Solver(const Options* opts = nullptr);
 
   /**
    * Destructor.
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index b6ead1b70..55b93a15c 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -50,10 +50,10 @@ void setNoLimitCPU() {
 #endif /* ! __WIN32__ */
 }
 
-CommandExecutor::CommandExecutor(Options& options)
+CommandExecutor::CommandExecutor(const Options& options)
     : d_solver(new api::Solver(&options)),
       d_symman(new SymbolManager(d_solver.get())),
-      d_options(options),
+      d_driverOptions(&options),
       d_result()
 {
 }
@@ -66,7 +66,7 @@ CommandExecutor::~CommandExecutor()
 
 void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  if (d_options.base.statistics)
+  if (d_solver->getOptions().base.statistics)
   {
     getSmtEngine()->printStatistics(out);
   }
@@ -74,7 +74,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const
 
 void CommandExecutor::printStatisticsSafe(int fd) const
 {
-  if (d_options.base.statistics)
+  if (d_solver->getOptions().base.statistics)
   {
     getSmtEngine()->printStatisticsSafe(fd);
   }
@@ -82,7 +82,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if (d_options.base.parseOnly)
+  if (d_solver->getOptions().base.parseOnly)
   {
     return true;
   }
@@ -101,9 +101,9 @@ bool CommandExecutor::doCommand(Command* cmd)
 
     return status;
   } else {
-    if (d_options.base.verbosity > 2)
+    if (d_solver->getOptions().base.verbosity > 2)
     {
-      *d_options.base.out << "Invoking: " << *cmd << std::endl;
+      *d_solver->getOptions().base.out << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -112,23 +112,24 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  printStatistics(*d_options.base.err);
+  printStatistics(*d_solver->getOptions().base.err);
   /* We have to keep options passed via CL on reset. These options are stored
-   * in CommandExecutor::d_options (populated and created in the driver), and
-   * CommandExecutor::d_options only contains *these* options since the
-   * NodeManager copies the options into a new options object before SmtEngine
-   * configures additional options based on the given CL options.
-   * We can thus safely reuse CommandExecutor::d_options here. */
-  d_solver.reset(new api::Solver(&d_options));
+   * in CommandExecutor::d_driverOptions (populated and created in the driver),
+   * and CommandExecutor::d_driverOptions only contains *these* options since
+   * the SmtEngine copies them into its own options object before configuring
+   * additional options based on the given CL options.
+   * We can thus safely reuse CommandExecutor::d_driverOptions here.
+   */
+  d_solver.reset(new api::Solver(d_driverOptions));
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
-  if (d_options.base.verbosity >= -1)
+  if (d_solver->getOptions().base.verbosity >= -1)
   {
     status = solverInvoke(
-        d_solver.get(), d_symman.get(), cmd, d_options.base.out);
+        d_solver.get(), d_symman.get(), cmd, d_solver->getOptions().base.out);
   }
   else
   {
@@ -151,9 +152,10 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if ((cs != nullptr || q != nullptr) && d_options.base.statisticsEveryQuery)
+  if ((cs != nullptr || q != nullptr)
+      && d_solver->getOptions().base.statisticsEveryQuery)
   {
-    getSmtEngine()->printStatisticsDiff(*d_options.base.err);
+    getSmtEngine()->printStatisticsDiff(*d_solver->getOptions().base.err);
   }
 
   bool isResultUnsat = res.isUnsat() || res.isEntailed();
@@ -161,32 +163,34 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   // dump the model/proof/unsat core if option is set
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
-    if (d_options.driver.dumpModels
+    if (d_solver->getOptions().driver.dumpModels
         && (res.isSat()
             || (res.isSatUnknown()
                 && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.driver.dumpProofs && isResultUnsat)
+    if (d_solver->getOptions().driver.dumpProofs && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
 
-    if (d_options.driver.dumpInstantiations
+    if (d_solver->getOptions().driver.dumpInstantiations
         && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if ((d_options.driver.dumpUnsatCores || d_options.driver.dumpUnsatCoresFull) && isResultUnsat)
+    if ((d_solver->getOptions().driver.dumpUnsatCores
+         || d_solver->getOptions().driver.dumpUnsatCoresFull)
+        && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
     if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
-      if (d_options.driver.forceNoLimitCpuWhileDump)
+      if (d_solver->getOptions().driver.forceNoLimitCpuWhileDump)
       {
         setNoLimitCPU();
       }
@@ -226,17 +230,17 @@ bool solverInvoke(api::Solver* solver,
 }
 
 void CommandExecutor::flushOutputStreams() {
-  printStatistics(*d_options.base.err);
+  printStatistics(*d_solver->getOptions().base.err);
 
   // make sure out and err streams are flushed too
 
-  if (d_options.base.out != nullptr)
+  if (d_solver->getOptions().base.out != nullptr)
   {
-    *d_options.base.out << std::flush;
+    *d_solver->getOptions().base.out << std::flush;
   }
-  if (d_options.base.err != nullptr)
+  if (d_solver->getOptions().base.err != nullptr)
   {
-    *d_options.base.err << std::flush;
+    *d_solver->getOptions().base.err << std::flush;
   }
 }
 
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 1f08d44a7..14866cd28 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -52,11 +52,16 @@ class CommandExecutor
    * symbol manager.
    */
   std::unique_ptr<SymbolManager> d_symman;
-  Options& d_options;
+  /**
+   * A pointer to the original options from the driver. Contain options as
+   * parsed from the command line. Used when the solver is reset.
+   */
+  const Options* d_driverOptions;
+
   api::Result d_result;
 
  public:
-  CommandExecutor(Options& options);
+  CommandExecutor(const Options& options);
 
   virtual ~CommandExecutor();
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 2bc5c59f3..9d221450b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -51,8 +51,6 @@ using namespace cvc5::main;
 
 namespace cvc5 {
 namespace main {
-/** Global options variable */
-thread_local Options* pOptions;
 
 /** Full argv[0] */
 const char* progPath;
@@ -79,7 +77,7 @@ TotalTimer::~TotalTimer()
     }  // namespace main
     }  // namespace cvc5
 
-void printUsage(Options& opts, bool full) {
+void printUsage(const Options& opts, bool full) {
   stringstream ss;
   ss << "usage: " << progName << " [options] [input-file]"
      << endl
@@ -98,8 +96,6 @@ void printUsage(Options& opts, bool full) {
 int runCvc5(int argc, char* argv[], Options& opts)
 {
   main::totalTime = std::make_unique<TotalTimer>();
-  // For the signal handlers' benefit
-  pOptions = &opts;
 
   // Initialize the signal handlers
   signal_handlers::install();
diff --git a/src/main/main.h b/src/main/main.h
index 14d99f79c..636df405f 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -59,14 +59,11 @@ extern std::unique_ptr<TotalTimer> totalTime;
  */
 extern bool segvSpin;
 
-/** A pointer to the options in play */
-extern thread_local Options* pOptions;
-
 }  // namespace main
 }  // namespace cvc5
 
 /** Actual cvc5 driver functions **/
 int runCvc5(int argc, char* argv[], cvc5::Options&);
-void printUsage(cvc5::Options&, bool full = false);
+void printUsage(const cvc5::Options&, bool full = false);
 
 #endif /* CVC5__MAIN__MAIN_H */
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index b65600eb5..cff8b47d3 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -36,7 +36,6 @@
 #include "base/exception.h"
 #include "main/command_executor.h"
 #include "main/main.h"
-#include "options/options.h"
 #include "util/safe_print.h"
 
 using cvc5::Exception;
diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2
index ae9d93b6f..d6d5325b0 100644
--- a/test/regress/regress0/options/statistics.smt2
+++ b/test/regress/regress0/options/statistics.smt2
@@ -15,6 +15,10 @@
 ; EXPECT: false
 ; EXPECT: false
 ; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
 (set-logic QF_UF)
 (get-option :stats)
 (get-option :stats-all)
@@ -40,4 +44,11 @@
 (get-option :stats)
 (get-option :stats-all)
 (get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats false)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
 (get-option :stats-expert)
\ No newline at end of file