diff options
| -rw-r--r-- | src/prop/prop_engine.cpp | 32 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 15 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_solver.cpp | 43 | ||||
| -rw-r--r-- | src/smt/smt_solver.h | 7 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 62 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 27 |
7 files changed, 92 insertions, 96 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 5903c1606..dfd4c4528 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -35,6 +35,7 @@ #include "prop/sat_solver.h" #include "prop/sat_solver_factory.h" #include "prop/theory_proxy.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" #include "theory/theory_engine.h" @@ -65,15 +66,13 @@ public: }; PropEngine::PropEngine(TheoryEngine* te, - context::Context* satContext, - context::UserContext* userContext, - ResourceManager* rm, + Env& env, OutputManager& outMgr, ProofNodeManager* pnm) : d_inCheckSat(false), d_theoryEngine(te), - d_context(satContext), - d_skdm(new SkolemDefManager(satContext, userContext)), + d_env(env), + d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())), d_theoryProxy(nullptr), d_satSolver(nullptr), d_pnm(pnm), @@ -81,11 +80,13 @@ PropEngine::PropEngine(TheoryEngine* te, d_pfCnfStream(nullptr), d_ppm(nullptr), d_interrupted(false), - d_resourceManager(rm), d_outMgr(outMgr), - d_assumptions(userContext) + d_assumptions(d_env.getUserContext()) { Debug("prop") << "Constructing the PropEngine" << std::endl; + context::Context* satContext = d_env.getContext(); + context::UserContext* userContext = d_env.getUserContext(); + ResourceManager* rm = d_env.getResourceManager(); d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm)); d_decisionEngine->init(); // enable appropriate strategies @@ -112,9 +113,9 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy->finishInit(d_cnfStream); // connect SAT solver d_satSolver->initialize( - d_context, + d_env.getContext(), d_theoryProxy, - userContext, + d_env.getUserContext(), options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS ? pnm : nullptr); @@ -395,13 +396,16 @@ Result PropEngine::checkSat() { } if( result == SAT_VALUE_UNKNOWN ) { - + ResourceManager* rm = d_env.getResourceManager(); Result::UnknownExplanation why = Result::INTERRUPTED; - if (d_resourceManager->outOfTime()) + if (rm->outOfTime()) + { why = Result::TIMEOUT; - if (d_resourceManager->outOfResources()) + } + if (rm->outOfResources()) + { why = Result::RESOURCEOUT; - + } return Result(Result::SAT_UNKNOWN, why); } @@ -576,7 +580,7 @@ void PropEngine::interrupt() void PropEngine::spendResource(Resource r) { - d_resourceManager->spendResource(r); + d_env.getResourceManager()->spendResource(r); } bool PropEngine::properExplanation(TNode node, TNode expl) const diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 6812a6549..631317c2d 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -29,6 +29,7 @@ namespace cvc5 { +class Env; class ResourceManager; class OutputManager; class ProofNodeManager; @@ -56,10 +57,8 @@ class PropEngine /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, - context::Context* satContext, - context::UserContext* userContext, - ResourceManager* rm, + PropEngine(TheoryEngine* te, + Env& env, OutputManager& outMgr, ProofNodeManager* pnm); @@ -341,12 +340,12 @@ class PropEngine /** The theory engine we will be using */ TheoryEngine* d_theoryEngine; + /** Reference to the environment */ + Env& d_env; + /** The decision engine we will be using */ std::unique_ptr<decision::DecisionEngine> d_decisionEngine; - /** The context */ - context::Context* d_context; - /** The skolem definition manager */ std::unique_ptr<SkolemDefManager> d_skdm; @@ -372,8 +371,6 @@ class PropEngine /** Whether we were just interrupted (or not) */ bool d_interrupted; - /** Pointer to resource manager for associated SmtEngine */ - ResourceManager* d_resourceManager; /** Reference to the output manager of the smt engine */ OutputManager& d_outMgr; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cee07a3dc..cccb4f544 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -133,7 +133,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr) new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats)); // make the SMT solver d_smtSolver.reset( - new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats)); + new SmtSolver(*this, *d_env.get(), *d_state, *d_pp, *d_stats)); // make the SyGuS solver d_sygusSolver.reset( new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr)); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 4c841ce9c..d7b70f501 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -18,6 +18,7 @@ #include "options/smt_options.h" #include "prop/prop_engine.h" #include "smt/assertions.h" +#include "smt/env.h" #include "smt/preprocessor.h" #include "smt/smt_engine.h" #include "smt/smt_engine_state.h" @@ -32,13 +33,13 @@ namespace cvc5 { namespace smt { SmtSolver::SmtSolver(SmtEngine& smt, + Env& env, SmtEngineState& state, - ResourceManager* rm, Preprocessor& pp, SmtEngineStatistics& stats) : d_smt(smt), + d_env(env), d_state(state), - d_rm(rm), d_pp(pp), d_stats(stats), d_pnm(nullptr), @@ -54,10 +55,7 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine.reset(new TheoryEngine( - d_smt.getContext(), - d_smt.getUserContext(), - d_rm, - logicInfo, + d_env, d_smt.getOutputManager(), // Other than whether d_pm is set, theory engine proofs are conditioned on // the relationshup between proofs and unsat cores: the unsat cores are in @@ -83,12 +81,8 @@ void SmtSolver::finishInit(const LogicInfo& logicInfo) * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), - d_smt.getContext(), - d_smt.getUserContext(), - d_rm, - d_smt.getOutputManager(), - d_pnm)); + d_propEngine.reset(new prop::PropEngine( + d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm)); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -104,12 +98,8 @@ void SmtSolver::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(), - d_smt.getContext(), - d_smt.getUserContext(), - d_rm, - d_smt.getOutputManager(), - d_pnm)); + d_propEngine.reset(new prop::PropEngine( + d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm)); d_theoryEngine->setPropEngine(getPropEngine()); // Notice that we do not reset TheoryEngine, nor does it require calling // finishInit again. In particular, TheoryEngine::finishInit does not @@ -159,13 +149,14 @@ Result SmtSolver::checkSatisfiability(Assertions& as, Trace("smt") << "SmtSolver::check()" << endl; const std::string& filename = d_state.getFilename(); - if (d_rm->out()) + ResourceManager* rm = d_env.getResourceManager(); + if (rm->out()) { Result::UnknownExplanation why = - d_rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; + rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; return Result(Result::ENTAILMENT_UNKNOWN, why, filename); } - d_rm->beginCall(); + rm->beginCall(); // Make sure the prop layer has all of the assertions Trace("smt") << "SmtSolver::check(): processing assertions" << endl; @@ -178,10 +169,10 @@ Result SmtSolver::checkSatisfiability(Assertions& as, Trace("smt") << "SmtSolver::check(): running check" << endl; Result result = d_propEngine->checkSat(); - d_rm->endCall(); + rm->endCall(); Trace("limit") << "SmtSolver::check(): cumulative millis " - << d_rm->getTimeUsage() << ", resources " - << d_rm->getResourceUsage() << endl; + << rm->getTimeUsage() << ", resources " + << rm->getResourceUsage() << endl; if ((options::solveRealAsInt() || options::solveIntAsBV() > 0) && result.asSatisfiabilityResult().isSat() == Result::UNSAT) @@ -202,7 +193,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, // includes linear arithmetic and bitvectors, which are the primary // targets for the global negate option. Other logics are possible here // but not considered. - LogicInfo logic = d_smt.getLogicInfo(); + LogicInfo logic = d_env.getLogicInfo(); if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) || logic.isPure(theory::THEORY_BV)) { @@ -228,7 +219,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as, void SmtSolver::processAssertions(Assertions& as) { TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime); - d_rm->spendResource(Resource::PreprocessStep); + d_env.getResourceManager()->spendResource(Resource::PreprocessStep); Assert(d_state.isFullyReady()); preprocessing::AssertionPipeline& ap = as.getAssertionPipeline(); diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 8689f152c..01e52fbfa 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -27,6 +27,7 @@ namespace cvc5 { class SmtEngine; +class Env; class TheoryEngine; class ResourceManager; class ProofNodeManager; @@ -64,8 +65,8 @@ class SmtSolver { public: SmtSolver(SmtEngine& smt, + Env& env, SmtEngineState& state, - ResourceManager* rm, Preprocessor& pp, SmtEngineStatistics& stats); ~SmtSolver(); @@ -135,10 +136,10 @@ class SmtSolver private: /** Reference to the parent SMT engine */ SmtEngine& d_smt; + /** Reference to the environment */ + Env& d_env; /** Reference to the state of the SmtEngine */ SmtEngineState& d_state; - /** Pointer to a resource manager (owned by SmtEngine) */ - ResourceManager* d_rm; /** Reference to the preprocessor of SmtEngine */ Preprocessor& d_pp; /** Reference to the statistics of SmtEngine */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index b4ad09d77..ccdd2bf4b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -31,6 +31,7 @@ #include "printer/printer.h" #include "prop/prop_engine.h" #include "smt/dump.h" +#include "smt/env.h" #include "smt/logic_exception.h" #include "smt/output_manager.h" #include "theory/combination_care_graph.h" @@ -156,7 +157,7 @@ void TheoryEngine::finishInit() if (options::relevanceFilter()) { d_relManager.reset( - new RelevanceManager(d_userContext, theory::Valuation(this))); + new RelevanceManager(d_env.getUserContext(), theory::Valuation(this))); } // initialize the quantifiers engine @@ -205,48 +206,55 @@ void TheoryEngine::finishInit() ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; } -TheoryEngine::TheoryEngine(context::Context* context, - context::UserContext* userContext, - ResourceManager* rm, - const LogicInfo& logicInfo, +context::Context* TheoryEngine::getSatContext() const +{ + return d_env.getContext(); +} + +context::UserContext* TheoryEngine::getUserContext() const +{ + return d_env.getUserContext(); +} + +TheoryEngine::TheoryEngine(Env& env, OutputManager& outMgr, ProofNodeManager* pnm) : d_propEngine(nullptr), - d_context(context), - d_userContext(userContext), - d_logicInfo(logicInfo), + d_env(env), + d_logicInfo(env.getLogicInfo()), d_outMgr(outMgr), d_pnm(pnm), - d_lazyProof( - d_pnm != nullptr ? new LazyCDProof( - d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") - : nullptr), - d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)), + d_lazyProof(d_pnm != nullptr + ? new LazyCDProof(d_pnm, + nullptr, + d_env.getUserContext(), + "TheoryEngine::LazyCDProof") + : nullptr), + d_tepg(new TheoryEngineProofGenerator(d_pnm, d_env.getUserContext())), d_tc(nullptr), d_sharedSolver(nullptr), d_quantEngine(nullptr), - d_decManager(new DecisionManager(userContext)), + d_decManager(new DecisionManager(d_env.getUserContext())), d_relManager(nullptr), d_eager_model_building(false), - d_inConflict(context, false), + d_inConflict(d_env.getContext(), false), d_inSatMode(false), d_hasShutDown(false), - d_incomplete(context, false), - d_incompleteTheory(context, THEORY_BUILTIN), - d_incompleteId(context, IncompleteId::UNKNOWN), - d_propagationMap(context), - d_propagationMapTimestamp(context, 0), - d_propagatedLiterals(context), - d_propagatedLiteralsIndex(context, 0), - d_atomRequests(context), + d_incomplete(d_env.getContext(), false), + d_incompleteTheory(d_env.getContext(), THEORY_BUILTIN), + d_incompleteId(d_env.getContext(), IncompleteId::UNKNOWN), + d_propagationMap(d_env.getContext()), + d_propagationMapTimestamp(d_env.getContext(), 0), + d_propagatedLiterals(d_env.getContext()), + d_propagatedLiteralsIndex(d_env.getContext(), 0), + d_atomRequests(d_env.getContext()), d_combineTheoriesTime(smtStatisticsRegistry().registerTimer( "TheoryEngine::combineTheoriesTime")), d_true(), d_false(), d_interrupted(false), - d_resourceManager(rm), d_inPreregister(false), - d_factsAsserted(context, false), + d_factsAsserted(d_env.getContext(), false), d_attr_handle() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; @@ -1041,7 +1049,7 @@ void TheoryEngine::assertFact(TNode literal) bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl; - Trace("dtview::prop") << std::string(d_context->getLevel(), ' ') + Trace("dtview::prop") << std::string(d_env.getContext()->getLevel(), ' ') << ":THEORY-PROP: " << literal << endl; // spendResource(); @@ -1924,7 +1932,7 @@ bool TheoryEngine::isFiniteType(TypeNode tn) const void TheoryEngine::spendResource(Resource r) { - d_resourceManager->spendResource(r); + d_env.getResourceManager()->spendResource(r); } void TheoryEngine::initializeProofChecker(ProofChecker* pc) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e870860c5..4c097a262 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -42,6 +42,7 @@ namespace cvc5 { +class Env; class ResourceManager; class OutputManager; class TheoryEngineProofGenerator; @@ -107,11 +108,10 @@ class TheoryEngine { /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; - /** Our context */ - context::Context* d_context; - - /** Our user context */ - context::UserContext* d_userContext; + /** + * Reference to the environment. + */ + Env& d_env; /** * A table of from theory IDs to theory pointers. Never use this table @@ -127,6 +127,7 @@ class TheoryEngine { * the cost of walking the DAG on registration, etc. */ const LogicInfo& d_logicInfo; + /** The separation logic location and data types */ TypeNode d_sepLocType; TypeNode d_sepDataType; @@ -290,16 +291,10 @@ class TheoryEngine { /** Whether we were just interrupted (or not) */ bool d_interrupted; - ResourceManager* d_resourceManager; public: /** Constructs a theory engine */ - TheoryEngine(context::Context* context, - context::UserContext* userContext, - ResourceManager* rm, - const LogicInfo& logic, - OutputManager& outMgr, - ProofNodeManager* pnm); + TheoryEngine(Env& env, OutputManager& outMgr, ProofNodeManager* pnm); /** Destroys a theory engine */ ~TheoryEngine(); @@ -318,8 +313,8 @@ class TheoryEngine { { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = new TheoryClass(d_context, - d_userContext, + d_theoryTable[theoryId] = new TheoryClass(getSatContext(), + getUserContext(), *d_theoryOut[theoryId], theory::Valuation(this), d_logicInfo, @@ -358,12 +353,12 @@ class TheoryEngine { /** * Get a pointer to the underlying sat context. */ - context::Context* getSatContext() const { return d_context; } + context::Context* getSatContext() const; /** * Get a pointer to the underlying user context. */ - context::UserContext* getUserContext() const { return d_userContext; } + context::UserContext* getUserContext() const; /** * Get a pointer to the underlying quantifiers engine. |