Remove more static option accesses (#7582)

This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers.

6 files changed, 28 insertions, 23 deletions

diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 0b7294f2c..3cf08a8d6 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1635,7 +1635,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
 
     int32_t lentTestSuccess = -1;
     Node lenConstraint;
-    if (options::stringCheckEntailLen())
+    if (options().strings.stringCheckEntailLen)
     {
       // If length entailment checks are enabled, we can save the case split by
       // inferring that `x` has to be longer than `y` or vice-versa.
@@ -1784,11 +1784,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
 
   TypeNode stype = veci[loop_index].getType();
 
-  if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT)
+  if (options().strings.stringProcessLoopMode
+      == options::ProcessLoopMode::ABORT)
   {
     throw LogicException("Looping word equation encountered.");
   }
-  else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE
+  else if (options().strings.stringProcessLoopMode
+               == options::ProcessLoopMode::NONE
            || stype.isSequence())
   {
     // note we cannot convert looping word equations into regular expressions if
@@ -1932,12 +1934,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   }
   else
   {
-    if (options::stringProcessLoopMode()
+    if (options().strings.stringProcessLoopMode
         == options::ProcessLoopMode::SIMPLE_ABORT)
     {
       throw LogicException("Normal looping word equation encountered.");
     }
-    else if (options::stringProcessLoopMode()
+    else if (options().strings.stringProcessLoopMode
              == options::ProcessLoopMode::SIMPLE)
     {
       d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
@@ -2081,7 +2083,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
     return;
   }
 
-  if (options::stringsDeqExt())
+  if (options().strings.stringsDeqExt)
   {
     processDeqExtensionality(ni, nj);
     return;
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 6e2f60c6d..cbd67f232 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -325,7 +325,7 @@ void ExtfSolver::checkExtfEval(int effort)
               << "  get symbolic definition..." << std::endl;
           Node nrs;
           // only use symbolic definitions if option is set
-          if (options::stringInferSym())
+          if (options().strings.stringInferSym)
           {
             nrs = d_termReg.getSymbolicDefinition(sn, exps);
           }
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index ead18e823..277cc72e1 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -185,13 +185,13 @@ void InferenceManager::sendInference(InferInfo& ii, bool asLemma)
     processConflict(ii);
     return;
   }
-  else if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
+  else if (asLemma || options().strings.stringInferAsLemmas || !ii.isFact())
   {
     Trace("strings-infer-debug") << "...as lemma" << std::endl;
     addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
     return;
   }
-  if (options::stringInferSym())
+  if (options().strings.stringInferSym)
   {
     std::vector<Node> unproc;
     for (const Node& ac : ii.d_premises)
@@ -325,7 +325,7 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
     utils::flattenOp(AND, ec, exp);
   }
   std::vector<Node> noExplain;
-  if (!options::stringRExplainLemmas())
+  if (!options().strings.stringRExplainLemmas)
   {
     // if we aren't regressing the explanation, we add all literals to
     // noExplain and ignore ii.d_ant.
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 898c0f1b7..050ec594a 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -247,7 +247,7 @@ void RegExpSolver::check(const std::map<Node, std::vector<Node> >& mems)
         }
         else
         {
-          if (!options::stringExp())
+          if (!options().strings.stringExp)
           {
             throw LogicException(
                 "Strings Incomplete (due to Negative Membership) by default, "
@@ -413,7 +413,7 @@ bool RegExpSolver::checkEqcInclusion(std::vector<Node>& mems)
 bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
 {
   // do not compute intersections if the re intersection mode is none
-  if (options::stringRegExpInterMode() == options::RegExpInterMode::NONE)
+  if (options().strings.stringRegExpInterMode == options::RegExpInterMode::NONE)
   {
     return true;
   }
@@ -436,7 +436,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
     }
     RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]);
     if (rct == RE_C_VARIABLE
-        || (options::stringRegExpInterMode()
+        || (options().strings.stringRegExpInterMode
                 == options::RegExpInterMode::CONSTANT
             && rct != RE_C_CONRETE_CONSTANT))
     {
@@ -444,7 +444,7 @@ bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
       // on option.
       continue;
     }
-    if (options::stringRegExpInterMode()
+    if (options().strings.stringRegExpInterMode
         == options::RegExpInterMode::ONE_CONSTANT)
     {
       if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT)
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 61fe786d6..1124be488 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -147,7 +147,7 @@ void TermRegistry::preRegisterTerm(TNode n)
       << "TheoryString::preregister : " << n << std::endl;
   // check for logic exceptions
   Kind k = n.getKind();
-  if (!options::stringExp())
+  if (!options().strings.stringExp)
   {
     if (k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
         || k == STRING_STOI || k == STRING_REPLACE || k == STRING_SUBSTR
@@ -259,7 +259,7 @@ void TermRegistry::preRegisterTerm(TNode n)
   {
     d_functionsTerms.push_back(n);
   }
-  if (options::stringFMF())
+  if (options().strings.stringFMF)
   {
     if (tn.isStringLike())
     {
@@ -289,7 +289,7 @@ void TermRegistry::registerTerm(Node n, int effort)
   TypeNode tn = n.getType();
   if (!tn.isStringLike())
   {
-    if (options::stringEagerLen())
+    if (options().strings.stringEagerLen)
     {
       do_register = effort == 0;
     }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index e0f0a8dac..799becd29 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -78,7 +78,7 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
                 d_statistics),
       d_rsolver(
           env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
-      d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()),
+      d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
       d_stringsFmf(env, valuation, d_termReg)
 {
   d_termReg.finishInit(&d_im);
@@ -123,7 +123,7 @@ void TheoryStrings::finishInit()
   // witness is used to eliminate str.from_code
   d_valuation.setUnevaluatedKind(WITNESS);
 
-  bool eagerEval = options::stringEagerEval();
+  bool eagerEval = options().strings.stringEagerEval;
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval);
   d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval);
@@ -186,11 +186,13 @@ TrustNode TheoryStrings::explain(TNode literal)
 }
 
 void TheoryStrings::presolve() {
-  Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
+  Debug("strings-presolve")
+      << "TheoryStrings::Presolving : get fmf options "
+      << (options().strings.stringFMF ? "true" : "false") << std::endl;
   d_strat.initializeStrategy();
 
   // if strings fmf is enabled, register the strategy
-  if (options::stringFMF())
+  if (options().strings.stringFMF)
   {
     d_stringsFmf.presolve();
     // This strategy is local to a check-sat call, since we refresh the strategy
@@ -721,7 +723,8 @@ void TheoryStrings::postCheck(Effort e)
 }
 
 bool TheoryStrings::needsCheckLastEffort() {
-  if( options::stringGuessModel() ){
+  if (options().strings.stringGuessModel)
+  {
     return d_esolver.hasExtendedFunctions();
   }
   return false;
@@ -1015,7 +1018,7 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
   }
   TrustNode ret;
   Node atomRet = atom;
-  if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
+  if (options().strings.regExpElim && atom.getKind() == STRING_IN_REGEXP)
   {
     // aggressive elimination of regular expression membership
     ret = d_regexp_elim.eliminateTrusted(atomRet);