Add Driver options (#7078)

This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.

7 files changed, 103 insertions, 66 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1eaae8761..e245dc415 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4749,6 +4749,25 @@ const static std::unordered_map<cvc5::RoundingMode,
     };
 
 /* -------------------------------------------------------------------------- */
+/* Options                                                                    */
+/* -------------------------------------------------------------------------- */
+
+DriverOptions::DriverOptions(const Solver& solver) : d_solver(solver) {}
+
+std::istream& DriverOptions::in() const
+{
+  return *d_solver.d_smtEngine->getOptions().base.in;
+}
+std::ostream& DriverOptions::err() const
+{
+  return *d_solver.d_smtEngine->getOptions().base.err;
+}
+std::ostream& DriverOptions::out() const
+{
+  return *d_solver.d_smtEngine->getOptions().base.out;
+}
+
+/* -------------------------------------------------------------------------- */
 /* Statistics                                                                 */
 /* -------------------------------------------------------------------------- */
 
@@ -7034,6 +7053,8 @@ std::vector<std::string> Solver::getOptionNames() const
   CVC5_API_TRY_CATCH_END;
 }
 
+DriverOptions Solver::getDriverOptions() const { return DriverOptions(*this); }
+
 std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 9f805fa65..d86fed14a 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2593,6 +2593,33 @@ struct CVC5_EXPORT hash<cvc5::api::RoundingMode>
 namespace cvc5::api {
 
 /* -------------------------------------------------------------------------- */
+/* Options                                                                    */
+/* -------------------------------------------------------------------------- */
+
+/**
+ * Provides access to options that can not be communicated via the regular
+ * getOption() or getOptionInfo() methods. This class does not store the options
+ * itself, but only acts as a wrapper to the solver object. It can thus no
+ * longer be used after the solver object has been destroyed.
+ */
+class CVC5_EXPORT DriverOptions
+{
+  friend class Solver;
+
+ public:
+  /** Access the solvers input stream */
+  std::istream& in() const;
+  /** Access the solvers error output stream */
+  std::ostream& err() const;
+  /** Access the solvers output stream */
+  std::ostream& out() const;
+
+ private:
+  DriverOptions(const Solver& solver);
+  const Solver& d_solver;
+};
+
+/* -------------------------------------------------------------------------- */
 /* Statistics                                                                 */
 /* -------------------------------------------------------------------------- */
 
@@ -2774,6 +2801,7 @@ class CVC5_EXPORT Solver
   friend class DatatypeConstructor;
   friend class DatatypeConstructorDecl;
   friend class DatatypeSelector;
+  friend class DriverOptions;
   friend class Grammar;
   friend class Op;
   friend class cvc5::Command;
@@ -3748,6 +3776,13 @@ class CVC5_EXPORT Solver
   std::vector<std::string> getOptionNames() const;
 
   /**
+   * Get the driver options, which provide access to options that can not be
+   * communicated properly via getOption() and getOptionInfo().
+   * @return a DriverOptions object.
+   */
+  DriverOptions getDriverOptions() const;
+
+  /**
    * Get the set of unsat ("failed") assumptions.
    * SMT-LIB:
    * \verbatim
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4089f4d1b..6501a1b0f 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -114,7 +114,7 @@ bool CommandExecutor::doCommand(Command* cmd)
   } else {
     if (d_solver->getOptions().base.verbosity > 2)
     {
-      *d_solver->getOptions().base.out << "Invoking: " << *cmd << std::endl;
+      d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -123,23 +123,14 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  printStatistics(*d_solver->getOptions().base.err);
-
+  printStatistics(d_solver->getDriverOptions().err());
   Command::resetSolver(d_solver.get());
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
-  bool status = true;
-  if (d_solver->getOptions().base.verbosity >= -1)
-  {
-    status = solverInvoke(
-        d_solver.get(), d_symman.get(), cmd, d_solver->getOptions().base.out);
-  }
-  else
-  {
-    status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
-  }
+  bool status = solverInvoke(
+      d_solver.get(), d_symman.get(), cmd, d_solver->getDriverOptions().out());
 
   api::Result res;
   const CheckSatCommand* cs = dynamic_cast<const CheckSatCommand*>(cmd);
@@ -210,16 +201,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 bool solverInvoke(api::Solver* solver,
                   SymbolManager* sm,
                   Command* cmd,
-                  std::ostream* out)
+                  std::ostream& out)
 {
-  if (out == NULL)
-  {
-    cmd->invoke(solver, sm);
-  }
-  else
-  {
-    cmd->invoke(solver, sm, *out);
-  }
+  cmd->invoke(solver, sm, out);
   // ignore the error if the command-verbosity is 0 for this command
   std::string commandName =
       std::string("command-verbosity:") + cmd->getCommandName();
@@ -231,18 +215,11 @@ bool solverInvoke(api::Solver* solver,
 }
 
 void CommandExecutor::flushOutputStreams() {
-  printStatistics(*d_solver->getOptions().base.err);
+  printStatistics(d_solver->getDriverOptions().err());
 
   // make sure out and err streams are flushed too
-
-  if (d_solver->getOptions().base.out != nullptr)
-  {
-    *d_solver->getOptions().base.out << std::flush;
-  }
-  if (d_solver->getOptions().base.err != nullptr)
-  {
-    *d_solver->getOptions().base.err << std::flush;
-  }
+  d_solver->getDriverOptions().out() << std::flush;
+  d_solver->getDriverOptions().err() << std::flush;
 }
 
 }  // namespace main
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index e8c2d25ac..d44986640 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -117,7 +117,7 @@ private:
 bool solverInvoke(api::Solver* solver,
                   SymbolManager* sm,
                   Command* cmd,
-                  std::ostream* out);
+                  std::ostream& out);
 
 }  // namespace main
 }  // namespace cvc5
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index f68545d00..005de6a34 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -80,21 +80,25 @@ TotalTimer::~TotalTimer()
     }  // namespace main
     }  // namespace cvc5
 
-void printUsage(const Options& opts, bool full) {
-  stringstream ss;
-  ss << "usage: " << progName << " [options] [input-file]"
-     << endl
-     << endl
-     << "Without an input file, or with `-', cvc5 reads from standard input."
-     << endl
-     << endl
-     << "cvc5 options:" << endl;
-  if(full) {
-    main::printUsage(ss.str(), *opts.base.out);
-  } else {
-    main::printShortUsage(ss.str(), *opts.base.out);
-  }
-}
+    void printUsage(const api::DriverOptions& dopts, bool full)
+    {
+      std::stringstream ss;
+      ss << "usage: " << progName << " [options] [input-file]" << std::endl
+         << std::endl
+         << "Without an input file, or with `-', cvc5 reads from standard "
+            "input."
+         << std::endl
+         << std::endl
+         << "cvc5 options:" << std::endl;
+      if (full)
+      {
+        main::printUsage(ss.str(), dopts.out());
+      }
+      else
+      {
+        main::printShortUsage(ss.str(), dopts.out());
+      }
+    }
 
 int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 {
@@ -107,6 +111,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 
   // Create the command executor to execute the parsed commands
   pExecutor = std::make_unique<CommandExecutor>(solver);
+  api::DriverOptions dopts = solver->getDriverOptions();
   Options* opts = &pExecutor->getOptions();
 
   // Parse the options
@@ -116,17 +121,17 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 
   if (opts->driver.help)
   {
-    printUsage(*opts, true);
+    printUsage(dopts, true);
     exit(1);
   }
   else if (opts->base.languageHelp)
   {
-    main::printLanguageHelp(*opts->base.out);
+    main::printLanguageHelp(dopts.out());
     exit(1);
   }
   else if (opts->driver.version)
   {
-    *opts->base.out << Configuration::about().c_str() << flush;
+    dopts.out() << Configuration::about().c_str() << flush;
     exit(0);
   }
 
@@ -134,7 +139,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
-  *opts->base.out << unitbuf;
+  dopts.out() << unitbuf;
 #endif /* CVC5_COMPETITION_MODE */
 
   // We only accept one input file
@@ -233,7 +238,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         try {
           cmd.reset(shell.readCommand());
         } catch(UnsafeInterruptException& e) {
-          *opts->base.out << CommandInterrupted();
+          dopts.out() << CommandInterrupted();
           break;
         }
         if (cmd == nullptr)
@@ -273,7 +278,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
       while (status)
       {
         if (interrupted) {
-          *opts->base.out << CommandInterrupted();
+          dopts.out() << CommandInterrupted();
           pExecutor->reset();
           opts = &pExecutor->getOptions();
           break;
@@ -309,10 +314,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     }
 
 #ifdef CVC5_COMPETITION_MODE
-    if (opts->base.out != nullptr)
-    {
-      *opts->base.out << std::flush;
-    }
+    dopts.out() << std::flush;
     // exit, don't return (don't want destructors to run)
     // _exit() from unistd.h doesn't run global destructors
     // or other on_exit/atexit stuff.
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8cb40cfdb..a47b8abb7 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -92,8 +92,8 @@ static set<string> s_declarations;
 
 InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     : d_solver(solver),
-      d_in(*solver->getOptions().base.in),
-      d_out(*solver->getOptions().base.out),
+      d_in(solver->getDriverOptions().in()),
+      d_out(solver->getDriverOptions().out()),
       d_quit(false)
 {
   ParserBuilder parserBuilder(solver, sm, true);
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 5fedc53da..d17bcaab1 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -59,7 +59,7 @@ int main(int argc, char* argv[])
   catch (cvc5::api::CVC5ApiOptionException& e)
   {
 #ifdef CVC5_COMPETITION_MODE
-    *solver->getOptions().base.out << "unknown" << endl;
+    solver->getDriverOptions().out() << "unknown" << std::endl;
 #endif
     cerr << "(error \"" << e.getMessage() << "\")" << endl
          << endl
@@ -68,7 +68,7 @@ int main(int argc, char* argv[])
   catch (OptionException& e)
   {
 #ifdef CVC5_COMPETITION_MODE
-    *solver->getOptions().base.out << "unknown" << endl;
+    solver->getDriverOptions().out() << "unknown" << std::endl;
 #endif
     cerr << "(error \"" << e.getMessage() << "\")" << endl
          << endl
@@ -77,20 +77,22 @@ int main(int argc, char* argv[])
   catch (Exception& e)
   {
 #ifdef CVC5_COMPETITION_MODE
-    *solver->getOptions().base.out << "unknown" << endl;
+    solver->getDriverOptions().out() << "unknown" << std::endl;
 #endif
     if (language::isLangSmt2(solver->getOptions().base.outputLanguage))
     {
-      *solver->getOptions().base.out << "(error \"" << e << "\")" << endl;
+      solver->getDriverOptions().out()
+          << "(error \"" << e << "\")" << std::endl;
     }
     else
     {
-      *solver->getOptions().base.err << "(error \"" << e << "\")" << endl;
+      solver->getDriverOptions().err()
+          << "(error \"" << e << "\")" << std::endl;
     }
     if (solver->getOptions().base.statistics && pExecutor != nullptr)
     {
       totalTime.reset();
-      pExecutor->printStatistics(*solver->getOptions().base.err);
+      pExecutor->printStatistics(solver->getDriverOptions().err());
     }
   }
   exit(1);