Move public wrapper functions out of options class (#6600)

This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.

5 files changed, 157 insertions, 95 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index c8e977f1f..5759ec856 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -26,6 +26,7 @@
 #include <vector>
 
 #include "main/main.h"
+#include "options/options_public.h"
 #include "smt/command.h"
 #include "smt/smt_engine.h"
 
@@ -64,7 +65,7 @@ CommandExecutor::~CommandExecutor()
 
 void CommandExecutor::printStatistics(std::ostream& out) const
 {
-  if (d_options.getStatistics())
+  if (options::getStatistics(d_options))
   {
     getSmtEngine()->printStatistics(out);
   }
@@ -72,7 +73,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const
 
 void CommandExecutor::printStatisticsSafe(int fd) const
 {
-  if (d_options.getStatistics())
+  if (options::getStatistics(d_options))
   {
     getSmtEngine()->printStatisticsSafe(fd);
   }
@@ -80,7 +81,8 @@ void CommandExecutor::printStatisticsSafe(int fd) const
 
 bool CommandExecutor::doCommand(Command* cmd)
 {
-  if( d_options.getParseOnly() ) {
+  if (options::getParseOnly(d_options))
+  {
     return true;
   }
 
@@ -98,8 +100,9 @@ bool CommandExecutor::doCommand(Command* cmd)
 
     return status;
   } else {
-    if(d_options.getVerbosity() > 2) {
-      *d_options.getOut() << "Invoking: " << *cmd << std::endl;
+    if (options::getVerbosity(d_options) > 2)
+    {
+      *options::getOut(d_options) << "Invoking: " << *cmd << std::endl;
     }
 
     return doCommandSingleton(cmd);
@@ -108,7 +111,7 @@ bool CommandExecutor::doCommand(Command* cmd)
 
 void CommandExecutor::reset()
 {
-  printStatistics(*d_options.getErr());
+  printStatistics(*options::getErr(d_options));
   /* 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
@@ -121,10 +124,13 @@ void CommandExecutor::reset()
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
-  if(d_options.getVerbosity() >= -1) {
-    status =
-        solverInvoke(d_solver.get(), d_symman.get(), cmd, d_options.getOut());
-  } else {
+  if (options::getVerbosity(d_options) >= -1)
+  {
+    status = solverInvoke(
+        d_solver.get(), d_symman.get(), cmd, options::getOut(d_options));
+  }
+  else
+  {
     status = solverInvoke(d_solver.get(), d_symman.get(), cmd, nullptr);
   }
 
@@ -144,8 +150,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_result = res = q->getResult();
   }
 
-  if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
-    getSmtEngine()->printStatisticsDiff(*d_options.getErr());
+  if ((cs != nullptr || q != nullptr) && options::getStatsEveryQuery(d_options))
+  {
+    getSmtEngine()->printStatisticsDiff(*options::getErr(d_options));
   }
 
   bool isResultUnsat = res.isUnsat() || res.isEntailed();
@@ -153,20 +160,21 @@ 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.getDumpModels()
+    if (options::getDumpModels(d_options)
         && (res.isSat()
             || (res.isSatUnknown()
                 && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.getDumpProofs() && isResultUnsat)
+    if (options::getDumpProofs(d_options) && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
 
-    if (d_options.getDumpInstantiations()
-        && ((d_options.getInstFormatMode() != options::InstFormatMode::SZS
+    if (options::getDumpInstantiations(d_options)
+        && ((options::getInstFormatMode(d_options)
+                 != options::InstFormatMode::SZS
              && (res.isSat()
                  || (res.isSatUnknown()
                      && res.getUnknownExplanation()
@@ -176,14 +184,15 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if (d_options.getDumpUnsatCores() && isResultUnsat)
+    if (options::getDumpUnsatCores(d_options) && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
     if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
-      if (d_options.getForceNoLimitCpuWhileDump()) {
+      if (options::getForceNoLimitCpuWhileDump(d_options))
+      {
         setNoLimitCPU();
       }
       for (const auto& getterCommand : getterCommands) {
@@ -222,11 +231,18 @@ bool solverInvoke(api::Solver* solver,
 }
 
 void CommandExecutor::flushOutputStreams() {
-  printStatistics(*(d_options.getErr()));
+  printStatistics(*(options::getErr(d_options)));
 
   // make sure out and err streams are flushed too
-  d_options.flushOut();
-  d_options.flushErr();
+
+  if (options::getOut(d_options) != nullptr)
+  {
+    *options::getOut(d_options) << std::flush;
+  }
+  if (options::getErr(d_options) != nullptr)
+  {
+    *options::getErr(d_options) << std::flush;
+  }
 }
 
 }  // namespace main
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index a26ee3b73..5785505d0 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -34,6 +34,7 @@
 #include "main/signal_handlers.h"
 #include "main/time_limit.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -78,16 +79,17 @@ TotalTimer::~TotalTimer()
 
 void printUsage(Options& opts, bool full) {
   stringstream ss;
-  ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl
+  ss << "usage: " << options::getBinaryName(opts) << " [options] [input-file]"
+     << endl
      << endl
      << "Without an input file, or with `-', cvc5 reads from standard input."
      << endl
      << endl
      << "cvc5 options:" << endl;
   if(full) {
-    Options::printUsage( ss.str(), *(opts.getOut()) );
+    Options::printUsage(ss.str(), *(options::getOut(opts)));
   } else {
-    Options::printShortUsage( ss.str(), *(opts.getOut()) );
+    Options::printShortUsage(ss.str(), *(options::getOut(opts)));
   }
 }
 
@@ -107,25 +109,30 @@ int runCvc5(int argc, char* argv[], Options& opts)
 
   auto limit = install_time_limit(opts);
 
-  string progNameStr = opts.getBinaryName();
+  string progNameStr = options::getBinaryName(opts);
   progName = &progNameStr;
 
-  if( opts.getHelp() ) {
+  if (options::getHelp(opts))
+  {
     printUsage(opts, true);
     exit(1);
-  } else if( opts.getLanguageHelp() ) {
-    Options::printLanguageHelp(*(opts.getOut()));
+  }
+  else if (options::getLanguageHelp(opts))
+  {
+    Options::printLanguageHelp(*(options::getOut(opts)));
     exit(1);
-  } else if( opts.getVersion() ) {
-    *(opts.getOut()) << Configuration::about().c_str() << flush;
+  }
+  else if (options::getVersion(opts))
+  {
+    *(options::getOut(opts)) << Configuration::about().c_str() << flush;
     exit(0);
   }
 
-  segvSpin = opts.getSegvSpin();
+  segvSpin = options::getSegvSpin(opts);
 
   // If in competition mode, set output stream option to flush immediately
 #ifdef CVC5_COMPETITION_MODE
-  *(opts.getOut()) << unitbuf;
+  *(options::getOut(opts)) << unitbuf;
 #endif /* CVC5_COMPETITION_MODE */
 
   // We only accept one input file
@@ -137,8 +144,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.wasSetByUserInteractive()) {
-    opts.setInteractive(inputFromStdin && isatty(fileno(stdin)));
+  if (!options::wasSetByUserInteractive(opts))
+  {
+    options::setInteractive(inputFromStdin && isatty(fileno(stdin)), opts);
   }
 
   // Auto-detect input language by filename extension
@@ -150,30 +158,33 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
   const char* filename = filenameStr.c_str();
 
-  if(opts.getInputLanguage() == language::input::LANG_AUTO) {
+  if (options::getInputLanguage(opts) == language::input::LANG_AUTO)
+  {
     if( inputFromStdin ) {
       // We can't do any fancy detection on stdin
-      opts.setInputLanguage(language::input::LANG_CVC);
+      options::setInputLanguage(language::input::LANG_CVC, opts);
     } else {
-      unsigned len = filenameStr.size();
+      size_t len = filenameStr.size();
       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6);
+        options::setInputLanguage(language::input::LANG_SMTLIB_V2_6, opts);
       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts.setInputLanguage(language::input::LANG_TPTP);
+        options::setInputLanguage(language::input::LANG_TPTP, opts);
       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts.setInputLanguage(language::input::LANG_CVC);
+        options::setInputLanguage(language::input::LANG_CVC, opts);
       } else if((len >= 3 && !strcmp(".sy", filename + len - 3))
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         // version 2 sygus is the default
-        opts.setInputLanguage(language::input::LANG_SYGUS_V2);
+        options::setInputLanguage(language::input::LANG_SYGUS_V2, opts);
       }
     }
   }
 
-  if(opts.getOutputLanguage() == language::output::LANG_AUTO) {
-    opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
+  if (options::getOutputLanguage(opts) == language::output::LANG_AUTO)
+  {
+    options::setOutputLanguage(
+        language::toOutputLanguage(options::getInputLanguage(opts)), opts);
   }
 
   // Determine which messages to show based on smtcomp_mode and verbosity
@@ -187,7 +198,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
   }
 
   // important even for muzzled builds (to get result output right)
-  (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage());
+  (*(options::getOut(opts)))
+      << language::SetLanguage(options::getOutputLanguage(opts));
 
   // Create the command executor to execute the parsed commands
   pExecutor = std::make_unique<CommandExecutor>(opts);
@@ -200,19 +212,23 @@ 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.getInteractive() && inputFromStdin) {
-      if(opts.getTearDownIncremental() > 0) {
+    if (options::getInteractive(opts) && inputFromStdin)
+    {
+      if (options::getTearDownIncremental(opts) > 0)
+      {
         throw Exception(
             "--tear-down-incremental doesn't work in interactive mode");
       }
-      if(!opts.wasSetByUserIncrementalSolving()) {
+      if (!options::wasSetByUserIncrementalSolving(opts))
+      {
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
       }
       InteractiveShell shell(pExecutor->getSolver(),
                              pExecutor->getSymbolManager());
-      if(opts.getInteractivePrompt()) {
+      if (options::getInteractivePrompt(opts))
+      {
         CVC5Message() << Configuration::getPackageName() << " "
                       << Configuration::getVersionString();
         if(Configuration::isGitBuild()) {
@@ -230,7 +246,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
         try {
           cmd.reset(shell.readCommand());
         } catch(UnsafeInterruptException& e) {
-          (*opts.getOut()) << CommandInterrupted();
+          (*options::getOut(opts)) << CommandInterrupted();
           break;
         }
         if (cmd == nullptr)
@@ -240,14 +256,18 @@ int runCvc5(int argc, char* argv[], Options& opts)
           break;
         }
       }
-    } else if( opts.getTearDownIncremental() > 0) {
-      if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
+    }
+    else if (options::getTearDownIncremental(opts) > 0)
+    {
+      if (!options::getIncrementalSolving(opts)
+          && options::getTearDownIncremental(opts) > 1)
+      {
         // For tear-down-incremental values greater than 1, need incremental
         // on too.
         cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
-        // if(opts.wasSetByUserIncrementalSolving()) {
+        // if(options::wasSetByUserIncrementalSolving(opts)) {
         //   throw OptionException(
         //     "--tear-down-incremental incompatible with --incremental");
         // }
@@ -262,13 +282,14 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
-        parser->setInput(
-            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+        parser->setInput(Input::newStreamInput(
+            options::getInputLanguage(opts), cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(
-            opts.getInputLanguage(), filename, opts.getMemoryMap()));
+        parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+                                             filename,
+                                             options::getMemoryMap(opts)));
       }
 
       vector< vector<Command*> > allCommands;
@@ -279,7 +300,7 @@ int runCvc5(int argc, char* argv[], Options& opts)
       while (status)
       {
         if (interrupted) {
-          (*opts.getOut()) << CommandInterrupted();
+          (*options::getOut(opts)) << CommandInterrupted();
           break;
         }
 
@@ -292,7 +313,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
         }
 
         if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) {
-          if(needReset >= opts.getTearDownIncremental()) {
+          if (needReset >= options::getTearDownIncremental(opts))
+          {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               if (interrupted) break;
@@ -320,7 +342,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         } else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) {
           allCommands.pop_back(); // fixme leaks cmds here
-          if (needReset >= opts.getTearDownIncremental()) {
+          if (needReset >= options::getTearDownIncremental(opts))
+          {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
@@ -335,9 +358,11 @@ int runCvc5(int argc, char* argv[], Options& opts)
               }
             }
             if (interrupted) continue;
-            (*opts.getOut()) << CommandSuccess();
+            (*options::getOut(opts)) << CommandSuccess();
             needReset = 0;
-          } else {
+          }
+          else
+          {
             status = pExecutor->doCommand(cmd);
             if(cmd->interrupted()) {
               interrupted = true;
@@ -346,7 +371,8 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         } else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr ||
                   dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) {
-          if(needReset >= opts.getTearDownIncremental()) {
+          if (needReset >= options::getTearDownIncremental(opts))
+          {
             pExecutor->reset();
             for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) {
               for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j)
@@ -362,7 +388,9 @@ int runCvc5(int argc, char* argv[], Options& opts)
               }
             }
             needReset = 0;
-          } else {
+          }
+          else
+          {
             ++needReset;
           }
           if (interrupted) {
@@ -406,8 +434,11 @@ int runCvc5(int argc, char* argv[], Options& opts)
           }
         }
       }
-    } else {
-      if(!opts.wasSetByUserIncrementalSolving()) {
+    }
+    else
+    {
+      if (!options::wasSetByUserIncrementalSolving(opts))
+      {
         cmd.reset(new SetOptionCommand("incremental", "false"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
@@ -418,20 +449,21 @@ int runCvc5(int argc, char* argv[], Options& opts)
                                   opts);
       std::unique_ptr<Parser> parser(parserBuilder.build());
       if( inputFromStdin ) {
-        parser->setInput(
-            Input::newStreamInput(opts.getInputLanguage(), cin, filename));
+        parser->setInput(Input::newStreamInput(
+            options::getInputLanguage(opts), cin, filename));
       }
       else
       {
-        parser->setInput(Input::newFileInput(
-            opts.getInputLanguage(), filename, opts.getMemoryMap()));
+        parser->setInput(Input::newFileInput(options::getInputLanguage(opts),
+                                             filename,
+                                             options::getMemoryMap(opts)));
       }
 
       bool interrupted = false;
       while (status)
       {
         if (interrupted) {
-          (*opts.getOut()) << CommandInterrupted();
+          (*options::getOut(opts)) << CommandInterrupted();
           pExecutor->reset();
           break;
         }
@@ -465,7 +497,10 @@ int runCvc5(int argc, char* argv[], Options& opts)
     }
 
 #ifdef CVC5_COMPETITION_MODE
-    opts.flushOut();
+    if (cvc5::options::getOut(options) != nullptr)
+    {
+      cvc5::options::getOut(options) << 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.
@@ -476,11 +511,13 @@ int runCvc5(int argc, char* argv[], Options& opts)
     pExecutor->flushOutputStreams();
 
 #ifdef CVC5_DEBUG
-    if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) {
+    if (options::getEarlyExit(opts) && options::wasSetByUserEarlyExit(opts))
+    {
       _exit(returnValue);
     }
 #else  /* CVC5_DEBUG */
-    if(opts.getEarlyExit()) {
+    if (options::getEarlyExit(opts))
+    {
       _exit(returnValue);
     }
 #endif /* CVC5_DEBUG */
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 8ca10799f..9a0539490 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -42,6 +42,7 @@
 #include "expr/symbol_manager.h"
 #include "options/language.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -87,15 +88,16 @@ static set<string> s_declarations;
 
 InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
     : d_options(solver->getOptions()),
-      d_in(*d_options.getIn()),
-      d_out(*d_options.getOutConst()),
+      d_in(*options::getIn(d_options)),
+      d_out(*options::getOut(d_options)),
       d_quit(false)
 {
   ParserBuilder parserBuilder(solver, sm, d_options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.build();
-  if(d_options.wasSetByUserForceLogicString()) {
-    LogicInfo tmp(d_options.getForceLogicString());
+  if (options::wasSetByUserForceLogicString(d_options))
+  {
+    LogicInfo tmp(options::getForceLogicString(d_options));
     d_parser->forceLogic(tmp.getLogicString());
   }
 
@@ -109,7 +111,8 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
 #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
-    OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
+    OutputLanguage lang =
+        toOutputLanguage(options::getInputLanguage(d_options));
     switch(lang) {
       case output::LANG_CVC:
         d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
@@ -195,7 +198,7 @@ restart:
   if (d_usingEditline)
   {
 #if HAVE_LIBEDITLINE
-    lineBuf = ::readline(d_options.getInteractivePrompt()
+    lineBuf = ::readline(options::getInteractivePrompt(d_options)
                              ? (line == "" ? "cvc5> " : "... > ")
                              : "");
     if(lineBuf != NULL && lineBuf[0] != '\0') {
@@ -207,7 +210,8 @@ restart:
   }
   else
   {
-    if(d_options.getInteractivePrompt()) {
+    if (options::getInteractivePrompt(d_options))
+    {
       if(line == "") {
         d_out << "cvc5> " << flush;
       } else {
@@ -280,7 +284,8 @@ restart:
       if (d_usingEditline)
       {
 #if HAVE_LIBEDITLINE
-        lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
+        lineBuf = ::readline(options::getInteractivePrompt(d_options) ? "... > "
+                                                                      : "");
         if(lineBuf != NULL && lineBuf[0] != '\0') {
           ::add_history(lineBuf);
         }
@@ -290,7 +295,8 @@ restart:
       }
       else
       {
-        if(d_options.getInteractivePrompt()) {
+        if (options::getInteractivePrompt(d_options))
+        {
           d_out << "... > " << flush;
         }
 
@@ -306,8 +312,8 @@ restart:
     }
   }
 
-  d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
-                                           input, INPUT_FILENAME));
+  d_parser->setInput(Input::newStringInput(
+      options::getInputLanguage(d_options), input, INPUT_FILENAME));
 
   /* There may be more than one command in the input. Build up a
      sequence. */
@@ -358,7 +364,7 @@ restart:
   }
   catch (ParserException& pe)
   {
-    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+    if (language::isOutputLang_smt2(options::getOutputLanguage(d_options)))
     {
       d_out << "(error \"" << pe << "\")" << endl;
     }
diff --git a/src/main/main.cpp b/src/main/main.cpp
index b96598b0b..2b25e6c93 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -14,12 +14,13 @@
  */
 #include "main/main.h"
 
+#include <stdio.h>
+#include <unistd.h>
+
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
 #include <iostream>
-#include <stdio.h>
-#include <unistd.h>
 
 #include "base/configuration.h"
 #include "base/output.h"
@@ -28,6 +29,7 @@
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
@@ -51,25 +53,25 @@ int main(int argc, char* argv[]) {
     return runCvc5(argc, argv, opts);
   } catch(OptionException& e) {
 #ifdef CVC5_COMPETITION_MODE
-    *opts.getOut() << "unknown" << endl;
+    *options::getOut(opts) << "unknown" << endl;
 #endif
     cerr << "(error \"" << e << "\")" << endl
          << endl
          << "Please use --help to get help on command-line options." << endl;
   } catch(Exception& e) {
 #ifdef CVC5_COMPETITION_MODE
-    *opts.getOut() << "unknown" << endl;
+    *options::getOut(opts) << "unknown" << endl;
 #endif
-    if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+    if (language::isOutputLang_smt2(options::getOutputLanguage(opts)))
     {
-      *opts.getOut() << "(error \"" << e << "\")" << endl;
+      *options::getOut(opts) << "(error \"" << e << "\")" << endl;
     } else {
-      *opts.getErr() << "(error \"" << e << "\")" << endl;
+      *options::getErr(opts) << "(error \"" << e << "\")" << endl;
     }
-    if (opts.getStatistics() && pExecutor != nullptr)
+    if (options::getStatistics(opts) && pExecutor != nullptr)
     {
       totalTime.reset();
-      pExecutor->printStatistics(*opts.getErr());
+      pExecutor->printStatistics(*options::getErr(opts));
     }
   }
   exit(1);
diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp
index 0f0a824f6..c0fc6846a 100644
--- a/src/main/time_limit.cpp
+++ b/src/main/time_limit.cpp
@@ -56,6 +56,7 @@
 #include <cstring>
 
 #include "base/exception.h"
+#include "options/options_public.h"
 #include "signal_handlers.h"
 
 namespace cvc5 {
@@ -79,7 +80,7 @@ TimeLimit::~TimeLimit()
 
 TimeLimit install_time_limit(const Options& opts)
 {
-  unsigned long ms = opts.getCumulativeTimeLimit();
+  unsigned long ms = options::getCumulativeTimeLimit(opts);
   // Skip if no time limit shall be set.
   if (ms == 0) {
     return TimeLimit();