From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 20 Aug 2021 21:47:04 +0000 (-0700)
Subject: Make driver use options from the solver (#6930)
X-Git-Tag: cvc5-1.0.0~1355
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d3df62e637057c77bab90ae644437fe250a64d37;p=cvc5.git

Make driver use options from the solver (#6930)

This PR removes explicit ownership of the options object from the main function and replaces it by an api::Solver object. To achieve this, it does a number of minor changes:
- api::Solver not takes a unique_ptr<Options> in its constructor
- CommandExecutor only holds a reference to (a unique ptr of) the api::Solver
- the main functions accesses options via the solver
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 82064b758..f5e2c8f0c 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4951,20 +4951,18 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats)
 /* Solver                                                                     */
 /* -------------------------------------------------------------------------- */
 
-Solver::Solver(const Options* opts)
+Solver::Solver(std::unique_ptr<Options>&& original)
 {
   d_nodeMgr.reset(new NodeManager());
-  d_originalOptions.reset(new Options());
-  if (opts != nullptr)
-  {
-    d_originalOptions->copyValues(*opts);
-  }
+  d_originalOptions = std::move(original);
   d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get()));
   d_smtEngine->setSolver(this);
   d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed));
   resetStatistics();
 }
 
+Solver::Solver() : Solver(std::make_unique<Options>()) {}
+
 Solver::~Solver() {}
 
 /* Helpers and private functions                                              */
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 62ee9ac32..3226dd4fd 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2781,6 +2781,13 @@ class CVC5_EXPORT Solver
   friend class Sort;
   friend class Term;
 
+ private:
+  /*
+   * Constructs a solver with the given original options. This should only be
+   * used internally when the Solver is reset.
+   */
+  Solver(std::unique_ptr<Options>&& original);
+
  public:
   /* .................................................................... */
   /* Constructors/Destructors                                             */
@@ -2788,10 +2795,9 @@ class CVC5_EXPORT Solver
 
   /**
    * Constructor.
-   * @param opts an optional pointer to a solver options object
    * @return the Solver
    */
-  Solver(const Options* opts = nullptr);
+  Solver();
 
   /**
    * Destructor.
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 99e471b0a..ee73187ff 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -155,7 +155,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
 
 
     cdef cppclass Solver:
-        Solver(Options*) except +
+        Solver() except +
         Sort getBooleanSort() except +
         Sort getIntegerSort() except +
         Sort getNullSort() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index d31fdc126..210eb0639 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -487,7 +487,7 @@ cdef class Solver:
     cdef c_Solver* csolver
 
     def __cinit__(self):
-        self.csolver = new c_Solver(NULL)
+        self.csolver = new c_Solver()
 
     def __dealloc__(self):
         del self.csolver
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4e25e984d..f60ed925b 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -29,6 +29,7 @@
 #include "options/base_options.h"
 #include "options/main_options.h"
 #include "smt/command.h"
+#include "smt/smt_engine.h"
 
 namespace cvc5 {
 namespace main {
@@ -49,17 +50,23 @@ void setNoLimitCPU() {
 #endif /* ! __WIN32__ */
 }
 
-CommandExecutor::CommandExecutor(const Options& options)
-    : d_solver(new api::Solver(&options)),
+CommandExecutor::CommandExecutor(std::unique_ptr<api::Solver>& solver)
+    : d_solver(solver),
       d_symman(new SymbolManager(d_solver.get())),
       d_result()
 {
 }
 CommandExecutor::~CommandExecutor()
 {
-  // ensure that symbol manager is destroyed before solver
-  d_symman.reset(nullptr);
-  d_solver.reset(nullptr);
+}
+
+Options& CommandExecutor::getOptions()
+{
+  return d_solver->d_smtEngine->getOptions();
+}
+void CommandExecutor::storeOptionsAsOriginal()
+{
+  d_solver->d_originalOptions->copyValues(getOptions());
 }
 
 void CommandExecutor::printStatistics(std::ostream& out) const
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index ff7b89928..e8c2d25ac 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -40,7 +40,7 @@ class CommandExecutor
    * The solver object, which is allocated by this class and is used for
    * executing most commands (e.g. check-sat).
    */
-  std::unique_ptr<api::Solver> d_solver;
+  std::unique_ptr<api::Solver>& d_solver;
   /**
    * The symbol manager, which is allocated by this class. This manages
    * all things related to definitions of symbols and their impact on behaviors
@@ -56,7 +56,7 @@ class CommandExecutor
   api::Result d_result;
 
  public:
-  CommandExecutor(const Options& options);
+  CommandExecutor(std::unique_ptr<api::Solver>& solver);
 
   virtual ~CommandExecutor();
 
@@ -83,6 +83,11 @@ class CommandExecutor
 
   SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); }
 
+  /** Get the current options from the solver */
+  Options& getOptions();
+  /** Store the current options as the original options */
+  void storeOptionsAsOriginal();
+
   /**
    * Prints statistics to an output stream.
    * Checks whether statistics should be printed according to the options.
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 0f1130234..93d458c32 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -95,7 +95,7 @@ void printUsage(const Options& opts, bool full) {
   }
 }
 
-int runCvc5(int argc, char* argv[], Options& opts)
+int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 {
   main::totalTime = std::make_unique<TotalTimer>();
 
@@ -104,32 +104,36 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
   progPath = argv[0];
 
+  // Create the command executor to execute the parsed commands
+  pExecutor = std::make_unique<CommandExecutor>(solver);
+  Options* opts = &pExecutor->getOptions();
+
   // Parse the options
-  std::vector<string> filenames = options::parse(opts, argc, argv, progName);
+  std::vector<string> filenames = options::parse(*opts, argc, argv, progName);
 
-  auto limit = install_time_limit(opts);
+  auto limit = install_time_limit(*opts);
 
-  if (opts.driver.help)
+  if (opts->driver.help)
   {
-    printUsage(opts, true);
+    printUsage(*opts, true);
     exit(1);
   }
-  else if (opts.base.languageHelp)
+  else if (opts->base.languageHelp)
   {
-    options::printLanguageHelp(*opts.base.out);
+    options::printLanguageHelp(*opts->base.out);
     exit(1);
   }
-  else if (opts.driver.version)
+  else if (opts->driver.version)
   {
-    *opts.base.out << Configuration::about().c_str() << flush;
+    *opts->base.out << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  segvSpin = opts.driver.segvSpin;
+  segvSpin = opts->driver.segvSpin;
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
-  *opts.base.out << unitbuf;
+  *opts->base.out << unitbuf;
 #endif /* CVC5_COMPETITION_MODE */
 
   // We only accept one input file
@@ -141,9 +145,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 
   // if we're reading from stdin on a TTY, default to interactive mode
-  if (!opts.driver.interactiveWasSetByUser)
+  if (!opts->driver.interactiveWasSetByUser)
   {
-    opts.driver.interactive = inputFromStdin && isatty(fileno(stdin));
+    opts->driver.interactive = inputFromStdin && isatty(fileno(stdin));
   }
 
   // Auto-detect input language by filename extension
@@ -153,33 +157,34 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
   const char* filename = filenameStr.c_str();
 
-  if (opts.base.inputLanguage == language::input::LANG_AUTO)
+  if (opts->base.inputLanguage == language::input::LANG_AUTO)
   {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      opts.base.inputLanguage = language::input::LANG_CVC;
+      opts->base.inputLanguage = language::input::LANG_CVC;
     } else {
       size_t len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
+        opts->base.inputLanguage = language::input::LANG_SMTLIB_V2_6;
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts.base.inputLanguage = language::input::LANG_TPTP;
+        opts->base.inputLanguage = language::input::LANG_TPTP;
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts.base.inputLanguage = language::input::LANG_CVC;
+        opts->base.inputLanguage = language::input::LANG_CVC;
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         // version 2 sygus is the default
-        opts.base.inputLanguage = language::input::LANG_SYGUS_V2;
+        opts->base.inputLanguage = language::input::LANG_SYGUS_V2;
       }
     }
   }
 
-  if (opts.base.outputLanguage == language::output::LANG_AUTO)
+  if (opts->base.outputLanguage == language::output::LANG_AUTO)
   {
-    opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage);
+    opts->base.outputLanguage = language::toOutputLanguage(opts->base.inputLanguage);
   }
+  pExecutor->storeOptionsAsOriginal();
 
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
@@ -192,11 +197,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
 
   // important even for muzzled builds (to get result output right)
-  (*opts.base.out)
-      << language::SetLanguage(opts.base.outputLanguage);
+  (*opts->base.out)
+      << language::SetLanguage(opts->base.outputLanguage);
 
-  // Create the command executor to execute the parsed commands
-  pExecutor = std::make_unique<CommandExecutor>(opts);
 
   int returnValue = 0;
   {
@@ -206,9 +209,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
     // Parse and execute commands until we are done
     std::unique_ptr<Command> cmd;
     bool status = true;
-    if (opts.driver.interactive && inputFromStdin)
+    if (opts->driver.interactive && inputFromStdin)
     {
-      if (!opts.base.incrementalSolvingWasSetByUser)
+      if (!opts->base.incrementalSolvingWasSetByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
@@ -234,12 +237,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
         try {
           cmd.reset(shell.readCommand());
         } catch(UnsafeInterruptException& e) {
-          *opts.base.out << CommandInterrupted();
+          *opts->base.out << CommandInterrupted();
           break;
         }
         if (cmd == nullptr)
           break;
         status = pExecutor->doCommand(cmd) && status;
+        opts = &pExecutor->getOptions();
         if (cmd->interrupted()) {
           break;
         }
@@ -247,7 +251,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
     else
     {
-      if (!opts.base.incrementalSolvingWasSetByUser)
+      if (!opts->base.incrementalSolvingWasSetByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "false"));
         cmd->setMuted(true);
@@ -256,25 +260,26 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
       ParserBuilder parserBuilder(pExecutor->getSolver(),
                                   pExecutor->getSymbolManager(),
-                                  opts);
+                                  *opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
         parser->setInput(Input::newStreamInput(
-            opts.base.inputLanguage, cin, filename));
+            opts->base.inputLanguage, cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(opts.base.inputLanguage,
+        parser->setInput(Input::newFileInput(opts->base.inputLanguage,
                                              filename,
-                                             opts.parser.memoryMap));
+                                             opts->parser.memoryMap));
       }
 
       bool interrupted = false;
       while (status)
       {
         if (interrupted) {
-          *opts.base.out << CommandInterrupted();
+          *opts->base.out << CommandInterrupted();
           pExecutor->reset();
+          opts = &pExecutor->getOptions();
           break;
         }
         try {
@@ -286,6 +291,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
 
         status = pExecutor->doCommand(cmd);
+        opts = &pExecutor->getOptions();
         if (cmd->interrupted() && status == 0) {
           interrupted = true;
           break;
@@ -307,9 +313,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
 
 #ifdef CVC5_COMPETITION_MODE
-    if (opts.base.out != nullptr)
+    if (opts->base.out != nullptr)
     {
-      *opts.base.out << std::flush;
+      *opts->base.out << std::flush;
     }
     // exit, don't return (don't want destructors to run)
     // _exit() from unistd.h doesn't run global destructors
@@ -321,12 +327,12 @@ int runCvc5(int argc, char* argv[], Options& opts)
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
-    if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser)
+    if (opts->driver.earlyExit && opts->driver.earlyExitWasSetByUser)
     {
       _exit(returnValue);
     }
 #else  /* CVC5_DEBUG */
-    if (opts.driver.earlyExit)
+    if (opts->driver.earlyExit)
     {
       _exit(returnValue);
     }
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 6173cfd69..12a2920b4 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -22,6 +22,7 @@
 #include <fstream>
 #include <iostream>
 
+#include "api/cpp/cvc5.h"
 #include "base/configuration.h"
 #include "base/output.h"
 #include "main/command_executor.h"
@@ -49,10 +50,11 @@ using namespace cvc5::language;
  */
 int main(int argc, char* argv[])
 {
-  Options opts;
+  std::unique_ptr<api::Solver> solver;
   try
   {
-    return runCvc5(argc, argv, opts);
+    solver = std::make_unique<api::Solver>();
+    return runCvc5(argc, argv, solver);
   }
   catch (cvc5::api::CVC5ApiOptionException& e)
   {
@@ -63,10 +65,10 @@ int main(int argc, char* argv[])
          << endl
          << "Please use --help to get help on command-line options." << endl;
   }
-  catch (cvc5::OptionException& e)
+  catch (OptionException& e)
   {
 #ifdef CVC5_COMPETITION_MODE
-    *opts.base.out << "unknown" << endl;
+    *solver->getOptions().base.out << "unknown" << endl;
 #endif
     cerr << "(error \"" << e.getMessage() << "\")" << endl
          << endl
@@ -75,20 +77,20 @@ int main(int argc, char* argv[])
   catch (Exception& e)
   {
 #ifdef CVC5_COMPETITION_MODE
-    *opts.base.out << "unknown" << endl;
+    *solver->getOptions().base.out << "unknown" << endl;
 #endif
-    if (language::isOutputLang_smt2(opts.base.outputLanguage))
+    if (language::isOutputLang_smt2(solver->getOptions().base.outputLanguage))
     {
-      *opts.base.out << "(error \"" << e << "\")" << endl;
+      *solver->getOptions().base.out << "(error \"" << e << "\")" << endl;
     }
     else
     {
-      *opts.base.err << "(error \"" << e << "\")" << endl;
+      *solver->getOptions().base.err << "(error \"" << e << "\")" << endl;
     }
-    if (opts.base.statistics && pExecutor != nullptr)
+    if (solver->getOptions().base.statistics && pExecutor != nullptr)
     {
       totalTime.reset();
-      pExecutor->printStatistics(*opts.base.err);
+      pExecutor->printStatistics(*solver->getOptions().base.err);
     }
   }
   exit(1);
diff --git a/src/main/main.h b/src/main/main.h
index 636df405f..e76836600 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -18,6 +18,7 @@
 #include <memory>
 #include <string>
 
+#include "api/cpp/cvc5.h"
 #include "base/cvc5config.h"
 #include "base/exception.h"
 #include "options/options.h"
@@ -63,7 +64,7 @@ extern bool segvSpin;
 }  // namespace cvc5
 
 /** Actual cvc5 driver functions **/
-int runCvc5(int argc, char* argv[], cvc5::Options&);
+int runCvc5(int argc, char* argv[], std::unique_ptr<cvc5::api::Solver>&);
 void printUsage(const cvc5::Options&, bool full = false);
 
 #endif /* CVC5__MAIN__MAIN_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 1981f1063..3dafdd7f0 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -249,7 +249,7 @@ void Command::resetSolver(api::Solver* solver)
   // CommandExecutor such that this reconstruction can be done within the
   // CommandExecutor, who actually owns the solver.
   solver->~Solver();
-  new (solver) api::Solver(opts.get());
+  new (solver) api::Solver(std::move(opts));
 }
 
 Node Command::termToNode(const api::Term& term) { return term.getNode(); }