From bbd00db10f2d8801212863a85b04bfd17955086c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 11 Jan 2022 08:03:41 -0800 Subject: [PATCH] Remove static accesses to options (#7913) This PR removes some more calls like options::foo() in favor of options().module.foo. --- src/preprocessing/passes/bv_to_int.cpp | 4 ++-- .../quantifiers/sygus/sygus_enumerator.cpp | 6 ++--- .../quantifiers/sygus/sygus_eval_unfold.cpp | 4 ++-- .../quantifiers/sygus/sygus_grammar_norm.cpp | 2 +- .../sygus/sygus_random_enumerator.cpp | 2 +- src/theory/quantifiers/sygus_inst.cpp | 24 +++++++++++-------- src/theory/quantifiers/sygus_sampler.cpp | 10 ++++---- src/theory/quantifiers/sygus_sampler.h | 6 ++--- src/theory/quantifiers/term_database.cpp | 2 +- 9 files changed, 32 insertions(+), 28 deletions(-) diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index ac1edeb96..547125290 100644 --- 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 b6ee1ca89..8d22804b4 100644 --- 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(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 d24ad25b2..b3c0522f9 100644 --- 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 cf7b71104..a1a314418 100644 --- 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::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 0711b44ae..c679d3ea9 100644 --- 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 559119dfb..b67743f59 100644 --- 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& terms, std::unordered_set& 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& terms, std::unordered_map>& 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 cache_max; std::unordered_map> 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 1402c845c..e1491936a 100644 --- 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 >::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 3695270e1..1fc2b8b66 100644 --- 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 + +#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 b218c3590..9ff181b9b 100644 --- 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 -- 2.30.2