Static options acceses again (#7771)

This PR removes some more static accesses to options from strings and solver engine.

diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h
index 32cff93788a4d7be48f81cf114a412d56104d6cc..354b8691f973da9151c0b4b1508a811970ea592a 100644 (file)
--- a/src/smt/abstract_values.h
+++ b/src/smt/abstract_values.h
@@ -48,7 +48,7 @@ class AbstractValues
 
   /**
    * Make a new (or return an existing) abstract value for a node.
-   * Can only use this if options::abstractValues() is on.
+   * Can only use this if abstractValues option is on.
    */
   Node mkAbstractValue(TNode n);
 
@@ -63,7 +63,7 @@ class AbstractValues
 
   /**
    * A map of AbsractValues to their actual constants.  Only used if
-   * options::abstractValues() is on.
+   * abstractValues option is on.
    */
   theory::SubstitutionMap d_abstractValueMap;
 
@@ -71,7 +71,7 @@ class AbstractValues
    * A mapping of all abstract values (actual value |-> abstract) that
    * we've handed out.  This is necessary to ensure that we give the
    * same AbstractValues for the same real constants.  Only used if
-   * options::abstractValues() is on.
+   * abstractValues option is on.
    */
   NodeToNodeHashMap d_abstractValues;
 };

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index be53bad80aa459e027095ff92521b29aaac6fb93..32838eccff03ba574ab4d445a061859802decf02 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1193,6 +1193,8 @@ std::vector<Node> SolverEngine::getAssertionsInternal()
   return res;
 }
 
+const Options& SolverEngine::options() const { return d_env->getOptions(); }
+
 std::vector<Node> SolverEngine::getExpandedAssertions()
 {
   std::vector<Node> easserts = getAssertions();
@@ -1270,7 +1272,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal()
   Assert(pe != nullptr);
 
   std::shared_ptr<ProofNode> pepf;
-  if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS)
+  if (options().smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS)
   {
     pepf = pe->getRefutation();
   }
@@ -1282,7 +1284,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal()
   std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts);
   std::vector<Node> core;
   d_ucManager->getUnsatCore(pfn, *d_asserts, core);
-  if (options::minimalUnsatCores())
+  if (options().smt.minimalUnsatCores)
   {
     core = reduceUnsatCore(core);
   }
@@ -1291,7 +1293,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal()
 
 std::vector<Node> SolverEngine::reduceUnsatCore(const std::vector<Node>& core)
 {
-  Assert(options::unsatCores())
+  Assert(options().smt.unsatCores)
       << "cannot reduce unsat core if unsat cores are turned off";
 
   d_env->verbose(1) << "SolverEngine::reduceUnsatCore(): reducing unsat core"
@@ -1432,7 +1434,7 @@ void SolverEngine::checkModel(bool hardFailure)
   Assert(m != nullptr);
 
   // check the model with the theory engine for debugging
-  if (options::debugCheckModels())
+  if (options().smt.debugCheckModels)
   {
     TheoryEngine* te = getTheoryEngine();
     Assert(te != nullptr);
@@ -1527,8 +1529,8 @@ void SolverEngine::printInstantiations(std::ostream& out)
       && getSmtMode() == SmtMode::UNSAT)
   {
     // minimize instantiations based on proof manager
-    getRelevantInstantiationTermVectors(rinsts,
-                                        options::dumpInstantiationsDebug());
+    getRelevantInstantiationTermVectors(
+        rinsts, options().driver.dumpInstantiationsDebug);
   }
   else
   {

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 1e710f21363cae974a93edd183a3b233fcc1dd64..95b31eab227a7a895f4bb568404b931ea1712600 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -1035,6 +1035,12 @@ class CVC5_EXPORT SolverEngine
    * changes.
    */
   std::vector<Node> getAssertionsInternal();
+
+  /**
+   * Return a reference to options like for `EnvObj`.
+   */
+  const Options& options() const;
+
   /* Members -------------------------------------------------------------- */
 
   /** Solver instance that owns this SolverEngine instance. */

diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp
index 7338b99fd6bc56ef24c8ae580614f9cee1885275..921a676d77ca05a5f5c54f919b1ab78598d6805d 100644 (file)
--- a/src/theory/strings/strategy.cpp
+++ b/src/theory/strings/strategy.cpp
@@ -43,7 +43,7 @@ std::ostream& operator<<(std::ostream& out, InferStep s)
   return out;
 }
 
-Strategy::Strategy() : d_strategy_init(false) {}
+Strategy::Strategy(Env& env) : EnvObj(env), d_strategy_init(false) {}
 
 Strategy::~Strategy() {}
 
@@ -93,7 +93,7 @@ void Strategy::initializeStrategy()
     d_strategy_init = true;
     // beginning indices
     step_begin[Theory::EFFORT_FULL] = 0;
-    if (options::stringEager())
+    if (options().strings.stringEager)
     {
       step_begin[Theory::EFFORT_STANDARD] = 0;
     }
@@ -103,45 +103,45 @@ void Strategy::initializeStrategy()
     addStrategyStep(CHECK_EXTF_EVAL, 0);
     // we must check cycles before using flat forms
     addStrategyStep(CHECK_CYCLES);
-    if (options::stringFlatForms())
+    if (options().strings.stringFlatForms)
     {
       addStrategyStep(CHECK_FLAT_FORMS);
     }
     addStrategyStep(CHECK_EXTF_REDUCTION, 1);
-    if (options::stringEager())
+    if (options().strings.stringEager)
     {
       // do only the above inferences at standard effort, if applicable
       step_end[Theory::EFFORT_STANDARD] = d_infer_steps.size() - 1;
     }
-    if (!options::stringEagerLen())
+    if (!options().strings.stringEagerLen)
     {
       addStrategyStep(CHECK_REGISTER_TERMS_PRE_NF);
     }
     addStrategyStep(CHECK_NORMAL_FORMS_EQ);
     addStrategyStep(CHECK_EXTF_EVAL, 1);
-    if (!options::stringEagerLen() && options::stringLenNorm())
+    if (!options().strings.stringEagerLen && options().strings.stringLenNorm)
     {
       addStrategyStep(CHECK_LENGTH_EQC, 0, false);
       addStrategyStep(CHECK_REGISTER_TERMS_NF);
     }
     addStrategyStep(CHECK_NORMAL_FORMS_DEQ);
     addStrategyStep(CHECK_CODES);
-    if (options::stringEagerLen() && options::stringLenNorm())
+    if (options().strings.stringEagerLen && options().strings.stringLenNorm)
     {
       addStrategyStep(CHECK_LENGTH_EQC);
     }
-    if (options::stringExp())
+    if (options().strings.stringExp)
     {
       addStrategyStep(CHECK_EXTF_REDUCTION, 2);
     }
     addStrategyStep(CHECK_MEMBERSHIP);
     addStrategyStep(CHECK_CARDINALITY);
     step_end[Theory::EFFORT_FULL] = d_infer_steps.size() - 1;
-    if (options::stringModelBasedReduction())
+    if (options().strings.stringModelBasedReduction)
     {
       step_begin[Theory::EFFORT_LAST_CALL] = d_infer_steps.size();
       addStrategyStep(CHECK_EXTF_EVAL, 3);
-      if (options::stringExp())
+      if (options().strings.stringExp)
       {
         addStrategyStep(CHECK_EXTF_REDUCTION, 3);
       }

diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h
index c390c559425b483331659f3a6d7a4a3b11fd57d2..48253c64ae302ced5c8a7542b162798918e76037 100644 (file)
--- a/src/theory/strings/strategy.h
+++ b/src/theory/strings/strategy.h
@@ -74,10 +74,10 @@ std::ostream& operator<<(std::ostream& out, InferStep i);
  * This stores a sequence of the above enum that indicates the calls to
  * runInferStep to make on the theory of strings, given by parent.
  */
-class Strategy
+class Strategy : protected EnvObj
 {
  public:
-  Strategy();
+  Strategy(Env& env);
   ~Strategy();
   /** is this strategy initialized? */
   bool isStrategyInit() const;

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4306718be98437c910ea551b137c2e7630ec398d..4ed754b16a6b6339dfa178b717fe6d62918f3f60 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -79,7 +79,8 @@ TheoryStrings::TheoryStrings(Env& env, OutputChannel& out, Valuation valuation)
       d_rsolver(
           env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
       d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
-      d_stringsFmf(env, valuation, d_termReg)
+      d_stringsFmf(env, valuation, d_termReg),
+      d_strat(d_env)
 {
   d_termReg.finishInit(&d_im);