diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-05 13:17:55 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-05 13:17:55 -0800 |
commit | a4151cb6755b9267cb90f7facc0ffd367aa7f0f2 (patch) | |
tree | d8d5511eeb12ecace73845785546df95e8f67f1f /src/decision | |
parent | bbba915f44f9e75eaa6238a10ba667643dacb00b (diff) |
Revert "Move ownership of DecisionEngine into PropEngine. (#3850)"
This reverts commit bbba915f44f9e75eaa6238a10ba667643dacb00b.
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_engine.cpp | 17 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 25 |
2 files changed, 32 insertions, 10 deletions
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<DecisionStrategy*>-s is the engine + */ + void enableStrategy(DecisionStrategy* ds); + };/* DecisionEngine class */ }/* CVC4 namespace */ |