From: Gereon Kremer Date: Wed, 8 Dec 2021 22:15:18 +0000 (-0800) Subject: Static options acceses again (#7771) X-Git-Tag: cvc5-1.0.0~700 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=15a1c744470514a9e1091989ad498b27cbca72f6;p=cvc5.git 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 32cff9378..354b8691f 100644 --- 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 be53bad80..32838eccf 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1193,6 +1193,8 @@ std::vector SolverEngine::getAssertionsInternal() return res; } +const Options& SolverEngine::options() const { return d_env->getOptions(); } + std::vector SolverEngine::getExpandedAssertions() { std::vector easserts = getAssertions(); @@ -1270,7 +1272,7 @@ UnsatCore SolverEngine::getUnsatCoreInternal() Assert(pe != nullptr); std::shared_ptr 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 pfn = d_pfManager->getFinalProof(pepf, *d_asserts); std::vector 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 SolverEngine::reduceUnsatCore(const std::vector& 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 1e710f213..95b31eab2 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -1035,6 +1035,12 @@ class CVC5_EXPORT SolverEngine * changes. */ std::vector 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 7338b99fd..921a676d7 100644 --- 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 c390c5594..48253c64a 100644 --- 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 4306718be..4ed754b16 100644 --- 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);