diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-05 15:12:57 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 15:12:57 -0600 |
commit | bbba915f44f9e75eaa6238a10ba667643dacb00b (patch) | |
tree | 981c352e9aae8c96539374e98065101ee3835b28 /src/decision | |
parent | d26ee67911fedfef966a0e4d64ffda02007d65a0 (diff) |
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.
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, 10 insertions, 32 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<DecisionStrategy*>-s is the engine - */ - void enableStrategy(DecisionStrategy* ds); - };/* DecisionEngine class */ }/* CVC4 namespace */ |