From: Andrew Reynolds Date: Wed, 25 May 2022 22:51:38 +0000 (-0500) Subject: Eliminate some static options access (#8795) X-Git-Tag: cvc5-1.0.1~94 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ef38a3b721c725eaff2c1dbf9cf828213a853758;p=cvc5.git Eliminate some static options access (#8795) In preparation for eliminating options scopes. --- diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index 350348927..c5cb6aa22 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -105,14 +105,6 @@ name = "Strings Theory" default = "true" help = "regression explanations for string lemmas" -[[option]] - name = "stringMinPrefixExplain" - category = "expert" - long = "strings-min-prefix-explain" - type = "bool" - default = "true" - help = "minimize explanations for prefix of normal forms in strings" - [[option]] name = "stringModelBasedReduction" category = "regular" diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 70544aa8e..c567c3190 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -703,7 +703,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, } } while (expanded); // now we should be able to close it - if (options::proofCheck() == options::ProofCheckMode::EAGER) + if (options().proof.proofCheck == options::ProofCheckMode::EAGER) { std::vector assumptionsVec; for (const Node& a : d_assumptions) diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index 76012e5bd..57dc93f6b 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -22,11 +22,8 @@ namespace cvc5::internal { namespace smt { -AbstractValues::AbstractValues(NodeManager* nm) - : d_nm(nm), - d_fakeContext(), - d_abstractValueMap(&d_fakeContext), - d_abstractValues() +AbstractValues::AbstractValues() + : d_fakeContext(), d_abstractValueMap(&d_fakeContext), d_abstractValues() { } AbstractValues::~AbstractValues() {} @@ -41,11 +38,10 @@ Node AbstractValues::substituteAbstractValues(TNode n) Node AbstractValues::mkAbstractValue(TNode n) { - Assert(options::abstractValues()); Node& val = d_abstractValues[n]; if (val.isNull()) { - val = d_nm->getSkolemManager()->mkDummySkolem( + val = NodeManager::currentNM()->getSkolemManager()->mkDummySkolem( "a", n.getType(), "an abstract value", diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h index 5cf66aa92..1d7e6e4ce 100644 --- a/src/smt/abstract_values.h +++ b/src/smt/abstract_values.h @@ -37,7 +37,7 @@ class AbstractValues typedef std::unordered_map NodeToNodeHashMap; public: - AbstractValues(NodeManager* nm); + AbstractValues(); ~AbstractValues(); /** * Substitute away all AbstractValues in a node, which replaces all diff --git a/src/smt/command.cpp b/src/smt/command.cpp index eb37c0c21..efd7f18ce 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -765,9 +765,9 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) d_commandStatus = CommandSuccess::instance(); d_solution.clear(); // check whether we should print the status - if (!d_result.hasSolution() - || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF - || options::sygusOut() == options::SygusSolutionOutMode::STATUS) + std::string sygusOut = solver->getOption("sygus-out"); + if (!d_result.hasSolution() || sygusOut == "status-and-def" + || sygusOut == "status") { if (d_result.hasSolution()) { @@ -783,8 +783,7 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) } } // check whether we should print the solution - if (d_result.hasSolution() - && options::sygusOut() != options::SygusSolutionOutMode::STATUS) + if (d_result.hasSolution() && sygusOut != "status") { std::vector synthFuns = sm->getFunctionsToSynthesize(); d_solution << "(" << std::endl; @@ -2402,12 +2401,13 @@ void GetUnsatAssumptionsCommand::toStream(std::ostream& out, /* class GetUnsatCoreCommand */ /* -------------------------------------------------------------------------- */ -GetUnsatCoreCommand::GetUnsatCoreCommand() : d_sm(nullptr) {} +GetUnsatCoreCommand::GetUnsatCoreCommand() : d_solver(nullptr), d_sm(nullptr) {} void GetUnsatCoreCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) { try { d_sm = sm; + d_solver = solver; d_result = solver->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); @@ -2430,7 +2430,7 @@ void GetUnsatCoreCommand::printResult(std::ostream& out) const } else { - if (options::printUnsatCoresFull()) + if (d_solver->getOption("print-unsat-cores-full") == "true") { // use the assertions UnsatCore ucr(termVectorToNodes(d_result)); @@ -2456,6 +2456,7 @@ const std::vector& GetUnsatCoreCommand::getUnsatCore() const Command* GetUnsatCoreCommand::clone() const { GetUnsatCoreCommand* c = new GetUnsatCoreCommand; + c->d_solver = d_solver; c->d_sm = d_sm; c->d_result = d_result; return c; diff --git a/src/smt/command.h b/src/smt/command.h index 0af8b4b48..d5801eb4b 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1288,6 +1288,8 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command internal::Language::LANG_AUTO) const override; protected: + /** The solver we were invoked with */ + cvc5::Solver* d_solver; /** The symbol manager we were invoked with */ SymbolManager* d_sm; /** the result of the unsat core call */ diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 2cb2efe39..2893ccb23 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -250,7 +250,7 @@ std::string PreprocessProofGenerator::identify() const { return d_name; } void PreprocessProofGenerator::checkEagerPedantic(PfRule r) { - if (options::proofCheck() == options::ProofCheckMode::EAGER) + if (options().proof.proofCheck == options::ProofCheckMode::EAGER) { // catch a pedantic failure now, which otherwise would not be // triggered since we are doing lazy proof generation diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index 2d109da17..1ec4a9c86 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -18,6 +18,7 @@ #include "options/proof_options.h" #include "proof/proof_checker.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/builtin/proof_checker.h" #include "theory/theory_id.h" @@ -28,22 +29,21 @@ using namespace cvc5::internal::theory; namespace cvc5::internal { namespace smt { -ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm) - : d_ruleCount(smtStatisticsRegistry().registerHistogram( +ProofFinalCallback::ProofFinalCallback(Env& env) + : EnvObj(env), + d_ruleCount(statisticsRegistry().registerHistogram( "finalProof::ruleCount")), - d_instRuleIds( - smtStatisticsRegistry().registerHistogram( - "finalProof::instRuleId")), + d_instRuleIds(statisticsRegistry().registerHistogram( + "finalProof::instRuleId")), d_annotationRuleIds( - smtStatisticsRegistry().registerHistogram( + statisticsRegistry().registerHistogram( "finalProof::annotationRuleId")), d_totalRuleCount( - smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")), + statisticsRegistry().registerInt("finalProof::totalRuleCount")), d_minPedanticLevel( - smtStatisticsRegistry().registerInt("finalProof::minPedanticLevel")), + statisticsRegistry().registerInt("finalProof::minPedanticLevel")), d_numFinalProofs( - smtStatisticsRegistry().registerInt("finalProofs::numFinalProofs")), - d_pnm(pnm), + statisticsRegistry().registerInt("finalProofs::numFinalProofs")), d_pedanticFailure(false) { d_minPedanticLevel += 10; @@ -61,23 +61,25 @@ bool ProofFinalCallback::shouldUpdate(std::shared_ptr pn, bool& continueUpdate) { PfRule r = pn->getRule(); + ProofNodeManager* pnm = d_env.getProofNodeManager(); + Assert(pnm != nullptr); // if not doing eager pedantic checking, fail if below threshold - if (options::proofCheck() != options::ProofCheckMode::EAGER) + if (options().proof.proofCheck != options::ProofCheckMode::EAGER) { if (!d_pedanticFailure) { Assert(d_pedanticFailureOut.str().empty()); - if (d_pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut)) + if (pnm->getChecker()->isPedanticFailure(r, d_pedanticFailureOut)) { d_pedanticFailure = true; } } } - if (options::proofCheck() != options::ProofCheckMode::NONE) + if (options().proof.proofCheck != options::ProofCheckMode::NONE) { - d_pnm->ensureChecked(pn.get()); + pnm->ensureChecked(pn.get()); } - uint32_t plevel = d_pnm->getChecker()->getPedanticLevel(r); + uint32_t plevel = pnm->getChecker()->getPedanticLevel(r); if (plevel != 0) { d_minPedanticLevel.minAssign(plevel); diff --git a/src/smt/proof_final_callback.h b/src/smt/proof_final_callback.h index 666e25a53..e5b2ff058 100644 --- a/src/smt/proof_final_callback.h +++ b/src/smt/proof_final_callback.h @@ -23,6 +23,7 @@ #include #include "proof/proof_node_updater.h" +#include "smt/env_obj.h" #include "theory/inference_id.h" #include "util/statistics_stats.h" @@ -30,10 +31,10 @@ namespace cvc5::internal { namespace smt { /** Final callback class, for stats and pedantic checking */ -class ProofFinalCallback : public ProofNodeUpdaterCallback +class ProofFinalCallback : protected EnvObj, public ProofNodeUpdaterCallback { public: - ProofFinalCallback(ProofNodeManager* pnm); + ProofFinalCallback(Env& env); /** * Initialize, called once for each new ProofNode to process. This initializes * static information to be used by successive calls to update. @@ -65,8 +66,6 @@ class ProofFinalCallback : public ProofNodeUpdaterCallback IntStat d_minPedanticLevel; /** The total number of final proofs */ IntStat d_numFinalProofs; - /** Proof node manager (used for pedantic checking) */ - ProofNodeManager* d_pnm; /** Was there a pedantic failure? */ bool d_pedanticFailure; /** The pedantic failure string for debugging */ diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 7317ed351..029bfdfcd 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1267,9 +1267,8 @@ ProofPostproccess::ProofPostproccess(Env& env, : EnvObj(env), d_cb(env, pppg, rdb, updateScopedAssumptions), // the update merges subproofs - d_updater( - env.getProofNodeManager(), d_cb, options().proof.proofPpMerge), - d_finalCb(env.getProofNodeManager()), + d_updater(env.getProofNodeManager(), d_cb, options().proof.proofPpMerge), + d_finalCb(env), d_finalizer(env.getProofNodeManager(), d_finalCb) { } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 952db55ff..5ef8257cb 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -86,7 +86,7 @@ namespace cvc5::internal { SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) : d_env(new Env(nm, optr)), d_state(new SolverEngineState(*d_env.get(), *this)), - d_absValues(new AbstractValues(getNodeManager())), + d_absValues(new AbstractValues), d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), d_routListener(new ResourceOutListener(*this)), d_smtSolver(nullptr), diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp index a2975f694..a75ccebeb 100644 --- a/src/theory/datatypes/inference.cpp +++ b/src/theory/datatypes/inference.cpp @@ -39,20 +39,13 @@ DatatypesInference::DatatypesInference(InferenceManager* im, bool DatatypesInference::mustCommunicateFact(Node n, Node exp) { Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; - // Force lemmas if option is set - if (options::dtInferAsLemmas()) - { - Trace("dt-lemma-debug") - << "Communicate " << n << " due to option" << std::endl; - return true; - } // Note that equalities due to instantiate are forced as lemmas if // necessary as they are created. This ensures that terms are shared with // external theories when necessary. We send the lemma here only if the // conclusion has kind LEQ (for datatypes size) or OR. Notice that // all equalities are kept internal, apart from those forced as lemmas // via instantiate. - else if (n.getKind() == LEQ || n.getKind() == OR) + if (n.getKind() == LEQ || n.getKind() == OR) { Trace("dt-lemma-debug") << "Communicate " << n << " due to kind" << std::endl; diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 32e86bd68..755c545f0 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -53,10 +53,11 @@ void InferenceManager::addPendingInference(Node conc, Node exp, bool forceLemma) { - // if we are forcing the inference to be processed as a lemma, or if the - // inference must be sent as a lemma based on the policy in - // mustCommunicateFact. - if (forceLemma || DatatypesInference::mustCommunicateFact(conc, exp)) + // if we are forcing the inference to be processed as a lemma, if the + // dtInferAsLemmas option is set, or if the inference must be sent as a lemma + // based on the policy in mustCommunicateFact. + if (forceLemma || options().datatypes.dtInferAsLemmas + || DatatypesInference::mustCommunicateFact(conc, exp)) { d_pendingLem.emplace_back(new DatatypesInference(this, conc, exp, id)); } diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index f49bfc035..750c07e5d 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -407,7 +407,7 @@ CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q) return hmin; } -CegHandledStatus CegInstantiator::isCbqiQuant(Node q) +CegHandledStatus CegInstantiator::isCbqiQuant(Node q, bool cegqiAll) { Assert(q.getKind() == FORALL); // compute attributes @@ -467,7 +467,7 @@ CegHandledStatus CegInstantiator::isCbqiQuant(Node q) ret = CEG_PARTIALLY_HANDLED; } } - if (ret == CEG_UNHANDLED && options::cegqiAll()) + if (ret == CEG_UNHANDLED && cegqiAll) { // try but not exclusively ret = CEG_PARTIALLY_HANDLED; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index e413e3089..12b8d019a 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -346,8 +346,11 @@ class CegInstantiator : protected EnvObj * returns CEG_PARTIALLY_HANDLED, then it may be worthwhile to handle the * quantified formula using cegqi, however other strategies should also be * tried. + * + * @param cegqiAll Whether we apply CEQGI to all quantifiers (option + * options::cegqiAll). */ - static CegHandledStatus isCbqiQuant(Node q); + static CegHandledStatus isCbqiQuant(Node q, bool cegqiAll); //------------------------------------ end static queries private: /** The quantified formula of this instantiator */ diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 7760b9391..e290b0f67 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -409,7 +409,8 @@ bool InstStrategyCegqi::doCbqi(Node q) { std::map::iterator it = d_do_cbqi.find(q); if( it==d_do_cbqi.end() ){ - CegHandledStatus ret = CegInstantiator::isCbqiQuant(q); + CegHandledStatus ret = + CegInstantiator::isCbqiQuant(q, options().quantifiers.cegqiAll); Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl; d_do_cbqi[q] = ret; return ret != CEG_UNHANDLED; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index d29b5a888..0a7a79af8 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -182,7 +182,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted) } else { - status = CegInstantiator::isCbqiQuant(d_single_inv); + status = CegInstantiator::isCbqiQuant(d_single_inv, + options().quantifiers.cegqiAll); } } Trace("sygus-si") << "CegHandledStatus is " << status << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index c138984fe..7395a583a 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -215,7 +215,8 @@ bool SygusRepairConst::repairSolution(Node sygusBody, if (fo_body.getKind() == FORALL) { // must be a CBQI quantifier - CegHandledStatus hstatus = CegInstantiator::isCbqiQuant(fo_body); + CegHandledStatus hstatus = + CegInstantiator::isCbqiQuant(fo_body, options().quantifiers.cegqiAll); if (hstatus < CEG_HANDLED) { // abort if less than fully handled diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp index e17a9afdf..52a1c5493 100644 --- a/src/theory/strings/normal_form.cpp +++ b/src/theory/strings/normal_form.cpp @@ -116,7 +116,7 @@ void NormalForm::addToExplanation(Node exp, void NormalForm::getExplanation(int index, std::vector& curr_exp) { - if (index == -1 || !options::stringMinPrefixExplain()) + if (index == -1) { curr_exp.insert(curr_exp.end(), d_exp.begin(), d_exp.end()); return;