Replace more static options accesses (#7531)

This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.

20 files changed, 215 insertions, 163 deletions

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index 51be8db51..36f8e2a8d 100644
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -41,7 +41,7 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
                                       const TypeNode& grammarType,
                                       Node& interpol)
 {
-  if (options::produceInterpols() == options::ProduceInterpols::NONE)
+  if (options().smt.produceInterpols == options::ProduceInterpols::NONE)
   {
     const char* msg =
         "Cannot get interpolation when produce-interpol options is off.";
@@ -57,7 +57,7 @@ bool InterpolationSolver::getInterpol(const std::vector<Node>& axioms,
   if (interpolSolver.solveInterpolation(
           name, axioms, conjn, grammarType, interpol))
   {
-    if (options::checkInterpols())
+    if (options().smt.checkInterpols)
     {
       checkInterpol(interpol, axioms, conj);
     }
diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp
index dfa6d5da4..16f43966e 100644
--- a/src/theory/combination_engine.cpp
+++ b/src/theory/combination_engine.cpp
@@ -44,7 +44,7 @@ CombinationEngine::CombinationEngine(Env& env,
                      : nullptr)
 {
   // create the equality engine, model manager, and shared solver
-  if (options::eeMode() == options::EqEngineMode::DISTRIBUTED)
+  if (options().theory.eeMode == options::EqEngineMode::DISTRIBUTED)
   {
     // use the distributed shared solver
     d_sharedSolver.reset(new SharedSolverDistributed(env, d_te));
@@ -55,7 +55,7 @@ CombinationEngine::CombinationEngine(Env& env,
     d_mmanager.reset(
         new ModelManagerDistributed(env, d_te, *d_eemanager.get()));
   }
-  else if (options::eeMode() == options::EqEngineMode::CENTRAL)
+  else if (options().theory.eeMode == options::EqEngineMode::CENTRAL)
   {
     // for now, the shared solver is the same in both approaches; use the
     // distributed one for now
@@ -70,7 +70,7 @@ CombinationEngine::CombinationEngine(Env& env,
   else
   {
     Unhandled() << "CombinationEngine::finishInit: equality engine mode "
-                << options::eeMode() << " not supported";
+                << options().theory.eeMode << " not supported";
   }
 }
 
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index d3e711c32..bacbf8c47 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -79,7 +79,8 @@ void SygusExtension::assertTester(int tindex, TNode n, Node exp)
       
       // check if parent is active
       bool do_add = true;
-      if( options::sygusSymBreakLazy() ){
+      if (options().datatypes.sygusSymBreakLazy)
+      {
         if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
           NodeSet::const_iterator it = d_active_terms.find( n[0] );
           if( it==d_active_terms.end() ){
@@ -120,7 +121,7 @@ void SygusExtension::assertFact(Node n, bool polarity)
     Node m = n[0];
     Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl;
     registerMeasureTerm( m );
-    if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
+    if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE)
     {
       std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
           d_szinfo.find(m);
@@ -231,7 +232,7 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
   Assert(itsz != d_szinfo.end());
   unsigned ssz = itsz->second->d_curr_search_size;
 
-  if (options::sygusFair() == options::SygusFairMode::DIRECT)
+  if (options().datatypes.sygusFair == options::SygusFairMode::DIRECT)
   {
     if( dt[tindex].getNumArgs()>0 ){
       quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn);
@@ -282,7 +283,8 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
   unsigned d = d_term_to_depth[n];
   Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl;
   //Assert( d<=ssz );
-  if( options::sygusSymBreakLazy() ){
+  if (options().datatypes.sygusSymBreakLazy)
+  {
     // dynamic symmetry breaking
     addSymBreakLemmasFor(ntn, n, d);
   }
@@ -361,7 +363,8 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
 
   // now activate the children those testers were previously asserted in this
   // context and are awaiting activation, if they exist.
-  if( options::sygusSymBreakLazy() ){
+  if (options().datatypes.sygusSymBreakLazy)
+  {
     Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
     for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
       Node sel = nm->mkNode(
@@ -379,7 +382,7 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
 }
 
 Node SygusExtension::getRelevancyCondition( Node n ) {
-  if (!options::sygusSymBreakRlv())
+  if (!options().datatypes.sygusSymBreakRlv)
   {
     return Node::null();
   }
@@ -391,7 +394,8 @@ Node SygusExtension::getRelevancyCondition( Node n ) {
       TypeNode ntn = n[0].getType();
       const DType& dt = ntn.getDType();
       Node sel = n.getOperator();
-      if( options::dtSharedSelectors() ){
+      if (options().datatypes.dtSharedSelectors)
+      {
         std::vector< Node > disj;
         bool excl = false;
         for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
@@ -410,7 +414,9 @@ Node SygusExtension::getRelevancyCondition( Node n ) {
           cond = disj.size() == 1 ? disj[0] : NodeManager::currentNM()->mkNode(
                                                   kind::AND, disj);
         }
-      }else{
+      }
+      else
+      {
         int sindex = utils::cindexOf(sel);
         Assert(sindex != -1);
         cond = utils::mkTester(n[0], sindex, dt).negate();
@@ -597,7 +603,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
   {
     Trace("sygus-sb-simple-debug") << "  Size..." << std::endl;
     // fairness
-    if (options::sygusFair() == options::SygusFairMode::DT_SIZE
+    if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE
         && !isAnyConstant)
     {
       Node szl = nm->mkNode(DT_SIZE, n);
@@ -685,7 +691,7 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
 
   // if we are the "any constant" constructor, we do no symmetry breaking
   // only do simple symmetry breaking up to depth 2
-  bool doSymBreak = options::sygusSymBreak();
+  bool doSymBreak = options().datatypes.sygusSymBreak;
   if (isAnyConstant || depth > 2)
   {
     doSymBreak = false;
@@ -961,7 +967,8 @@ void SygusExtension::registerSearchTerm(TypeNode tn,
   {
     Trace("sygus-sb-debug") << "  register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl;
     sca.d_search_terms[tn][d].push_back(n);
-    if( !options::sygusSymBreakLazy() ){
+    if (!options().datatypes.sygusSymBreakLazy)
+    {
       addSymBreakLemmasFor(tn, n, d);
     }
   }
@@ -1060,7 +1067,7 @@ Node SygusExtension::registerSearchValue(Node a,
       {
         // Is it equivalent under examples?
         Node bvr_equiv;
-        if (aconj != nullptr && options::sygusSymBreakPbe())
+        if (aconj != nullptr && options().datatypes.sygusSymBreakPbe)
         {
           // If the enumerator has examples, see if it is equivalent up to its
           // examples with a previous term.
@@ -1097,7 +1104,7 @@ Node SygusExtension::registerSearchValue(Node a,
         }
       }
 
-      if (options::sygusRewVerify())
+      if (options().quantifiers.sygusRewVerify)
       {
         if (bv != bvr)
         {
@@ -1111,7 +1118,7 @@ Node SygusExtension::registerSearchValue(Node a,
           {
             smap[tn].reset(new quantifiers::SygusSampler(d_env));
             smap[tn]->initializeSygus(
-                d_tds, nv, options::sygusSamples(), false);
+                d_tds, nv, options().quantifiers.sygusSamples, false);
             its = d_sampler[a].find(tn);
           }
           // check equivalent
@@ -1220,7 +1227,7 @@ void SygusExtension::registerSymBreakLemma(TypeNode tn,
     {
       for (const Node& t : itt->second)
       {
-        if (!options::sygusSymBreakLazy()
+        if (!options().datatypes.sygusSymBreakLazy
             || d_active_terms.find(t) != d_active_terms.end())
         {
           Node slem = lem.substitute(x, t);
@@ -1360,11 +1367,11 @@ void SygusExtension::registerSizeTerm(Node e)
   d_szinfo[m]->d_anchors.push_back(e);
   d_anchor_to_measure_term[e] = m;
   NodeManager* nm = NodeManager::currentNM();
-  if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
+  if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE)
   {
     // update constraints on the measure term
     Node slem;
-    if (options::sygusFairMax())
+    if (options().datatypes.sygusFairMax)
     {
       Node ds = nm->mkNode(DT_SIZE, e);
       slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue());
@@ -1490,7 +1497,7 @@ void SygusExtension::incrementCurrentSearchSize(TNode m)
           if( itt!=itc->second.d_search_terms[tn].end() ){
             for (const Node& t : itt->second)
             {
-              if (!options::sygusSymBreakLazy()
+              if (!options().datatypes.sygusSymBreakLazy
                   || (d_active_terms.find(t) != d_active_terms.end()
                       && !s.second.empty()))
               {
@@ -1598,7 +1605,7 @@ void SygusExtension::check()
       {
         isExc = false;
         //debugging : ensure fairness was properly handled
-        if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
+        if (options().datatypes.sygusFair == options::SygusFairMode::DT_SIZE)
         {
           Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog );
           Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz);
@@ -1617,7 +1624,7 @@ void SygusExtension::check()
 
         // register the search value ( prog -> progv ), this may invoke symmetry
         // breaking
-        if (!isExc && options::sygusSymBreakDynamic())
+        if (!isExc && options().datatypes.sygusSymBreakDynamic)
         {
           bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog);
           // check that it is unique up to theory-specific rewriting and
@@ -1793,15 +1800,15 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
 
 Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
 {
-  if (options::sygusFair() == options::SygusFairMode::NONE)
+  if (options().datatypes.sygusFair == options::SygusFairMode::NONE)
   {
     return Node::null();
   }
-  if (options::sygusAbortSize() != -1
-      && static_cast<int>(s) > options::sygusAbortSize())
+  if (options().datatypes.sygusAbortSize != -1
+      && static_cast<int>(s) > options().datatypes.sygusAbortSize)
   {
     std::stringstream ss;
-    ss << "Maximum term size (" << options::sygusAbortSize()
+    ss << "Maximum term size (" << options().datatypes.sygusAbortSize
        << ") for enumerative SyGuS exceeded.";
     throw LogicException(ss.str());
   }
diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index 23cd6430f..8c8d63231 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -34,7 +34,7 @@ ModelManager::ModelManager(Env& env, TheoryEngine& te, EqEngineManager& eem)
       d_modelEqualityEngine(nullptr),
       d_modelEqualityEngineAlloc(nullptr),
       d_model(new TheoryModel(
-          env, "DefaultModel", options::assignFunctionValues())),
+          env, "DefaultModel", options().theory.assignFunctionValues)),
       d_modelBuilder(nullptr),
       d_modelBuilt(false),
       d_modelBuiltSuccess(false)
@@ -118,7 +118,7 @@ void ModelManager::postProcessModel(bool incomplete)
   Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
   // model construction should always succeed unless lemmas were added
   AlwaysAssert(d_modelBuiltSuccess);
-  if (!options::produceModels())
+  if (!options().smt.produceModels)
   {
     return;
   }
diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp
index e856f1519..4f9a46181 100644
--- a/src/theory/quantifiers/candidate_rewrite_filter.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp
@@ -73,15 +73,17 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
   bool keep = true;
 
   // ----- check redundancy based on variables
-  if (options::sygusRewSynthFilterOrder()
-      || options::sygusRewSynthFilterNonLinear())
+  if (options().quantifiers.sygusRewSynthFilterOrder
+      || options().quantifiers.sygusRewSynthFilterNonLinear)
   {
-    bool nor = d_ss->checkVariables(bn,
-                                    options::sygusRewSynthFilterOrder(),
-                                    options::sygusRewSynthFilterNonLinear());
-    bool eqor = d_ss->checkVariables(beq_n,
-                                     options::sygusRewSynthFilterOrder(),
-                                     options::sygusRewSynthFilterNonLinear());
+    bool nor = d_ss->checkVariables(
+        bn,
+        options().quantifiers.sygusRewSynthFilterOrder,
+        options().quantifiers.sygusRewSynthFilterNonLinear);
+    bool eqor = d_ss->checkVariables(
+        beq_n,
+        options().quantifiers.sygusRewSynthFilterOrder,
+        options().quantifiers.sygusRewSynthFilterNonLinear);
     Trace("cr-filter-debug")
         << "Variables ok? : " << nor << " " << eqor << std::endl;
     if (eqor || nor)
@@ -118,7 +120,7 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
   }
 
   // ----- check rewriting redundancy
-  if (keep && options::sygusRewSynthFilterCong())
+  if (keep && options().quantifiers.sygusRewSynthFilterCong)
   {
     // When using sygus types, this filtering applies to the builtin versions
     // of n and eq_n. This means that we may filter out a rewrite rule for one
@@ -135,7 +137,7 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n)
     }
   }
 
-  if (keep && options::sygusRewSynthFilterMatch())
+  if (keep && options().quantifiers.sygusRewSynthFilterMatch)
   {
     // ----- check matchable
     // check whether the pair is matchable with a previous one
@@ -186,13 +188,13 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n)
     beq_n = d_tds->sygusToBuiltin(eq_n);
   }
   // ----- check rewriting redundancy
-  if (options::sygusRewSynthFilterCong())
+  if (options().quantifiers.sygusRewSynthFilterCong)
   {
     Trace("cr-filter-debug") << "Add rewrite pair..." << std::endl;
     Assert(!d_drewrite->areEqual(bn, beq_n));
     d_drewrite->addRewrite(bn, beq_n);
   }
-  if (options::sygusRewSynthFilterMatch())
+  if (options().quantifiers.sygusRewSynthFilterMatch)
   {
     // cache based on the builtin type
     TypeNode tn = bn.getType();
@@ -258,7 +260,7 @@ bool CandidateRewriteFilter::notify(Node s,
     Node nrs =
         nr.substitute(vars.begin(), vars.end(), esubs.begin(), esubs.end());
     bool areEqual = (nrs == d_curr_pair_rhs);
-    if (!areEqual && options::sygusRewSynthFilterCong())
+    if (!areEqual && options().quantifiers.sygusRewSynthFilterCong)
     {
       // if dynamic rewriter is available, consult it
       areEqual = d_drewrite->areEqual(nrs, d_curr_pair_rhs);
diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index 85e91fee3..163a49b8c 100644
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -166,7 +166,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
   }
   // compute how many bounds we will consider
   unsigned rmax = 1;
-  if (atom.getKind() == EQUAL && (pol || !options::cegqiModel()))
+  if (atom.getKind() == EQUAL && (pol || !options().quantifiers.cegqiModel))
   {
     rmax = 2;
   }
@@ -205,7 +205,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
     {
       // disequalities are either strict upper or lower bounds
       bool is_upper;
-      if (options::cegqiModel())
+      if (options().quantifiers.cegqiModel)
       {
         // disequality is a disjunction : only consider the bound in the
         // direction of the model
@@ -272,7 +272,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
     // take into account delta
     if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT)
     {
-      if (options::cegqiModel())
+      if (options().quantifiers.cegqiModel)
       {
         Node delta_coeff =
             nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1));
@@ -294,7 +294,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci,
         uval = rewrite(uval);
       }
     }
-    if (options::cegqiModel())
+    if (options().quantifiers.cegqiModel)
     {
       // just store bounds, will choose based on tighest bound
       unsigned index = isUpperBoundCTT(uires) ? 0 : 1;
@@ -329,15 +329,15 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
                                           Node pv,
                                           CegInstEffort effort)
 {
-  if (!options::cegqiModel())
+  if (!options().quantifiers.cegqiModel)
   {
     return false;
   }
   NodeManager* nm = NodeManager::currentNM();
-  bool use_inf =
-      d_type.isInteger() ? options::cegqiUseInfInt() : options::cegqiUseInfReal();
+  bool use_inf = d_type.isInteger() ? options().quantifiers.cegqiUseInfInt
+                                    : options().quantifiers.cegqiUseInfReal;
   bool upper_first = Random::getRandom().pickWithProb(0.5);
-  if (options::cegqiMinBounds())
+  if (options().quantifiers.cegqiMinBounds)
   {
     upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size();
   }
@@ -369,7 +369,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         {
           return true;
         }
-        else if (!options::cegqiMultiInst())
+        else if (!options().quantifiers.cegqiMultiInst)
         {
           return false;
         }
@@ -508,7 +508,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
         best_used[rr] = best;
         // if using cbqiMidpoint, only add the instance based on one bound if
         // the bound is non-strict
-        if (!options::cegqiMidpoint() || d_type.isInteger()
+        if (!options().quantifiers.cegqiMidpoint || d_type.isInteger()
             || d_mbp_vts_coeff[rr][1][best].isNull())
         {
           Node val = d_mbp_bounds[rr][best];
@@ -531,7 +531,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
             {
               return true;
             }
-            else if (!options::cegqiMultiInst())
+            else if (!options().quantifiers.cegqiMultiInst)
             {
               return false;
             }
@@ -562,13 +562,13 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       {
         return true;
       }
-      else if (!options::cegqiMultiInst())
+      else if (!options().quantifiers.cegqiMultiInst)
       {
         return false;
       }
     }
   }
-  if (options::cegqiMidpoint() && !d_type.isInteger())
+  if (options().quantifiers.cegqiMidpoint && !d_type.isInteger())
   {
     Node vals[2];
     bool bothBounds = true;
@@ -633,7 +633,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
       {
         return true;
       }
-      else if (!options::cegqiMultiInst())
+      else if (!options().quantifiers.cegqiMultiInst)
       {
         return false;
       }
@@ -642,7 +642,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
   // generally should not make it to this point, unless we are using a
   // non-monotonic selection function
 
-  if (!options::cegqiNopt())
+  if (!options().quantifiers.cegqiNopt)
   {
     // if not trying non-optimal bounds, return
     return false;
@@ -655,7 +655,8 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
     for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
     {
       if ((int)j != best_used[rr]
-          && (!options::cegqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull()))
+          && (!options().quantifiers.cegqiMidpoint
+              || d_mbp_vts_coeff[rr][1][j].isNull()))
       {
         Node val = getModelBasedProjectionValue(ci,
                                                 pv,
@@ -676,7 +677,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci,
           {
             return true;
           }
-          else if (!options::cegqiMultiInst())
+          else if (!options().quantifiers.cegqiMultiInst)
           {
             return false;
           }
@@ -748,7 +749,7 @@ bool ArithInstantiator::postProcessInstantiationForVariable(
         << "...bound type is : " << sf.d_props[index].d_type << std::endl;
     // intger division rounding up if from a lower bound
     if (sf.d_props[index].d_type == CEG_TT_UPPER
-        && options::cegqiRoundUpLowerLia())
+        && options().quantifiers.cegqiRoundUpLowerLia)
     {
       sf.d_subs[index] = nm->mkNode(
           PLUS,
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index d61dd2bd2..28314c730 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -629,7 +629,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf, unsigned i)
     // - the instantiator uses model values at this effort or
     //   if we are solving for a subfield of a datatype (is_sv), and
     // - the instantiator allows model values.
-    if ((options::cegqiMultiInst() || !hasTriedInstantiation(pv))
+    if ((options().quantifiers.cegqiMultiInst || !hasTriedInstantiation(pv))
         && (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
         && vinst->allowModelValue(this, sf, pv, d_effort))
     {
@@ -677,7 +677,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
                            << "], rep=" << pvr << ", instantiator is "
                            << vinst->identify() << std::endl;
   Node pv_value;
-  if (options::cegqiModel())
+  if (options().quantifiers.cegqiModel)
   {
     pv_value = getModelValue(pv);
     Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
@@ -730,7 +730,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
               {
                 return true;
               }
-              else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
+              else if (!options().quantifiers.cegqiMultiInst
+                       && hasTriedInstantiation(pv))
               {
                 return false;
               }
@@ -746,7 +747,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
       {
         return true;
       }
-      else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
+      else if (!options().quantifiers.cegqiMultiInst
+               && hasTriedInstantiation(pv))
       {
         return false;
       }
@@ -817,7 +819,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
                 {
                   return true;
                 }
-                else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
+                else if (!options().quantifiers.cegqiMultiInst
+                         && hasTriedInstantiation(pv))
                 {
                   return false;
                 }
@@ -866,7 +869,7 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
         {
           lits.insert(lit);
           Node plit;
-          if (options::cegqiRepeatLit() || !isSolvedAssertion(lit))
+          if (options().quantifiers.cegqiRepeatLit || !isSolvedAssertion(lit))
           {
             plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
           }
@@ -892,7 +895,8 @@ bool CegInstantiator::constructInstantiation(SolvedForm& sf,
                 {
                   return true;
                 }
-                else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
+                else if (!options().quantifiers.cegqiMultiInst
+                         && hasTriedInstantiation(pv))
                 {
                   return false;
                 }
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 339524d94..6340e2a2a 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -63,12 +63,12 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_small_const(d_small_const_multiplier)
 {
   d_check_vts_lemma_lc = false;
-  if (options::cegqiBv())
+  if (options().quantifiers.cegqiBv)
   {
     // if doing instantiation for BV, need the inverter class
     d_bv_invert.reset(new BvInverter);
   }
-  if (options::cegqiNestedQE())
+  if (options().quantifiers.cegqiNestedQE)
   {
     d_nestedQe.reset(new NestedQe(d_env));
   }
@@ -225,7 +225,8 @@ void InstStrategyCegqi::reset_round(Theory::Effort effort)
   }
 
   //refinement: only consider innermost active quantified formulas
-  if( options::cegqiInnermost() ){
+  if (options().quantifiers.cegqiInnermost)
+  {
     if( !d_children_quant.empty() && !d_active_quant.empty() ){
       Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
       std::vector< Node > ninner;
@@ -297,10 +298,14 @@ void InstStrategyCegqi::check(Theory::Effort e, QEffort quant_e)
 
 bool InstStrategyCegqi::checkComplete(IncompleteId& incId)
 {
-  if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
+  if ((!options().quantifiers.cegqiSat && d_cbqi_set_quant_inactive)
+      || d_incomplete_check)
+  {
     incId = IncompleteId::QUANTIFIERS_CEGQI;
     return false;
-  }else{
+  }
+  else
+  {
     return true;
   }
 }
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index d778a679e..2c6419de1 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -279,7 +279,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
                 Assert(eqt.getType() == tn);
                 registerPattern(eqt, tn);
                 if (isUniversalLessThan(eqt, t)
-                    || (options::conjectureUeeIntro()
+                    || (options().quantifiers.conjectureUeeIntro
                         && d_pattern_fun_sum[t] >= d_pattern_fun_sum[eqt]))
                 {
                   setUniversalRelevant(eqt);
@@ -344,12 +344,13 @@ bool ConjectureGenerator::needsCheck( Theory::Effort e ) {
 }
 
 bool ConjectureGenerator::hasEnumeratedUf( Node n ) {
-  if( options::conjectureGenGtEnum()>0 ){
+  if (options().quantifiers.conjectureGenGtEnum > 0)
+  {
     std::map< Node, bool >::iterator it = d_uf_enum.find( n.getOperator() );
     if( it==d_uf_enum.end() ){
       d_uf_enum[n.getOperator()] = true;
       std::vector< Node > lem;
-      getEnumeratePredUfTerm( n, options::conjectureGenGtEnum(), lem );
+      getEnumeratePredUfTerm(n, options().quantifiers.conjectureGenGtEnum, lem);
       if( !lem.empty() ){
         for (const Node& l : lem)
         {
@@ -665,7 +666,7 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
       std::vector< TypeNode > rt_types;
       std::map< TypeNode, std::map< int, std::vector< Node > > > conj_lhs;
       unsigned addedLemmas = 0;
-      unsigned maxDepth = options::conjectureGenMaxDepth();
+      unsigned maxDepth = options().quantifiers.conjectureGenMaxDepth;
       for( unsigned depth=1; depth<=maxDepth; depth++ ){
         Trace("sg-proc") << "Generate relevant LHS at depth " << depth << "..." << std::endl;
         Trace("sg-rel-term") << "Relevant terms of depth " << depth << " : " << std::endl;
@@ -676,7 +677,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
         while( d_tge.getNextTerm() ){
           //construct term
           Node nn = d_tge.getTerm();
-          if( !options::conjectureFilterCanonical() || considerTermCanon( nn, true ) ){
+          if (!options().quantifiers.conjectureFilterCanonical
+              || considerTermCanon(nn, true))
+          {
             rel_term_count++;
             Trace("sg-rel-term") << "*** Relevant term : ";
             d_tge.debugPrint( "sg-rel-term", "sg-rel-term-debug2" );
@@ -771,7 +774,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
               }
             }
             Trace("sg-gen-tg-debug") << "...done build substitutions for ground EQC" << std::endl;
-          }else{
+          }
+          else
+          {
             Trace("sg-gen-tg-debug") << "> not canonical : " << nn << std::endl;
           }
         }
@@ -827,7 +832,9 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
           //consider against all LHS up to depth
           if( rdepth==depth ){
             for( unsigned lhs_depth = 1; lhs_depth<=depth; lhs_depth++ ){
-              if( (int)addedLemmas<options::conjectureGenPerRound() ){
+              if ((int)addedLemmas
+                  < options().quantifiers.conjectureGenPerRound)
+              {
                 Trace("sg-proc") << "Consider conjectures at depth (" << lhs_depth << ", " << rdepth << ")..." << std::endl;
                 for( std::map< TypeNode, std::vector< Node > >::iterator it = conj_rhs.begin(); it != conj_rhs.end(); ++it ){
                   for( unsigned j=0; j<it->second.size(); j++ ){
@@ -840,11 +847,13 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
               }
             }
           }
-          if( (int)addedLemmas>=options::conjectureGenPerRound() ){
+          if ((int)addedLemmas >= options().quantifiers.conjectureGenPerRound)
+          {
             break;
           }
         }
-        if( (int)addedLemmas>=options::conjectureGenPerRound() ){
+        if ((int)addedLemmas >= options().quantifiers.conjectureGenPerRound)
+        {
           break;
         }
       }
@@ -887,7 +896,8 @@ void ConjectureGenerator::check(Theory::Effort e, QEffort quant_e)
 unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ) {
   if( !d_waiting_conjectures_lhs.empty() ){
     Trace("sg-proc") << "Generated " << d_waiting_conjectures_lhs.size() << " conjectures at depth " << ldepth << "/" << rdepth << "." << std::endl;
-    if( (int)addedLemmas<options::conjectureGenPerRound() ){
+    if ((int)addedLemmas < options().quantifiers.conjectureGenPerRound)
+    {
       /*
       std::vector< unsigned > indices;
       for( unsigned i=0; i<d_waiting_conjectures_lhs.size(); i++ ){
@@ -908,9 +918,14 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
           //we have determined a relevant subgoal
           Node lhs = d_waiting_conjectures_lhs[i];
           Node rhs = d_waiting_conjectures_rhs[i];
-          if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
+          if (options().quantifiers.conjectureFilterCanonical
+              && (getUniversalRepresentative(lhs) != lhs
+                  || getUniversalRepresentative(rhs) != rhs))
+          {
             //skip
-          }else{
+          }
+          else
+          {
             Trace("sg-engine") << "*** Consider conjecture : " << lhs << " == " << rhs << std::endl;
             Trace("sg-engine-debug") << "      score : " << d_waiting_conjectures_score[i] << std::endl;
             if( optStatsOnly() ){
@@ -942,7 +957,9 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in
                                     InferenceId::QUANTIFIERS_CONJ_GEN_SPLIT);
               d_qim.addPendingPhaseRequirement(rsg, false);
               addedLemmas++;
-              if( (int)addedLemmas>=options::conjectureGenPerRound() ){
+              if ((int)addedLemmas
+                  >= options().quantifiers.conjectureGenPerRound)
+              {
                 break;
               }
             }
@@ -1304,10 +1321,12 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
         return -1;
       }
     }
-    //check if canonical representation (should be, but for efficiency this is not guarenteed)
-    //if( options::conjectureFilterCanonical() && ( getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs )!=rhs ) ){
-    //  Trace("sg-cconj") << "  -> after processing, not canonical." << std::endl;
-    //  return -1;
+    // check if canonical representation (should be, but for efficiency this is
+    // not guarenteed) if( options().quantifiers.conjectureFilterCanonical && (
+    // getUniversalRepresentative( lhs )!=lhs || getUniversalRepresentative( rhs
+    // )!=rhs ) ){
+    //  Trace("sg-cconj") << "  -> after processing, not canonical." <<
+    //  std::endl; return -1;
     //}
 
     int score;
@@ -1315,7 +1334,8 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
 
     Trace("sg-cconj") << "Consider possible candidate conjecture : " << lhs << " == " << rhs << "?" << std::endl;
     //find witness for counterexample, if possible
-    if( options::conjectureFilterModel() ){
+    if (options().quantifiers.conjectureFilterModel)
+    {
       Assert(d_rel_pattern_var_sum.find(lhs) != d_rel_pattern_var_sum.end());
       Trace("sg-cconj-debug") << "Notify substitutions over " << d_rel_pattern_var_sum[lhs] << " variables." << std::endl;
       std::map< TNode, TNode > subs;
@@ -1342,7 +1362,9 @@ int ConjectureGenerator::considerCandidateConjecture( TNode lhs, TNode rhs ) {
       for( std::map< TNode, std::vector< TNode > >::iterator it = d_subs_confirmWitnessDomain.begin(); it != d_subs_confirmWitnessDomain.end(); ++it ){
         Trace("sg-cconj") << "     #witnesses for " << it->first << " : " << it->second.size() << std::endl;
       }
-    }else{
+    }
+    else
+    {
       score = 1;
     }
 
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index d2b0b0542..f6d245fd9 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -205,7 +205,7 @@ uint64_t HigherOrderTrigger::addInstantiations()
 
 bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
 {
-  if (options::hoMatching())
+  if (options().quantifiers.hoMatching)
   {
     // get substitution corresponding to m
     std::vector<TNode> vars;
@@ -342,7 +342,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
               // value at this argument position
               d_arg_vector[vnum][index].push_back(bv_at_index);
               d_arg_vector[vnum][index].push_back(itf->second);
-              if (!options::hoMatchingVarArgPriority())
+              if (!options().quantifiers.hoMatchingVarArgPriority)
               {
                 std::reverse(d_arg_vector[vnum][index].begin(),
                              d_arg_vector[vnum][index].end());
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp
index 30d223b2a..2c5dd73d1 100644
--- a/src/theory/quantifiers/equality_query.cpp
+++ b/src/theory/quantifiers/equality_query.cpp
@@ -51,7 +51,8 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
 {
   Assert(q.isNull() || q.getKind() == FORALL);
   Node r = d_qstate.getRepresentative(a);
-  if( options::finiteModelFind() ){
+  if (options().quantifiers.finiteModelFind)
+  {
     if( r.isConst() && quantifiers::TermUtil::containsUninterpretedConstant( r ) ){
       //map back from values assigned by model, if any
       if (d_model != nullptr)
@@ -72,7 +73,7 @@ Node EqualityQuery::getInternalRepresentative(Node a, Node q, size_t index)
     }
   }
   TypeNode v_tn = q.isNull() ? a.getType() : q[0][index].getType();
-  if (options::quantRepMode() == options::QuantRepMode::EE)
+  if (options().quantifiers.quantRepMode == options::QuantRepMode::EE)
   {
     int32_t score = getRepScore(r, q, index, v_tn);
     if (score >= 0)
@@ -166,23 +167,28 @@ Node EqualityQuery::getInstance(Node n,
 //-2 : invalid, -1 : undesired, otherwise : smaller the score, the better
 int32_t EqualityQuery::getRepScore(Node n, Node q, size_t index, TypeNode v_tn)
 {
-  if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){  //reject
+  if (options().quantifiers.cegqi && quantifiers::TermUtil::hasInstConstAttr(n))
+  {  // reject
     return -2;
-  }else if( !n.getType().isSubtypeOf( v_tn ) ){  //reject if incorrect type
+  }
+  else if (!n.getType().isSubtypeOf(v_tn))
+  {  // reject if incorrect type
     return -2;
-  }else if( options::instMaxLevel()!=-1 ){
+  }
+  else if (options().quantifiers.instMaxLevel != -1)
+  {
     //score prefer lowest instantiation level
     if( n.hasAttribute(InstLevelAttribute()) ){
       return n.getAttribute(InstLevelAttribute());
     }
-    return options::instLevelInputOnly() ? -1 : 0;
+    return options().quantifiers.instLevelInputOnly ? -1 : 0;
   }
-  else if (options::quantRepMode() == options::QuantRepMode::FIRST)
+  else if (options().quantifiers.quantRepMode == options::QuantRepMode::FIRST)
   {
     // score prefers earliest use of this term as a representative
     return d_rep_score.find(n) == d_rep_score.end() ? -1 : d_rep_score[n];
   }
-  Assert(options::quantRepMode() == options::QuantRepMode::DEPTH);
+  Assert(options().quantifiers.quantRepMode == options::QuantRepMode::DEPTH);
   return quantifiers::TermUtil::getTermDepth(n);
 }
 
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f47a71926..23f789f4e 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -152,7 +152,7 @@ bool Instantiate::addInstantiation(Node q,
                     << std::endl;
       bad_inst = true;
     }
-    else if (options::cegqi())
+    else if (options().quantifiers.cegqi)
     {
       Node icf = TermUtil::getInstConstAttr(terms[i]);
       if (!icf.isNull())
@@ -198,7 +198,7 @@ bool Instantiate::addInstantiation(Node q,
   // lead to very small gains).
 
   // check for positive entailment
-  if (options::instNoEntail())
+  if (options().quantifiers.instNoEntail)
   {
     // should check consistency of equality engine
     // (if not aborting on utility's reset)
@@ -216,7 +216,7 @@ bool Instantiate::addInstantiation(Node q,
   }
 
   // check based on instantiation level
-  if (options::instMaxLevel() != -1)
+  if (options().quantifiers.instMaxLevel != -1)
   {
     TermDb* tdb = d_treg.getTermDatabase();
     for (Node& t : terms)
@@ -362,7 +362,7 @@ bool Instantiate::addInstantiation(Node q,
       }
     }
   }
-  if (options::instMaxLevel() != -1)
+  if (options().quantifiers.instMaxLevel != -1)
   {
     if (doVts)
     {
@@ -447,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     // check whether we are still redundant
     bool success = false;
     // check entailment, only if option is set
-    if (options::instNoEntail())
+    if (options().quantifiers.instNoEntail)
     {
       Trace("inst-exp-fail") << "  check entailment" << std::endl;
       success = echeck->isEntailed(q[1], subs, false, true);
@@ -505,7 +505,7 @@ bool Instantiate::existsInstantiation(Node q,
                                       const std::vector<Node>& terms,
                                       bool modEq)
 {
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
@@ -593,7 +593,7 @@ Node Instantiate::getInstantiation(Node q,
 bool Instantiate::recordInstantiationInternal(Node q,
                                               const std::vector<Node>& terms)
 {
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     Trace("inst-add-debug")
         << "Adding into context-dependent inst trie" << std::endl;
@@ -612,7 +612,7 @@ bool Instantiate::recordInstantiationInternal(Node q,
 bool Instantiate::removeInstantiationInternal(Node q,
                                               const std::vector<Node>& terms)
 {
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     std::map<Node, CDInstMatchTrie*>::iterator it = d_c_inst_match_trie.find(q);
     if (it != d_c_inst_match_trie.end())
@@ -637,8 +637,7 @@ void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs) const
 void Instantiate::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node> >& tvecs)
 {
-
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     std::map<Node, CDInstMatchTrie*>::const_iterator it =
         d_c_inst_match_trie.find(q);
@@ -661,7 +660,7 @@ void Instantiate::getInstantiationTermVectors(
 void Instantiate::getInstantiationTermVectors(
     std::map<Node, std::vector<std::vector<Node> > >& insts)
 {
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     for (const auto& t : d_c_inst_match_trie)
     {
@@ -709,7 +708,7 @@ void Instantiate::notifyEndRound()
   }
   if (d_env.isOutputOn(options::OutputTag::INST))
   {
-    bool req = !options::printInstFull();
+    bool req = !options().printer.printInstFull;
     for (std::pair<const Node, uint32_t>& i : d_instDebugTemp)
     {
       Node name;
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index 1a42ec337..3e1a5b34c 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -99,21 +99,22 @@ void SygusInterpol::getIncludeCons(
     std::map<TypeNode, std::unordered_set<Node>>& result)
 {
   NodeManager* nm = NodeManager::currentNM();
-  Assert(options::produceInterpols() != options::ProduceInterpols::NONE);
+  Assert(options().smt.produceInterpols != options::ProduceInterpols::NONE);
   // ASSUMPTIONS
-  if (options::produceInterpols() == options::ProduceInterpols::ASSUMPTIONS)
+  if (options().smt.produceInterpols == options::ProduceInterpols::ASSUMPTIONS)
   {
     Node tmpAssumptions =
         (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
     expr::getOperatorsMap(tmpAssumptions, result);
   }
   // CONJECTURE
-  else if (options::produceInterpols() == options::ProduceInterpols::CONJECTURE)
+  else if (options().smt.produceInterpols
+           == options::ProduceInterpols::CONJECTURE)
   {
     expr::getOperatorsMap(conj, result);
   }
   // SHARED
-  else if (options::produceInterpols() == options::ProduceInterpols::SHARED)
+  else if (options().smt.produceInterpols == options::ProduceInterpols::SHARED)
   {
     // Get operators from axioms
     std::map<TypeNode, std::unordered_set<Node>> include_cons_axioms;
@@ -153,7 +154,7 @@ void SygusInterpol::getIncludeCons(
     }
   }
   // ALL
-  else if (options::produceInterpols() == options::ProduceInterpols::ALL)
+  else if (options().smt.produceInterpols == options::ProduceInterpols::ALL)
   {
     Node tmpAssumptions =
         (axioms.size() == 1 ? axioms[0] : nm->mkNode(kind::AND, axioms));
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 805f19b34..6c3f5e70b 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -73,15 +73,16 @@ SynthConjecture::SynthConjecture(Env& env,
       d_repair_index(0),
       d_guarded_stream_exc(false)
 {
-  if (options::sygusSymBreakPbe() || options::sygusUnifPbe())
+  if (options().datatypes.sygusSymBreakPbe
+      || options().quantifiers.sygusUnifPbe)
   {
     d_modules.push_back(d_ceg_pbe.get());
   }
-  if (options::sygusUnifPi() != options::SygusUnifPiMode::NONE)
+  if (options().quantifiers.sygusUnifPi != options::SygusUnifPiMode::NONE)
   {
     d_modules.push_back(d_ceg_cegisUnif.get());
   }
-  if (options::sygusCoreConnective())
+  if (options().quantifiers.sygusCoreConnective)
   {
     d_modules.push_back(d_sygus_ccore.get());
   }
@@ -202,10 +203,10 @@ void SynthConjecture::assign(Node q)
   Trace("cegqi") << "Base instantiation is :      " << d_base_inst << std::endl;
 
   // initialize the sygus constant repair utility
-  if (options::sygusRepairConst())
+  if (options().quantifiers.sygusRepairConst)
   {
     d_sygus_rconst->initialize(d_base_inst.negate(), d_candidates);
-    if (options::sygusConstRepairAbort())
+    if (options().quantifiers.sygusConstRepairAbort)
     {
       if (!d_sygus_rconst->isActive())
       {
@@ -337,7 +338,7 @@ bool SynthConjecture::doCheck()
   // sygusRepairConst  is true, we use a default scheme for trying to repair
   // constants here.
   bool doRepairConst =
-      options::sygusRepairConst() && !d_master->usingRepairConst();
+      options().quantifiers.sygusRepairConst && !d_master->usingRepairConst();
   if (doRepairConst)
   {
     // have we tried to repair the previous solution?
@@ -502,7 +503,7 @@ bool SynthConjecture::doCheck()
   }
 
   // if we trust the sampling we ran, we terminate now
-  if (options::cegisSample() == options::CegisSampleMode::TRUST)
+  if (options().quantifiers.cegisSample == options::CegisSampleMode::TRUST)
   {
     // we have that the current candidate passed a sample test
     // since we trust sampling in this mode, we assert there is no
@@ -565,7 +566,7 @@ bool SynthConjecture::doCheck()
 
   // now mark that we have a solution
   d_hasSolution = true;
-  if (options::sygusStream())
+  if (options().quantifiers.sygusStream)
   {
     // immediately print the current solution
     printAndContinueStream(terms, candidate_values);
@@ -805,10 +806,10 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out)
       bool is_unique_term = true;
 
       if (status != 0
-          && (options::sygusRewSynth()
+          && (options().quantifiers.sygusRewSynth
               || options().quantifiers.sygusQueryGen
                      != options::SygusQueryGenMode::NONE
-              || options::sygusFilterSolMode()
+              || options().quantifiers.sygusFilterSolMode
                      != options::SygusFilterSolMode::NONE))
       {
         Trace("cegqi-sol-debug") << "Run expression mining..." << std::endl;
@@ -819,7 +820,7 @@ void SynthConjecture::printSynthSolutionInternal(std::ostream& out)
           d_exprm[prog].reset(new ExpressionMinerManager(d_env));
           ExpressionMinerManager* emm = d_exprm[prog].get();
           emm->initializeSygus(
-              d_tds, d_candidates[i], options::sygusSamples(), true);
+              d_tds, d_candidates[i], options().quantifiers.sygusSamples, true);
           emm->initializeMinersForOptions();
           its = d_exprm.find(prog);
         }
@@ -989,7 +990,7 @@ bool SynthConjecture::getSynthSolutionsInternal(std::vector<Node>& sols,
           Trace("cegqi-inv-debug")
               << sf << " used template : " << templ << std::endl;
           // if it was not embedded into the grammar
-          if (!options::sygusTemplEmbedGrammar())
+          if (!options().quantifiers.sygusTemplEmbedGrammar)
           {
             TNode templa = d_templInfer->getTemplateArg(sf);
             // make the builtin version of the full solution
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index d11fb0b8d..5cefb4275 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -44,14 +44,15 @@ TermRegistry::TermRegistry(Env& env,
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {
-  if (options::sygus() || options::sygusInst())
+  if (options().quantifiers.sygus || options().quantifiers.sygusInst)
   {
     // must be constructed here since it is required for datatypes finistInit
     d_sygusTdb.reset(new TermDbSygus(env, qs));
   }
   Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
   Trace("quant-engine-debug")
-      << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
+      << "Initialize model, mbqi : " << options().quantifiers.mbqiMode
+      << std::endl;
 }
 
 void TermRegistry::finishInit(FirstOrderModel* fm,
@@ -69,7 +70,7 @@ void TermRegistry::presolve()
 {
   d_presolve = false;
   // add all terms to database
-  if (options::incrementalSolving() && !options::termDbCd())
+  if (options().base.incrementalSolving && !options().quantifiers.termDbCd)
   {
     Trace("quant-engine-proc")
         << "Add presolve cache " << d_presolveCache.size() << std::endl;
@@ -84,19 +85,20 @@ void TermRegistry::presolve()
 void TermRegistry::addTerm(Node n, bool withinQuant)
 {
   // don't add terms in quantifier bodies
-  if (withinQuant && !options::registerQuantBodyTerms())
+  if (withinQuant && !options().quantifiers.registerQuantBodyTerms)
   {
     return;
   }
-  if (options::incrementalSolving() && !options::termDbCd())
+  if (options().base.incrementalSolving && !options().quantifiers.termDbCd)
   {
     d_presolveCache.insert(n);
   }
   // only wait if we are doing incremental solving
-  if (!d_presolve || !options::incrementalSolving() || options::termDbCd())
+  if (!d_presolve || !options().base.incrementalSolving
+      || options().quantifiers.termDbCd)
   {
     d_termDb->addTerm(n);
-    if (d_sygusTdb.get() && options::sygusEvalUnfold())
+    if (d_sygusTdb.get() && options().quantifiers.sygusEvalUnfold)
     {
       d_sygusTdb->getEvalUnfold()->registerEvalTerm(n);
     }
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e0863f953..1098cd9fe 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -64,15 +64,15 @@ QuantifiersEngine::QuantifiersEngine(
       d_numInstRoundsLemma(0)
 {
   Trace("quant-init-debug")
-      << "Initialize model engine, mbqi : " << options::mbqiMode() << " "
-      << options::fmfBound() << std::endl;
+      << "Initialize model engine, mbqi : " << options().quantifiers.mbqiMode
+      << " " << options().quantifiers.fmfBound << std::endl;
   // Finite model finding requires specialized ways of building the model.
   // We require constructing the model here, since it is required for
   // initializing the CombinationEngine and the rest of quantifiers engine.
-  if (options::fmfBound() || options::stringExp()
-      || (options::finiteModelFind()
-          && (options::mbqiMode() == options::MbqiMode::FMC
-              || options::mbqiMode() == options::MbqiMode::TRUST)))
+  if (options().quantifiers.fmfBound || options().strings.stringExp
+      || (options().quantifiers.finiteModelFind
+          && (options().quantifiers.mbqiMode == options::MbqiMode::FMC
+              || options().quantifiers.mbqiMode == options::MbqiMode::TRUST)))
   {
     Trace("quant-init-debug") << "...make fmc builder." << std::endl;
     d_builder.reset(
@@ -168,14 +168,15 @@ void QuantifiersEngine::ppNotifyAssertions(
   Trace("quant-engine-proc")
       << "ppNotifyAssertions in QE, #assertions = " << assertions.size()
       << std::endl;
-  if (options::instLevelInputOnly() && options::instMaxLevel() != -1)
+  if (options().quantifiers.instLevelInputOnly
+      && options().quantifiers.instMaxLevel != -1)
   {
     for (const Node& a : assertions)
     {
       quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0);
     }
   }
-  if (options::sygus())
+  if (options().quantifiers.sygus)
   {
     quantifiers::SynthEngine* sye = d_qmodules->d_synth_e.get();
     for (const Node& a : assertions)
@@ -186,7 +187,7 @@ void QuantifiersEngine::ppNotifyAssertions(
   /* The SyGuS instantiation module needs a global view of all available
    * assertions to collect global terms that get added to each grammar.
    */
-  if (options::sygusInst())
+  if (options().quantifiers.sygusInst)
   {
     quantifiers::SygusInst* si = d_qmodules->d_sygus_inst.get();
     si->ppNotifyAssertions(assertions);
@@ -250,8 +251,9 @@ void QuantifiersEngine::check( Theory::Effort e ){
   d_qim.reset();
   bool setIncomplete = false;
   IncompleteId setIncompleteId = IncompleteId::QUANTIFIERS;
-  if (options::instMaxRounds() >= 0
-      && d_numInstRoundsLemma >= static_cast<uint32_t>(options::instMaxRounds()))
+  if (options().quantifiers.instMaxRounds >= 0
+      && d_numInstRoundsLemma
+             >= static_cast<uint32_t>(options().quantifiers.instMaxRounds))
   {
     needsCheck = false;
     setIncomplete = true;
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9844d13bc..cfa8f82cf 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -339,7 +339,7 @@ bool Theory::isLegalElimination(TNode x, TNode val)
   {
     return false;
   }
-  if (!options::produceModels() && !logicInfo().isQuantified())
+  if (!options().smt.produceModels && !logicInfo().isQuantified())
   {
     // Don't care about the model and logic is not quantified, we can eliminate.
     return true;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a186c05a0..03880bfbb 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -145,17 +145,17 @@ void TheoryEngine::finishInit()
   CVC5_FOR_EACH_THEORY;
 
   // Initialize the theory combination architecture
-  if (options::tcMode() == options::TcMode::CARE_GRAPH)
+  if (options().theory.tcMode == options::TcMode::CARE_GRAPH)
   {
     d_tc.reset(new CombinationCareGraph(d_env, *this, paraTheories));
   }
   else
   {
     Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
-                    << options::tcMode() << " not supported";
+                    << options().theory.tcMode << " not supported";
   }
   // create the relevance filter if any option requires it
-  if (options::relevanceFilter() || options::produceDifficulty())
+  if (options().theory.relevanceFilter || options().smt.produceDifficulty)
   {
     d_relManager.reset(new RelevanceManager(userContext(), Valuation(this)));
   }
@@ -247,7 +247,7 @@ TheoryEngine::TheoryEngine(Env& env)
     d_theoryOut[theoryId] = NULL;
   }
 
-  if (options::sortInference())
+  if (options().smt.sortInference)
   {
     d_sortInfer.reset(new SortInference(env));
   }
@@ -633,7 +633,7 @@ TheoryModel* TheoryEngine::getBuiltModel()
   Assert(d_tc != nullptr);
   // If this method was called, we should be in SAT mode, and produceModels
   // should be true.
-  AlwaysAssert(options::produceModels());
+  AlwaysAssert(options().smt.produceModels);
   if (!d_inSatMode)
   {
     // not available, perhaps due to interuption.
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index a5ec0867a..599e192f8 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -143,7 +143,7 @@ Node TheoryModel::getValue(TNode n) const
   }
   else if (nn.getKind() == kind::LAMBDA)
   {
-    if (options::condenseFunctionValues())
+    if (options().theory.condenseFunctionValues)
     {
       // normalize the body. Do not normalize the entire node, which
       // involves array normalization.
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index f50e7e0ee..71fe48de8 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -567,7 +567,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
     // finished traversing the equality engine
     TypeNode eqct = eqc.getType();
     // count the number of equivalence classes of sorts in finite model finding
-    if (options::finiteModelFind())
+    if (options().quantifiers.finiteModelFind)
     {
       if (eqct.isSort())
       {
@@ -660,7 +660,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
   // then the type enumerator for list of U should enumerate:
   //   nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
   // instead of enumerating (cons U3 nil).
-  if (options::finiteModelFind())
+  if (options().quantifiers.finiteModelFind)
   {
     tep.d_fixed_usort_card = true;
     for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
@@ -847,7 +847,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm)
       }
 #ifdef CVC5_ASSERTIONS
       bool isUSortFiniteRestricted = false;
-      if (options::finiteModelFind())
+      if (options().quantifiers.finiteModelFind)
       {
         isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
       }
@@ -1080,7 +1080,7 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m)
   }
   Assert(m != nullptr);
   // debug-check the model if the checkModels() is enabled.
-  if (options::debugCheckModels())
+  if (options().smt.debugCheckModels)
   {
     debugCheckModel(m);
   }
@@ -1258,7 +1258,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
     default_v = (*te);
   }
   ufmt.setDefaultValue(m, default_v);
-  bool condenseFuncValues = options::condenseFunctionValues();
+  bool condenseFuncValues = options().theory.condenseFunctionValues;
   if (condenseFuncValues)
   {
     ufmt.simplify();
@@ -1389,7 +1389,7 @@ struct sortTypeSize
 
 void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
 {
-  if (!options::assignFunctionValues())
+  if (!options().theory.assignFunctionValues)
   {
     return;
   }