diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-12-04 21:41:51 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-12-04 21:41:51 +0000 |
commit | 7efd777609f7fbc20701402ad949971cbc251f8f (patch) | |
tree | 88283b279c87ded14f5ecc7b1a54aa084c19139a /src/decision/decision_engine.cpp | |
parent | af44cd27d5b079f1279c407e610e557e81285d8f (diff) |
* Add support for --decision=justification + incremental (bug 437)
- Fix a destruction order issue this triggered in DE
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/decision/decision_engine.cpp')
-rw-r--r-- | src/decision/decision_engine.cpp | 23 |
1 files changed, 8 insertions, 15 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 22c70eb6d..9e8add752 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -33,7 +33,7 @@ DecisionEngine::DecisionEngine(context::Context *sc, d_enabledStrategies(), d_needIteSkolemMap(), d_relevancyStrategy(NULL), - d_assertions(), + d_assertions(uc), d_cnfStream(NULL), d_satSolver(NULL), d_satContext(sc), @@ -50,18 +50,6 @@ void DecisionEngine::init() d_engineState = 1; Trace("decision-init") << "DecisionEngine::init()" << std::endl; - if(options::incrementalSolving()) { - if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) { - if(options::decisionMode.wasSetByUser()) { - Warning() << "Ignorning decision option since using incremental mode (currently not supported together)" - << std::endl; - } else { - Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)" - << std::endl; - } - } - return; - } Trace("decision-init") << " * options->decisionMode: " << options::decisionMode() << std:: endl; Trace("decision-init") << " * options->decisionStopOnly: " @@ -70,11 +58,16 @@ void DecisionEngine::init() if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { } if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) { ITEDecisionStrategy* ds = - new decision::JustificationHeuristic(this, d_satContext); + new decision::JustificationHeuristic(this, d_userContext, d_satContext); enableStrategy(ds); d_needIteSkolemMap.push_back(ds); } if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) { + if(options::incrementalSolving()) { + Warning() << "Relevancy decision heuristic and incremental not supported together" + << std::endl; + return; // Currently not supported with incremental + } RelevancyStrategy* ds = new decision::Relevancy(this, d_satContext); enableStrategy(ds); @@ -137,7 +130,7 @@ void DecisionEngine::addAssertions(const vector<Node> &assertions, // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; - d_assertions.reserve(assertions.size()); + // d_assertions.reserve(assertions.size()); for(unsigned i = 0; i < assertions.size(); ++i) d_assertions.push_back(assertions[i]); |