From 5676b8bddcf001ba567ebb6d8e7b42dbd13ac9f3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Mon, 23 Apr 2012 17:56:19 +0000 Subject: Merge from decision branch -- partially working justification heuristic Overview of changes * command line option --decision={internal,justification} * justification heuristic handles all operators except ITEs revelant stats: decision::jh::* * if decisionEngine has solved the problem PropEngine returns unknown and smtEngine queries DE to get the answer relevant stat: smt::resultSource * there are known bugs Full list of commits being merged r3330 use CD data structures in JH r3329 add command-line option --decision=MODE r3328 timer stat, other fixes r3326 more trace r3325 enable implies, iff, xor (no further regression losses) r3324 feed decision engine lemmas, changes to quitting mechanism r3322 In progress r3321 more fixes... r3318 bugfix1 (69 more to go) r3317 Handle other boolean operators in JH (except ITE) r3316 mechanism for DE to stopSearch r3315 merge from trunk + JH translation continuation r3275 change option to enable JH by default[A --- src/decision/decision_engine.cpp | 25 ++++++++++++++++++++++--- 1 file changed, 22 insertions(+), 3 deletions(-) (limited to 'src/decision/decision_engine.cpp') diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index dbdbb83a9..7c8718370 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -26,16 +26,23 @@ using namespace std; namespace CVC4 { -DecisionEngine::DecisionEngine() : +DecisionEngine::DecisionEngine(context::Context *c) : + d_enabledStrategies(), d_needSimplifiedPreITEAssertions(), + d_assertions(), d_cnfStream(NULL), - d_satSolver(NULL) + d_satSolver(NULL), + d_satContext(c), + d_result(SAT_VALUE_UNKNOWN) { const Options* options = Options::current(); Trace("decision") << "Creating decision engine" << std::endl; + + if(options->incrementalSolving) return; + if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { } if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) { - DecisionStrategy* ds = new decision::JustificationHeuristic(this); + DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext); enableStrategy(ds); } } @@ -49,6 +56,7 @@ void DecisionEngine::enableStrategy(DecisionStrategy* ds) void DecisionEngine::informSimplifiedPreITEAssertions(const vector &assertions) { + d_result = SAT_VALUE_UNKNOWN; d_assertions.reserve(assertions.size()); for(unsigned i = 0; i < assertions.size(); ++i) d_assertions.push_back(assertions[i]); @@ -56,4 +64,15 @@ void DecisionEngine::informSimplifiedPreITEAssertions(const vector &assert d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); } +void DecisionEngine::addAssertion(Node n) +{ + d_result = SAT_VALUE_UNKNOWN; + if(needSimplifiedPreITEAssertions()) { + d_assertions.push_back(n); + } + for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i) + d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); +} + + }/* CVC4 namespace */ -- cgit v1.2.3