From: Gereon Kremer <nafur42@gmail.com>
Date: Sat, 9 Oct 2021 15:19:15 +0000 (-0700)
Subject: Remove static accesses to options where EnvObj is used (#7330)
X-Git-Tag: cvc5-1.0.0~1097
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7990b5285c69e9a42aa430af5607b1c47b1602e6;p=cvc5.git

Remove static accesses to options where EnvObj is used (#7330)

This PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().
---

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 501e0c939..ce11c5718 100644
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -40,7 +40,7 @@ bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
                                 const TypeNode& grammarType,
                                 Node& abd)
 {
-  if (!options::produceAbducts())
+  if (!options().smt.produceAbducts)
   {
     const char* msg = "Cannot get abduct when produce-abducts options is off.";
     throw ModalException(msg);
@@ -129,7 +129,7 @@ bool AbductionSolver::getAbductInternal(const std::vector<Node>& axioms,
       }
 
       // if check abducts option is set, we check the correctness
-      if (options::checkAbducts())
+      if (options().smt.checkAbducts)
       {
         checkAbduct(axioms, abd);
       }
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index a9f7ce18e..77646c002 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -55,7 +55,7 @@ void Assertions::finishInit()
   // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
   // first, some user-context-dependent TNodes might still exist
   // with rc == 0.
-  if (options::produceAssertions() || options::incrementalSolving())
+  if (options().smt.produceAssertions || options().base.incrementalSolving)
   {
     // In the case of incremental solving, we appear to need these to
     // ensure the relevant Nodes remain live.
@@ -122,7 +122,7 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions,
 void Assertions::assertFormula(const Node& n)
 {
   ensureBoolean(n);
-  bool maybeHasFv = language::isLangSygus(options::inputLanguage());
+  bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
   addFormula(n, false, false, maybeHasFv);
 }
 
@@ -193,7 +193,7 @@ void Assertions::addFormula(TNode n,
       else
       {
         se << "Cannot process assertion with free variable.";
-        if (language::isLangSygus(options::inputLanguage()))
+        if (language::isLangSygus(options().base.inputLanguage))
         {
           // Common misuse of SyGuS is to use top-level assert instead of
           // constraint when defining the synthesis conjecture.
@@ -215,7 +215,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
   {
     // Global definitions are asserted at check-sat-time because we have to
     // make sure that they are always present
-    Assert(!language::isLangSygus(options::inputLanguage()));
+    Assert(!language::isLangSygus(options().base.inputLanguage));
     d_globalDefineFunLemmas->emplace_back(n);
   }
   else
@@ -223,14 +223,14 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
     // We don't permit functions-to-synthesize within recursive function
     // definitions currently. Thus, we should check for free variables if the
     // input language is SyGuS.
-    bool maybeHasFv = language::isLangSygus(options::inputLanguage());
+    bool maybeHasFv = language::isLangSygus(options().base.inputLanguage);
     addFormula(n, false, true, maybeHasFv);
   }
 }
 
 void Assertions::ensureBoolean(const Node& n)
 {
-  TypeNode type = n.getType(options::typeChecking());
+  TypeNode type = n.getType(options().expr.typeChecking);
   if (!type.isBoolean())
   {
     std::stringstream ss;
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index a4eacbfab..bdf807181 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -74,7 +74,7 @@ bool Preprocessor::process(Assertions& as)
   Assert(ap.size() != 0)
       << "Can only preprocess a non-empty list of assertions";
 
-  if (d_assertionsProcessed && options::incrementalSolving())
+  if (d_assertionsProcessed && options().base.incrementalSolving)
   {
     // TODO(b/1255): Substitutions in incremental mode should be managed with a
     // proper data structure.
@@ -91,7 +91,7 @@ bool Preprocessor::process(Assertions& as)
   // now, post-process the assertions
 
   // if incremental, compute which variables are assigned
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     d_ppContext->recordSymbolsInAssertions(ap.ref());
   }
@@ -121,7 +121,7 @@ Node Preprocessor::expandDefinitions(const Node& node,
   Trace("smt") << "SMT expandDefinitions(" << node << ")" << endl;
   // Substitute out any abstract values in node.
   Node n = d_absValues.substituteAbstractValues(node);
-  if (options::typeChecking())
+  if (options().expr.typeChecking)
   {
     // Ensure node is type-checked at this point.
     n.getType(true);
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index f269bfb53..73578f2cb 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -110,7 +110,7 @@ bool ProcessAssertions::apply(Assertions& as)
     return true;
   }
 
-  if (options::bvGaussElim())
+  if (options().bv.bvGaussElim)
   {
     d_passes["bv-gauss"]->apply(&assertions);
   }
@@ -140,34 +140,34 @@ bool ProcessAssertions::apply(Assertions& as)
 
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
-  if (options::globalNegate())
+  if (options().quantifiers.globalNegate)
   {
     // global negation of the formula
     d_passes["global-negate"]->apply(&assertions);
     as.flipGlobalNegated();
   }
 
-  if (options::nlExtPurify())
+  if (options().arith.nlExtPurify)
   {
     d_passes["nl-ext-purify"]->apply(&assertions);
   }
 
-  if (options::solveRealAsInt())
+  if (options().smt.solveRealAsInt)
   {
     d_passes["real-to-int"]->apply(&assertions);
   }
 
-  if (options::solveIntAsBV() > 0)
+  if (options().smt.solveIntAsBV > 0)
   {
     d_passes["int-to-bv"]->apply(&assertions);
   }
 
-  if (options::ackermann())
+  if (options().smt.ackermann)
   {
     d_passes["ackermann"]->apply(&assertions);
   }
 
-  if (options::bvAbstraction())
+  if (options().bv.bvAbstraction)
   {
     d_passes["bv-abstraction"]->apply(&assertions);
   }
@@ -176,33 +176,33 @@ bool ProcessAssertions::apply(Assertions& as)
 
   bool noConflict = true;
 
-  if (options::extRewPrep())
+  if (options().smt.extRewPrep)
   {
     d_passes["ext-rew-pre"]->apply(&assertions);
   }
 
   // Unconstrained simplification
-  if (options::unconstrainedSimp())
+  if (options().smt.unconstrainedSimp)
   {
     d_passes["rewrite"]->apply(&assertions);
     d_passes["unconstrained-simplifier"]->apply(&assertions);
   }
 
-  if (options::bvIntroducePow2())
+  if (options().bv.bvIntroducePow2)
   {
     d_passes["bv-intro-pow2"]->apply(&assertions);
   }
 
   // Lift bit-vectors of size 1 to bool
-  if (options::bitvectorToBool())
+  if (options().bv.bitvectorToBool)
   {
     d_passes["bv-to-bool"]->apply(&assertions);
   }
-  if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF)
+  if (options().smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
   {
     d_passes["bv-to-int"]->apply(&assertions);
   }
-  if (options::foreignTheoryRewrite())
+  if (options().smt.foreignTheoryRewrite)
   {
     d_passes["foreign-theory-rewrite"]->apply(&assertions);
   }
@@ -215,11 +215,11 @@ bool ProcessAssertions::apply(Assertions& as)
   d_passes["rewrite"]->apply(&assertions);
 
   // Convert non-top-level Booleans to bit-vectors of size 1
-  if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+  if (options().bv.boolToBitvector != options::BoolToBVMode::OFF)
   {
     d_passes["bool-to-bv"]->apply(&assertions);
   }
-  if (options::sepPreSkolemEmp())
+  if (options().sep.sepPreSkolemEmp)
   {
     d_passes["sep-skolem-emp"]->apply(&assertions);
   }
@@ -231,21 +231,21 @@ bool ProcessAssertions::apply(Assertions& as)
 
     // fmf-fun : assume admissible functions, applying preprocessing reduction
     // to FMF
-    if (options::fmfFunWellDefined())
+    if (options().quantifiers.fmfFunWellDefined)
     {
       d_passes["fun-def-fmf"]->apply(&assertions);
     }
   }
-  if (!options::stringLazyPreproc())
+  if (!options().strings.stringLazyPreproc)
   {
     d_passes["strings-eager-pp"]->apply(&assertions);
   }
-  if (options::sortInference() || options::ufssFairnessMonotone())
+  if (options().smt.sortInference || options().uf.ufssFairnessMonotone)
   {
     d_passes["sort-inference"]->apply(&assertions);
   }
 
-  if (options::pbRewrites())
+  if (options().arith.pbRewrites)
   {
     d_passes["pseudo-boolean-processor"]->apply(&assertions);
   }
@@ -274,18 +274,18 @@ bool ProcessAssertions::apply(Assertions& as)
                     << endl;
   dumpAssertions("post-simplify", as);
 
-  if (options::doStaticLearning())
+  if (options().smt.doStaticLearning)
   {
     d_passes["static-learning"]->apply(&assertions);
   }
   Debug("smt") << " assertions     : " << assertions.size() << endl;
 
-  if (options::learnedRewrite())
+  if (options().smt.learnedRewrite)
   {
     d_passes["learned-rewrite"]->apply(&assertions);
   }
 
-  if (options::earlyIteRemoval())
+  if (options().smt.earlyIteRemoval)
   {
     d_smtStats.d_numAssertionsPre += assertions.size();
     d_passes["ite-removal"]->apply(&assertions);
@@ -297,7 +297,7 @@ bool ProcessAssertions::apply(Assertions& as)
   }
 
   dumpAssertions("pre-repeat-simplify", as);
-  if (options::repeatSimp())
+  if (options().smt.repeatSimp)
   {
     Trace("smt-proc")
         << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
@@ -311,7 +311,7 @@ bool ProcessAssertions::apply(Assertions& as)
   }
   dumpAssertions("post-repeat-simplify", as);
 
-  if (options::ufHo())
+  if (options().uf.ufHo)
   {
     d_passes["ho-elim"]->apply(&assertions);
   }
@@ -334,7 +334,7 @@ bool ProcessAssertions::apply(Assertions& as)
   // notice that we do not apply substitutions as a last step here, since
   // the range of substitutions is not theory-preprocessed.
 
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  if (options().bv.bitblastMode == options::BitblastMode::EAGER)
   {
     d_passes["bv-eager-atoms"]->apply(&assertions);
   }
@@ -356,7 +356,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
 
     Trace("simplify") << "ProcessAssertions::simplify()" << endl;
 
-    if (options::simplificationMode() != options::SimplificationMode::NONE)
+    if (options().smt.simplificationMode != options::SimplificationMode::NONE)
     {
       // Perform non-clausal simplification
       PreprocessingPassResult res =
@@ -369,7 +369,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
       // We piggy-back off of the BackEdgesMap in the CircuitPropagator to
       // do the miplib trick.
       if (  // check that option is on
-          options::arithMLTrick() &&
+          options().arith.arithMLTrick &&
           // only useful in arith
           logicInfo().isTheoryEnabled(THEORY_ARITH) &&
           // we add new assertions and need this (in practice, this
@@ -389,8 +389,8 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
     Debug("smt") << " assertions     : " << assertions.size() << endl;
 
     // ITE simplification
-    if (options::doITESimp()
-        && (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
+    if (options().smt.doITESimp
+        && (d_simplifyAssertionsDepth <= 1 || options().smt.doITESimpOnRepeat))
     {
       PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions);
       if (res == PreprocessingPassResult::CONFLICT)
@@ -403,13 +403,14 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
     Debug("smt") << " assertions     : " << assertions.size() << endl;
 
     // Unconstrained simplification
-    if (options::unconstrainedSimp())
+    if (options().smt.unconstrainedSimp)
     {
       d_passes["unconstrained-simplifier"]->apply(&assertions);
     }
 
-    if (options::repeatSimp()
-        && options::simplificationMode() != options::SimplificationMode::NONE)
+    if (options().smt.repeatSimp
+        && options().smt.simplificationMode
+               != options::SimplificationMode::NONE)
     {
       PreprocessingPassResult res =
           d_passes["non-clausal-simp"]->apply(&assertions);
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 4759008dc..7f024c289 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -68,10 +68,11 @@ PfManager::PfManager(Env& env)
       env,
       d_pppg.get(),
       nullptr,
-      options::proofFormatMode() != options::ProofFormatMode::ALETHE));
+      options().proof.proofFormatMode != options::ProofFormatMode::ALETHE));
 
   // add rules to eliminate here
-  if (options::proofGranularityMode() != options::ProofGranularityMode::OFF)
+  if (options().proof.proofGranularityMode
+      != options::ProofGranularityMode::OFF)
   {
     d_pfpp->setEliminateRule(PfRule::MACRO_SR_EQ_INTRO);
     d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
@@ -80,12 +81,12 @@ PfManager::PfManager(Env& env)
     d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST);
     d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION);
     d_pfpp->setEliminateRule(PfRule::MACRO_ARITH_SCALE_SUM_UB);
-    if (options::proofGranularityMode()
+    if (options().proof.proofGranularityMode
         != options::ProofGranularityMode::REWRITE)
     {
       d_pfpp->setEliminateRule(PfRule::SUBS);
       d_pfpp->setEliminateRule(PfRule::REWRITE);
-      if (options::proofGranularityMode()
+      if (options().proof.proofGranularityMode
           != options::ProofGranularityMode::THEORY_REWRITE)
       {
         // this eliminates theory rewriting steps with finer-grained DSL rules
@@ -160,8 +161,8 @@ void PfManager::printProof(std::ostream& out,
   std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as);
   // if we are in incremental mode, we don't want to invalidate the proof
   // nodes in fp, since these may be reused in further check-sat calls
-  if (options::incrementalSolving()
-      && options::proofFormatMode() != options::ProofFormatMode::NONE)
+  if (options().base.incrementalSolving
+      && options().proof.proofFormatMode != options::ProofFormatMode::NONE)
   {
     fp = d_pnm->clone(fp);
   }
@@ -169,18 +170,18 @@ void PfManager::printProof(std::ostream& out,
   // TODO (proj #37) according to the proof format, print the proof node
 
   // according to the proof format, post process and print the proof node
-  if (options::proofFormatMode() == options::ProofFormatMode::DOT)
+  if (options().proof.proofFormatMode == options::ProofFormatMode::DOT)
   {
     proof::DotPrinter dotPrinter;
     dotPrinter.print(out, fp.get());
   }
-  else if (options::proofFormatMode() == options::ProofFormatMode::ALETHE)
+  else if (options().proof.proofFormatMode == options::ProofFormatMode::ALETHE)
   {
     proof::AletheNodeConverter anc;
     proof::AletheProofPostprocess vpfpp(d_pnm.get(), anc);
     vpfpp.process(fp);
   }
-  else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
+  else if (options().proof.proofFormatMode == options::ProofFormatMode::TPTP)
   {
     out << "% SZS output start Proof for " << options().driver.filename
         << std::endl;
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index d6a5f7652..adc15ca2c 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -1207,7 +1207,8 @@ ProofPostproccess::ProofPostproccess(Env& env,
                                      bool updateScopedAssumptions)
     : d_cb(env, pppg, rdb, updateScopedAssumptions),
       // the update merges subproofs
-      d_updater(env.getProofNodeManager(), d_cb, options::proofPpMerge()),
+      d_updater(
+          env.getProofNodeManager(), d_cb, env.getOptions().proof.proofPpMerge),
       d_finalCb(env.getProofNodeManager()),
       d_finalizer(env.getProofNodeManager(), d_finalCb)
 {
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 9452081c9..becfd1466 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -64,7 +64,7 @@ void SmtEngineState::notifyCheckSat(bool hasAssumptions)
 {
   // process the pending pops
   doPendingPops();
-  if (d_queryMade && !options::incrementalSolving())
+  if (d_queryMade && !options().base.incrementalSolving)
   {
     throw ModalException(
         "Cannot make multiple queries unless "
@@ -157,7 +157,7 @@ void SmtEngineState::shutdown()
 {
   doPendingPops();
 
-  while (options::incrementalSolving() && userContext()->getLevel() > 1)
+  while (options().base.incrementalSolving && userContext()->getLevel() > 1)
   {
     internalPop(true);
   }
@@ -171,7 +171,7 @@ void SmtEngineState::cleanup()
 
 void SmtEngineState::userPush()
 {
-  if (!options::incrementalSolving())
+  if (!options().base.incrementalSolving)
   {
     throw ModalException(
         "Cannot push when not solving incrementally (use --incremental)");
@@ -189,7 +189,7 @@ void SmtEngineState::userPush()
 
 void SmtEngineState::userPop()
 {
-  if (!options::incrementalSolving())
+  if (!options().base.incrementalSolving)
   {
     throw ModalException(
         "Cannot pop when not solving incrementally (use --incremental)");
@@ -249,7 +249,7 @@ void SmtEngineState::internalPush()
   Assert(d_fullyInited);
   Trace("smt") << "SmtEngineState::internalPush()" << std::endl;
   doPendingPops();
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     // notifies the SolverEngine to process the assertions immediately
     d_slv.notifyPushPre();
@@ -263,7 +263,7 @@ void SmtEngineState::internalPop(bool immediate)
 {
   Assert(d_fullyInited);
   Trace("smt") << "SmtEngineState::internalPop()" << std::endl;
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     ++d_pendingPops;
   }
@@ -276,7 +276,7 @@ void SmtEngineState::internalPop(bool immediate)
 void SmtEngineState::doPendingPops()
 {
   Trace("smt") << "SmtEngineState::doPendingPops()" << std::endl;
-  Assert(d_pendingPops == 0 || options::incrementalSolving());
+  Assert(d_pendingPops == 0 || options().base.incrementalSolving);
   // check to see if a postsolve() is pending
   if (d_needPostsolve)
   {
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 65ede41b8..eb6073fbe 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -178,7 +178,7 @@ void SygusSolver::assertSygusInvConstraint(Node inv,
 
 Result SygusSolver::checkSynth(Assertions& as)
 {
-  if (options::incrementalSolving())
+  if (options().base.incrementalSolving)
   {
     // TODO (project #7)
     throw ModalException(
@@ -225,7 +225,7 @@ Result SygusSolver::checkSynth(Assertions& as)
   Result r = d_smtSolver.checkSatisfiability(as, query, false);
 
   // Check that synthesis solutions satisfy the conjecture
-  if (options::checkSynthSol()
+  if (options().smt.checkSynthSol
       && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
   {
     checkSynthSolution(as);
diff --git a/src/theory/quantifiers/ematching/inst_strategy.cpp b/src/theory/quantifiers/ematching/inst_strategy.cpp
index 644fba6f1..b96c378da 100644
--- a/src/theory/quantifiers/ematching/inst_strategy.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy.cpp
@@ -37,12 +37,13 @@ std::string InstStrategy::identify() const { return std::string("Unknown"); }
 
 options::UserPatMode InstStrategy::getInstUserPatMode() const
 {
-  if (options::userPatternsQuant() == options::UserPatMode::INTERLEAVE)
+  if (options().quantifiers.userPatternsQuant
+      == options::UserPatMode::INTERLEAVE)
   {
     return d_qstate.getInstRounds() % 2 == 0 ? options::UserPatMode::USE
                                              : options::UserPatMode::RESORT;
   }
-  return options::userPatternsQuant();
+  return options().quantifiers.userPatternsQuant;
 }
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 8da91ec57..30be83ecc 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -74,12 +74,15 @@ InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
     : InstStrategy(env, td, qs, qim, qr, tr), d_quant_rel(qrlv)
 {
   //how to select trigger terms
-  d_tr_strategy = options::triggerSelMode();
+  d_tr_strategy = options().quantifiers.triggerSelMode;
   //whether to select new triggers during the search
-  if( options::incrementTriggers() ){
+  if (options().quantifiers.incrementTriggers)
+  {
     d_regenerate_frequency = 3;
     d_regenerate = true;
-  }else{
+  }
+  else
+  {
     d_regenerate_frequency = 1;
     d_regenerate = false;
   }
@@ -157,7 +160,8 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
       }
     }
   }
-  if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
+  if (options().quantifiers.triggerActiveSelMode
+      != options::TriggerActiveSelMode::ALL)
   {
     int max_score = -1;
     Trigger* max_trigger = nullptr;
@@ -167,7 +171,8 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
     {
       Trigger* t = it->first;
       int score = t->getActiveScore();
-      if (options::triggerActiveSelMode() == options::TriggerActiveSelMode::MIN)
+      if (options().quantifiers.triggerActiveSelMode
+          == options::TriggerActiveSelMode::MIN)
       {
         if (score >= 0 && (score < max_score || max_score < 0))
         {
@@ -222,7 +227,8 @@ InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
         break;
       }
     }
-    if (d_qstate.isInConflict() || (hasInst && options::multiTriggerPriority()))
+    if (d_qstate.isInConflict()
+        || (hasInst && options().quantifiers.multiTriggerPriority))
     {
       break;
     }
@@ -243,7 +249,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
 
   // then, group them to make triggers
   unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
-  unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
+  unsigned rmax = options().quantifiers.multiTriggerWhenSingle ? 1 : rmin;
   for (unsigned r = rmin; r <= rmax; r++)
   {
     std::vector<Node> patTerms;
@@ -261,7 +267,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     }
     Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
     // sort terms based on relevance
-    if (options::relevantTriggers())
+    if (options().quantifiers.relevantTriggers)
     {
       Assert(d_quant_rel);
       sortQuantifiersForSymbol sqfs;
@@ -305,7 +311,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
       // exist
       if (!d_patTerms[0][f].empty())
       {
-        if (options::multiTriggerWhenSingle())
+        if (options().quantifiers.multiTriggerWhenSingle)
         {
           Trace("multi-trigger-debug")
               << "Resort to choosing multi-triggers..." << std::endl;
@@ -350,7 +356,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
     {
       // check if similar patterns exist, and if so, add them additionally
       unsigned nqfs_curr = 0;
-      if (options::relevantTriggers())
+      if (options().quantifiers.relevantTriggers)
       {
         nqfs_curr =
             d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
@@ -361,7 +367,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
              && d_is_single_trigger[patTerms[index]])
       {
         success = false;
-        if (!options::relevantTriggers()
+        if (!options().quantifiers.relevantTriggers
             || d_quant_rel->getNumQuantifiersForSymbol(
                    patTerms[index].getOperator())
                    <= nqfs_curr)
@@ -392,12 +398,12 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
   // strategy d_tr_strategy
   d_patTerms[0][f].clear();
   d_patTerms[1][f].clear();
-  bool ntrivTriggers = options::relationalTriggers();
+  bool ntrivTriggers = options().quantifiers.relationalTriggers;
   std::vector<Node> patTermsF;
   std::map<Node, inst::TriggerTermInfo> tinfo;
   NodeManager* nm = NodeManager::currentNM();
   // well-defined function: can assume LHS is only pattern
-  if (options::quantFunWellDefined())
+  if (options().quantifiers.quantFunWellDefined)
   {
     Node hd = QuantAttributes::getFunDefHead(f);
     if (!hd.isNull())
@@ -485,7 +491,7 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
     // quantifier elimination.
     QAttributes qa;
     QuantAttributes::computeQuantAttributes(f, qa);
-    if (options::partialTriggers() && qa.isStandard())
+    if (options().quantifiers.partialTriggers && qa.isStandard())
     {
       std::vector<Node> vcs[2];
       for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
@@ -533,11 +539,12 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
         Assert(TriggerTermInfo::isAtomicTrigger(pat));
         if (pat.getType().isBoolean() && rpoleq.isNull())
         {
-          if (options::literalMatchMode() == options::LiteralMatchMode::USE)
+          if (options().quantifiers.literalMatchMode
+              == options::LiteralMatchMode::USE)
           {
             pat = pat.eqNode(nm->mkConst(rpol == -1)).negate();
           }
-          else if (options::literalMatchMode()
+          else if (options().quantifiers.literalMatchMode
                    != options::LiteralMatchMode::NONE)
           {
             pat = pat.eqNode(nm->mkConst(rpol == 1));
@@ -548,7 +555,8 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
           Assert(!rpoleq.isNull());
           if (rpol == -1)
           {
-            if (options::literalMatchMode() != options::LiteralMatchMode::NONE)
+            if (options().quantifiers.literalMatchMode
+                != options::LiteralMatchMode::NONE)
             {
               // all equivalence classes except rpoleq
               pat = pat.eqNode(rpoleq).negate();
@@ -556,7 +564,8 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
           }
           else if (rpol == 1)
           {
-            if (options::literalMatchMode() == options::LiteralMatchMode::AGG)
+            if (options().quantifiers.literalMatchMode
+                == options::LiteralMatchMode::AGG)
             {
               // only equivalence class rpoleq
               pat = pat.eqNode(rpoleq);
@@ -603,7 +612,9 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
 
 void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
   d_pat_to_mpat[pat] = mpat;
-  unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
+  unsigned num_vars = options().quantifiers.partialTriggers
+                          ? d_num_trigger_vars[q]
+                          : q[0].getNumChildren();
   if (num_fv == num_vars)
   {
     d_patTerms[0][q].push_back( pat );
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index 1f7d7f37b..5506f9e1d 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -45,14 +45,15 @@ InstantiationEngine::InstantiationEngine(Env& env,
       d_trdb(d_env, qs, qim, qr, tr),
       d_quant_rel(nullptr)
 {
-  if (options::relevantTriggers())
+  if (options().quantifiers.relevantTriggers)
   {
     d_quant_rel.reset(new quantifiers::QuantRelevance(env));
   }
-  if (options::eMatching()) {
+  if (options().quantifiers.eMatching)
+  {
     // these are the instantiation strategies for E-matching
     // user-provided patterns
-    if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
+    if (options().quantifiers.userPatternsQuant != options::UserPatMode::IGNORE)
     {
       d_isup.reset(
           new InstStrategyUserPatterns(d_env, d_trdb, qs, qim, qr, tr));
@@ -202,7 +203,7 @@ bool InstantiationEngine::checkCompleteFor( Node q ) {
 
 void InstantiationEngine::checkOwnership(Node q)
 {
-  if (options::userPatternsQuant() == options::UserPatMode::STRICT
+  if (options().quantifiers.userPatternsQuant == options::UserPatMode::STRICT
       && q.getNumChildren() == 3)
   {
     //if strict triggers, take ownership of this quantified formula
diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp
index b75c523ae..ff02e5f3e 100644
--- a/src/theory/quantifiers/ematching/trigger.cpp
+++ b/src/theory/quantifiers/ematching/trigger.cpp
@@ -96,9 +96,12 @@ Trigger::Trigger(Env& env,
       ++(stats.d_simple_triggers);
     }
   }else{
-    if( options::multiTriggerCache() ){
+    if (options().quantifiers.multiTriggerCache)
+    {
       d_mg = new InstMatchGeneratorMulti(this, q, d_nodes);
-    }else{
+    }
+    else
+    {
       d_mg = InstMatchGenerator::mkInstMatchGeneratorMulti(this, q, d_nodes);
     }
     if (Trace.isOn("multi-trigger"))
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index a8ad07734..6e1fb9cc9 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -57,9 +57,12 @@ bool ModelEngine::needsCheck( Theory::Effort e ) {
 
 QuantifiersModule::QEffort ModelEngine::needsModel(Theory::Effort e)
 {
-  if( options::mbqiInterleave() ){
+  if (options().quantifiers.mbqiInterleave)
+  {
     return QEFFORT_STANDARD;
-  }else{
+  }
+  else
+  {
     return QEFFORT_MODEL;
   }
 }
@@ -70,7 +73,8 @@ void ModelEngine::reset_round( Theory::Effort e ) {
 void ModelEngine::check(Theory::Effort e, QEffort quant_e)
 {
   bool doCheck = false;
-  if( options::mbqiInterleave() ){
+  if (options().quantifiers.mbqiInterleave)
+  {
     doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
   }
   if( !doCheck ){
@@ -139,7 +143,8 @@ void ModelEngine::registerQuantifier( Node f ){
         if (!d_env.isFiniteType(tn))
         {
           if( tn.isInteger() ){
-            if( !options::fmfBound() ){
+            if (!options().quantifiers.fmfBound)
+            {
               canHandle = false;
             }
           }else{
@@ -211,9 +216,11 @@ int ModelEngine::checkModel(){
 
   Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
   // FMC uses two sub-effort levels
-  int e_max = options::mbqiMode() == options::MbqiMode::FMC
-                  ? 2
-                  : (options::mbqiMode() == options::MbqiMode::TRUST ? 0 : 1);
+  int e_max =
+      options().quantifiers.mbqiMode == options::MbqiMode::FMC
+          ? 2
+          : (options().quantifiers.mbqiMode == options::MbqiMode::TRUST ? 0
+                                                                        : 1);
   for( int e=0; e<e_max; e++) {
     d_incompleteQuants.clear();
     for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
@@ -292,7 +299,10 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
         int triedLemmas = 0;
         int addedLemmas = 0;
         Instantiate* inst = d_qim.getInstantiate();
-        while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+        while (
+            !riter.isFinished()
+            && (addedLemmas == 0 || !options().quantifiers.fmfOneInstPerRound))
+        {
           //instantiation was not shown to be true, construct the match
           InstMatch m( f );
           for (unsigned i = 0; i < riter.getNumTerms(); i++)
@@ -365,7 +375,7 @@ bool ModelEngine::shouldProcess(Node q)
     return false;
   }
   // if finite model finding or fmf bound is on, we process everything
-  if (options::finiteModelFind() || options::fmfBound())
+  if (options().quantifiers.finiteModelFind || options().quantifiers.fmfBound)
   {
     return true;
   }
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp
index 39af9c2c9..bdf689581 100644
--- a/src/theory/quantifiers/quantifiers_state.cpp
+++ b/src/theory/quantifiers/quantifiers_state.cpp
@@ -30,12 +30,14 @@ QuantifiersState::QuantifiersState(Env& env,
       d_logicInfo(logicInfo)
 {
   // allow theory combination to go first, once initially
-  d_ierCounter = options::instWhenTcFirst() ? 0 : 1;
+  d_ierCounter = options().quantifiers.instWhenTcFirst ? 0 : 1;
   d_ierCounterc = d_ierCounter;
   d_ierCounterLc = 0;
   d_ierCounterLastLc = 0;
-  d_instWhenPhase =
-      1 + (options::instWhenPhase() < 1 ? 1 : options::instWhenPhase());
+  d_instWhenPhase = 1
+                    + (options().quantifiers.instWhenPhase < 1
+                           ? 1
+                           : options().quantifiers.instWhenPhase);
 }
 
 void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
@@ -45,7 +47,7 @@ void QuantifiersState::incrementInstRoundCounters(Theory::Effort e)
     // increment if a last call happened, we are not strictly enforcing
     // interleaving, or already were in phase
     if (d_ierCounterLastLc != d_ierCounterLc
-        || !options::instWhenStrictInterleave()
+        || !options().quantifiers.instWhenStrictInterleave
         || d_ierCounter % d_instWhenPhase != 0)
     {
       d_ierCounter = d_ierCounter + 1;
@@ -65,28 +67,31 @@ bool QuantifiersState::getInstWhenNeedsCheck(Theory::Effort e) const
                         << ", " << d_ierCounterLc << std::endl;
   // determine if we should perform check, based on instWhenMode
   bool performCheck = false;
-  if (options::instWhenMode() == options::InstWhenMode::FULL)
+  if (options().quantifiers.instWhenMode == options::InstWhenMode::FULL)
   {
     performCheck = (e >= Theory::EFFORT_FULL);
   }
-  else if (options::instWhenMode() == options::InstWhenMode::FULL_DELAY)
+  else if (options().quantifiers.instWhenMode
+           == options::InstWhenMode::FULL_DELAY)
   {
     performCheck = (e >= Theory::EFFORT_FULL) && !d_valuation.needCheck();
   }
-  else if (options::instWhenMode() == options::InstWhenMode::FULL_LAST_CALL)
+  else if (options().quantifiers.instWhenMode
+           == options::InstWhenMode::FULL_LAST_CALL)
   {
     performCheck =
         ((e == Theory::EFFORT_FULL && d_ierCounter % d_instWhenPhase != 0)
          || e == Theory::EFFORT_LAST_CALL);
   }
-  else if (options::instWhenMode()
+  else if (options().quantifiers.instWhenMode
            == options::InstWhenMode::FULL_DELAY_LAST_CALL)
   {
     performCheck = ((e == Theory::EFFORT_FULL && !d_valuation.needCheck()
                      && d_ierCounter % d_instWhenPhase != 0)
                     || e == Theory::EFFORT_LAST_CALL);
   }
-  else if (options::instWhenMode() == options::InstWhenMode::LAST_CALL)
+  else if (options().quantifiers.instWhenMode
+           == options::InstWhenMode::LAST_CALL)
   {
     performCheck = (e >= Theory::EFFORT_LAST_CALL);
   }
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index ad9da816b..33cfc09d3 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -110,7 +110,8 @@ void CegSingleInv::initialize(Node q)
   {
     // We are fully single invocation, set single invocation if we haven't
     // disabled single invocation techniques.
-    if (options::cegqiSingleInvMode() != options::CegqiSingleInvMode::NONE)
+    if (options().quantifiers.cegqiSingleInvMode
+        != options::CegqiSingleInvMode::NONE)
     {
       d_single_invocation = true;
     }
@@ -122,7 +123,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
   Trace("sygus-si-debug") << "Single invocation: finish init" << std::endl;
   // do not do single invocation if grammar is restricted and
   // options::CegqiSingleInvMode::ALL is not enabled
-  if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE
+  if (options().quantifiers.cegqiSingleInvMode
+          == options::CegqiSingleInvMode::USE
       && d_single_invocation && syntaxRestricted)
   {
     d_single_invocation = false;
@@ -134,7 +136,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted)
   {
     d_single_inv = Node::null();
     Trace("sygus-si") << "Formula is not single invocation." << std::endl;
-    if (options::cegqiSingleInvAbort())
+    if (options().quantifiers.cegqiSingleInvAbort)
     {
       std::stringstream ss;
       ss << "Property is not handled by single invocation." << std::endl;
@@ -444,20 +446,20 @@ Node CegSingleInv::reconstructToSyntax(Node s,
 
   // reconstruct the solution into sygus if necessary
   reconstructed = 0;
-  if (options::cegqiSingleInvReconstruct()
+  if (options().quantifiers.cegqiSingleInvReconstruct
           != options::CegqiSingleInvRconsMode::NONE
       && !dt.getSygusAllowAll() && !stn.isNull() && rconsSygus)
   {
     int64_t enumLimit = -1;
-    if (options::cegqiSingleInvReconstruct()
+    if (options().quantifiers.cegqiSingleInvReconstruct
         == options::CegqiSingleInvRconsMode::TRY)
     {
       enumLimit = 0;
     }
-    else if (options::cegqiSingleInvReconstruct()
+    else if (options().quantifiers.cegqiSingleInvReconstruct
              == options::CegqiSingleInvRconsMode::ALL_LIMIT)
     {
-      enumLimit = options::cegqiSingleInvReconstructLimit();
+      enumLimit = options().quantifiers.cegqiSingleInvReconstructLimit;
     }
     sol = d_srcons->reconstructSolution(s, stn, reconstructed, enumLimit);
     if (reconstructed == 1)
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 688d66cc3..c8e14e4bd 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -57,12 +57,13 @@ bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates)
   }
 
   // assign the cegis sampler if applicable
-  if (options::cegisSample() != options::CegisSampleMode::NONE)
+  if (options().quantifiers.cegisSample != options::CegisSampleMode::NONE)
   {
     Trace("cegis-sample") << "Initialize sampler for " << d_base_body << "..."
                           << std::endl;
     TypeNode bt = d_base_body.getType();
-    d_cegis_sampler.initialize(bt, d_base_vars, options::sygusSamples());
+    d_cegis_sampler.initialize(
+        bt, d_base_vars, options().quantifiers.sygusSamples);
   }
   return processInitialize(conj, n, candidates);
 }
@@ -83,8 +84,8 @@ bool Cegis::processInitialize(Node conj,
     Trace("cegis") << "...register enumerator " << candidates[i];
     // We use symbolic constants if we are doing repair constants or if the
     // grammar construction was not simple.
-    if (options::sygusRepairConst()
-        || options::sygusGrammarConsMode()
+    if (options().quantifiers.sygusRepairConst
+        || options().quantifiers.sygusGrammarConsMode
                != options::SygusGrammarConsMode::SIMPLE)
     {
       TypeNode ctn = candidates[i].getType();
@@ -173,7 +174,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     }
   }
   // we only do evaluation unfolding for passive enumerators
-  bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
+  bool doEvalUnfold =
+      (doGen && options().quantifiers.sygusEvalUnfold) || d_usingSymCons;
   if (doEvalUnfold)
   {
     Trace("sygus-engine") << "  *** Do evaluation unfolding..." << std::endl;
@@ -243,7 +245,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     }
   }
   // if we are using grammar-based repair
-  if (d_usingSymCons && options::sygusRepairConst())
+  if (d_usingSymCons && options().quantifiers.sygusRepairConst)
   {
     SygusRepairConst* src = d_parent->getRepairConst();
     Assert(src != nullptr);
@@ -302,7 +304,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     return false;
   }
 
-  if (options::cegisSample() != options::CegisSampleMode::NONE
+  if (options().quantifiers.cegisSample != options::CegisSampleMode::NONE
       && !addedEvalLemmas)
   {
     // if we didn't add a lemma, trying sampling to add a refinement lemma
@@ -673,7 +675,8 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
           Trace("sygus-engine") << "  *** Refine by sampling" << std::endl;
           addRefinementLemma(rlem);
           // if trust, we are not interested in sending out refinement lemmas
-          if (options::cegisSample() != options::CegisSampleMode::TRUST)
+          if (options().quantifiers.cegisSample
+              != options::CegisSampleMode::TRUST)
           {
             Node lem = nm->mkNode(OR, d_parent->getGuard().negate(), rlem);
             d_qim.addPendingLemma(
diff --git a/src/theory/quantifiers/sygus/enum_value_manager.cpp b/src/theory/quantifiers/sygus/enum_value_manager.cpp
index 937537ce9..f91127dbe 100644
--- a/src/theory/quantifiers/sygus/enum_value_manager.cpp
+++ b/src/theory/quantifiers/sygus/enum_value_manager.cpp
@@ -89,26 +89,26 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
       // or basic. The auto mode always prefers the optimized enumerator over
       // the basic one.
       Assert(d_tds->isBasicEnumerator(e));
-      if (options::sygusActiveGenMode()
+      if (options().quantifiers.sygusActiveGenMode
           == options::SygusActiveGenMode::ENUM_BASIC)
       {
         d_evg.reset(new EnumValGeneratorBasic(d_tds, e.getType()));
       }
       else
       {
-        Assert(options::sygusActiveGenMode()
+        Assert(options().quantifiers.sygusActiveGenMode
                    == options::SygusActiveGenMode::ENUM
-               || options::sygusActiveGenMode()
+               || options().quantifiers.sygusActiveGenMode
                       == options::SygusActiveGenMode::AUTO);
         // create the enumerator callback
-        if (options::sygusSymBreakDynamic())
+        if (options().datatypes.sygusSymBreakDynamic)
         {
           std::ostream* out = nullptr;
-          if (options::sygusRewVerify())
+          if (options().quantifiers.sygusRewVerify)
           {
             d_samplerRrV.reset(new SygusSampler(d_env));
             d_samplerRrV->initializeSygus(
-                d_tds, e, options::sygusSamples(), false);
+                d_tds, e, options().quantifiers.sygusSamples, false);
             // use the default output for the output of sygusRewVerify
             out = options().base.out;
           }
@@ -117,8 +117,12 @@ Node EnumValueManager::getEnumeratedValue(bool& activeIncomplete)
         }
         // if sygus repair const is enabled, we enumerate terms with free
         // variables as arguments to any-constant constructors
-        d_evg.reset(new SygusEnumerator(
-            d_tds, d_secd.get(), &d_stats, false, options::sygusRepairConst()));
+        d_evg.reset(
+            new SygusEnumerator(d_tds,
+                                d_secd.get(),
+                                &d_stats,
+                                false,
+                                options().quantifiers.sygusRepairConst));
       }
     }
     Trace("sygus-active-gen")