diff options
Diffstat (limited to 'src/decision/decision_engine.cpp')
-rw-r--r-- | src/decision/decision_engine.cpp | 57 |
1 files changed, 39 insertions, 18 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 7c8718370..1d4f2fd42 100644 --- a/src/decision/decision_engine.cpp +++ b/src/decision/decision_engine.cpp @@ -26,13 +26,15 @@ using namespace std; namespace CVC4 { -DecisionEngine::DecisionEngine(context::Context *c) : + DecisionEngine::DecisionEngine(context::Context *sc, + context::Context *uc) : d_enabledStrategies(), - d_needSimplifiedPreITEAssertions(), + d_needIteSkolemMap(), d_assertions(), d_cnfStream(NULL), d_satSolver(NULL), - d_satContext(c), + d_satContext(sc), + d_userContext(uc), d_result(SAT_VALUE_UNKNOWN) { const Options* options = Options::current(); @@ -42,37 +44,56 @@ DecisionEngine::DecisionEngine(context::Context *c) : if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { } if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) { - DecisionStrategy* ds = new decision::JustificationHeuristic(this, d_satContext); + ITEDecisionStrategy* ds = + new decision::JustificationHeuristic(this, d_satContext); enableStrategy(ds); + d_needIteSkolemMap.push_back(ds); } } void DecisionEngine::enableStrategy(DecisionStrategy* ds) { d_enabledStrategies.push_back(ds); - if( ds->needSimplifiedPreITEAssertions() ) - d_needSimplifiedPreITEAssertions.push_back(ds); } -void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions) + +void DecisionEngine::addAssertions(const vector<Node> &assertions) +{ + Assert(false); // doing this so that we revisit what to do + // here. Currently not being used. + + // d_result = SAT_VALUE_UNKNOWN; + // d_assertions.reserve(assertions.size()); + // for(unsigned i = 0; i < assertions.size(); ++i) + // d_assertions.push_back(assertions[i]); +} + +void DecisionEngine::addAssertions + (const vector<Node> &assertions, + int assertionsEnd, + IteSkolemMap iteSkolemMap) { + // new assertions, reset whatever result we knew d_result = SAT_VALUE_UNKNOWN; + d_assertions.reserve(assertions.size()); for(unsigned i = 0; i < assertions.size(); ++i) d_assertions.push_back(assertions[i]); - for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i) - d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); + + for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) + d_needIteSkolemMap[i]-> + addAssertions(assertions, assertionsEnd, iteSkolemMap); } -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(); -} +// void DecisionEngine::addAssertion(Node n) +// { +// d_result = SAT_VALUE_UNKNOWN; +// if(needIteSkolemMap()) { +// d_assertions.push_back(n); +// } +// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i) +// d_needIteSkolemMap[i]->notifyAssertionsAvailable(); +// } }/* CVC4 namespace */ |