No longer use direct access to options in driver (#7094)

This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 6171c147b8d65bcdbd560a95cde65fe802b7d75b..d03b8975e39501ffab13169e39fcacbdee42bf1e 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7906,12 +7906,6 @@ std::vector<Term> Solver::getSynthSolutions(
  */
 SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
 
-/*
- * !!! This is only temporarily available until the parser is fully migrated to
- * the new API. !!!
- */
-Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
-
 Statistics Solver::getStatistics() const
 {
   return Statistics(d_smtEngine->getStatisticsRegistry());

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 5abcc578e3e85cd5f30970fb62f0cd6ea45ffb85..11b138a50d21ede03f596d5d04436ff868ed9e67 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4333,10 +4333,6 @@ class CVC5_EXPORT Solver
   // to the new API. !!!
   SmtEngine* getSmtEngine(void) const;
 
-  // !!! This is only temporarily available until options are refactored at
-  // the driver level. !!!
-  Options& getOptions(void);
-
   /**
    * Returns a snapshot of the current state of the statistic values of this
    * solver. The returned object is completely decoupled from the solver and

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index b337f819a4726b0ce133d6ae3689622b3ce2a00a..da8a5625418131fc3ae8efe5e03c8bdefcf9f1d7 100644 (file)
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -19,6 +19,7 @@
 #include <cstdio>
 #include <cstdlib>
 #include <cstring>
+#include <ostream>
 #include <sstream>
 #include <string>
 
@@ -35,6 +36,8 @@ std::string Exception::toString() const
   return ss.str();
 }
 
+void Exception::toStream(std::ostream& os) const { os << d_msg; }
+
 thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr;
 
 LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {}

diff --git a/src/base/exception.h b/src/base/exception.h
index 0f053e4152252a5adb6610e176637b50e10e906a..e37b69ec8fe92853d3f2b0805c939975f2aac195 100644 (file)
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -66,7 +66,7 @@ class CVC5_EXPORT Exception : public std::exception
    * a derived class, it's recommended that this method print the
    * type of exception before the actual message.
    */
-  virtual void toStream(std::ostream& os) const { os << d_msg; }
+  virtual void toStream(std::ostream& os) const;
 
 }; /* class Exception */
 

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 6501a1b0f56a1f4475c6c827df9bf5d3eb8370f9..98e93ca5a14bbe91b4e875e84caa1334e751e03d 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -26,8 +26,6 @@
 #include <vector>
 
 #include "main/main.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 
@@ -60,22 +58,18 @@ CommandExecutor::~CommandExecutor()
 {
 }
 
-Options& CommandExecutor::getOptions()
-{
-  return d_solver->d_smtEngine->getOptions();
-}
 void CommandExecutor::storeOptionsAsOriginal()
 {
-  d_solver->d_originalOptions->copyValues(getOptions());
+  d_solver->d_originalOptions->copyValues(d_solver->d_smtEngine->getOptions());
 }
 
 void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  const auto& baseopts = d_solver->getOptions().base;
-  if (baseopts.statistics)
+  if (d_solver->getOptionInfo("stats").boolValue())
   {
     const auto& stats = d_solver->getStatistics();
-    auto it = stats.begin(baseopts.statisticsExpert, baseopts.statisticsAll);
+    auto it = stats.begin(d_solver->getOptionInfo("stats-expert").boolValue(),
+                          d_solver->getOptionInfo("stats-all").boolValue());
     for (; it != stats.end(); ++it)
     {
       out << it->first << " = " << it->second << std::endl;
@@ -85,7 +79,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const
 
 void CommandExecutor::printStatisticsSafe(int fd) const
 {
-  if (d_solver->getOptions().base.statistics)
+  if (d_solver->getOptionInfo("stats").boolValue())
   {
     d_solver->printStatisticsSafe(fd);
   }
@@ -93,7 +87,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if (d_solver->getOptions().base.parseOnly)
+  if (d_solver->getOptionInfo("parse-only").boolValue())
   {
     return true;
   }
@@ -112,7 +106,7 @@ bool CommandExecutor::doCommand(Command* cmd)
 
     return status;
   } else {
-    if (d_solver->getOptions().base.verbosity > 2)
+    if (d_solver->getOptionInfo("verbosity").intValue() > 2)
     {
       d_solver->getDriverOptions().out() << "Invoking: " << *cmd << std::endl;
     }
@@ -154,27 +148,27 @@ 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_solver->getOptions().driver.dumpModels
+    if (d_solver->getOptionInfo("dump-models").boolValue()
         && (isResultSat
             || (res.isSatUnknown()
                 && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_solver->getOptions().driver.dumpProofs && isResultUnsat)
+    if (d_solver->getOptionInfo("dump-proofs").boolValue() && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
 
-    if ((d_solver->getOptions().driver.dumpInstantiations
-         || d_solver->getOptions().driver.dumpInstantiationsDebug)
+    if ((d_solver->getOptionInfo("dump-instantiations").boolValue()
+         || d_solver->getOptionInfo("dump-instantiations-debug").boolValue())
         && GetInstantiationsCommand::isEnabled(d_solver.get(), res))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if ((d_solver->getOptions().driver.dumpUnsatCores
-         || d_solver->getOptions().driver.dumpUnsatCoresFull)
+    if ((d_solver->getOptionInfo("dump-unsat-cores").boolValue()
+         || d_solver->getOptionInfo("dump-unsat-cores-full").boolValue())
         && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
@@ -182,7 +176,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 
     if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
-      if (d_solver->getOptions().driver.forceNoLimitCpuWhileDump)
+      if (d_solver->getOptionInfo("force-no-limit-cpu-while-dump").boolValue())
       {
         setNoLimitCPU();
       }

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index d4498664015d93a251533efeb6de331fd16169cd..0a7a56e5bb08d63d850d2f11bfcea76c7726f2ec 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -83,8 +83,6 @@ 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();
 

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 2c64135037256a8344c738fc5894d1eab6ed0ab8..25726f45826864de5d98f5f8094f29264290845f 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -34,13 +34,6 @@
 #include "main/options.h"
 #include "main/signal_handlers.h"
 #include "main/time_limit.h"
-#include "options/base_options.h"
-#include "options/main_options.h"
-#include "options/option_exception.h"
-#include "options/options.h"
-#include "options/options_public.h"
-#include "options/parser_options.h"
-#include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "smt/command.h"
@@ -112,30 +105,29 @@ 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
   std::vector<string> filenames = main::parse(*solver, argc, argv, progName);
 
-  auto limit = install_time_limit(*opts);
+  auto limit = install_time_limit(solver->getOptionInfo("tlimit").uintValue());
 
-  if (opts->driver.help)
+  if (solver->getOptionInfo("help").boolValue())
   {
     printUsage(dopts, true);
     exit(1);
   }
-  else if (opts->base.languageHelp)
+  else if (solver->getOptionInfo("language-help").boolValue())
   {
     main::printLanguageHelp(dopts.out());
     exit(1);
   }
-  else if (opts->driver.version)
+  else if (solver->getOptionInfo("version").boolValue())
   {
     dopts.out() << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  segvSpin = opts->driver.segvSpin;
+  segvSpin = solver->getOptionInfo("segv-spin").boolValue();
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
@@ -151,9 +143,9 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
   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 (!solver->getOptionInfo("interactive").setByUser)
   {
-    opts->driver.interactive = inputFromStdin && isatty(fileno(stdin));
+    solver->setOption("interactive", (inputFromStdin && isatty(fileno(stdin))) ? "true" : "false");
   }
 
   // Auto-detect input language by filename extension
@@ -210,9 +202,9 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     // Parse and execute commands until we are done
     std::unique_ptr<Command> cmd;
     bool status = true;
-    if (opts->driver.interactive && inputFromStdin)
+    if (solver->getOptionInfo("interactive").boolValue() && inputFromStdin)
     {
-      if (!opts->base.incrementalSolvingWasSetByUser)
+      if (!solver->getOptionInfo("incremental").setByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
@@ -244,7 +236,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         if (cmd == nullptr)
           break;
         status = pExecutor->doCommand(cmd) && status;
-        opts = &pExecutor->getOptions();
         if (cmd->interrupted()) {
           break;
         }
@@ -252,7 +243,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     }
     else
     {
-      if (!opts->base.incrementalSolvingWasSetByUser)
+      if (!solver->getOptionInfo("incremental").setByUser)
       {
         cmd.reset(new SetOptionCommand("incremental", "false"));
         cmd->setMuted(true);
@@ -271,7 +262,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         parser->setInput(
             Input::newFileInput(solver->getOption("input-language"),
                                 filename,
-                                solver->getOption("mmap") == "true"));
+                                solver->getOptionInfo("mmap").boolValue()));
       }
 
       bool interrupted = false;
@@ -280,7 +271,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         if (interrupted) {
           dopts.out() << CommandInterrupted();
           pExecutor->reset();
-          opts = &pExecutor->getOptions();
           break;
         }
         try {
@@ -292,7 +282,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
         }
 
         status = pExecutor->doCommand(cmd);
-        opts = &pExecutor->getOptions();
         if (cmd->interrupted() && status == 0) {
           interrupted = true;
           break;
@@ -325,12 +314,15 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
-    if (opts->driver.earlyExit && opts->driver.earlyExitWasSetByUser)
     {
-      _exit(returnValue);
+      auto info = solver->getOptionInfo("early-exit");
+      if (info.boolValue() && info.setByUser)
+      {
+        _exit(returnValue);
+      }
     }
 #else  /* CVC5_DEBUG */
-    if (opts->driver.earlyExit)
+    if (solver->getOptionInfo("early-exit").boolValue())
     {
       _exit(returnValue);
     }

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index a47b8abb734c132282db01f70bd388d4c46ab490..ea408012a627a5b4066ab81e212373d5de0602f4 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -42,11 +42,6 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "expr/symbol_manager.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/main_options.h"
-#include "options/options.h"
-#include "options/parser_options.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -99,7 +94,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
   ParserBuilder parserBuilder(solver, sm, true);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.build();
-  if (d_solver->getOptions().parser.forceLogicStringWasSetByUser)
+  if (d_solver->getOptionInfo("force-logic").setByUser)
   {
     LogicInfo tmp(d_solver->getOption("force-logic"));
     d_parser->forceLogic(tmp.getLogicString());

diff --git a/src/main/main.cpp b/src/main/main.cpp
index d17bcaab1ff79260ad78ab2e821fbabc44379f0c..18be1b406f7b4b0b8ec6341357cf24b5e230e5d4 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -79,7 +79,7 @@ int main(int argc, char* argv[])
 #ifdef CVC5_COMPETITION_MODE
     solver->getDriverOptions().out() << "unknown" << std::endl;
 #endif
-    if (language::isLangSmt2(solver->getOptions().base.outputLanguage))
+    if (solver->getOption("output-language") == "LANG_SMTLIB_V2_6")
     {
       solver->getDriverOptions().out()
           << "(error \"" << e << "\")" << std::endl;
@@ -89,7 +89,8 @@ int main(int argc, char* argv[])
       solver->getDriverOptions().err()
           << "(error \"" << e << "\")" << std::endl;
     }
-    if (solver->getOptions().base.statistics && pExecutor != nullptr)
+    if (solver->getOptionInfo("stats").boolValue()
+        && main::pExecutor != nullptr)
     {
       totalTime.reset();
       pExecutor->printStatistics(solver->getDriverOptions().err());

diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index 28a0087bb996f4ff078b2d30b34ef5577e527aeb..698d08c6d2cbf81f116482a9bcd41b1deb91aa4a 100644 (file)
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -56,7 +56,6 @@
 #include <cstring>
 
 #include "base/exception.h"
-#include "options/base_options.h"
 #include "signal_handlers.h"
 
 namespace cvc5 {
@@ -78,9 +77,8 @@ TimeLimit::~TimeLimit()
 }
 #endif
 
-TimeLimit install_time_limit(const Options& opts)
+TimeLimit install_time_limit(uint64_t ms)
 {
-  uint64_t ms = opts.base.cumulativeMillisecondLimit;
   // Skip if no time limit shall be set.
   if (ms == 0) {
     return TimeLimit();

diff --git a/src/main/time_limit.h b/src/main/time_limit.h
index c84e22b4bd06d590cf26dc4ea290e332319be1db..de0a28a266d4bdd5bc1071865cf2517c1bc7275b 100644 (file)
--- a/src/main/time_limit.h
+++ b/src/main/time_limit.h
@@ -43,7 +43,7 @@ struct TimeLimit
  * thread needs to communicate back to the timer thread when it wants to
  * terminate, which is done via the TimeLimit object.
  */
-TimeLimit install_time_limit(const Options& opts);
+TimeLimit install_time_limit(uint64_t ms);
 
 }  // namespace main
 }  // namespace cvc5

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 439a1beba8043e1d8d75e529352dbd392b6b0770..adc2d845624307564ca09ea33636a3d859c5fb7c 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -55,6 +55,7 @@ public = true
 
 [[option]]
   name       = "languageHelp"
+  long       = "language-help"
   category   = "undocumented"
   type       = "bool"
 

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index bd0f56b2d6e456c5da14b1242a4756781d71cd09..39b38be30563ea73dd22c8be923b6257a009ec6b 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -26,8 +26,6 @@
 #include "base/check.h"
 #include "base/output.h"
 #include "expr/kind.h"
-#include "options/base_options.h"
-#include "options/options.h"
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
@@ -899,7 +897,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s)
 
 api::Term Parser::mkStringConstant(const std::string& s)
 {
-  if (language::isLangSmt2(d_solver->getOptions().base.inputLanguage))
+  if (d_solver->getOption("input-language") == "LANG_SMTLIB_V2_6")
   {
     return d_solver->mkString(s, true);
   }

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 6658364021d6851b21ea7ce3c2ab2b9b1cc6f634..b1bb9a4328944ca2c8a4bb00d29167506af789e0 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -21,9 +21,6 @@
 #include "api/cpp/cvc5.h"
 #include "base/check.h"
 #include "cvc/cvc.h"
-#include "options/base_options.h"
-#include "options/options.h"
-#include "options/parser_options.h"
 #include "parser/antlr_input.h"
 #include "parser/input.h"
 #include "parser/parser.h"
@@ -41,7 +38,7 @@ ParserBuilder::ParserBuilder(api::Solver* solver,
   init(solver, sm);
   if (useOptions)
   {
-    withOptions(solver->getOptions());
+    withOptions();
   }
 }
 
@@ -109,17 +106,18 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withOptions(const Options& opts)
+ParserBuilder& ParserBuilder::withOptions()
 {
   ParserBuilder& retval = *this;
   retval = retval.withInputLanguage(d_solver->getOption("input-language"))
-               .withChecks(opts.parser.semanticChecks)
-               .withStrictMode(opts.parser.strictParsing)
-               .withParseOnly(opts.base.parseOnly)
-               .withIncludeFile(opts.parser.filesystemAccess);
-  if (opts.parser.forceLogicStringWasSetByUser)
+               .withChecks(d_solver->getOptionInfo("semantic-checks").boolValue())
+               .withStrictMode(d_solver->getOptionInfo("strict-parsing").boolValue())
+               .withParseOnly(d_solver->getOptionInfo("parse-only").boolValue())
+               .withIncludeFile(d_solver->getOptionInfo("filesystem-access").boolValue());
+  auto info = d_solver->getOptionInfo("force-logic");
+  if (info.setByUser)
   {
-    LogicInfo tmp(opts.parser.forceLogicString);
+    LogicInfo tmp(info.stringValue());
     retval = retval.withForcedLogic(tmp.getLogicString());
   }
   return retval;

diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 23a9daae2f00583359afe196d042b219cc1cbda1..d148a538d82606042ddab010b381817ac48c6d27 100644 (file)
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -104,8 +104,8 @@ class CVC5_EXPORT ParserBuilder
    */
   ParserBuilder& withParseOnly(bool flag = true);
 
-  /** Derive settings from the given options. */
-  ParserBuilder& withOptions(const Options& opts);
+  /** Derive settings from the solver's options. */
+  ParserBuilder& withOptions();
 
   /**
    * Should the parser use strict mode?

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 1a0a3d52a28ce5feb2f55894df47d2282d82c89d..2fd4a55967e3fa53cedd90783d0531af8d61f4a4 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -17,9 +17,6 @@
 #include <algorithm>
 
 #include "base/check.h"
-#include "options/base_options.h"
-#include "options/options.h"
-#include "options/options_public.h"
 #include "parser/antlr_input.h"
 #include "parser/parser.h"
 #include "parser/smt2/smt2_input.h"
@@ -843,11 +840,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
   return d_solver->mkAbstractValue(name.substr(1));
 }
 
-Language Smt2::getLanguage() const
-{
-  return d_solver->getOptions().base.inputLanguage;
-}
-
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
 {
   Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index c3f93708d9f3031dd2c08106c798c366c5b0658c..97eb95c003b30f33f73695d2585be3b02f51fdd4 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -413,8 +413,6 @@ class Smt2 : public Parser
 
   void addSepOperators();
 
-  Language getLanguage() const;
-
   /**
    * Utility function to create a conjunction of expressions.
    *