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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1eaae87617c217783361283c6f8be6c1b7574d87..e245dc4153f0b6ee8e235e3650c8eb3a1c87f3f3 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4748,6 +4748,25 @@ const static std::unordered_map<cvc5::RoundingMode,
          ROUND_NEAREST_TIES_TO_AWAY},
     };
 
+/* -------------------------------------------------------------------------- */
+/* 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 9f805fa65440c0a65289b035ef56dd7937b28720..d86fed14aba8ed05c372ace8833838ee243247ee 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2592,6 +2592,33 @@ struct CVC5_EXPORT hash<cvc5::api::RoundingMode>
 }  // namespace std
 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;
@@ -3747,6 +3775,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:

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 4089f4d1b78a7bb076af81fe3d74a380441852ea..6501a1b0f56a1f4475c6c827df9bf5d3eb8370f9 100644 (file)
--- 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 e8c2d25ac7b60d1bc1a4a68c70ed2153aa3ec966..d4498664015d93a251533efeb6de331fd16169cd 100644 (file)
--- 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 f68545d0026c9721d99f0257a22e0e8559476ba8..005de6a34044e80e6bf6b6744b36e12094800ddf 100644 (file)
--- 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 8cb40cfdb6df960c5c7036980ee0f52cf490e484..a47b8abb734c132282db01f70bd388d4c46ab490 100644 (file)
--- 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 5fedc53da376b12b069b199bc88a955584717402..d17bcaab1ff79260ad78ab2e821fbabc44379f0c 100644 (file)
--- 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);