Remove static accesses to options (#7913)

This PR removes some more calls like options::foo() in favor of options().module.foo.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index ac1edeb96c1a80bb7178f97558bbad0726dcf154..547125290ff0096b57a2545f96e7632e12396776 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -43,8 +43,8 @@ using namespace cvc5::theory::bv;
 BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-to-int"),
       d_intBlaster(preprocContext->getEnv(),
-                   options::solveBVAsInt(),
-                   options::BVAndIntegerGranularity()) {}
+                   options().smt.solveBVAsInt,
+                   options().smt.BVAndIntegerGranularity) {}
 
 PreprocessingPassResult BVToInt::applyInternal(
     AssertionPipeline* assertionsToPreprocess)

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index b6ee1ca89afd9bf464faeb30ece26a364c89838c..8d22804b411808c6631412348e4e03ce48867fac 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -55,7 +55,7 @@ void SygusEnumerator::initialize(Node e)
   Trace("sygus-enum") << "SygusEnumerator::initialize " << e << std::endl;
   d_enum = e;
   // allocate the default callback
-  if (d_sec == nullptr && options::sygusSymBreakDynamic())
+  if (d_sec == nullptr && options().datatypes.sygusSymBreakDynamic)
   {
     d_secd =
         std::make_unique<SygusEnumeratorCallbackDefault>(d_env, e, d_stats);
@@ -65,7 +65,7 @@ void SygusEnumerator::initialize(Node e)
   Assert(d_etype.isDatatype());
   Assert(d_etype.getDType().isSygus());
   d_tlEnum = getMasterEnumForType(d_etype);
-  d_abortSize = options::sygusAbortSize();
+  d_abortSize = options().datatypes.sygusAbortSize;
 
   // if we don't have a term database, we don't register symmetry breaking
   // lemmas
@@ -147,7 +147,7 @@ Node SygusEnumerator::getCurrent()
     if (cs > d_abortSize)
     {
       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/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index d24ad25b241915c44502594273d8c17213cfef36..b3c0522f93cb85aac6f2b75d550ea06ede68f81d 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -37,7 +37,7 @@ SygusEvalUnfold::SygusEvalUnfold(Env& env, TermDbSygus* tds)
 
 void SygusEvalUnfold::registerEvalTerm(Node n)
 {
-  Assert(options::sygusEvalUnfold());
+  Assert(options().quantifiers.sygusEvalUnfold);
   // is this a sygus evaluation function application?
   if (n.getKind() != DT_SYGUS_EVAL)
   {
@@ -141,7 +141,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
         Node expn;
         // should we unfold?
         bool do_unfold = false;
-        if (options::sygusEvalUnfoldBool())
+        if (options().quantifiers.sygusEvalUnfoldBool)
         {
           Node bTermUse = bTerm;
           if (bTerm.getKind() == APPLY_UF)

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index cf7b71104c62156cbdc3598622a96f175b22195d..a1a31441843bc055b282ba22f9919c16b1658f7c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -303,7 +303,7 @@ std::unique_ptr<SygusGrammarNorm::Transf> SygusGrammarNorm::inferTransf(
 
   // if normalization option is not enabled, we do not infer the transformations
   // below
-  if (!options::sygusGrammarNorm())
+  if (!options().quantifiers.sygusGrammarNorm)
   {
     return nullptr;
   }

diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp
index 0711b44ae99aded190decddfc8e3a46f2ca7559c..c679d3ea94d2ad952786f49769a4be3f9a6e8ee3 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp
@@ -75,7 +75,7 @@ Node SygusRandomEnumerator::incrementH()
   NodeManager* nm = NodeManager::currentNM();
   SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
   Random& rnd = Random::getRandom();
-  double p = options::sygusActiveGenRandomP();
+  double p = options().quantifiers.sygusActiveGenRandomP;
 
   Node mainSkolem = sm->mkDummySkolem("sygus_rand", d_tn);
   // List of skolems with no corresponding constructor.

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 559119dfb8c158787fa7608735b6e7871b441d5b..b67743f59abefee7ba39f1aba954a99ae68715ea 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -45,14 +45,16 @@ namespace {
  * @param cache: Caches visited nodes.
  * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
  */
-void getMaxGroundTerms(TNode n,
+void getMaxGroundTerms(const Options& options,
+                       TNode n,
                        TypeNode tn,
                        std::unordered_set<Node>& terms,
                        std::unordered_set<TNode>& cache,
                        bool skip_quant = false)
 {
-  if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MAX
-      && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
+  if (options.quantifiers.sygusInstTermSel != options::SygusInstTermSelMode::MAX
+      && options.quantifiers.sygusInstTermSel
+             != options::SygusInstTermSelMode::BOTH)
   {
     return;
   }
@@ -100,14 +102,16 @@ void getMaxGroundTerms(TNode n,
  *               term was already found in a subterm.
  * @param skip_quant: Do not traverse quantified formulas (skip quantifiers).
  */
-void getMinGroundTerms(TNode n,
+void getMinGroundTerms(const Options& options,
+                       TNode n,
                        TypeNode tn,
                        std::unordered_set<Node>& terms,
                        std::unordered_map<TNode, std::pair<bool, bool>>& cache,
                        bool skip_quant = false)
 {
-  if (options::sygusInstTermSel() != options::SygusInstTermSelMode::MIN
-      && options::sygusInstTermSel() != options::SygusInstTermSelMode::BOTH)
+  if (options.quantifiers.sygusInstTermSel != options::SygusInstTermSelMode::MIN
+      && options.quantifiers.sygusInstTermSel
+             != options::SygusInstTermSelMode::BOTH)
   {
     return;
   }
@@ -361,8 +365,8 @@ void SygusInst::registerQuantifier(Node q)
         std::unordered_set<TNode> cache_max;
         std::unordered_map<TNode, std::pair<bool, bool>> cache_min;
 
-        getMinGroundTerms(q, tn, terms, cache_min);
-        getMaxGroundTerms(q, tn, terms, cache_max);
+        getMinGroundTerms(options(), q, tn, terms, cache_min);
+        getMaxGroundTerms(options(), q, tn, terms, cache_max);
         relevant_terms.emplace(tn, terms);
       }
 
@@ -394,8 +398,8 @@ void SygusInst::registerQuantifier(Node q)
 
         for (const Node& a : d_notified_assertions)
         {
-          getMinGroundTerms(a, tn, terms, cache_min, true);
-          getMaxGroundTerms(a, tn, terms, cache_max, true);
+          getMinGroundTerms(options(), a, tn, terms, cache_min, true);
+          getMaxGroundTerms(options(), a, tn, terms, cache_max, true);
         }
         d_global_terms.insert(tn, terms);
       }

diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 1402c845c47e013e8a2f4ef5f3b394828a40f5ab..e1491936af4f673e95d52fc3d0286ea76ff47f6e 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -39,7 +39,7 @@ namespace theory {
 namespace quantifiers {
 
 SygusSampler::SygusSampler(Env& env)
-    : d_env(env), d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
+    : EnvObj(env), d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
 {
 }
 
@@ -186,7 +186,7 @@ void SygusSampler::initializeSamples(unsigned nsamples)
                           << vt << std::endl;
   }
   std::map<unsigned, std::map<Node, std::vector<TypeNode> >::iterator> sts;
-  if (options::sygusSampleGrammar())
+  if (options().quantifiers.sygusSampleGrammar)
   {
     for (unsigned j = 0, size = types.size(); j < size; j++)
     {
@@ -202,7 +202,7 @@ void SygusSampler::initializeSamples(unsigned nsamples)
     {
       Node v = d_vars[j];
       Node r;
-      if (options::sygusSampleGrammar())
+      if (options().quantifiers.sygusSampleGrammar)
       {
         // choose a random start sygus type, if possible
         if (sts[j] != d_var_sygus_types.end())
@@ -515,7 +515,7 @@ Node SygusSampler::getRandomValue(TypeNode tn)
   {
     unsigned e = tn.getFloatingPointExponentSize();
     unsigned s = tn.getFloatingPointSignificandSize();
-    return nm->mkConst(options::sygusSampleFpUniform()
+    return nm->mkConst(options().quantifiers.sygusSampleFpUniform
                            ? Sampler::pickFpUniform(e, s)
                            : Sampler::pickFpBiased(e, s));
   }
@@ -832,7 +832,7 @@ void SygusSampler::checkEquivalent(Node bv, Node bvr, std::ostream& out)
     Assert(bve != bvre);
     out << "where they evaluate to " << bve << " and " << bvre << std::endl;
 
-    if (options::sygusRewVerifyAbort())
+    if (options().quantifiers.sygusRewVerifyAbort)
     {
       AlwaysAssert(false)
           << "--sygus-rr-verify detected unsoundness in the rewriter!";

diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h
index 3695270e1ea4954a170b69711fa828b78a236935..1fc2b8b6647312bcb1344441129c2d5896f72287 100644 (file)
--- a/src/theory/quantifiers/sygus_sampler.h
+++ b/src/theory/quantifiers/sygus_sampler.h
@@ -19,6 +19,8 @@
 #define CVC5__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H
 
 #include <map>
+
+#include "smt/env_obj.h"
 #include "theory/quantifiers/lazy_trie.h"
 #include "theory/quantifiers/term_enumeration.h"
 
@@ -65,7 +67,7 @@ class TermDbSygus;
  * Notice that the number of sample points can be configured for the above
  * options using sygus-samples=N.
  */
-class SygusSampler : public LazyTrieEvaluator
+class SygusSampler : protected EnvObj, public LazyTrieEvaluator
 {
  public:
   SygusSampler(Env& env);
@@ -181,8 +183,6 @@ class SygusSampler : public LazyTrieEvaluator
   void checkEquivalent(Node bv, Node bvr, std::ostream& out);
 
  protected:
-  /** The environment we are using to evaluate terms and samples */
-  Env& d_env;
   /** sygus term database of d_qe */
   TermDbSygus* d_tds;
   /** term enumerator object (used for random sampling) */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b218c35906c3ca75675e5996180e818889735cfa..9ff181b9ba1ae5c4e6b09e626ac53e3f1fad790b 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -168,7 +168,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
   {
     SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
     std::stringstream ss;
-    options::ioutils::applyOutputLang(ss, options::outputLanguage());
+    options::ioutils::applyOutputLang(ss, options().base.outputLanguage);
     ss << "e_" << tn;
     Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable");
     Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn