From: Aina Niemetz Date: Thu, 5 Mar 2020 21:17:55 +0000 (-0800) Subject: Revert "Move ownership of DecisionEngine into PropEngine. (#3850)" X-Git-Tag: cvc5-1.0.0~3565 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a4151cb6755b9267cb90f7facc0ffd367aa7f0f2;p=cvc5.git Revert "Move ownership of DecisionEngine into PropEngine. (#3850)" This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b. --- diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 7d31d930f..dc798626e 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -56,21 +56,20 @@ void DecisionEngine::init() { ITEDecisionStrategy* ds = new decision::JustificationHeuristic(this, d_userContext, d_satContext); - d_enabledStrategies.push_back(ds); + enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } } -void DecisionEngine::shutdown() -{ - Trace("decision") << "Shutting down decision engine" << std::endl; - Assert(d_engineState == 1); - d_engineState = 2; +void DecisionEngine::enableStrategy(DecisionStrategy* ds) +{ + d_enabledStrategies.push_back(ds); +} - for (DecisionStrategy* s : d_enabledStrategies) - { - delete s; +void DecisionEngine::clearStrategies(){ + for(unsigned i = 0; i < d_enabledStrategies.size(); ++i){ + delete d_enabledStrategies[i]; } d_enabledStrategies.clear(); d_needIteSkolemMap.clear(); diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index afa306325..5ebcda8fe 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -96,12 +96,22 @@ 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(); + void shutdown() { + Assert(d_engineState == 1); + d_engineState = 2; + + Trace("decision") << "Shutting down decision engine" << std::endl; + clearStrategies(); + } // Interface for External World to use our services @@ -160,6 +170,11 @@ 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. */ @@ -193,6 +208,14 @@ 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 b32a2a86f..70b1f70c2 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -45,6 +45,7 @@ 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 546567b98..05704c0fa 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -75,12 +75,14 @@ public: }; PropEngine::PropEngine(TheoryEngine* te, + DecisionEngine* de, Context* satContext, - UserContext* userContext, + Context* userContext, std::ostream* replayLog, ExprStream* replayStream) : d_inCheckSat(false), d_theoryEngine(te), + d_decisionEngine(de), d_context(satContext), d_theoryProxy(NULL), d_satSolver(NULL), @@ -92,9 +94,6 @@ 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); @@ -103,7 +102,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_theoryProxy = new TheoryProxy(this, d_theoryEngine, - d_decisionEngine.get(), + d_decisionEngine, d_context, d_cnfStream, replayLog, @@ -119,7 +118,6 @@ PropEngine::PropEngine(TheoryEngine* te, PropEngine::~PropEngine() { Debug("prop") << "Destructing the PropEngine" << endl; - d_decisionEngine->shutdown(); delete d_cnfStream; delete d_registrar; delete d_satSolver; @@ -144,12 +142,6 @@ 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 707244ff5..061fbbca6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -27,7 +27,6 @@ #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" @@ -61,8 +60,9 @@ class PropEngine * Create a PropEngine with a particular decision and theory engine. */ PropEngine(TheoryEngine*, + DecisionEngine*, context::Context* satContext, - context::UserContext* userContext, + context::Context* userContext, std::ostream* replayLog, ExprStream* replayStream); @@ -104,12 +104,6 @@ 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 @@ -229,7 +223,7 @@ class PropEngine TheoryEngine* d_theoryEngine; /** The decision engine we will be using */ - std::unique_ptr d_decisionEngine; + DecisionEngine* d_decisionEngine; /** The context */ context::Context* d_context; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 89f3acd56..3e9b81263 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -850,6 +850,7 @@ 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), @@ -934,8 +935,12 @@ 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(), @@ -943,6 +948,7 @@ 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(); @@ -1027,6 +1033,9 @@ void SmtEngine::shutdown() { if(d_theoryEngine != NULL) { d_theoryEngine->shutdown(); } + if(d_decisionEngine != NULL) { + d_decisionEngine->shutdown(); + } } SmtEngine::~SmtEngine() @@ -1083,6 +1092,8 @@ SmtEngine::~SmtEngine() d_theoryEngine = NULL; delete d_propEngine; d_propEngine = NULL; + delete d_decisionEngine; + d_decisionEngine = NULL; delete d_stats; d_stats = NULL; @@ -3089,6 +3100,22 @@ 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; @@ -3589,11 +3616,10 @@ 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_propEngine->addAssertionsToDecisionEngine(d_assertions); + d_smt.d_decisionEngine->addAssertions(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 1424352ef..0ef22f353 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1059,7 +1059,9 @@ 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 60ad00fc5..a39c014a6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -315,6 +315,7 @@ 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), @@ -1923,9 +1924,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, } // assert to decision engine - if (!removable) - { - d_propEngine->addAssertionsToDecisionEngine(additionalLemmas); + if(!removable) { + d_decisionEngine->addAssertions(additionalLemmas); } // Mark that we added some lemmas diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e8223f1a1..1757d7a6d 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -101,6 +101,7 @@ namespace theory { class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ +class DecisionEngine; class RemoveTermFormulas; /** @@ -118,6 +119,9 @@ class TheoryEngine { /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; + /** Access to decision engine */ + DecisionEngine* d_decisionEngine; + /** Our context */ context::Context* d_context; @@ -501,6 +505,11 @@ 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();