Remove `Options::operator[]` (#6649)

This PR removes the next heavily specialized template function Options::operator[] in favor of direct access to the option data.

9 files changed, 84 insertions, 107 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0f2d5ad1b..668fc9382 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4743,7 +4743,7 @@ Solver::Solver(Options* opts)
   }
   d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get()));
   d_smtEngine->setSolver(this);
-  d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed]));
+  d_rng.reset(new Random(d_smtEngine->getOptions().driver.seed));
   resetStatistics();
 }
 
@@ -6452,7 +6452,7 @@ Result Solver::checkEntailed(const Term& term) const
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions()[options::incrementalSolving])
+                 || d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM(term);
@@ -6468,7 +6468,7 @@ Result Solver::checkEntailed(const std::vector<Term>& terms) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions()[options::incrementalSolving])
+                 || d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERMS(terms);
@@ -6497,7 +6497,7 @@ Result Solver::checkSat(void) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions()[options::incrementalSolving])
+                 || d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   //////// all checks before this line
@@ -6512,7 +6512,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade()
-                 || d_smtEngine->getOptions()[options::incrementalSolving])
+                 || d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort());
@@ -6528,7 +6528,7 @@ Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
   CVC5_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
-                 || d_smtEngine->getOptions()[options::incrementalSolving])
+                 || d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot make multiple queries unless incremental solving is enabled "
          "(try --incremental)";
   CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(assumptions, getBooleanSort());
@@ -6863,10 +6863,10 @@ std::vector<Term> Solver::getUnsatAssumptions(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot get unsat assumptions unless incremental solving is enabled "
          "(try --incremental)";
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatAssumptions)
       << "Cannot get unsat assumptions unless explicitly enabled "
          "(try --produce-unsat-assumptions)";
   CVC5_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
@@ -6891,7 +6891,7 @@ std::vector<Term> Solver::getUnsatCore(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.unsatCores)
       << "Cannot get unsat core unless explicitly enabled "
          "(try --produce-unsat-cores)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
@@ -6925,7 +6925,7 @@ std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   NodeManagerScope scope(getNodeManager());
-  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions()[options::produceModels])
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
@@ -6992,7 +6992,7 @@ Term Solver::getSeparationHeap() const
       d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
       << "Cannot obtain separation logic expressions if not using the "
          "separation logic theory.";
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get separation heap term unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
@@ -7011,7 +7011,7 @@ Term Solver::getSeparationNilTerm() const
       d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
       << "Cannot obtain separation logic expressions if not using the "
          "separation logic theory.";
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get separation nil term unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
@@ -7044,7 +7044,7 @@ void Solver::pop(uint32_t nscopes) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot pop when not solving incrementally (use --incremental)";
   CVC5_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
       << "Cannot pop beyond first pushed context";
@@ -7133,7 +7133,7 @@ void Solver::blockModel() const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
@@ -7148,7 +7148,7 @@ void Solver::blockModelValues(const std::vector<Term>& terms) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceModels)
       << "Cannot get value unless model generation is enabled "
          "(try --produce-models)";
   CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat())
@@ -7176,7 +7176,7 @@ void Solver::push(uint32_t nscopes) const
 {
   NodeManagerScope scope(getNodeManager());
   CVC5_API_TRY_CATCH_BEGIN;
-  CVC5_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.incrementalSolving)
       << "Cannot push when not solving incrementally (use --incremental)";
   //////// all checks before this line
   for (uint32_t n = 0; n < nscopes; ++n)
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 91a5c32e0..c355ff436 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -129,16 +129,6 @@ TPL_OPTION_STRUCT_RW = \
   type operator()() const;
 }} thread_local {name};"""
 
-TPL_DECL_OP_BRACKET = \
-"""template <> const options::{name}__option_t::type& Options::operator[](
-    options::{name}__option_t) const;"""
-
-TPL_IMPL_OP_BRACKET = TPL_DECL_OP_BRACKET[:-1] + \
-"""
-{{
-  return {module}.{name};
-}}"""
-
 TPL_DECL_WAS_SET_BY_USER = \
 """template <> bool Options::wasSetByUser(options::{name}__option_t) const;"""
 
@@ -151,10 +141,8 @@ TPL_IMPL_WAS_SET_BY_USER = TPL_DECL_WAS_SET_BY_USER[:-1] + \
 # Option specific methods
 
 TPL_IMPL_OP_PAR = \
-"""inline {name}__option_t::type {name}__option_t::operator()() const
-{{
-  return Options::current()[*this];
-}}"""
+"""inline {type} {name}__option_t::operator()() const
+{{ return Options::current().{module}.{name}; }}"""
 
 # Mode templates
 TPL_DECL_MODE_ENUM = \
@@ -591,7 +579,6 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
 
         # Generate module specialization
         default_decl.append(TPL_DECL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
-        specs.append(TPL_DECL_OP_BRACKET.format(name=option.name))
         specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name))
 
         if option.long and option.type not in ['bool', 'void'] and \
@@ -606,14 +593,13 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
                     module.id, option.long, option.type))
 
         # Generate module inlines
-        inls.append(TPL_IMPL_OP_PAR.format(name=option.name))
+        inls.append(TPL_IMPL_OP_PAR.format(module=module.id, name=option.name, type=option.type))
 
 
         ### Generate code for {module.name}_options.cpp
 
         # Accessors
         default_impl.append(TPL_IMPL_SET_DEFAULT.format(module=module.id, name=option.name, funcname=capoptionname, type=option.type))
-        accs.append(TPL_IMPL_OP_BRACKET.format(module=module.id, name=option.name))
         accs.append(TPL_IMPL_WAS_SET_BY_USER.format(module=module.id, name=option.name))
 
         # Global definitions
@@ -872,17 +858,17 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_
                         'if ({}) {{'.format(cond))
                     if option.type == 'bool':
                         getoption_handlers.append(
-                            'return (*this)[options::{}] ? "true" : "false";'.format(option.name))
+                            'return options.{}.{} ? "true" : "false";'.format(module.id, option.name))
                     elif option.type == 'std::string':
                         getoption_handlers.append(
-                            'return (*this)[options::{}];'.format(option.name))
+                            'return options.{}.{};'.format(module.id, option.name))
                     elif is_numeric_cpp_type(option.type):
                         getoption_handlers.append(
-                            'return std::to_string((*this)[options::{}]);'.format(option.name))
+                            'return std::to_string(options.{}.{});'.format(module.id, option.name))
                     else:
                         getoption_handlers.append('std::stringstream ss;')
                         getoption_handlers.append(
-                            'ss << (*this)[options::{}];'.format(option.name))
+                            'ss << options.{}.{};'.format(module.id, option.name))
                         getoption_handlers.append('return ss.str();')
                     getoption_handlers.append('}')
 
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 251072ba5..0d6b7f01b 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -563,6 +563,7 @@ void Options::setOptionInternal(const std::string& key,
 std::string Options::getOption(const std::string& key) const
 {
   Trace("options") << "Options::getOption(" << key << ")" << std::endl;
+  const Options& options = *this;
   ${getoption_handlers}$
 
   throw UnrecognizedOptionException(key);
diff --git a/src/options/options_template.h b/src/options/options_template.h
index 6e28aad85..6ce77d7a1 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -124,10 +124,6 @@ public:
    */
   void setOption(const std::string& key, const std::string& optionarg);
 
-  /** Get the value of the given option.  Const access only. */
-  template <class T>
-  const typename T::type& operator[](T) const;
-
   /**
    * Gets the value of the given option by key and returns value as a string.
    *
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 87c19d0e1..1381ef87c 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -104,7 +104,7 @@ ResourceManager* Env::getResourceManager() const
 
 const Printer& Env::getPrinter()
 {
-  return *Printer::getPrinter(d_options[options::outputLanguage]);
+  return *Printer::getPrinter(d_options.base.outputLanguage);
 }
 
 std::ostream& Env::getDumpOut() { return *d_options.base.out; }
diff --git a/src/smt/env.h b/src/smt/env.h
index 667497683..29a360209 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -91,12 +91,6 @@ class Env
   /** Get a pointer to the underlying dump manager. */
   smt::DumpManager* getDumpManager();
 
-  template <typename Opt>
-  const auto& getOption(Opt opt) const
-  {
-    return d_options[opt];
-  }
-
   /** Get the options object (const version only) owned by this Env. */
   const Options& getOptions() const;
 
diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index 3fc58ff05..37541751e 100644
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -71,7 +71,7 @@ void OptionsManager::notifySetOption(const std::string& key)
                << std::endl;
   if (key == options::expr::defaultExprDepth__name)
   {
-    int depth = (*d_options)[options::defaultExprDepth];
+    int depth = d_options->expr.defaultExprDepth;
     Debug.getStream() << expr::ExprSetDepth(depth);
     Trace.getStream() << expr::ExprSetDepth(depth);
     Notice.getStream() << expr::ExprSetDepth(depth);
@@ -82,7 +82,7 @@ void OptionsManager::notifySetOption(const std::string& key)
   }
   else if (key == options::expr::defaultDagThresh__name)
   {
-    int dag = (*d_options)[options::defaultDagThresh];
+    int dag = d_options->expr.defaultDagThresh;
     Debug.getStream() << expr::ExprDag(dag);
     Trace.getStream() << expr::ExprDag(dag);
     Notice.getStream() << expr::ExprDag(dag);
@@ -93,12 +93,12 @@ void OptionsManager::notifySetOption(const std::string& key)
   }
   else if (key == options::smt::dumpModeString__name)
   {
-    const std::string& value = (*d_options)[options::dumpModeString];
+    const std::string& value = d_options->smt.dumpModeString;
     Dump.setDumpFromString(value);
   }
   else if (key == options::base::printSuccess__name)
   {
-    bool value = (*d_options)[options::printSuccess];
+    bool value = d_options->base.printSuccess;
     Debug.getStream() << Command::printsuccess(value);
     Trace.getStream() << Command::printsuccess(value);
     Notice.getStream() << Command::printsuccess(value);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7abeac44f..c84a29055 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -193,7 +193,7 @@ void SmtEngine::finishInit()
   }
 
   // set the random seed
-  Random::getRandom().setSeed(d_env->getOption(options::seed));
+  Random::getRandom().setSeed(d_env->getOptions().driver.seed);
 
   // Call finish init on the options manager. This inializes the resource
   // manager based on the options, and sets up the best default options
@@ -201,7 +201,7 @@ void SmtEngine::finishInit()
   d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver);
 
   ProofNodeManager* pnm = nullptr;
-  if (d_env->getOption(options::produceProofs))
+  if (d_env->getOptions().smt.produceProofs)
   {
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
@@ -262,11 +262,11 @@ void SmtEngine::finishInit()
   getDumpManager()->finishInit();
 
   // subsolvers
-  if (d_env->getOption(options::produceAbducts))
+  if (d_env->getOptions().smt.produceAbducts)
   {
     d_abductSolver.reset(new AbductionSolver(this));
   }
-  if (d_env->getOption(options::produceInterpols)
+  if (d_env->getOptions().smt.produceInterpols
       != options::ProduceInterpols::NONE)
   {
     d_interpolSolver.reset(new InterpolationSolver(this));
@@ -459,10 +459,10 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
     if (!Options::current().wasSetByUser(options::outputLanguage))
     {
       language::output::Language olang = language::toOutputLanguage(ilang);
-      if (d_env->getOption(options::outputLanguage) != olang)
+      if (d_env->getOptions().base.outputLanguage != olang)
       {
         getOptions().base.outputLanguage = olang;
-        *d_env->getOption(options::out) << language::SetLanguage(olang);
+        *d_env->getOptions().base.out << language::SetLanguage(olang);
       }
     }
   }
@@ -575,7 +575,7 @@ void SmtEngine::debugCheckFunctionBody(Node formula,
                                        Node func)
 {
   TypeNode formulaType =
-      formula.getType(d_env->getOption(options::typeChecking));
+      formula.getType(d_env->getOptions().expr.typeChecking);
   TypeNode funcType = func.getType();
   // We distinguish here between definitions of constants and functions,
   // because the type checking for them is subtly different.  Perhaps we
@@ -741,7 +741,7 @@ Result SmtEngine::quickCheck() {
 
 Model* SmtEngine::getAvailableModel(const char* c) const
 {
-  if (!d_env->getOption(options::assignFunctionValues))
+  if (!d_env->getOptions().theory.assignFunctionValues)
   {
     std::stringstream ss;
     ss << "Cannot " << c << " when --assign-function-values is false.";
@@ -758,7 +758,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const
     throw RecoverableModalException(ss.str().c_str());
   }
 
-  if (!d_env->getOption(options::produceModels))
+  if (!d_env->getOptions().smt.produceModels)
   {
     std::stringstream ss;
     ss << "Cannot " << c << " when produce-models options is off.";
@@ -902,7 +902,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
                  << "(" << assumptions << ") => " << r << endl;
 
     // Check that SAT results generate a model correctly.
-    if (d_env->getOption(options::checkModels))
+    if (d_env->getOptions().smt.checkModels)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
       {
@@ -910,14 +910,14 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate a proof correctly.
-    if (d_env->getOption(options::checkProofs)
-        || d_env->getOption(options::proofEagerChecking))
+    if (d_env->getOptions().smt.checkProofs
+        || d_env->getOptions().proof.proofEagerChecking)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
-        if ((d_env->getOption(options::checkProofs)
-             || d_env->getOption(options::proofEagerChecking))
-            && !d_env->getOption(options::produceProofs))
+        if ((d_env->getOptions().smt.checkProofs
+             || d_env->getOptions().proof.proofEagerChecking)
+            && !d_env->getOptions().smt.produceProofs)
         {
           throw ModalException(
               "Cannot check-proofs because proofs were disabled.");
@@ -926,7 +926,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate an unsat core correctly.
-    if (d_env->getOption(options::checkUnsatCores))
+    if (d_env->getOptions().smt.checkUnsatCores)
     {
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
       {
@@ -955,7 +955,7 @@ std::vector<Node> SmtEngine::getUnsatAssumptions(void)
 {
   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
   SmtScope smts(this);
-  if (!d_env->getOption(options::unsatAssumptions))
+  if (!d_env->getOptions().smt.unsatAssumptions)
   {
     throw ModalException(
         "Cannot get unsat assumptions when produce-unsat-assumptions option "
@@ -1166,7 +1166,7 @@ Node SmtEngine::getValue(const Node& ex) const
   Assert(m->hasApproximations() || resultNode.getKind() == kind::LAMBDA
          || resultNode.isConst());
 
-  if (d_env->getOption(options::abstractValues)
+  if (d_env->getOptions().smt.abstractValues
       && resultNode.getType().isArray())
   {
     resultNode = d_absValues->mkAbstractValue(resultNode);
@@ -1207,7 +1207,7 @@ Model* SmtEngine::getModel() {
   Assert(te != nullptr);
   te->setEagerModelBuilding();
 
-  if (d_env->getOption(options::modelCoresMode)
+  if (d_env->getOptions().smt.modelCoresMode
       != options::ModelCoresMode::NONE)
   {
     // If we enabled model cores, we compute a model core for m based on our
@@ -1215,7 +1215,7 @@ Model* SmtEngine::getModel() {
     std::vector<Node> eassertsProc = getExpandedAssertions();
     ModelCoreBuilder::setModelCore(eassertsProc,
                                    m->getTheoryModel(),
-                                   d_env->getOption(options::modelCoresMode));
+                                   d_env->getOptions().smt.modelCoresMode);
   }
   // set the information on the SMT-level model
   Assert(m != nullptr);
@@ -1238,7 +1238,7 @@ Result SmtEngine::blockModel()
 
   Model* m = getAvailableModel("block model");
 
-  if (d_env->getOption(options::blockModelsMode)
+  if (d_env->getOptions().smt.blockModelsMode
       == options::BlockModelsMode::NONE)
   {
     std::stringstream ss;
@@ -1251,7 +1251,7 @@ Result SmtEngine::blockModel()
   Node eblocker =
       ModelBlocker::getModelBlocker(eassertsProc,
                                     m->getTheoryModel(),
-                                    d_env->getOption(options::blockModelsMode));
+                                    d_env->getOptions().smt.blockModelsMode);
   Trace("smt") << "Block formula: " << eblocker << std::endl;
   return assertFormula(eblocker);
 }
@@ -1349,17 +1349,17 @@ Node SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
 void SmtEngine::checkProof()
 {
-  Assert(d_env->getOption(options::produceProofs));
+  Assert(d_env->getOptions().smt.produceProofs);
   // internal check the proof
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
-  if (d_env->getOption(options::proofEagerChecking))
+  if (d_env->getOptions().proof.proofEagerChecking)
   {
     pe->checkProof(d_asserts->getAssertionList());
   }
   Assert(pe->getProof() != nullptr);
   std::shared_ptr<ProofNode> pePfn = pe->getProof();
-  if (d_env->getOption(options::checkProofs))
+  if (d_env->getOptions().smt.checkProofs)
   {
     d_pfManager->checkProof(pePfn, *d_asserts);
   }
@@ -1372,7 +1372,7 @@ StatisticsRegistry& SmtEngine::getStatisticsRegistry()
 
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
-  if (!d_env->getOption(options::unsatCores))
+  if (!d_env->getOptions().smt.unsatCores)
   {
     throw ModalException(
         "Cannot get an unsat core when produce-unsat-cores or produce-proofs "
@@ -1405,7 +1405,7 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
 }
 
 void SmtEngine::checkUnsatCore() {
-  Assert(d_env->getOption(options::unsatCores))
+  Assert(d_env->getOptions().smt.unsatCores)
       << "cannot check unsat core if unsat cores are turned off";
 
   Notice() << "SmtEngine::checkUnsatCore(): generating unsat core" << endl;
@@ -1514,7 +1514,7 @@ std::string SmtEngine::getProof()
   {
     getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut());
   }
-  if (!d_env->getOption(options::produceProofs))
+  if (!d_env->getOptions().smt.produceProofs)
   {
     throw ModalException("Cannot get a proof when proof option is off.");
   }
@@ -1537,7 +1537,7 @@ std::string SmtEngine::getProof()
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
+  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
     out << "% SZS output start Proof for " << d_state->getFilename()
         << std::endl;
@@ -1546,9 +1546,9 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
 
   // First, extract and print the skolemizations
   bool printed = false;
-  bool reqNames = !d_env->getOption(options::printInstFull);
+  bool reqNames = !d_env->getOptions().printer.printInstFull;
   // only print when in list mode
-  if (d_env->getOption(options::printInstMode) == options::PrintInstMode::LIST)
+  if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST)
   {
     std::map<Node, std::vector<Node>> sks;
     qe->getSkolemTermVectors(sks);
@@ -1583,14 +1583,14 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
       continue;
     }
     // must have a name
-    if (d_env->getOption(options::printInstMode) == options::PrintInstMode::NUM)
+    if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM)
     {
       out << "(num-instantiations " << name << " " << i.second.size() << ")"
           << std::endl;
     }
     else
     {
-      Assert(d_env->getOption(options::printInstMode)
+      Assert(d_env->getOptions().printer.printInstMode
              == options::PrintInstMode::LIST);
       InstantiationList ilist(name, i.second);
       out << ilist;
@@ -1602,7 +1602,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   {
     out << "No instantiations" << std::endl;
   }
-  if (d_env->getOption(options::instFormatMode) == options::InstFormatMode::SZS)
+  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
   {
     out << "% SZS output end Proof for " << d_state->getFilename() << std::endl;
   }
@@ -1613,9 +1613,9 @@ void SmtEngine::getInstantiationTermVectors(
 {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOption(options::produceProofs)
-      && (!d_env->getOption(options::unsatCores)
-          || d_env->getOption(options::unsatCoresMode) == options::UnsatCoresMode::FULL_PROOF)
+  if (d_env->getOptions().smt.produceProofs
+      && (!d_env->getOptions().smt.unsatCores
+          || d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF)
       && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
@@ -1716,7 +1716,7 @@ std::vector<Node> SmtEngine::getAssertions()
     getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut());
   }
   Trace("smt") << "SMT getAssertions()" << endl;
-  if (!d_env->getOption(options::produceAssertions))
+  if (!d_env->getOptions().smt.produceAssertions)
   {
     const char* msg =
       "Cannot query the current assertion list when not in produce-assertions mode.";
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index de9a32248..f0cc78789 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -164,7 +164,7 @@ ResourceManager::ResourceManager(StatisticsRegistry& stats,
 
   d_infidWeights.fill(1);
   d_resourceWeights.fill(1);
-  for (const auto& opt : d_options[options::resourceWeightHolder])
+  for (const auto& opt : d_options.resman.resourceWeightHolder)
   {
     std::string name;
     uint64_t weight;
@@ -189,9 +189,9 @@ uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
 
 uint64_t ResourceManager::getResourceRemaining() const
 {
-  if (d_options[options::cumulativeResourceLimit] <= d_cumulativeResourceUsed)
+  if (d_options.resman.cumulativeResourceLimit <= d_cumulativeResourceUsed)
     return 0;
-  return d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed;
+  return d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed;
 }
 
 void ResourceManager::spendResource(uint64_t amount)
@@ -237,21 +237,21 @@ void ResourceManager::spendResource(theory::InferenceId iid)
 
 void ResourceManager::beginCall()
 {
-  d_perCallTimer.set(d_options[options::perCallMillisecondLimit]);
+  d_perCallTimer.set(d_options.resman.perCallMillisecondLimit);
   d_thisCallResourceUsed = 0;
 
-  if (d_options[options::cumulativeResourceLimit] > 0)
+  if (d_options.resman.cumulativeResourceLimit > 0)
   {
     // Compute remaining cumulative resource budget
     d_thisCallResourceBudget =
-        d_options[options::cumulativeResourceLimit] - d_cumulativeResourceUsed;
+        d_options.resman.cumulativeResourceLimit - d_cumulativeResourceUsed;
   }
-  if (d_options[options::perCallResourceLimit] > 0)
+  if (d_options.resman.perCallResourceLimit > 0)
   {
     // Check if per-call resource budget is even smaller
-    if (d_options[options::perCallResourceLimit] < d_thisCallResourceBudget)
+    if (d_options.resman.perCallResourceLimit < d_thisCallResourceBudget)
     {
-      d_thisCallResourceBudget = d_options[options::perCallResourceLimit];
+      d_thisCallResourceBudget = d_options.resman.perCallResourceLimit;
     }
   }
 }
@@ -265,25 +265,25 @@ void ResourceManager::endCall()
 
 bool ResourceManager::limitOn() const
 {
-  return (d_options[options::cumulativeResourceLimit] > 0)
-         || (d_options[options::perCallMillisecondLimit] > 0)
-         || (d_options[options::perCallResourceLimit] > 0);
+  return (d_options.resman.cumulativeResourceLimit > 0)
+         || (d_options.resman.perCallMillisecondLimit > 0)
+         || (d_options.resman.perCallResourceLimit > 0);
 }
 
 bool ResourceManager::outOfResources() const
 {
-  if (d_options[options::perCallResourceLimit] > 0)
+  if (d_options.resman.perCallResourceLimit > 0)
   {
     // Check if per-call resources are exhausted
-    if (d_thisCallResourceUsed >= d_options[options::perCallResourceLimit])
+    if (d_thisCallResourceUsed >= d_options.resman.perCallResourceLimit)
     {
       return true;
     }
   }
-  if (d_options[options::cumulativeResourceLimit] > 0)
+  if (d_options.resman.cumulativeResourceLimit > 0)
   {
     // Check if cumulative resources are exhausted
-    if (d_cumulativeResourceUsed >= d_options[options::cumulativeResourceLimit])
+    if (d_cumulativeResourceUsed >= d_options.resman.cumulativeResourceLimit)
     {
       return true;
     }
@@ -293,7 +293,7 @@ bool ResourceManager::outOfResources() const
 
 bool ResourceManager::outOfTime() const
 {
-  if (d_options[options::perCallMillisecondLimit] == 0) return false;
+  if (d_options.resman.perCallMillisecondLimit == 0) return false;
   return d_perCallTimer.expired();
 }