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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 5a34f145389c0b9c20e86bca780701ed081c5d86..4e14b8e34068e3f5c5cce6fb0631116d8158b201 100644 (file)
--- 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 1615226547585601b99016aa5b62c72d0bae508d..0ee5990da7545f92aff437537c8cb21dfd539890 100644 (file)
--- 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 b6ead1b708f103d4ac306233b45aac2c49945f26..55b93a15c26777ebc014949788e482503256dbdc 100644 (file)
--- 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 1f08d44a7da85db7d6473925f4e77e523a5deb89..14866cd28d935ab6bc0242735cc551cb6e984efc 100644 (file)
--- 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 2bc5c59f3804df2cab40708b3e9b3eecb57d7b4a..9d221450b5f151f6237accba939d25474b5e890a 100644 (file)
--- 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 14d99f79cc18136b836085ee17bc078045fdd4ad..636df405f3347070ff85a9b56769c82596a4aa5b 100644 (file)
--- 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 b65600eb5fb39128abe2ffc0995b636aeb2e6fd6..cff8b47d3e815c6cce5de0a55637c658a34eec59 100644 (file)
--- 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 ae9d93b6f8cfabd016fe0176cab480fb0c19e7d3..d6d5325b08658a579085edf3b83277a6065a4bd1 100644 (file)
--- 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)
@@ -37,6 +41,13 @@
 
 (set-option :stats-expert true)
 
+(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)