From b337c99fde04f4efc1824880183e29ca6253ee37 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 10 Mar 2021 17:00:59 -0600 Subject: [PATCH] Add Env class (#6093) This class contains all globally available utilities for internal code. --- src/CMakeLists.txt | 2 + src/smt/env.cpp | 111 ++++++++++++++ src/smt/env.h | 187 ++++++++++++++++++++++++ src/smt/output_manager.cpp | 5 +- src/smt/smt_engine.cpp | 275 ++++++++++++++++++----------------- src/smt/smt_engine.h | 61 +++----- src/smt/smt_engine_scope.cpp | 2 +- src/smt/smt_engine_state.cpp | 15 +- src/smt/smt_engine_state.h | 6 +- 9 files changed, 476 insertions(+), 188 deletions(-) create mode 100644 src/smt/env.cpp create mode 100644 src/smt/env.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9124977ef..3fc12c585 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -223,6 +223,8 @@ libcvc4_add_sources( smt/dump.h smt/dump_manager.cpp smt/dump_manager.h + smt/env.cpp + smt/env.h smt/expand_definitions.cpp smt/expand_definitions.h smt/listeners.cpp diff --git a/src/smt/env.cpp b/src/smt/env.cpp new file mode 100644 index 000000000..0b6607c35 --- /dev/null +++ b/src/smt/env.cpp @@ -0,0 +1,111 @@ +/********************* */ +/*! \file env.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Smt Environment, main access to global utilities available to + ** internal code. + **/ + +#include "smt/env.h" + +#include "context/context.h" +#include "expr/node.h" +#include "expr/term_conversion_proof_generator.h" +#include "options/base_options.h" +#include "printer/printer.h" +#include "smt/dump_manager.h" +#include "smt/smt_engine_stats.h" +#include "theory/rewriter.h" +#include "util/resource_manager.h" + +using namespace CVC4::smt; + +namespace CVC4 { + +Env::Env(NodeManager* nm) + : d_context(new context::Context()), + d_userContext(new context::UserContext()), + d_nodeManager(nm), + d_proofNodeManager(nullptr), + d_rewriter(new theory::Rewriter()), + d_dumpManager(new DumpManager(d_userContext.get())), + d_logic(), + d_statisticsRegistry(nullptr), + d_resourceManager(nullptr) +{ +} + +Env::~Env() {} + +void Env::setOptions(Options* optr) +{ + if (optr != nullptr) + { + // if we provided a set of options, copy their values to the options + // owned by this Env. + d_options.copyValues(*optr); + } +} + +void Env::setStatisticsRegistry(StatisticsRegistry* statReg) +{ + d_statisticsRegistry = statReg; + // now initialize resource manager + d_resourceManager.reset(new ResourceManager(*statReg, d_options)); +} + +void Env::setProofNodeManager(ProofNodeManager* pnm) +{ + d_proofNodeManager = pnm; + d_rewriter->setProofNodeManager(pnm); +} + +void Env::shutdown() +{ + d_rewriter.reset(nullptr); + d_dumpManager.reset(nullptr); + // d_resourceManager must be destroyed before d_statisticsRegistry + d_resourceManager.reset(nullptr); +} + +context::UserContext* Env::getUserContext() { return d_userContext.get(); } + +context::Context* Env::getContext() { return d_context.get(); } + +NodeManager* Env::getNodeManager() const { return d_nodeManager; } + +ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } + +theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); } + +DumpManager* Env::getDumpManager() { return d_dumpManager.get(); } + +const LogicInfo& Env::getLogicInfo() const { return d_logic; } + +StatisticsRegistry* Env::getStatisticsRegistry() +{ + return d_statisticsRegistry; +} + +const Options& Env::getOptions() const { return d_options; } + +ResourceManager* Env::getResourceManager() const +{ + return d_resourceManager.get(); +} + +const Printer& Env::getPrinter() +{ + return *Printer::getPrinter(d_options[options::outputLanguage]); +} + +std::ostream& Env::getDumpOut() { return *d_options.getOut(); } + +} // namespace CVC4 diff --git a/src/smt/env.h b/src/smt/env.h new file mode 100644 index 000000000..e8f73a4f2 --- /dev/null +++ b/src/smt/env.h @@ -0,0 +1,187 @@ +/********************* */ +/*! \file env.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Smt Environment, main access to global utilities available to + ** internal code + **/ + +#include "cvc4_public.h" + +#ifndef CVC4__SMT__ENV_H +#define CVC4__SMT__ENV_H + +#include + +#include "options/options.h" +#include "theory/logic_info.h" +#include "util/sexpr.h" +#include "util/statistics.h" + +namespace CVC4 { + +class NodeManager; +class StatisticsRegistry; +class ProofNodeManager; +class Printer; +class ResourceManager; + +namespace context { +class Context; +class UserContext; +} // namespace context + +namespace smt { +class DumpManager; +} + +namespace theory { +class Rewriter; +} + +/** + * The environment class. + * + * This class lives in the SmtEngine and contains all utilities that are + * globally available to all internal code. + */ +class Env +{ + friend class SmtEngine; + + public: + /** + * Construct an Env with the given node manager. + */ + Env(NodeManager* nm); + /** Destruct the env. */ + ~Env(); + + /* Access to members------------------------------------------------------- */ + /** Get a pointer to the Context owned by this Env. */ + context::Context* getContext(); + + /** Get a pointer to the UserContext owned by this Env. */ + context::UserContext* getUserContext(); + + /** Get a pointer to the underlying NodeManager. */ + NodeManager* getNodeManager() const; + + /** + * Get the underlying proof node manager. Note since proofs depend on option + * initialization, this is only available after the SmtEngine that owns this + * environment is initialized, and only non-null if proofs are enabled. + */ + ProofNodeManager* getProofNodeManager(); + + /** Get a pointer to the Rewriter owned by this Env. */ + theory::Rewriter* getRewriter(); + + /** Get a pointer to the underlying dump manager. */ + smt::DumpManager* getDumpManager(); + + /** Get the options object (const version only) owned by this Env. */ + const Options& getOptions() const; + + /** Get the resource manager owned by this Env. */ + ResourceManager* getResourceManager() const; + + /** Get the logic information currently set. */ + const LogicInfo& getLogicInfo() const; + + /** Get a pointer to the StatisticsRegistry. */ + StatisticsRegistry* getStatisticsRegistry(); + + /* Option helpers---------------------------------------------------------- */ + + /** + * Get the current printer based on the current options + * @return the current printer + */ + const Printer& getPrinter(); + + /** + * Get the output stream that --dump=X should print to + * @return the output stream + */ + std::ostream& getDumpOut(); + + private: + /* Private initialization ------------------------------------------------- */ + + /** Set options, which makes a deep copy of optr if non-null */ + void setOptions(Options* optr = nullptr); + /** Set the statistics registry */ + void setStatisticsRegistry(StatisticsRegistry* statReg); + /** Set proof node manager if it exists */ + void setProofNodeManager(ProofNodeManager* pnm); + + /* Private shutdown ------------------------------------------------------- */ + /** + * Shutdown method, which destroys the non-essential members of this class + * in preparation for destroying SMT engine. + */ + void shutdown(); + /* Members ---------------------------------------------------------------- */ + + /** The SAT context owned by this Env */ + std::unique_ptr d_context; + /** User level context owned by this Env */ + std::unique_ptr d_userContext; + /** + * A pointer to the node manager of this environment. A node manager is + * not necessarily unique to an SmtEngine instance. + */ + NodeManager* d_nodeManager; + /** + * A pointer to the proof node manager, which is non-null if proofs are + * enabled. This is owned by the proof manager of the SmtEngine that owns + * this environment. + */ + ProofNodeManager* d_proofNodeManager; + /** + * The rewriter owned by this Env. We have a different instance + * of the rewriter for each Env instance. This is because rewriters may + * hold references to objects that belong to theory solvers, which are + * specific to an SmtEngine/TheoryEngine instance. + */ + std::unique_ptr d_rewriter; + /** The dump manager */ + std::unique_ptr d_dumpManager; + /** + * The logic we're in. This logic may be an extension of the logic set by the + * user, which may be different from the user-provided logic due to the + * options we have set. + * + * This is the authorative copy of the logic that internal subsolvers should + * consider during solving and initialization. + */ + LogicInfo d_logic; + /** + * The statistics registry, which is owned by the SmtEngine that owns this. + */ + StatisticsRegistry* d_statisticsRegistry; + /** + * The options object, which contains the modified version of the options + * provided as input to the SmtEngine that owns this environment. Note + * that d_options may be modified by the options manager, e.g. based + * on the input logic. + * + * This is the authorative copy of the options that internal subsolvers should + * consider during solving and initialization. + */ + Options d_options; + /** Manager for limiting time and abstract resource usage. */ + std::unique_ptr d_resourceManager; +}; /* class Env */ + +} // namespace CVC4 + +#endif /* CVC4__SMT__ENV_H */ diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp index 31b55a4f9..e01d5879e 100644 --- a/src/smt/output_manager.cpp +++ b/src/smt/output_manager.cpp @@ -22,10 +22,7 @@ namespace CVC4 { OutputManager::OutputManager(SmtEngine* smt) : d_smt(smt) {} -const Printer& OutputManager::getPrinter() const -{ - return *d_smt->getPrinter(); -} +const Printer& OutputManager::getPrinter() const { return d_smt->getPrinter(); } std::ostream& OutputManager::getDumpOut() const { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7e8a4fb86..d89b30c87 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -42,6 +42,7 @@ #include "smt/defined_function.h" #include "smt/dump.h" #include "smt/dump_manager.h" +#include "smt/env.h" #include "smt/interpolation_solver.h" #include "smt/listeners.h" #include "smt/logic_exception.h" @@ -81,32 +82,27 @@ using namespace CVC4::theory; namespace CVC4 { SmtEngine::SmtEngine(NodeManager* nm, Options* optr) - : d_state(new SmtEngineState(*this)), - d_nodeManager(nm), - d_absValues(new AbstractValues(d_nodeManager)), + : d_env(new Env(nm)), + d_state(new SmtEngineState(getContext(), getUserContext(), *this)), + d_absValues(new AbstractValues(getNodeManager())), d_asserts(new Assertions(getUserContext(), *d_absValues.get())), - d_dumpm(new DumpManager(getUserContext())), d_routListener(new ResourceOutListener(*this)), - d_snmListener(new SmtNodeManagerListener(*d_dumpm.get(), d_outMgr)), + d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), d_smtSolver(nullptr), d_proofManager(nullptr), d_model(nullptr), d_checkModels(nullptr), d_pfManager(nullptr), d_ucManager(nullptr), - d_rewriter(new theory::Rewriter()), d_definedFunctions(nullptr), d_sygusSolver(nullptr), d_abductSolver(nullptr), d_interpolSolver(nullptr), d_quantElimSolver(nullptr), - d_logic(), d_originalOptions(), d_isInternalSubsolver(false), - d_statisticsRegistry(nullptr), d_stats(nullptr), d_outMgr(this), - d_resourceManager(nullptr), d_optm(nullptr), d_pp(nullptr), d_scope(nullptr) @@ -124,20 +120,20 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) // On the other hand, this hack breaks use cases where multiple SmtEngine // objects are created by the user. d_scope.reset(new SmtScope(this)); - if (optr != nullptr) - { - // if we provided a set of options, copy their values to the options - // owned by this SmtEngine. - d_options.copyValues(*optr); - } + // Set options in the environment, which makes a deep copy of optr if + // non-null. This may throw an options exception. + d_env->setOptions(optr); + // now construct the statistics registry d_statisticsRegistry.reset(new StatisticsRegistry()); - d_resourceManager.reset( - new ResourceManager(*d_statisticsRegistry.get(), d_options)); - d_optm.reset(new smt::OptionsManager(&d_options, d_resourceManager.get())); + // initialize the environment, which keeps a pointer to statistics registry + // and sets up resource manager + d_env->setStatisticsRegistry(d_statisticsRegistry.get()); + // set the options manager + d_optm.reset(new smt::OptionsManager(&getOptions(), getResourceManager())); // listen to node manager events - d_nodeManager->subscribeEvents(d_snmListener.get()); + getNodeManager()->subscribeEvents(d_snmListener.get()); // listen to resource out - d_resourceManager->registerListener(d_routListener.get()); + getResourceManager()->registerListener(d_routListener.get()); // make statistics d_stats.reset(new SmtEngineStatistics()); // reset the preprocessor @@ -145,7 +141,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) *this, getUserContext(), *d_absValues.get(), *d_stats)); // make the SMT solver d_smtSolver.reset( - new SmtSolver(*this, *d_state, d_resourceManager.get(), *d_pp, *d_stats)); + new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats)); // make the SyGuS solver d_sygusSolver.reset( new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); @@ -185,9 +181,9 @@ Result SmtEngine::getStatusOfLastCommand() const } context::UserContext* SmtEngine::getUserContext() { - return d_state->getUserContext(); + return d_env->getUserContext(); } -context::Context* SmtEngine::getContext() { return d_state->getContext(); } +context::Context* SmtEngine::getContext() { return d_env->getContext(); } TheoryEngine* SmtEngine::getTheoryEngine() { @@ -212,7 +208,8 @@ void SmtEngine::finishInit() // of SMT-LIB 2.6 standard. // set the logic - if (!d_logic.isLocked()) + const LogicInfo& logic = getLogicInfo(); + if (!logic.isLocked()) { setLogicInternal(); } @@ -223,13 +220,13 @@ void SmtEngine::finishInit() // Call finish init on the options manager. This inializes the resource // manager based on the options, and sets up the best default options // based on our heuristics. - d_optm->finishInit(d_logic, d_isInternalSubsolver); + d_optm->finishInit(d_env->d_logic, d_isInternalSubsolver); ProofNodeManager* pnm = nullptr; if (options::proof()) { // ensure bound variable uses canonical bound variables - d_nodeManager->getBoundVarManager()->enableKeepCacheValues(); + getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); // make the proof manager d_pfManager.reset(new PfManager(getUserContext(), this)); PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); @@ -237,8 +234,8 @@ void SmtEngine::finishInit() d_ucManager.reset(new UnsatCoreManager()); // use this proof node manager pnm = d_pfManager->getProofNodeManager(); - // enable proof support in the rewriter - d_rewriter->setProofNodeManager(pnm); + // enable proof support in the environment/rewriter + d_env->setProofNodeManager(pnm); // enable it in the assertions pipeline d_asserts->setProofGenerator(pppg); // enable it in the SmtSolver @@ -248,7 +245,7 @@ void SmtEngine::finishInit() } Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; - d_smtSolver->finishInit(const_cast(d_logic)); + d_smtSolver->finishInit(logic); // now can construct the SMT-level model object TheoryEngine* te = d_smtSolver->getTheoryEngine(); @@ -274,17 +271,17 @@ void SmtEngine::finishInit() { LogicInfo everything; everything.lock(); - getOutputManager().getPrinter().toStreamCmdComment( + getPrinter().toStreamCmdComment( getOutputManager().getDumpOut(), "CVC4 always dumps the most general, all-supported logic (below), as " "some internals might require the use of a logic more general than " "the input."); - getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic( - getOutputManager().getDumpOut(), everything.getLogicString()); + getPrinter().toStreamCmdSetBenchmarkLogic(getOutputManager().getDumpOut(), + everything.getLogicString()); } // initialize the dump manager - d_dumpm->finishInit(); + getDumpManager()->finishInit(); // subsolvers if (options::produceAbducts()) @@ -302,7 +299,7 @@ void SmtEngine::finishInit() << "The PropEngine has pushed but the SmtEngine " "hasn't finished initializing!"; - Assert(d_logic.isLocked()); + Assert(getLogicInfo().isLocked()); // store that we are finished initializing d_state->finishInit(); @@ -313,6 +310,8 @@ void SmtEngine::shutdown() { d_state->shutdown(); d_smtSolver->shutdown(); + + d_env->shutdown(); } SmtEngine::~SmtEngine() @@ -341,13 +340,11 @@ SmtEngine::~SmtEngine() #ifdef CVC4_PROOF d_proofManager.reset(nullptr); #endif - d_rewriter.reset(nullptr); d_pfManager.reset(nullptr); d_ucManager.reset(nullptr); d_absValues.reset(nullptr); d_asserts.reset(nullptr); - d_dumpm.reset(nullptr); d_model.reset(nullptr); d_sygusSolver.reset(nullptr); @@ -355,16 +352,16 @@ SmtEngine::~SmtEngine() d_smtSolver.reset(nullptr); d_stats.reset(nullptr); - d_nodeManager->unsubscribeEvents(d_snmListener.get()); + getNodeManager()->unsubscribeEvents(d_snmListener.get()); d_snmListener.reset(nullptr); d_routListener.reset(nullptr); d_optm.reset(nullptr); d_pp.reset(nullptr); - // d_resourceManager must be destroyed before d_statisticsRegistry - d_resourceManager.reset(nullptr); d_statisticsRegistry.reset(nullptr); // destroy the state d_state.reset(nullptr); + // destroy the environment + d_env.reset(nullptr); } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; @@ -379,7 +376,7 @@ void SmtEngine::setLogic(const LogicInfo& logic) throw ModalException("Cannot set logic in SmtEngine after the engine has " "finished initializing."); } - d_logic = logic; + d_env->d_logic = logic; d_userLogic = logic; setLogicInternal(); } @@ -393,8 +390,8 @@ void SmtEngine::setLogic(const std::string& s) // dump out a set-logic command if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdSetBenchmarkLogic( - getOutputManager().getDumpOut(), d_logic.getLogicString()); + getPrinter().toStreamCmdSetBenchmarkLogic( + getOutputManager().getDumpOut(), getLogicInfo().getLogicString()); } } catch (IllegalArgumentException& e) @@ -405,7 +402,10 @@ void SmtEngine::setLogic(const std::string& s) void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); } -const LogicInfo& SmtEngine::getLogicInfo() const { return d_logic; } +const LogicInfo& SmtEngine::getLogicInfo() const +{ + return d_env->getLogicInfo(); +} LogicInfo SmtEngine::getUserLogicInfo() const { @@ -422,7 +422,7 @@ void SmtEngine::notifyStartParsing(std::string filename) // Copy the original options. This is called prior to beginning parsing. // Hence reset should revert to these options, which note is after reading // the command line. - d_originalOptions.copyValues(d_options); + d_originalOptions.copyValues(getOptions()); } const std::string& SmtEngine::getFilename() const @@ -434,7 +434,7 @@ void SmtEngine::setLogicInternal() Assert(!d_state->isFullyInited()) << "setting logic in SmtEngine but the engine has already" " finished initializing for this run"; - d_logic.lock(); + d_env->d_logic.lock(); d_userLogic.lock(); } @@ -452,12 +452,12 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) (value == "sat") ? Result::SAT : ((value == "unsat") ? Result::UNSAT : Result::SAT_UNKNOWN); - getOutputManager().getPrinter().toStreamCmdSetBenchmarkStatus( + getPrinter().toStreamCmdSetBenchmarkStatus( getOutputManager().getDumpOut(), status); } else { - getOutputManager().getPrinter().toStreamCmdSetInfo( + getPrinter().toStreamCmdSetInfo( getOutputManager().getDumpOut(), key, value); } } @@ -513,7 +513,7 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const if (key == "all-statistics") { vector stats; - StatisticsRegistry* sr = d_nodeManager->getStatisticsRegistry(); + StatisticsRegistry* sr = getNodeManager()->getStatisticsRegistry(); for (StatisticsRegistry::const_iterator i = sr->begin(); i != sr->end(); ++i) { @@ -671,7 +671,7 @@ void SmtEngine::defineFunction(Node func, } DefineFunctionNodeCommand nc(ss.str(), func, nFormals, formula); - d_dumpm->addToDump(nc, "declarations"); + getDumpManager()->addToDump(nc, "declarations"); // type check body debugCheckFunctionBody(formula, formals, func); @@ -726,7 +726,7 @@ void SmtEngine::defineFunctionsRec( if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdDefineFunctionRec( + getPrinter().toStreamCmdDefineFunctionRec( getOutputManager().getDumpOut(), funcs, formals, formulas); } @@ -891,8 +891,8 @@ Result SmtEngine::checkSat(const Node& assumption, bool inUnsatCore) { if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdCheckSat( - getOutputManager().getDumpOut(), assumption); + getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut(), + assumption); } std::vector assump; if (!assumption.isNull()) @@ -909,13 +909,12 @@ Result SmtEngine::checkSat(const std::vector& assumptions, { if (assumptions.empty()) { - getOutputManager().getPrinter().toStreamCmdCheckSat( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdCheckSat(getOutputManager().getDumpOut()); } else { - getOutputManager().getPrinter().toStreamCmdCheckSatAssuming( - getOutputManager().getDumpOut(), assumptions); + getPrinter().toStreamCmdCheckSatAssuming(getOutputManager().getDumpOut(), + assumptions); } } return checkSatInternal(assumptions, inUnsatCore, false); @@ -925,8 +924,7 @@ Result SmtEngine::checkEntailed(const Node& node, bool inUnsatCore) { if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdQuery( - getOutputManager().getDumpOut(), node); + getPrinter().toStreamCmdQuery(getOutputManager().getDumpOut(), node); } return checkSatInternal( node.isNull() ? std::vector() : std::vector{node}, @@ -992,13 +990,15 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, } return r; - } catch (UnsafeInterruptException& e) { - AlwaysAssert(d_resourceManager->out()); + } + catch (UnsafeInterruptException& e) + { + AlwaysAssert(getResourceManager()->out()); // Notice that we do not notify the state of this result. If we wanted to // make the solver resume a working state after an interupt, then we would // implement a different callback and use it here, e.g. // d_state.notifyCheckSatInterupt. - Result::UnknownExplanation why = d_resourceManager->outOfResources() + Result::UnknownExplanation why = getResourceManager()->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); @@ -1024,7 +1024,7 @@ std::vector SmtEngine::getUnsatAssumptions(void) finishInit(); if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdGetUnsatAssumptions( + getPrinter().toStreamCmdGetUnsatAssumptions( getOutputManager().getDumpOut()); } UnsatCore core = getUnsatCoreInternal(); @@ -1048,9 +1048,9 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore) Trace("smt") << "SmtEngine::assertFormula(" << formula << ")" << endl; - if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdAssert( - getOutputManager().getDumpOut(), formula); + if (Dump.isOn("raw-benchmark")) + { + getPrinter().toStreamCmdAssert(getOutputManager().getDumpOut(), formula); } // Substitute out any abstract values in ex @@ -1072,7 +1072,7 @@ void SmtEngine::declareSygusVar(Node var) d_sygusSolver->declareSygusVar(var); if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdDeclareVar( + getPrinter().toStreamCmdDeclareVar( getOutputManager().getDumpOut(), var, var.getType()); } // don't need to set that the conjecture is stale @@ -1093,7 +1093,7 @@ void SmtEngine::declareSynthFun(Node func, if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdSynthFun( + getPrinter().toStreamCmdSynthFun( getOutputManager().getDumpOut(), func, vars, isInv, sygusType); } } @@ -1113,8 +1113,8 @@ void SmtEngine::assertSygusConstraint(Node constraint) d_sygusSolver->assertSygusConstraint(constraint); if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdConstraint( - getOutputManager().getDumpOut(), constraint); + getPrinter().toStreamCmdConstraint(getOutputManager().getDumpOut(), + constraint); } } @@ -1128,7 +1128,7 @@ void SmtEngine::assertSygusInvConstraint(Node inv, d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post); if (Dump.isOn("raw-benchmark")) { - getOutputManager().getPrinter().toStreamCmdInvConstraint( + getPrinter().toStreamCmdInvConstraint( getOutputManager().getDumpOut(), inv, pre, trans, post); } } @@ -1158,7 +1158,8 @@ Node SmtEngine::simplify(const Node& ex) Node SmtEngine::expandDefinitions(const Node& ex, bool expandOnly) { - d_resourceManager->spendResource(ResourceManager::Resource::PreprocessStep); + getResourceManager()->spendResource( + ResourceManager::Resource::PreprocessStep); SmtScope smts(this); finishInit(); @@ -1172,8 +1173,9 @@ Node SmtEngine::getValue(const Node& ex) const SmtScope smts(this); Trace("smt") << "SMT getValue(" << ex << ")" << endl; - if(Dump.isOn("benchmark")) { - d_outMgr.getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex}); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetValue(d_outMgr.getDumpOut(), {ex}); } TypeNode expectedType = ex.getType(); @@ -1237,9 +1239,9 @@ Model* SmtEngine::getModel() { finishInit(); - if(Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdGetModel( - getOutputManager().getDumpOut()); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetModel(getOutputManager().getDumpOut()); } Model* m = getAvailableModel("get model"); @@ -1275,8 +1277,7 @@ Result SmtEngine::blockModel() if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdBlockModel( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdBlockModel(getOutputManager().getDumpOut()); } Model* m = getAvailableModel("block model"); @@ -1304,8 +1305,8 @@ Result SmtEngine::blockModelValues(const std::vector& exprs) if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdBlockModelValues( - getOutputManager().getDumpOut(), exprs); + getPrinter().toStreamCmdBlockModelValues(getOutputManager().getDumpOut(), + exprs); } Model* m = getAvailableModel("block model values"); @@ -1323,14 +1324,14 @@ Result SmtEngine::blockModelValues(const std::vector& exprs) std::pair SmtEngine::getSepHeapAndNilExpr(void) { - if (!d_logic.isTheoryEnabled(THEORY_SEP)) + if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) { const char* msg = "Cannot obtain separation logic expressions if not using the " "separation logic theory."; throw RecoverableModalException(msg); } - NodeManagerScope nms(d_nodeManager); + NodeManagerScope nms(getNodeManager()); Node heap; Node nil; Model* m = getAvailableModel("get separation logic heap and nil"); @@ -1361,7 +1362,7 @@ std::vector SmtEngine::getExpandedAssertions() void SmtEngine::declareSepHeap(TypeNode locT, TypeNode dataT) { - if (!d_logic.isTheoryEnabled(THEORY_SEP)) + if (!getLogicInfo().isTheoryEnabled(THEORY_SEP)) { const char* msg = "Cannot declare heap if not using the separation logic theory."; @@ -1403,6 +1404,11 @@ void SmtEngine::checkProof() } } +StatisticsRegistry* SmtEngine::getStatisticsRegistry() +{ + return d_statisticsRegistry.get(); +} + UnsatCore SmtEngine::getUnsatCoreInternal() { #if IS_PROOFS_BUILD @@ -1512,8 +1518,7 @@ UnsatCore SmtEngine::getUnsatCore() { finishInit(); if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdGetUnsatCore( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetUnsatCore(getOutputManager().getDumpOut()); } return getUnsatCoreInternal(); } @@ -1525,8 +1530,7 @@ std::string SmtEngine::getProof() finishInit(); if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdGetProof( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdGetProof(getOutputManager().getDumpOut()); } #if IS_PROOFS_BUILD if (!options::proof()) @@ -1660,8 +1664,11 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict) { SmtScope smts(this); finishInit(); - if(!d_logic.isPure(THEORY_ARITH) && strict){ - Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; + const LogicInfo& logic = getLogicInfo(); + if (!logic.isPure(THEORY_ARITH) && strict) + { + Warning() << "Unexpected logic for quantifier elimination " << logic + << endl; } return d_quantElimSolver->getQuantifierElimination( *d_asserts, q, doFull, d_isInternalSubsolver); @@ -1727,9 +1734,9 @@ std::vector SmtEngine::getAssertions() SmtScope smts(this); finishInit(); d_state->doPendingPops(); - if(Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdGetAssertions( - getOutputManager().getDumpOut()); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdGetAssertions(getOutputManager().getDumpOut()); } Trace("smt") << "SMT getAssertions()" << endl; if(!options::produceAssertions()) { @@ -1756,8 +1763,7 @@ void SmtEngine::push() Trace("smt") << "SMT push()" << endl; d_smtSolver->processAssertions(*d_asserts); if(Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdPush( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdPush(getOutputManager().getDumpOut()); } d_state->userPush(); } @@ -1766,9 +1772,9 @@ void SmtEngine::pop() { SmtScope smts(this); finishInit(); Trace("smt") << "SMT pop()" << endl; - if(Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdPop( - getOutputManager().getDumpOut()); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdPop(getOutputManager().getDumpOut()); } d_state->userPop(); @@ -1785,17 +1791,18 @@ void SmtEngine::pop() { void SmtEngine::reset() { - SmtScope smts(this); + // save pointer to the current node manager + NodeManager* nm = getNodeManager(); Trace("smt") << "SMT reset()" << endl; - if(Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdReset( - getOutputManager().getDumpOut()); + if (Dump.isOn("benchmark")) + { + getPrinter().toStreamCmdReset(getOutputManager().getDumpOut()); } std::string filename = d_state->getFilename(); Options opts; opts.copyValues(d_originalOptions); this->~SmtEngine(); - new (this) SmtEngine(d_nodeManager, &opts); + new (this) SmtEngine(nm, &opts); // Restore data set after creation notifyStartParsing(filename); } @@ -1810,7 +1817,7 @@ void SmtEngine::resetAssertions() // (see solver execution modes in the SMT-LIB standard) Assert(getContext()->getLevel() == 0); Assert(getUserContext()->getLevel() == 0); - d_dumpm->resetAssertions(); + getDumpManager()->resetAssertions(); return; } @@ -1818,13 +1825,12 @@ void SmtEngine::resetAssertions() Trace("smt") << "SMT resetAssertions()" << endl; if (Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdResetAssertions( - getOutputManager().getDumpOut()); + getPrinter().toStreamCmdResetAssertions(getOutputManager().getDumpOut()); } d_asserts->clearCurrent(); d_state->notifyResetAssertions(); - d_dumpm->resetAssertions(); + getDumpManager()->resetAssertions(); // push the state to maintain global context around everything d_state->setup(); @@ -1841,28 +1847,34 @@ void SmtEngine::interrupt() d_smtSolver->interrupt(); } -void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) { - d_resourceManager->setResourceLimit(units, cumulative); +void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) +{ + getResourceManager()->setResourceLimit(units, cumulative); } void SmtEngine::setTimeLimit(unsigned long milis) { - d_resourceManager->setTimeLimit(milis); + getResourceManager()->setTimeLimit(milis); } -unsigned long SmtEngine::getResourceUsage() const { - return d_resourceManager->getResourceUsage(); +unsigned long SmtEngine::getResourceUsage() const +{ + return getResourceManager()->getResourceUsage(); } -unsigned long SmtEngine::getTimeUsage() const { - return d_resourceManager->getTimeUsage(); +unsigned long SmtEngine::getTimeUsage() const +{ + return getResourceManager()->getTimeUsage(); } unsigned long SmtEngine::getResourceRemaining() const { - return d_resourceManager->getResourceRemaining(); + return getResourceManager()->getResourceRemaining(); } -NodeManager* SmtEngine::getNodeManager() const { return d_nodeManager; } +NodeManager* SmtEngine::getNodeManager() const +{ + return d_env->getNodeManager(); +} Statistics SmtEngine::getStatistics() const { @@ -1876,13 +1888,13 @@ SExpr SmtEngine::getStatistic(std::string name) const void SmtEngine::flushStatistics(std::ostream& out) const { - d_nodeManager->getStatisticsRegistry()->flushInformation(out); + getNodeManager()->getStatisticsRegistry()->flushInformation(out); d_statisticsRegistry->flushInformation(out); } void SmtEngine::safeFlushStatistics(int fd) const { - d_nodeManager->getStatisticsRegistry()->safeFlushInformation(fd); + getNodeManager()->getStatisticsRegistry()->safeFlushInformation(fd); d_statisticsRegistry->safeFlushInformation(fd); } @@ -1900,11 +1912,11 @@ void SmtEngine::setUserAttribute(const std::string& attr, void SmtEngine::setOption(const std::string& key, const std::string& value) { - NodeManagerScope nms(d_nodeManager); + NodeManagerScope nms(getNodeManager()); Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - getOutputManager().getPrinter().toStreamCmdSetOption( + getPrinter().toStreamCmdSetOption( getOutputManager().getDumpOut(), key, value); } @@ -1932,7 +1944,7 @@ void SmtEngine::setOption(const std::string& key, const std::string& value) } std::string optionarg = value; - d_options.setOption(key, optionarg); + getOptions().setOption(key, optionarg); } void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } @@ -1941,7 +1953,7 @@ bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; } CVC4::SExpr SmtEngine::getOption(const std::string& key) const { - NodeManagerScope nms(d_nodeManager); + NodeManagerScope nms(getNodeManager()); Trace("smt") << "SMT getOption(" << key << ")" << endl; @@ -1959,7 +1971,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const } if(Dump.isOn("benchmark")) { - d_outMgr.getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key); + getPrinter().toStreamCmdGetOption(d_outMgr.getDumpOut(), key); } if(key == "command-verbosity") { @@ -1991,25 +2003,24 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr(result); } - return SExpr::parseAtom(d_options.getOption(key)); + return SExpr::parseAtom(getOptions().getOption(key)); } -Options& SmtEngine::getOptions() { return d_options; } +Options& SmtEngine::getOptions() { return d_env->d_options; } -const Options& SmtEngine::getOptions() const { return d_options; } +const Options& SmtEngine::getOptions() const { return d_env->getOptions(); } -ResourceManager* SmtEngine::getResourceManager() +ResourceManager* SmtEngine::getResourceManager() const { - return d_resourceManager.get(); + return d_env->getResourceManager(); } -DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); } +DumpManager* SmtEngine::getDumpManager() { return d_env->getDumpManager(); } -const Printer* SmtEngine::getPrinter() const -{ - return Printer::getPrinter(d_options[options::outputLanguage]); -} +const Printer& SmtEngine::getPrinter() const { return d_env->getPrinter(); } OutputManager& SmtEngine::getOutputManager() { return d_outMgr; } +theory::Rewriter* SmtEngine::getRewriter() { return d_env->getRewriter(); } + }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 4f10b6bc5..94c11be5b 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -33,10 +33,6 @@ #include "util/sexpr.h" #include "util/statistics.h" -// In terms of abstraction, this is below (and provides services to) -// ValidityChecker and above (and requires the services of) -// PropEngine. - namespace CVC4 { template class NodeTemplate; @@ -45,6 +41,7 @@ typedef NodeTemplate TNode; class TypeNode; struct NodeHashFunction; +class Env; class NodeManager; class TheoryEngine; class ProofManager; @@ -855,19 +852,19 @@ class CVC4_PUBLIC SmtEngine ProofManager* getProofManager() { return d_proofManager.get(); }; /** Get the resource manager of this SMT engine */ - ResourceManager* getResourceManager(); + ResourceManager* getResourceManager() const; /** Permit access to the underlying dump manager. */ smt::DumpManager* getDumpManager(); /** Get the printer used by this SMT engine */ - const Printer* getPrinter() const; + const Printer& getPrinter() const; /** Get the output manager for this SMT engine */ OutputManager& getOutputManager(); /** Get a pointer to the Rewriter owned by this SmtEngine. */ - theory::Rewriter* getRewriter() { return d_rewriter.get(); } + theory::Rewriter* getRewriter(); /** The type of our internal map of defined functions */ using DefinedFunctionMap = @@ -896,10 +893,7 @@ class CVC4_PUBLIC SmtEngine smt::PfManager* getPfManager() { return d_pfManager.get(); }; /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */ - StatisticsRegistry* getStatisticsRegistry() - { - return d_statisticsRegistry.get(); - }; + StatisticsRegistry* getStatisticsRegistry(); /** * Internal method to get an unsatisfiable core (only if immediately preceded @@ -1047,20 +1041,27 @@ class CVC4_PUBLIC SmtEngine /** Solver instance that owns this SmtEngine instance. */ api::Solver* d_solver = nullptr; + /** + * The statistics registry. Notice that this definition must be before the + * other members since it must be destroyed last if exceptions occur in the + * constructor of SmtEngine. + */ + std::unique_ptr d_statisticsRegistry; + /** + * The environment object, which contains all utilities that are globally + * available to internal code. + */ + std::unique_ptr d_env; /** * The state of this SmtEngine, which is responsible for maintaining which * SMT mode we are in, the contexts, the last result, etc. */ std::unique_ptr d_state; - /** Our internal node manager */ - NodeManager* d_nodeManager; /** Abstract values */ std::unique_ptr d_absValues; /** Assertions manager */ std::unique_ptr d_asserts; - /** The dump manager */ - std::unique_ptr d_dumpm; /** Resource out listener */ std::unique_ptr d_routListener; /** Node manager listener */ @@ -1094,14 +1095,6 @@ class CVC4_PUBLIC SmtEngine * from refutations. */ std::unique_ptr d_ucManager; - /** - * The rewriter associated with this SmtEngine. We have a different instance - * of the rewriter for each SmtEngine instance. This is because rewriters may - * hold references to objects that belong to theory solvers, which are - * specific to an SmtEngine/TheoryEngine instance. - */ - std::unique_ptr d_rewriter; - /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; @@ -1114,17 +1107,16 @@ class CVC4_PUBLIC SmtEngine std::unique_ptr d_interpolSolver; /** The solver for quantifier elimination queries */ std::unique_ptr d_quantElimSolver; + /** - * The logic we're in. This logic may be an extension of the logic set by the - * user. + * The logic set by the user. The actual logic, which may extend the user's + * logic, lives in the Env class. */ - LogicInfo d_logic; - - /** The logic set by the user. */ LogicInfo d_userLogic; /** - * Keep a copy of the original option settings (for reset()). + * Keep a copy of the original option settings (for reset()). The current + * options live in the Env object. */ Options d_originalOptions; @@ -1136,22 +1128,11 @@ class CVC4_PUBLIC SmtEngine */ std::map d_commandVerbosity; - /** The statistics registry */ - std::unique_ptr d_statisticsRegistry; - /** The statistics class */ std::unique_ptr d_stats; - /** The options object */ - Options d_options; - /** the output manager for commands */ mutable OutputManager d_outMgr; - - /** - * Manager for limiting time and abstract resource usage. - */ - std::unique_ptr d_resourceManager; /** * The options manager, which is responsible for implementing core options * such as those related to time outs and printing. It is also responsible diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp index 598e78080..cc528f89c 100644 --- a/src/smt/smt_engine_scope.cpp +++ b/src/smt/smt_engine_scope.cpp @@ -51,7 +51,7 @@ ResourceManager* currentResourceManager() } SmtScope::SmtScope(const SmtEngine* smt) - : NodeManagerScope(smt->d_nodeManager), + : NodeManagerScope(smt->getNodeManager()), d_oldSmtEngine(s_smtEngine_current), d_optionsScope(smt ? &const_cast(smt)->getOptions() : nullptr) { diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index 1da33cde4..504709942 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -20,10 +20,12 @@ namespace CVC4 { namespace smt { -SmtEngineState::SmtEngineState(SmtEngine& smt) +SmtEngineState::SmtEngineState(context::Context* c, + context::UserContext* u, + SmtEngine& smt) : d_smt(smt), - d_context(new context::Context()), - d_userContext(new context::UserContext()), + d_context(c), + d_userContext(u), d_pendingPops(0), d_fullyInited(false), d_queryMade(false), @@ -233,12 +235,9 @@ void SmtEngineState::popto(int toLevel) d_userContext->popto(toLevel); } -context::UserContext* SmtEngineState::getUserContext() -{ - return d_userContext.get(); -} +context::UserContext* SmtEngineState::getUserContext() { return d_userContext; } -context::Context* SmtEngineState::getContext() { return d_context.get(); } +context::Context* SmtEngineState::getContext() { return d_context; } Result SmtEngineState::getStatus() const { return d_status; } diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h index 032e15c79..3c3075bf5 100644 --- a/src/smt/smt_engine_state.h +++ b/src/smt/smt_engine_state.h @@ -47,7 +47,7 @@ namespace smt { class SmtEngineState { public: - SmtEngineState(SmtEngine& smt); + SmtEngineState(context::Context* c, context::UserContext* u, SmtEngine& smt); ~SmtEngineState() {} /** * Notify that the expected status of the next check-sat is given by the @@ -203,9 +203,9 @@ class SmtEngineState /** Reference to the SmtEngine */ SmtEngine& d_smt; /** Expr manager context */ - std::unique_ptr d_context; + context::Context* d_context; /** User level context */ - std::unique_ptr d_userContext; + context::UserContext* d_userContext; /** The context levels of user pushes */ std::vector d_userLevels; -- 2.30.2