From: Andrew Reynolds Date: Fri, 8 Oct 2021 16:36:55 +0000 (-0500) Subject: A few more miscellaneous uses of EnvObj (#7325) X-Git-Tag: cvc5-1.0.0~1100 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e6a6658573e0d11e7bac8fd51066f401c3aa25c;p=cvc5.git A few more miscellaneous uses of EnvObj (#7325) --- diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp index fa6a01791..c40414bac 100644 --- a/src/preprocessing/learned_literal_manager.cpp +++ b/src/preprocessing/learned_literal_manager.cpp @@ -15,15 +15,15 @@ #include "preprocessing/learned_literal_manager.h" +#include "smt/env.h" #include "theory/rewriter.h" +#include "theory/trust_substitutions.h" namespace cvc5 { namespace preprocessing { -LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls, - context::UserContext* u, - ProofNodeManager* pnm) - : d_topLevelSubs(tls), d_learnedLits(u) +LearnedLiteralManager::LearnedLiteralManager(Env& env) + : EnvObj(env), d_learnedLits(userContext()) { } @@ -35,12 +35,13 @@ void LearnedLiteralManager::notifyLearnedLiteral(TNode lit) std::vector LearnedLiteralManager::getLearnedLiterals() const { + theory::TrustSubstitutionMap& tls = d_env.getTopLevelSubstitutions(); std::vector currLearnedLits; for (const auto& lit: d_learnedLits) { // update based on substitutions - Node tlsNode = d_topLevelSubs.get().apply(lit); - tlsNode = theory::Rewriter::rewrite(tlsNode); + Node tlsNode = tls.get().apply(lit); + tlsNode = rewrite(tlsNode); currLearnedLits.push_back(tlsNode); Trace("pp-llm") << "Learned literal : " << tlsNode << " from " << lit << std::endl; diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h index 2b0273628..5e7898da4 100644 --- a/src/preprocessing/learned_literal_manager.h +++ b/src/preprocessing/learned_literal_manager.h @@ -20,7 +20,7 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "theory/trust_substitutions.h" +#include "smt/env_obj.h" namespace cvc5 { namespace preprocessing { @@ -35,12 +35,10 @@ namespace preprocessing { * a literal like (> x t) is learned at top-level, it may be useful to remember * this information. This class is concerned with the latter kind of literals. */ -class LearnedLiteralManager +class LearnedLiteralManager : protected EnvObj { public: - LearnedLiteralManager(theory::TrustSubstitutionMap& tls, - context::UserContext* u, - ProofNodeManager* pnm); + LearnedLiteralManager(Env& env); /** * Notify learned literal. This method is called when a literal is * entailed by the current set of assertions. @@ -59,8 +57,6 @@ class LearnedLiteralManager private: /** Learned literal map */ typedef context::CDHashSet NodeSet; - /* The top level substitutions */ - theory::TrustSubstitutionMap& d_topLevelSubs; /** Learned literals */ NodeSet d_learnedLits; }; diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index e380a1073..4bf29157e 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -52,12 +52,12 @@ NonClausalSimp::Statistics::Statistics(StatisticsRegistry& reg) NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) : PreprocessingPass(preprocContext, "non-clausal-simp"), d_statistics(statisticsRegistry()), - d_pnm(preprocContext->getProofNodeManager()), + d_pnm(d_env.getProofNodeManager()), d_llpg(d_pnm ? new smt::PreprocessProofGenerator( - d_pnm, userContext(), "NonClausalSimp::llpg") + d_pnm, userContext(), "NonClausalSimp::llpg") : nullptr), d_llra(d_pnm ? new LazyCDProof( - d_pnm, nullptr, userContext(), "NonClausalSimp::llra") + d_pnm, nullptr, userContext(), "NonClausalSimp::llra") : nullptr), d_tsubsList(userContext()) { diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 91f83c56e..e316c2f81 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -32,8 +32,7 @@ PreprocessingPassContext::PreprocessingPassContext( d_theoryEngine(te), d_propEngine(pe), d_circuitPropagator(circuitPropagator), - d_llm( - env.getTopLevelSubstitutions(), userContext(), getProofNodeManager()), + d_llm(env), d_symsInAssertions(userContext()) { } @@ -97,10 +96,5 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); } -ProofNodeManager* PreprocessingPassContext::getProofNodeManager() const -{ - return d_env.getProofNodeManager(); -} - } // namespace preprocessing } // namespace cvc5 diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index fc3faa7ab..d452e23ff 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -26,6 +26,7 @@ #include "preprocessing/learned_literal_manager.h" #include "smt/env_obj.h" #include "theory/logic_info.h" +#include "theory/trust_substitutions.h" #include "util/resource_manager.h" namespace cvc5 { @@ -116,8 +117,6 @@ class PreprocessingPassContext : protected EnvObj PfRule id, const std::vector& args); - /** The the proof node manager associated with this context, if it exists */ - ProofNodeManager* getProofNodeManager() const; private: /** Pointer to the theory engine associated with this context. */ diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 37b057048..9452081c9 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -27,8 +27,8 @@ namespace cvc5 { namespace smt { SmtEngineState::SmtEngineState(Env& env, SolverEngine& slv) - : d_slv(slv), - d_env(env), + : EnvObj(env), + d_slv(slv), d_pendingPops(0), d_fullyInited(false), d_queryMade(false), @@ -44,7 +44,7 @@ void SmtEngineState::notifyExpectedStatus(const std::string& status) Assert(status == "sat" || status == "unsat" || status == "unknown") << "SmtEngineState::notifyExpectedStatus: unexpected status string " << status; - d_expectedStatus = Result(status, d_env.getOptions().driver.filename); + d_expectedStatus = Result(status, options().driver.filename); } void SmtEngineState::notifyResetAssertions() @@ -56,7 +56,7 @@ void SmtEngineState::notifyResetAssertions() } // Remember the global push/pop around everything when beyond Start mode // (see solver execution modes in the SMT-LIB standard) - Assert(d_userLevels.size() == 0 && getUserContext()->getLevel() == 1); + Assert(d_userLevels.size() == 0 && userContext()->getLevel() == 1); popto(0); } @@ -157,7 +157,7 @@ void SmtEngineState::shutdown() { doPendingPops(); - while (options::incrementalSolving() && getUserContext()->getLevel() > 1) + while (options::incrementalSolving() && userContext()->getLevel() > 1) { internalPop(true); } @@ -181,10 +181,10 @@ void SmtEngineState::userPush() // staying symmetric with pop. d_smtMode = SmtMode::ASSERT; - d_userLevels.push_back(getUserContext()->getLevel()); + d_userLevels.push_back(userContext()->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngineState: pushed to level " - << getUserContext()->getLevel() << std::endl; + << userContext()->getLevel() << std::endl; } void SmtEngineState::userPop() @@ -206,35 +206,30 @@ void SmtEngineState::userPop() // is no longer in scope!). d_smtMode = SmtMode::ASSERT; - AlwaysAssert(getUserContext()->getLevel() > 0); - AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel()); - while (d_userLevels.back() < getUserContext()->getLevel()) + AlwaysAssert(userContext()->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < userContext()->getLevel()); + while (d_userLevels.back() < userContext()->getLevel()) { internalPop(true); } d_userLevels.pop_back(); } -context::Context* SmtEngineState::getContext() { return d_env.getContext(); } -context::UserContext* SmtEngineState::getUserContext() -{ - return d_env.getUserContext(); -} void SmtEngineState::push() { - getUserContext()->push(); - getContext()->push(); + userContext()->push(); + context()->push(); } void SmtEngineState::pop() { - getUserContext()->pop(); - getContext()->pop(); + userContext()->pop(); + context()->pop(); } void SmtEngineState::popto(int toLevel) { - getContext()->popto(toLevel); - getUserContext()->popto(toLevel); + context()->popto(toLevel); + userContext()->popto(toLevel); } Result SmtEngineState::getStatus() const { return d_status; } @@ -258,7 +253,7 @@ void SmtEngineState::internalPush() { // notifies the SolverEngine to process the assertions immediately d_slv.notifyPushPre(); - getUserContext()->push(); + userContext()->push(); // the context push is done inside of the SAT solver d_slv.notifyPushPost(); } @@ -292,7 +287,7 @@ void SmtEngineState::doPendingPops() // the context pop is done inside of the SAT solver d_slv.notifyPopPre(); // pop the context - getUserContext()->pop(); + userContext()->pop(); --d_pendingPops; // no need for pop post (for now) } diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index 535be2092..d7a0e2290 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -21,13 +21,13 @@ #include #include "context/context.h" +#include "smt/env_obj.h" #include "smt/smt_mode.h" #include "util/result.h" namespace cvc5 { class SolverEngine; -class Env; namespace smt { @@ -48,7 +48,7 @@ namespace smt { * It maintains a reference to the SolverEngine for the sake of making * callbacks. */ -class SmtEngineState +class SmtEngineState : protected EnvObj { public: SmtEngineState(Env& env, SolverEngine& smt); @@ -176,10 +176,6 @@ class SmtEngineState //---------------------------- end queries private: - /** get the sat context we are using */ - context::Context* getContext(); - /** get the user context we are using */ - context::UserContext* getUserContext(); /** Pushes the user and SAT contexts */ void push(); /** Pops the user and SAT contexts */ @@ -199,8 +195,6 @@ class SmtEngineState void internalPop(bool immediate = false); /** Reference to the SolverEngine */ SolverEngine& d_slv; - /** Reference to the env of the parent SolverEngine */ - Env& d_env; /** The context levels of user pushes */ std::vector d_userLevels;