From bbba915f44f9e75eaa6238a10ba667643dacb00b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Mar 2020 15:12:57 -0600 Subject: [PATCH] Move ownership of DecisionEngine into PropEngine. (#3850) This is in preparation of fixing the issue we currently have with reset-assertions. This also removes a competition hack for QF_LRA. --- src/decision/decision_engine.cpp | 17 +++++----- src/decision/decision_engine.h | 25 +-------------- .../preprocessing_pass_context.h | 1 - src/prop/prop_engine.cpp | 16 +++++++--- src/prop/prop_engine.h | 12 +++++-- src/smt/smt_engine.cpp | 32 ++----------------- src/smt/smt_engine.h | 2 -- src/theory/theory_engine.cpp | 6 ++-- src/theory/theory_engine.h | 9 ------ 9 files changed, 37 insertions(+), 83 deletions(-) diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index dc798626e..7d31d930f 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -56,20 +56,21 @@ void DecisionEngine::init() { ITEDecisionStrategy* ds = new decision::JustificationHeuristic(this, d_userContext, d_satContext); - enableStrategy(ds); + d_enabledStrategies.push_back(ds); d_needIteSkolemMap.push_back(ds); } } - -void DecisionEngine::enableStrategy(DecisionStrategy* ds) +void DecisionEngine::shutdown() { - d_enabledStrategies.push_back(ds); -} + Trace("decision") << "Shutting down decision engine" << std::endl; -void DecisionEngine::clearStrategies(){ - for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){ - delete d_enabledStrategies[i]; + Assert(d_engineState == 1); + d_engineState = 2; + + for (DecisionStrategy* s : d_enabledStrategies) + { + delete s; } d_enabledStrategies.clear(); d_needIteSkolemMap.clear(); diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 5ebcda8fe..afa306325 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -96,22 +96,12 @@ public: /* enables decision stragies based on options */ void init(); - /* clears all of the strategies */ - void clearStrategies(); - - /** * This is called by SmtEngine, at shutdown time, just before * destruction. It is important because there are destruction * ordering issues between some parts of the system. */ - void shutdown() { - Assert(d_engineState == 1); - d_engineState = 2; - - Trace("decision") << "Shutting down decision engine" << std::endl; - clearStrategies(); - } + void shutdown(); // Interface for External World to use our services @@ -170,11 +160,6 @@ public: // External World helping us help the Strategies - /** If one of the enabled strategies needs them */ - /* bool needIteSkolemMap() { */ - /* return d_needIteSkolemMap.size() > 0; */ - /* } */ - /** * Add a list of assertions from an AssertionPipeline. */ @@ -208,14 +193,6 @@ public: Node getNode(SatLiteral l) { return d_cnfStream->getNode(l); } - -private: - /** - * Enable a particular decision strategy, also updating - * corresponding vector-s is the engine - */ - void enableStrategy(DecisionStrategy* ds); - };/* DecisionEngine class */ }/* CVC4 namespace */ diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 70b1f70c2..b32a2a86f 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -45,7 +45,6 @@ class PreprocessingPassContext SmtEngine* getSmt() { return d_smt; } TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; } - DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } context::Context* getDecisionContext() { return d_smt->d_context; } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 05704c0fa..546567b98 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -75,14 +75,12 @@ public: }; PropEngine::PropEngine(TheoryEngine* te, - DecisionEngine* de, Context* satContext, - Context* userContext, + UserContext* userContext, std::ostream* replayLog, ExprStream* replayStream) : d_inCheckSat(false), d_theoryEngine(te), - d_decisionEngine(de), d_context(satContext), d_theoryProxy(NULL), d_satSolver(NULL), @@ -94,6 +92,9 @@ PropEngine::PropEngine(TheoryEngine* te, Debug("prop") << "Constructing the PropEngine" << endl; + d_decisionEngine.reset(new DecisionEngine(satContext, userContext)); + d_decisionEngine->init(); // enable appropriate strategies + d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry()); d_registrar = new theory::TheoryRegistrar(d_theoryEngine); @@ -102,7 +103,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy = new TheoryProxy(this, d_theoryEngine, - d_decisionEngine, + d_decisionEngine.get(), d_context, d_cnfStream, replayLog, @@ -118,6 +119,7 @@ PropEngine::PropEngine(TheoryEngine* te, PropEngine::~PropEngine() { Debug("prop") << "Destructing the PropEngine" << endl; + d_decisionEngine->shutdown(); delete d_cnfStream; delete d_registrar; delete d_satSolver; @@ -142,6 +144,12 @@ void PropEngine::assertLemma(TNode node, bool negated, d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } +void PropEngine::addAssertionsToDecisionEngine( + const preprocessing::AssertionPipeline& assertions) +{ + d_decisionEngine->addAssertions(assertions); +} + void PropEngine::requirePhase(TNode n, bool phase) { Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << endl; diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 061fbbca6..707244ff5 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -27,6 +27,7 @@ #include "expr/expr_stream.h" #include "expr/node.h" #include "options/options.h" +#include "preprocessing/assertion_pipeline.h" #include "proof/proof_manager.h" #include "util/resource_manager.h" #include "util/result.h" @@ -60,9 +61,8 @@ class PropEngine * Create a PropEngine with a particular decision and theory engine. */ PropEngine(TheoryEngine*, - DecisionEngine*, context::Context* satContext, - context::Context* userContext, + context::UserContext* userContext, std::ostream* replayLog, ExprStream* replayStream); @@ -104,6 +104,12 @@ class PropEngine ProofRule rule, TNode from = TNode::null()); + /** + * Pass a list of assertions from an AssertionPipeline to the decision engine. + */ + void addAssertionsToDecisionEngine( + const preprocessing::AssertionPipeline& assertions); + /** * If ever n is decided upon, it must be in the given phase. This * occurs *globally*, i.e., even if the literal is untranslated by @@ -223,7 +229,7 @@ class PropEngine TheoryEngine* d_theoryEngine; /** The decision engine we will be using */ - DecisionEngine* d_decisionEngine; + std::unique_ptr d_decisionEngine; /** The context */ context::Context* d_context; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3e9b81263..89f3acd56 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -850,7 +850,6 @@ SmtEngine::SmtEngine(ExprManager* em) d_userLevels(), d_exprManager(em), d_nodeManager(d_exprManager->getNodeManager()), - d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), d_proofManager(NULL), @@ -935,12 +934,8 @@ void SmtEngine::finishInit() Trace("smt-debug") << "Making decision engine..." << std::endl; - d_decisionEngine = new DecisionEngine(d_context, d_userContext); - d_decisionEngine->init(); // enable appropriate strategies - Trace("smt-debug") << "Making prop engine..." << std::endl; d_propEngine = new PropEngine(d_theoryEngine, - d_decisionEngine, d_context, d_userContext, d_private->getReplayLog(), @@ -948,7 +943,6 @@ void SmtEngine::finishInit() Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(d_propEngine); - d_theoryEngine->setDecisionEngine(d_decisionEngine); Trace("smt-debug") << "Finishing init for theory engine..." << std::endl; d_theoryEngine->finishInit(); @@ -1033,9 +1027,6 @@ void SmtEngine::shutdown() { if(d_theoryEngine != NULL) { d_theoryEngine->shutdown(); } - if(d_decisionEngine != NULL) { - d_decisionEngine->shutdown(); - } } SmtEngine::~SmtEngine() @@ -1092,8 +1083,6 @@ SmtEngine::~SmtEngine() d_theoryEngine = NULL; delete d_propEngine; d_propEngine = NULL; - delete d_decisionEngine; - d_decisionEngine = NULL; delete d_stats; d_stats = NULL; @@ -3100,22 +3089,6 @@ Result SmtEngine::check() { d_private->processAssertions(); Trace("smt") << "SmtEngine::check(): done processing assertions" << endl; - // Turn off stop only for QF_LRA - // TODO: Bring up in a meeting where to put this - if(options::decisionStopOnly() && !options::decisionMode.wasSetByUser() ){ - if( // QF_LRA - (not d_logic.isQuantified() && - d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areIntegersUsed() - )){ - if (d_private->getIteSkolemMap().empty()) - { - options::decisionStopOnly.set(false); - d_decisionEngine->clearStrategies(); - Trace("smt") << "SmtEngine::check(): turning off stop only" << endl; - } - } - } - TimerStat::CodeTimer solveTimer(d_stats->d_solveTime); Chat() << "solving..." << endl; @@ -3616,10 +3589,11 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() ); // Push the formula to decision engine - if(noConflict) { + if (noConflict) + { Chat() << "pushing to decision engine..." << endl; Assert(iteRewriteAssertionsEnd == d_assertions.size()); - d_smt.d_decisionEngine->addAssertions(d_assertions); + d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions); } // end: INVARIANT to maintain: no reordering of assertions or diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0ef22f353..1424352ef 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1059,9 +1059,7 @@ class CVC4_PUBLIC SmtEngine ExprManager* d_exprManager; /** Our internal expression/node manager */ NodeManager* d_nodeManager; - /** The decision engine */ - DecisionEngine* d_decisionEngine; /** The theory engine */ TheoryEngine* d_theoryEngine; /** The propositional engine */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a39c014a6..60ad00fc5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -315,7 +315,6 @@ TheoryEngine::TheoryEngine(context::Context* context, RemoveTermFormulas& iteRemover, const LogicInfo& logicInfo) : d_propEngine(nullptr), - d_decisionEngine(nullptr), d_context(context), d_userContext(userContext), d_logicInfo(logicInfo), @@ -1924,8 +1923,9 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to decision engine - if(!removable) { - d_decisionEngine->addAssertions(additionalLemmas); + if (!removable) + { + d_propEngine->addAssertionsToDecisionEngine(additionalLemmas); } // Mark that we added some lemmas diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 1757d7a6d..e8223f1a1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -101,7 +101,6 @@ namespace theory { class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ -class DecisionEngine; class RemoveTermFormulas; /** @@ -119,9 +118,6 @@ class TheoryEngine { /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; - /** Access to decision engine */ - DecisionEngine* d_decisionEngine; - /** Our context */ context::Context* d_context; @@ -505,11 +501,6 @@ class TheoryEngine { d_propEngine = propEngine; } - inline void setDecisionEngine(DecisionEngine* decisionEngine) { - Assert(d_decisionEngine == NULL); - d_decisionEngine = decisionEngine; - } - /** Called when all initialization of options/logic is done */ void finishInit(); -- 2.30.2