From: Andrew Reynolds Date: Tue, 17 Aug 2021 17:52:15 +0000 (-0500) Subject: Make SmtEngineState use Env (#7028) X-Git-Tag: cvc5-1.0.0~1375 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8f18dd65c829c3c12158d57e1fc7d2c9dcdcfd4;p=cvc5.git Make SmtEngineState use Env (#7028) Also moves d_filename to Env. --- diff --git a/src/smt/env.cpp b/src/smt/env.cpp index a4e07d2c9..3ec9899ad 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -65,6 +65,8 @@ void Env::setProofNodeManager(ProofNodeManager* pnm) d_topLevelSubs->setProofNodeManager(pnm); } +void Env::setFilename(const std::string& filename) { d_filename = filename; } + void Env::shutdown() { d_rewriter.reset(nullptr); @@ -81,6 +83,8 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; } ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } +const std::string& Env::getFilename() const { return d_filename; } + bool Env::isTheoryProofProducing() const { return d_proofNodeManager != nullptr diff --git a/src/smt/env.h b/src/smt/env.h index fa2fe6ab8..9887aea08 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -82,6 +82,9 @@ class Env */ ProofNodeManager* getProofNodeManager(); + /** Return the input name, or the empty string if not set */ + const std::string& getFilename() const; + /** * Check whether theories should produce proofs as well. Other than whether * the proof node manager is set, theory engine proofs are conditioned on the @@ -133,6 +136,11 @@ class Env /** Set proof node manager if it exists */ void setProofNodeManager(ProofNodeManager* pnm); + /** + * Set that the file name of the current instance is the given string. This + * is used for various purposes (e.g. get-info, SZS status). + */ + void setFilename(const std::string& filename); /* Private shutdown ------------------------------------------------------- */ /** @@ -199,6 +207,12 @@ class Env const Options* d_originalOptions; /** Manager for limiting time and abstract resource usage. */ std::unique_ptr d_resourceManager; + + /** + * The input file name or the name set through (set-info :filename ...), if + * any. + */ + std::string d_filename; }; /* class Env */ } // namespace cvc5 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3e4c1efa7..43177a73a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -86,7 +86,7 @@ namespace cvc5 { SmtEngine::SmtEngine(NodeManager* nm, Options* optr) : d_env(new Env(nm, optr)), - d_state(new SmtEngineState(getContext(), getUserContext(), *this)), + d_state(new SmtEngineState(*d_env.get(), *this)), d_absValues(new AbstractValues(getNodeManager())), d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), d_routListener(new ResourceOutListener(*this)), @@ -381,7 +381,7 @@ LogicInfo SmtEngine::getUserLogicInfo() const void SmtEngine::notifyStartParsing(const std::string& filename) { - d_state->setFilename(filename); + d_env->setFilename(filename); d_env->getStatisticsRegistry().registerValue("driver::filename", filename); // Copy the original options. This is called prior to beginning parsing. @@ -391,7 +391,7 @@ void SmtEngine::notifyStartParsing(const std::string& filename) const std::string& SmtEngine::getFilename() const { - return d_state->getFilename(); + return d_env->getFilename(); } void SmtEngine::setResultStatistic(const std::string& result) { @@ -436,7 +436,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) if (key == "filename") { - d_state->setFilename(value); + d_env->setFilename(value); } else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) { @@ -728,7 +728,7 @@ void SmtEngine::defineFunctionRec(Node func, Result SmtEngine::quickCheck() { Assert(d_state->isFullyInited()); Trace("smt") << "SMT quickCheck()" << endl; - const std::string& filename = d_state->getFilename(); + const std::string& filename = d_env->getFilename(); return Result( Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); } @@ -944,7 +944,7 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, { printStatisticsDiff(); } - return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); + return Result(Result::SAT_UNKNOWN, why, d_env->getFilename()); } } @@ -1213,7 +1213,7 @@ Model* SmtEngine::getModel() { } // set the information on the SMT-level model Assert(m != nullptr); - m->d_inputName = d_state->getFilename(); + m->d_inputName = d_env->getFilename(); m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT); return m; } @@ -1603,8 +1603,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { finishInit(); if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { - out << "% SZS output start Proof for " << d_state->getFilename() - << std::endl; + out << "% SZS output start Proof for " << d_env->getFilename() << std::endl; } QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); @@ -1694,7 +1693,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { } if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { - out << "% SZS output end Proof for " << d_state->getFilename() << std::endl; + out << "% SZS output end Proof for " << d_env->getFilename() << std::endl; } } diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index cb0a94123..a61c18384 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -19,17 +19,15 @@ #include "options/base_options.h" #include "options/option_exception.h" #include "options/smt_options.h" +#include "smt/env.h" #include "smt/smt_engine.h" namespace cvc5 { namespace smt { -SmtEngineState::SmtEngineState(context::Context* c, - context::UserContext* u, - SmtEngine& smt) +SmtEngineState::SmtEngineState(Env& env, SmtEngine& smt) : d_smt(smt), - d_context(c), - d_userContext(u), + d_env(env), d_pendingPops(0), d_fullyInited(false), d_queryMade(false), @@ -45,7 +43,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_filename); + d_expectedStatus = Result(status, d_env.getFilename()); } void SmtEngineState::notifyResetAssertions() @@ -57,7 +55,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 && d_userContext->getLevel() == 1); + Assert(d_userLevels.size() == 0 && getUserContext()->getLevel() == 1); popto(0); } @@ -158,7 +156,7 @@ void SmtEngineState::shutdown() { doPendingPops(); - while (options::incrementalSolving() && d_userContext->getLevel() > 1) + while (options::incrementalSolving() && getUserContext()->getLevel() > 1) { internalPop(true); } @@ -170,11 +168,6 @@ void SmtEngineState::cleanup() popto(0); } -void SmtEngineState::setFilename(const std::string& filename) -{ - d_filename = filename; -} - void SmtEngineState::userPush() { if (!options::incrementalSolving()) @@ -187,10 +180,10 @@ void SmtEngineState::userPush() // staying symmetric with pop. d_smtMode = SmtMode::ASSERT; - d_userLevels.push_back(d_userContext->getLevel()); + d_userLevels.push_back(getUserContext()->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngineState: pushed to level " - << d_userContext->getLevel() << std::endl; + << getUserContext()->getLevel() << std::endl; } void SmtEngineState::userPop() @@ -212,37 +205,37 @@ void SmtEngineState::userPop() // is no longer in scope!). d_smtMode = SmtMode::ASSERT; - AlwaysAssert(d_userContext->getLevel() > 0); - AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); - while (d_userLevels.back() < d_userContext->getLevel()) + AlwaysAssert(getUserContext()->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < getUserContext()->getLevel()); + while (d_userLevels.back() < getUserContext()->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() { - d_userContext->push(); - d_context->push(); + getUserContext()->push(); + getContext()->push(); } void SmtEngineState::pop() { - d_userContext->pop(); - d_context->pop(); + getUserContext()->pop(); + getContext()->pop(); } void SmtEngineState::popto(int toLevel) { - d_context->popto(toLevel); - d_userContext->popto(toLevel); + getContext()->popto(toLevel); + getUserContext()->popto(toLevel); } -context::UserContext* SmtEngineState::getUserContext() { return d_userContext; } - -context::Context* SmtEngineState::getContext() { return d_context; } - Result SmtEngineState::getStatus() const { return d_status; } bool SmtEngineState::isFullyInited() const { return d_fullyInited; } @@ -255,8 +248,6 @@ size_t SmtEngineState::getNumUserLevels() const { return d_userLevels.size(); } SmtMode SmtEngineState::getMode() const { return d_smtMode; } -const std::string& SmtEngineState::getFilename() const { return d_filename; } - void SmtEngineState::internalPush() { Assert(d_fullyInited); @@ -266,7 +257,7 @@ void SmtEngineState::internalPush() { // notifies the SmtEngine to process the assertions immediately d_smt.notifyPushPre(); - d_userContext->push(); + getUserContext()->push(); // the context push is done inside of the SAT solver d_smt.notifyPushPost(); } @@ -300,7 +291,7 @@ void SmtEngineState::doPendingPops() // the context pop is done inside of the SAT solver d_smt.notifyPopPre(); // pop the context - d_userContext->pop(); + getUserContext()->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 042efb4de..f20180672 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -27,6 +27,7 @@ namespace cvc5 { class SmtEngine; +class Env; namespace smt { @@ -48,7 +49,7 @@ namespace smt { class SmtEngineState { public: - SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt); + SmtEngineState(Env& env, SmtEngine& smt); ~SmtEngineState() {} /** * Notify that the expected status of the next check-sat is given by the @@ -126,11 +127,6 @@ class SmtEngineState * Cleanup, which pops all contexts to level zero. */ void cleanup(); - /** - * Set that the file name of the current instance is the given string. This - * is used for various purposes (e.g. get-info, SZS status). - */ - void setFilename(const std::string& filename); //---------------------------- context management /** @@ -149,10 +145,6 @@ class SmtEngineState * the SMT-LIB command pop. */ void userPop(); - /** Get a pointer to the UserContext owned by this SmtEngine. */ - context::UserContext* getUserContext(); - /** Get a pointer to the Context owned by this SmtEngine. */ - context::Context* getContext(); //---------------------------- end context management //---------------------------- queries @@ -179,11 +171,13 @@ class SmtEngineState Result getStatus() const; /** Get the SMT mode we are in */ SmtMode getMode() const; - /** return the input name (if any) */ - const std::string& getFilename() const; //---------------------------- 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 */ @@ -203,10 +197,8 @@ class SmtEngineState void internalPop(bool immediate = false); /** Reference to the SmtEngine */ SmtEngine& d_smt; - /** Expr manager context */ - context::Context* d_context; - /** User level context */ - context::UserContext* d_userContext; + /** Reference to the env of the parent SmtEngine */ + Env& d_env; /** The context levels of user pushes */ std::vector d_userLevels; @@ -253,12 +245,6 @@ class SmtEngineState /** The SMT mode, for details see enumeration above. */ SmtMode d_smtMode; - - /** - * The input file name or the name set through (set-info :filename ...), if - * any. - */ - std::string d_filename; }; } // namespace smt diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 595a3808c..1014b218d 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -133,7 +133,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, Trace("smt") << "SmtSolver::check()" << endl; - const std::string& filename = d_state.getFilename(); + const std::string& filename = d_env.getFilename(); ResourceManager* rm = d_env.getResourceManager(); if (rm->out()) {