From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 2 Jun 2021 12:11:05 +0000 (+0200)
Subject: Move public wrapper functions out of options class (#6600)
X-Git-Tag: cvc5-1.0.0~1660
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d359817283f196034d8e36d0b9c1f10fb16d644;p=cvc5.git

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.
---

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();
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt
index 2107865c0..978c32888 100644
--- a/src/options/CMakeLists.txt
+++ b/src/options/CMakeLists.txt
@@ -30,7 +30,8 @@ libcvc5_add_sources(
   options_handler.cpp
   options_handler.h
   options_listener.h
-  options_public_functions.cpp
+  options_public.cpp
+  options_public.h
   printer_modes.cpp
   printer_modes.h
   set_language.cpp
diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
new file mode 100644
index 000000000..778056553
--- /dev/null
+++ b/src/options/options_public.cpp
@@ -0,0 +1,155 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Tim King, Gereon Kremer, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Definitions of public facing interface functions for Options.
+ *
+ * These are all one line wrappers for accessing the internal option data.
+ */
+
+#include "options_public.h"
+
+#include <fstream>
+#include <ostream>
+#include <string>
+#include <vector>
+
+#include "base/listener.h"
+#include "base/modal_exception.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/option_exception.h"
+#include "options/options.h"
+#include "options/parser_options.h"
+#include "options/printer_modes.h"
+#include "options/printer_options.h"
+#include "options/resource_manager_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+
+namespace cvc5::options {
+
+InputLanguage getInputLanguage(const Options& opts)
+{
+  return opts.base.inputLanguage;
+}
+InstFormatMode getInstFormatMode(const Options& opts)
+{
+  return opts.printer.instFormatMode;
+}
+OutputLanguage getOutputLanguage(const Options& opts)
+{
+  return opts.base.outputLanguage;
+}
+bool getUfHo(const Options& opts) { return opts.uf.ufHo; }
+bool getDumpInstantiations(const Options& opts)
+{
+  return opts.smt.dumpInstantiations;
+}
+bool getDumpModels(const Options& opts) { return opts.smt.dumpModels; }
+bool getDumpProofs(const Options& opts) { return opts.smt.dumpProofs; }
+bool getDumpUnsatCores(const Options& opts)
+{
+  return opts.smt.dumpUnsatCores || opts.smt.dumpUnsatCoresFull;
+}
+bool getEarlyExit(const Options& opts) { return opts.driver.earlyExit; }
+bool getFilesystemAccess(const Options& opts)
+{
+  return opts.parser.filesystemAccess;
+}
+bool getForceNoLimitCpuWhileDump(const Options& opts)
+{
+  return opts.smt.forceNoLimitCpuWhileDump;
+}
+bool getHelp(const Options& opts) { return opts.driver.help; }
+bool getIncrementalSolving(const Options& opts)
+{
+  return opts.smt.incrementalSolving;
+}
+bool getInteractive(const Options& opts) { return opts.driver.interactive; }
+bool getInteractivePrompt(const Options& opts)
+{
+  return opts.driver.interactivePrompt;
+}
+bool getLanguageHelp(const Options& opts) { return opts.base.languageHelp; }
+bool getMemoryMap(const Options& opts) { return opts.parser.memoryMap; }
+bool getParseOnly(const Options& opts) { return opts.base.parseOnly; }
+bool getProduceModels(const Options& opts) { return opts.smt.produceModels; }
+bool getSegvSpin(const Options& opts) { return opts.driver.segvSpin; }
+bool getSemanticChecks(const Options& opts)
+{
+  return opts.parser.semanticChecks;
+}
+bool getStatistics(const Options& opts) { return opts.base.statistics; }
+bool getStatsEveryQuery(const Options& opts)
+{
+  return opts.base.statisticsEveryQuery;
+}
+bool getStrictParsing(const Options& opts)
+{
+  return opts.parser.strictParsing;
+}
+int32_t getTearDownIncremental(const Options& opts)
+{
+  return opts.driver.tearDownIncremental;
+}
+uint64_t getCumulativeTimeLimit(const Options& opts)
+{
+  return opts.resman.cumulativeMillisecondLimit;
+}
+bool getVersion(const Options& opts) { return opts.driver.version; }
+const std::string& getForceLogicString(const Options& opts)
+{
+  return opts.parser.forceLogicString;
+}
+int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; }
+
+std::istream* getIn(const Options& opts) { return opts.base.in; }
+std::ostream* getErr(const Options& opts) { return opts.base.err; }
+std::ostream* getOut(const Options& opts) { return opts.base.out; }
+const std::string& getBinaryName(const Options& opts)
+{
+  return opts.base.binary_name;
+}
+
+void setInputLanguage(InputLanguage val, Options& opts)
+{
+  opts.base.inputLanguage = val;
+}
+void setInteractive(bool val, Options& opts)
+{
+  opts.driver.interactive = val;
+}
+void setOut(std::ostream* val, Options& opts) { opts.base.out = val; }
+void setOutputLanguage(OutputLanguage val, Options& opts)
+{
+  opts.base.outputLanguage = val;
+}
+
+bool wasSetByUserEarlyExit(const Options& opts)
+{
+  return opts.driver.earlyExit__setByUser;
+}
+bool wasSetByUserForceLogicString(const Options& opts)
+{
+  return opts.parser.forceLogicString__setByUser;
+}
+bool wasSetByUserIncrementalSolving(const Options& opts)
+{
+  return opts.smt.incrementalSolving__setByUser;
+}
+bool wasSetByUserInteractive(const Options& opts)
+{
+  return opts.driver.interactive__setByUser;
+}
+
+}  // namespace cvc5::options
diff --git a/src/options/options_public.h b/src/options/options_public.h
new file mode 100644
index 000000000..a6d93cae7
--- /dev/null
+++ b/src/options/options_public.h
@@ -0,0 +1,79 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Public facing functions for options that need to be accessed from the
+ * outside.
+ *
+ * These are all one line wrappers for accessing the internal option data so
+ * that external code (including parser/ and main/) does not need to include
+ * the option modules (*_options.h).
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__OPTIONS__OPTIONS_PUBLIC_H
+#define CVC5__OPTIONS__OPTIONS_PUBLIC_H
+
+#include "options/language.h"
+#include "options/options.h"
+#include "options/printer_modes.h"
+
+namespace cvc5::options {
+
+InputLanguage getInputLanguage(const Options& opts) CVC5_EXPORT;
+InstFormatMode getInstFormatMode(const Options& opts) CVC5_EXPORT;
+OutputLanguage getOutputLanguage(const Options& opts) CVC5_EXPORT;
+bool getUfHo(const Options& opts) CVC5_EXPORT;
+bool getDumpInstantiations(const Options& opts) CVC5_EXPORT;
+bool getDumpModels(const Options& opts) CVC5_EXPORT;
+bool getDumpProofs(const Options& opts) CVC5_EXPORT;
+bool getDumpUnsatCores(const Options& opts) CVC5_EXPORT;
+bool getEarlyExit(const Options& opts) CVC5_EXPORT;
+bool getFilesystemAccess(const Options& opts) CVC5_EXPORT;
+bool getForceNoLimitCpuWhileDump(const Options& opts) CVC5_EXPORT;
+bool getHelp(const Options& opts) CVC5_EXPORT;
+bool getIncrementalSolving(const Options& opts) CVC5_EXPORT;
+bool getInteractive(const Options& opts) CVC5_EXPORT;
+bool getInteractivePrompt(const Options& opts) CVC5_EXPORT;
+bool getLanguageHelp(const Options& opts) CVC5_EXPORT;
+bool getMemoryMap(const Options& opts) CVC5_EXPORT;
+bool getParseOnly(const Options& opts) CVC5_EXPORT;
+bool getProduceModels(const Options& opts) CVC5_EXPORT;
+bool getSegvSpin(const Options& opts) CVC5_EXPORT;
+bool getSemanticChecks(const Options& opts) CVC5_EXPORT;
+bool getStatistics(const Options& opts) CVC5_EXPORT;
+bool getStatsEveryQuery(const Options& opts) CVC5_EXPORT;
+bool getStrictParsing(const Options& opts) CVC5_EXPORT;
+int32_t getTearDownIncremental(const Options& opts) CVC5_EXPORT;
+uint64_t getCumulativeTimeLimit(const Options& opts) CVC5_EXPORT;
+bool getVersion(const Options& opts) CVC5_EXPORT;
+const std::string& getForceLogicString(const Options& opts) CVC5_EXPORT;
+int32_t getVerbosity(const Options& opts) CVC5_EXPORT;
+
+std::istream* getIn(const Options& opts) CVC5_EXPORT;
+std::ostream* getErr(const Options& opts) CVC5_EXPORT;
+std::ostream* getOut(const Options& opts) CVC5_EXPORT;
+const std::string& getBinaryName(const Options& opts) CVC5_EXPORT;
+
+void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT;
+void setInteractive(bool val, Options& opts) CVC5_EXPORT;
+void setOut(std::ostream* val, Options& opts) CVC5_EXPORT;
+void setOutputLanguage(OutputLanguage val, Options& opts) CVC5_EXPORT;
+
+bool wasSetByUserEarlyExit(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserForceLogicString(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserIncrementalSolving(const Options& opts) CVC5_EXPORT;
+bool wasSetByUserInteractive(const Options& opts) CVC5_EXPORT;
+
+}  // namespace cvc5::options
+
+#endif
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
deleted file mode 100644
index 2789b2d68..000000000
--- a/src/options/options_public_functions.cpp
+++ /dev/null
@@ -1,234 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Tim King, Gereon Kremer, Andrew Reynolds
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * Definitions of public facing interface functions for Options.
- *
- * These are all 1 line wrappers for Options::get<T>, Options::set<T>, and
- * Options::wasSetByUser<T> for different option types T.
- */
-
-#include <fstream>
-#include <ostream>
-#include <string>
-#include <vector>
-
-#include "base/listener.h"
-#include "base/modal_exception.h"
-#include "options/options.h"
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/main_options.h"
-#include "options/option_exception.h"
-#include "options/parser_options.h"
-#include "options/printer_modes.h"
-#include "options/printer_options.h"
-#include "options/quantifiers_options.h"
-#include "options/resource_manager_options.h"
-#include "options/smt_options.h"
-#include "options/uf_options.h"
-
-namespace cvc5 {
-
-// Get accessor functions.
-InputLanguage Options::getInputLanguage() const {
-  return (*this)[options::inputLanguage];
-}
-
-options::InstFormatMode Options::getInstFormatMode() const
-{
-  return (*this)[options::instFormatMode];
-}
-
-OutputLanguage Options::getOutputLanguage() const {
-  return (*this)[options::outputLanguage];
-}
-
-bool Options::getUfHo() const { return (*this)[options::ufHo]; }
-
-bool Options::getDumpInstantiations() const{
-  return (*this)[options::dumpInstantiations];
-}
-
-bool Options::getDumpModels() const{
-  return (*this)[options::dumpModels];
-}
-
-bool Options::getDumpProofs() const{
-  return (*this)[options::dumpProofs];
-}
-
-bool Options::getDumpUnsatCores() const{
-  // dump unsat cores full enables dumpUnsatCores
-  return (*this)[options::dumpUnsatCores]
-         || (*this)[options::dumpUnsatCoresFull];
-}
-
-bool Options::getEarlyExit() const{
-  return (*this)[options::earlyExit];
-}
-
-bool Options::getFilesystemAccess() const{
-  return (*this)[options::filesystemAccess];
-}
-
-bool Options::getForceNoLimitCpuWhileDump() const{
-  return (*this)[options::forceNoLimitCpuWhileDump];
-}
-
-bool Options::getHelp() const{
-  return (*this)[options::help];
-}
-
-bool Options::getIncrementalSolving() const{
-  return (*this)[options::incrementalSolving];
-}
-
-bool Options::getInteractive() const{
-  return (*this)[options::interactive];
-}
-
-bool Options::getInteractivePrompt() const{
-  return (*this)[options::interactivePrompt];
-}
-
-bool Options::getLanguageHelp() const{
-  return (*this)[options::languageHelp];
-}
-
-bool Options::getMemoryMap() const{
-  return (*this)[options::memoryMap];
-}
-
-bool Options::getParseOnly() const{
-  return (*this)[options::parseOnly];
-}
-
-bool Options::getProduceModels() const{
-  return (*this)[options::produceModels];
-}
-
-bool Options::getSegvSpin() const{
-  return (*this)[options::segvSpin];
-}
-
-bool Options::getSemanticChecks() const{
-  return (*this)[options::semanticChecks];
-}
-
-bool Options::getStatistics() const{
-  // statsEveryQuery enables stats
-  return (*this)[options::statistics] || (*this)[options::statisticsEveryQuery];
-}
-
-bool Options::getStatsEveryQuery() const{
-  return (*this)[options::statisticsEveryQuery];
-}
-
-bool Options::getStrictParsing() const{
-  return (*this)[options::strictParsing];
-}
-
-int Options::getTearDownIncremental() const{
-  return (*this)[options::tearDownIncremental];
-}
-
-uint64_t Options::getCumulativeTimeLimit() const
-{
-  return (*this)[options::cumulativeMillisecondLimit];
-}
-
-bool Options::getVersion() const{
-  return (*this)[options::version];
-}
-
-const std::string& Options::getForceLogicString() const{
-  return (*this)[options::forceLogicString];
-}
-
-int Options::getVerbosity() const{
-  return (*this)[options::verbosity];
-}
-
-std::istream* Options::getIn() const{
-  return (*this)[options::in];
-}
-
-std::ostream* Options::getErr(){
-  return (*this)[options::err];
-}
-
-std::ostream* Options::getOut(){
-  return (*this)[options::out];
-}
-
-std::ostream* Options::getOutConst() const{
-  // #warning "Remove Options::getOutConst"
-  return (*this)[options::out];
-}
-
-std::string Options::getBinaryName() const{
-  return (*this)[options::binary_name];
-}
-
-std::ostream* Options::currentGetOut() {
-  return current().getOut();
-}
-
-
-// TODO: Document these.
-
-void Options::setInputLanguage(InputLanguage value) {
-  base.inputLanguage = value;
-}
-
-void Options::setInteractive(bool value) {
-  driver.interactive = value;
-}
-
-void Options::setOut(std::ostream* value) {
-  base.out = value;
-}
-
-void Options::setOutputLanguage(OutputLanguage value) {
-  base.outputLanguage = value;
-}
-
-bool Options::wasSetByUserEarlyExit() const {
-  return wasSetByUser(options::earlyExit);
-}
-
-bool Options::wasSetByUserForceLogicString() const {
-  return wasSetByUser(options::forceLogicString);
-}
-
-bool Options::wasSetByUserIncrementalSolving() const {
-  return wasSetByUser(options::incrementalSolving);
-}
-
-bool Options::wasSetByUserInteractive() const {
-  return wasSetByUser(options::interactive);
-}
-
-
-void Options::flushErr() {
-  if(getErr() != NULL) {
-    *(getErr()) << std::flush;
-  }
-}
-
-void Options::flushOut() {
-  if(getOut() != NULL) {
-    *(getOut()) << std::flush;
-  }
-}
-
-}  // namespace cvc5
diff --git a/src/options/options_template.h b/src/options/options_template.h
index 346096169..6e28aad85 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -136,53 +136,6 @@ public:
    */
   std::string getOption(const std::string& key) const;
 
-  // Get accessor functions.
-  InputLanguage getInputLanguage() const;
-  options::InstFormatMode getInstFormatMode() const;
-  OutputLanguage getOutputLanguage() const;
-  bool getUfHo() const;
-  bool getDumpInstantiations() const;
-  bool getDumpModels() const;
-  bool getDumpProofs() const;
-  bool getDumpUnsatCores() const;
-  bool getEarlyExit() const;
-  bool getFilesystemAccess() const;
-  bool getForceNoLimitCpuWhileDump() const;
-  bool getHelp() const;
-  bool getIncrementalSolving() const;
-  bool getInteractive() const;
-  bool getInteractivePrompt() const;
-  bool getLanguageHelp() const;
-  bool getMemoryMap() const;
-  bool getParseOnly() const;
-  bool getProduceModels() const;
-  bool getSegvSpin() const;
-  bool getSemanticChecks() const;
-  bool getStatistics() const;
-  bool getStatsEveryQuery() const;
-  bool getStrictParsing() const;
-  int getTearDownIncremental() const;
-  uint64_t getCumulativeTimeLimit() const;
-  bool getVersion() const;
-  const std::string& getForceLogicString() const;
-  int getVerbosity() const;
-  std::istream* getIn() const;
-  std::ostream* getErr();
-  std::ostream* getOut();
-  std::ostream* getOutConst() const; // TODO: Remove this.
-  std::string getBinaryName() const;
-
-  // TODO: Document these.
-  void setInputLanguage(InputLanguage);
-  void setInteractive(bool);
-  void setOut(std::ostream*);
-  void setOutputLanguage(OutputLanguage);
-
-  bool wasSetByUserEarlyExit() const;
-  bool wasSetByUserForceLogicString() const;
-  bool wasSetByUserIncrementalSolving() const;
-  bool wasSetByUserInteractive() const;
-
   // Static accessor functions.
   // TODO: Document these.
   static std::ostream* currentGetOut();
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index eb952f8db..f6592a931 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -27,6 +27,7 @@
 #include "base/output.h"
 #include "expr/kind.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/input.h"
 #include "parser/parser_exception.h"
 #include "smt/command.h"
@@ -898,7 +899,8 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s)
 
 api::Term Parser::mkStringConstant(const std::string& s)
 {
-  if (language::isInputLang_smt2_6(d_solver->getOptions().getInputLanguage()))
+  if (language::isInputLang_smt2_6(
+          options::getInputLanguage(d_solver->getOptions())))
   {
     return d_solver->mkString(s, true);
   }
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 26a867f95..e4f46326f 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -22,6 +22,7 @@
 #include "base/check.h"
 #include "cvc/cvc.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/antlr_input.h"
 #include "parser/input.h"
 #include "parser/parser.h"
@@ -116,16 +117,17 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
   return *this;
 }
 
-ParserBuilder& ParserBuilder::withOptions(const Options& options) {
+ParserBuilder& ParserBuilder::withOptions(const Options& opts)
+{
   ParserBuilder& retval = *this;
-  retval =
-      retval.withInputLanguage(options.getInputLanguage())
-      .withChecks(options.getSemanticChecks())
-      .withStrictMode(options.getStrictParsing())
-      .withParseOnly(options.getParseOnly())
-      .withIncludeFile(options.getFilesystemAccess());
-  if(options.wasSetByUserForceLogicString()) {
-    LogicInfo tmp(options.getForceLogicString());
+  retval = retval.withInputLanguage(options::getInputLanguage(opts))
+               .withChecks(options::getSemanticChecks(opts))
+               .withStrictMode(options::getStrictParsing(opts))
+               .withParseOnly(options::getParseOnly(opts))
+               .withIncludeFile(options::getFilesystemAccess(opts));
+  if (options::wasSetByUserForceLogicString(opts))
+  {
+    LogicInfo tmp(options::getForceLogicString(opts));
     retval = retval.withForcedLogic(tmp.getLogicString());
   }
   return retval;
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 992ca408a..aed3b06f1 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -109,7 +109,7 @@ class CVC5_EXPORT ParserBuilder
   ParserBuilder& withParseOnly(bool flag = true);
 
   /** Derive settings from the given options. */
-  ParserBuilder& withOptions(const Options& options);
+  ParserBuilder& withOptions(const Options& opts);
 
   /**
    * Should the parser use strict mode?
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index d32f149bf..4f5440944 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -18,6 +18,7 @@
 
 #include "base/check.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"
@@ -316,7 +317,7 @@ bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
 
 bool Smt2::isHoEnabled() const
 {
-  return getLogic().isHigherOrder() && d_solver->getOptions().getUfHo();
+  return getLogic().isHigherOrder() && options::getUfHo(d_solver->getOptions());
 }
 
 bool Smt2::logicIsSet() {
@@ -842,7 +843,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
 
 InputLanguage Smt2::getLanguage() const
 {
-  return d_solver->getOptions().getInputLanguage();
+  return options::getInputLanguage(d_solver->getOptions());
 }
 
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
@@ -1094,7 +1095,8 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   }
   else if (isBuiltinOperator)
   {
-    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!options::getUfHo(opts)
+        && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -1146,7 +1148,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!opts.getUfHo())
+        if (!options::getUfHo(opts))
         {
           parseError("Cannot partially apply functions unless --uf-ho is set.");
         }
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 156f2e1e6..764e83361 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -22,6 +22,7 @@
 #include "api/cpp/cvc5.h"
 #include "base/check.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "parser/parser.h"
 #include "smt/command.h"
 
@@ -315,7 +316,8 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {
-    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!options::getUfHo(opts)
+        && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -362,7 +364,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!opts.getUfHo())
+        if (!options::getUfHo(opts))
         {
           parseError("Cannot partially apply functions unless --uf-ho is set.");
         }
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 647981ab3..87c19d0e1 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -107,6 +107,6 @@ const Printer& Env::getPrinter()
   return *Printer::getPrinter(d_options[options::outputLanguage]);
 }
 
-std::ostream& Env::getDumpOut() { return *d_options.getOut(); }
+std::ostream& Env::getDumpOut() { return *d_options.base.out; }
 
 }  // namespace cvc5
diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp
index 6395a4c2c..aa91bb184 100644
--- a/src/smt/output_manager.cpp
+++ b/src/smt/output_manager.cpp
@@ -15,6 +15,7 @@
 
 #include "smt/output_manager.h"
 
+#include "options/base_options.h"
 #include "smt/smt_engine.h"
 
 namespace cvc5 {
@@ -25,7 +26,7 @@ const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); }
 
 std::ostream& OutputManager::getDumpOut() const
 {
-  return *d_smt->getOptions().getOut();
+  return *d_smt->getOptions().base.out;
 }
 
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 582d67b31..6069745e0 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -76,7 +76,7 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
                                   Node query)
 {
   Assert (!query.isNull());
-  if (Options::current().wasSetByUser(options::sygusExprMinerCheckTimeout))
+  if (Options::current().quantifiers.sygusExprMinerCheckTimeout__setByUser)
   {
     initializeSubsolver(checker, true, options::sygusExprMinerCheckTimeout());
   }
diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp
index 5a4c2d142..ccc0763b7 100644
--- a/src/theory/quantifiers/solution_filter.cpp
+++ b/src/theory/quantifiers/solution_filter.cpp
@@ -16,6 +16,8 @@
 #include "theory/quantifiers/solution_filter.h"
 
 #include <fstream>
+
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -90,7 +92,7 @@ bool SolutionFilterStrength::addTerm(Node n, std::ostream& out)
       else
       {
         Options& opts = smt::currentSmtEngine()->getOptions();
-        std::ostream* smtOut = opts.getOut();
+        std::ostream* smtOut = opts.base.out;
         (*smtOut) << "; (filtered " << (d_isStrong ? s : s.negate()) << ")"
                   << std::endl;
       }
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e4ec40325..62c61fe1e 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -444,7 +444,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
       if (printDebug)
       {
         Options& sopts = smt::currentSmtEngine()->getOptions();
-        std::ostream& out = *sopts.getOut();
+        std::ostream& out = *sopts.base.out;
         out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl;
       }
     }
@@ -529,7 +529,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     if (printDebug)
     {
       Options& sopts = smt::currentSmtEngine()->getOptions();
-      std::ostream& out = *sopts.getOut();
+      std::ostream& out = *sopts.base.out;
       out << "(sygus-candidate ";
       Assert(d_quant[0].getNumChildren() == candidate_values.size());
       for (unsigned i = 0, ncands = candidate_values.size(); i < ncands; i++)
@@ -995,7 +995,7 @@ void SynthConjecture::printAndContinueStream(const std::vector<Node>& enums,
   // we have generated a solution, print it
   // get the current output stream
   Options& sopts = smt::currentSmtEngine()->getOptions();
-  printSynthSolutionInternal(*sopts.getOut());
+  printSynthSolutionInternal(*sopts.base.out);
   excludeCurrentSolution(enums, values);
 }
 
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 36602d3ae..48dce7cf3 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -828,7 +828,7 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr)
     }
     // we have detected unsoundness in the rewriter
     Options& sopts = smt::currentSmtEngine()->getOptions();
-    std::ostream* out = sopts.getOut();
+    std::ostream* out = sopts.base.out;
     (*out) << "(unsound-rewrite " << bv << " " << bvr << ")" << std::endl;
     // debugging information
     (*out) << "Terms are not equivalent for : " << std::endl;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 40f5b901f..4f20fae22 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers_engine.h"
 
+#include "options/base_options.h"
 #include "options/printer_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -461,7 +462,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
       if (options::debugInst() || debugInstTrace)
       {
         Options& sopts = smt::currentSmtEngine()->getOptions();
-        std::ostream& out = *sopts.getOut();
+        std::ostream& out = *sopts.base.out;
         d_qim.getInstantiate()->debugPrint(out);
       }
     }
diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp
index 04b366cf0..9794888b2 100644
--- a/test/api/smt2_compliance.cpp
+++ b/test/api/smt2_compliance.cpp
@@ -19,6 +19,7 @@
 
 #include "api/cpp/cvc5.h"
 #include "options/options.h"
+#include "options/options_public.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -34,8 +35,8 @@ void testGetInfo(api::Solver* solver, const char* s);
 int main()
 {
   Options opts;
-  opts.setInputLanguage(language::input::LANG_SMTLIB_V2);
-  opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+  options::setInputLanguage(language::input::LANG_SMTLIB_V2, opts);
+  options::setOutputLanguage(language::output::LANG_SMTLIB_V2, opts);
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);