diff options
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/decision_engine.cpp | 25 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 14 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 2 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 594 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 148 | ||||
-rw-r--r-- | src/decision/relevancy.h | 2 |
6 files changed, 380 insertions, 405 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp index 22c70eb6d..08a3e49d0 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); @@ -103,7 +96,7 @@ bool DecisionEngine::isRelevant(SatVariable var) SatValue DecisionEngine::getPolarity(SatVariable var) { - Debug("decision") << "getPolariry(" << var <<")" << std::endl; + Debug("decision") << "getPolarity(" << var <<")" << std::endl; if(d_relevancyStrategy != NULL) { Assert(isRelevant(var)); return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) ); @@ -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]); diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 4d354af2a..ea16cec16 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -42,7 +42,8 @@ class DecisionEngine { vector <ITEDecisionStrategy* > d_needIteSkolemMap; RelevancyStrategy* d_relevancyStrategy; - vector <Node> d_assertions; + typedef context::CDList<Node> AssertionsList; + AssertionsList d_assertions; // PropEngine* d_propEngine; CnfStream* d_cnfStream; @@ -55,7 +56,7 @@ class DecisionEngine { context::CDO<SatValue> d_result; // Disable creating decision engine without required parameters - DecisionEngine() : d_result(NULL) {} + DecisionEngine(); // init/shutdown state unsigned d_engineState; // 0=pre-init; 1=init,pre-shutdown; 2=shutdown @@ -68,8 +69,6 @@ public: /** Destructor, currently does nothing */ ~DecisionEngine() { Trace("decision") << "Destroying decision engine" << std::endl; - for(unsigned i = 0; i < d_enabledStrategies.size(); ++i) - delete d_enabledStrategies[i]; } // void setPropEngine(PropEngine* pe) { @@ -99,14 +98,15 @@ public: /** * 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. For now, - * there's nothing to do here in the DecisionEngine. + * 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; + for(unsigned i = 0; i < d_enabledStrategies.size(); ++i) + delete d_enabledStrategies[i]; } // Interface for External World to use our services @@ -191,7 +191,7 @@ public: /** * Get the assertions. Strategies are notified when these are available. */ - const vector<Node>& getAssertions() { + AssertionsList& getAssertions() { return d_assertions; } diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index a3c0d1684..a2fda44fe 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -9,7 +9,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Decision stategy + ** \brief Decision strategy ** ** Decision strategy **/ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 4ec4588f3..0b63dfbe1 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -16,25 +16,6 @@ ** ** It needs access to the simplified but non-clausal formula. **/ -/*****************************************************************************/ -/*! - * file search_sat.cpp - * brief Implementation of Search engine with generic external sat solver - * - * Author: Clark Barrett - * - * Created: Wed Dec 7 21:00:24 2005 - * - * <hr> - * - * License to use, copy, modify, sell and/or distribute this software - * and its documentation for any purpose is hereby granted without - * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * - * <hr> - */ -/*****************************************************************************/ #include "justification_heuristic.h" @@ -43,7 +24,158 @@ #include "theory/rewriter.h" #include "util/ite_removal.h" -// JustificationHeuristic stuff + +using namespace CVC4; + +JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de, + context::Context *uc, + context::Context *c): + ITEDecisionStrategy(de, c), + d_justified(c), + d_prvsIndex(c, 0), + d_helfulness("decision::jh::helpfulness", 0), + d_giveup("decision::jh::giveup", 0), + d_timestat("decision::jh::time"), + d_assertions(uc), + d_iteAssertions(uc), + d_iteCache(), + d_visited(), + d_visitedComputeITE(), + d_curDecision() { + StatisticsRegistry::registerStat(&d_helfulness); + StatisticsRegistry::registerStat(&d_giveup); + StatisticsRegistry::registerStat(&d_timestat); + Trace("decision") << "Justification heuristic enabled" << std::endl; +} + +JustificationHeuristic::~JustificationHeuristic() { + StatisticsRegistry::unregisterStat(&d_helfulness); + StatisticsRegistry::unregisterStat(&d_giveup); + StatisticsRegistry::unregisterStat(&d_timestat); +} + +CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { + Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; + TimerStat::CodeTimer codeTimer(d_timestat); + + d_visited.clear(); + + if(Trace.isOn("justified")) { + for(JustifiedSet::key_iterator i = d_justified.key_begin(); + i != d_justified.key_end(); ++i) { + TNode n = *i; + SatLiteral l = d_decisionEngine->hasSatLiteral(n) ? + d_decisionEngine->getSatLiteral(n) : -1; + SatValue v = tryGetSatValue(n); + Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl; + } + } + + for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { + Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl; + + // Sanity check: if it was false, aren't we inconsistent? + Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); + + SatValue desiredVal = SAT_VALUE_TRUE; + SatLiteral litDecision; + + litDecision = findSplitter(d_assertions[i], desiredVal); + + if(litDecision != undefSatLiteral) { + d_prvsIndex = i; + return litDecision; + } + } + + Trace("decision") << "jh: Nothing to split on " << std::endl; + +#if defined CVC4_DEBUG + bool alljustified = true; + for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) { + TNode curass = d_assertions[i]; + while(curass.getKind() == kind::NOT) + curass = curass[0]; + alljustified &= checkJustified(curass); + + if(Debug.isOn("decision")) { + if(!checkJustified(curass)) + Debug("decision") << "****** Not justified [i="<<i<<"]: " + << d_assertions[i] << std::endl; + } + } + Assert(alljustified); +#endif + + // SAT solver can stop... + stopSearch = true; + d_decisionEngine->setResult(SAT_VALUE_TRUE); + return prop::undefSatLiteral; +} + + +inline void computeXorIffDesiredValues +(Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2) +{ + Assert(k == kind::IFF || k == kind::XOR); + + bool shouldInvert = + (desiredVal == SAT_VALUE_TRUE && k == kind::IFF) || + (desiredVal == SAT_VALUE_FALSE && k == kind::XOR); + + if(desiredVal1 == SAT_VALUE_UNKNOWN && + desiredVal2 == SAT_VALUE_UNKNOWN) { + // CHOICE: pick one of them arbitarily + desiredVal1 = SAT_VALUE_FALSE; + } + + if(desiredVal2 == SAT_VALUE_UNKNOWN) { + desiredVal2 = shouldInvert ? invertValue(desiredVal1) : desiredVal1; + } else if(desiredVal1 == SAT_VALUE_UNKNOWN) { + desiredVal1 = shouldInvert ? invertValue(desiredVal2) : desiredVal2; + } +} + + + +void JustificationHeuristic::addAssertions +(const std::vector<Node> &assertions, + unsigned assertionsEnd, + IteSkolemMap iteSkolemMap) { + + Trace("decision") + << "JustificationHeuristic::addAssertions()" + << " size = " << assertions.size() + << " assertionsEnd = " << assertionsEnd + << std::endl; + + // Save the 'real' assertions locally + for(unsigned i = 0; i < assertionsEnd; ++i) + d_assertions.push_back(assertions[i]); + + // Save mapping between ite skolems and ite assertions + for(IteSkolemMap::iterator i = iteSkolemMap.begin(); + i != iteSkolemMap.end(); ++i) { + + Trace("decision::jh::ite") + << " jh-ite: " << (i->first) << " maps to " + << assertions[(i->second)] << std::endl; + Assert(i->second >= assertionsEnd && i->second < assertions.size()); + + d_iteAssertions[i->first] = assertions[i->second]; + } +} + +SatLiteral JustificationHeuristic::findSplitter(TNode node, + SatValue desiredVal) +{ + d_curDecision = undefSatLiteral; + if(findSplitterRec(node, desiredVal)) { + ++d_helfulness; + } + return d_curDecision; +} + void JustificationHeuristic::setJustified(TNode n) { @@ -67,14 +199,30 @@ SatValue JustificationHeuristic::tryGetSatValue(Node n) }//end of else } +const JustificationHeuristic::IteList& +JustificationHeuristic::getITEs(TNode n) +{ + IteCache::iterator it = d_iteCache.find(n); + if(it != d_iteCache.end()) { + return it->second; + } else { + // Compute the list of ITEs + // TODO: optimize by avoiding multiple lookup for d_iteCache[n] + d_iteCache[n] = IteList(); + d_visitedComputeITE.clear(); + computeITEs(n, d_iteCache[n]); + return d_iteCache[n]; + } +} + void JustificationHeuristic::computeITEs(TNode n, IteList &l) { - Trace("jh-ite") << " computeITEs( " << n << ", &l)\n"; + Trace("decision::jh::ite") << " computeITEs( " << n << ", &l)\n"; d_visitedComputeITE.insert(n); for(unsigned i=0; i<n.getNumChildren(); ++i) { SkolemMap::iterator it2 = d_iteAssertions.find(n[i]); if(it2 != d_iteAssertions.end()) { - l.push_back(make_pair(n[i], it2->second)); + l.push_back(make_pair(n[i], (*it2).second)); Assert(n[i].getNumChildren() == 0); } if(d_visitedComputeITE.find(n[i]) == @@ -84,26 +232,19 @@ void JustificationHeuristic::computeITEs(TNode n, IteList &l) } } -const JustificationHeuristic::IteList& JustificationHeuristic::getITEs(TNode n) -{ - IteCache::iterator it = d_iteCache.find(n); - if(it != d_iteCache.end()) { - return it->second; - } else { - // Compute the list of ITEs - // TODO: optimize by avoiding multiple lookup for d_iteCache[n] - d_iteCache[n] = IteList(); - d_visitedComputeITE.clear(); - computeITEs(n, d_iteCache[n]); - return d_iteCache[n]; - } -} - bool JustificationHeuristic::findSplitterRec(TNode node, - SatValue desiredVal, - SatLiteral* litDecision) + SatValue desiredVal) { - Trace("jh-findSplitterRec") + /** + * Main idea + * + * Given a boolean formula "node", the goal is to try to make it + * evaluate to "desiredVal" (true/false). for instance if "node" is a OR + * formula we want to make it evaluate to true, we'd like one of the + * children to be true. this is done recursively. + */ + + Trace("decision::jh") << "findSplitterRec(" << node << ", " << desiredVal << ", .. )" << std::endl; @@ -113,13 +254,9 @@ bool JustificationHeuristic::findSplitterRec(TNode node, node = node[0]; } - if(Debug.isOn("decision")) { - if(checkJustified(node)) - Debug("decision") << " justified, returning" << std::endl; - } - /* Base case */ if (checkJustified(node)) { + Debug("decision::jh") << " justified, returning" << std::endl; return false; } @@ -132,7 +269,6 @@ bool JustificationHeuristic::findSplitterRec(TNode node, Debug("decision") << "no sat literal for this node" << std::endl; } } - //Assert(litPresent); -- fails #endif // Get value of sat literal for the node, if there is one @@ -142,11 +278,6 @@ bool JustificationHeuristic::findSplitterRec(TNode node, Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); /* Good luck, hope you can get what you want */ - // if(not (litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN)) { - // Warning() << "WARNING: IMPORTANT: Please look into this. Sat solver is asking for a decision" << std::endl - // << "when the assertion we are trying to justify is already unsat. OR there is a bug" << std::endl; - // GiveUpException(); - // } Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, "invariant violated"); @@ -155,247 +286,192 @@ bool JustificationHeuristic::findSplitterRec(TNode node, theory::TheoryId tId = theory::kindToTheoryId(k); /* Some debugging stuff */ - Debug("jh-findSplitterRec") << "kind = " << k << std::endl; - Debug("jh-findSplitterRec") << "theoryId = " << tId << std::endl; - Debug("jh-findSplitterRec") << "node = " << node << std::endl; - Debug("jh-findSplitterRec") << "litVal = " << litVal << std::endl; + Debug("decision::jh") << "kind = " << k << std::endl + << "theoryId = " << tId << std::endl + << "node = " << node << std::endl + << "litVal = " << litVal << std::endl; /** - * If not in theory of booleans, and not a "boolean" EQUAL (IFF), - * then check if this is something to split-on. + * If not in theory of booleans, check if this is something to split-on. */ - if(tId != theory::THEORY_BOOL - // && !(k == kind::EQUAL && node[0].getType().isBoolean()) - ) { - - // if node has embedded ites -- which currently happens iff it got - // replaced during ite removal -- then try to resolve that first - const IteList& l = getITEs(node); - Trace("jh-ite") << " ite size = " << l.size() << std::endl; - /*d_visited.insert(node);*/ - for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) { - if(d_visited.find(i->first) == d_visited.end()) { - d_visited.insert(i->first); - Debug("jh-ite") << "jh-ite: adding visited " << i->first << std::endl; - if(findSplitterRec(i->second, SAT_VALUE_TRUE, litDecision)) - return true; - Debug("jh-ite") << "jh-ite: removing visited " << i->first << std::endl; - d_visited.erase(i->first); - } else { - Debug("jh-ite") << "jh-ite: already visited " << i->first << std::endl; - } - } + if(tId != theory::THEORY_BOOL) { + + // if node has embedded ites, resolve that first + if(handleEmbeddedITEs(node)) + return true; if(litVal != SAT_VALUE_UNKNOWN) { setJustified(node); return false; - } else { - Assert(d_decisionEngine->hasSatLiteral(node)); - /* if(not d_decisionEngine->hasSatLiteral(node)) - throw GiveUpException(); */ + } + else { Assert(d_decisionEngine->hasSatLiteral(node)); - SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); - *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); - Trace("decision") << "decision " << *litDecision << std::endl; - Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; + SatVariable v = + d_decisionEngine->getSatLiteral(node).getSatVariable(); + d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); return true; } } - SatValue valHard = SAT_VALUE_FALSE; + bool ret = false; switch (k) { case kind::CONST_BOOLEAN: Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE); - Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE); - setJustified(node); - return false; + Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE); + break; case kind::AND: - valHard = SAT_VALUE_TRUE; + if (desiredVal == SAT_VALUE_FALSE) + ret = handleAndOrEasy(node, desiredVal); + else + ret = handleAndOrHard(node, desiredVal); + break; case kind::OR: - if (desiredVal == valHard) { - int n = node.getNumChildren(); - for(int i = 0; i < n; ++i) { - if (findSplitterRec(node[i], valHard, litDecision)) { - return true; - } - } - Assert(litPresent == false || litVal == valHard, - "Output should be justified"); - setJustified(node); - return false; - } - else { - SatValue valEasy = invertValue(valHard); - int n = node.getNumChildren(); - for(int i = 0; i < n; ++i) { - Debug("jh-findSplitterRec") << " node[i] = " << node[i] << " " - << tryGetSatValue(node[i]) << std::endl; - if ( tryGetSatValue(node[i]) != valHard) { - Debug("jh-findSplitterRec") << "hi"<< std::endl; - if (findSplitterRec(node[i], valEasy, litDecision)) { - return true; - } - Assert(litPresent == false || litVal == valEasy, "Output should be justified"); - setJustified(node); - return false; - } - } - if(Debug.isOn("jh-findSplitterRec")) { - Debug("jh-findSplitterRec") << " * ** " << std::endl; - Debug("jh-findSplitterRec") << node.getKind() << " " - << node << std::endl; - for(unsigned i = 0; i < node.getNumChildren(); ++i) - Debug("jh-findSplitterRec") << "child: " << tryGetSatValue(node[i]) - << std::endl; - Debug("jh-findSplitterRec") << "node: " << tryGetSatValue(node) - << std::endl; - } - Assert(false, "No controlling input found (2)"); - } + if (desiredVal == SAT_VALUE_FALSE) + ret = handleAndOrHard(node, desiredVal); + else + ret = handleAndOrEasy(node, desiredVal); break; case kind::IMPLIES: - //throw GiveUpException(); - Assert(node.getNumChildren() == 2, "Expected 2 fanins"); - if (desiredVal == SAT_VALUE_FALSE) { - if (findSplitterRec(node[0], SAT_VALUE_TRUE, litDecision)) { - return true; - } - if (findSplitterRec(node[1], SAT_VALUE_FALSE, litDecision)) { - return true; - } - Assert(litPresent == false || litVal == SAT_VALUE_FALSE, - "Output should be justified"); - setJustified(node); - return false; - } - else { - if (tryGetSatValue(node[0]) != SAT_VALUE_TRUE) { - if (findSplitterRec(node[0], SAT_VALUE_FALSE, litDecision)) { - return true; - } - Assert(litPresent == false || litVal == SAT_VALUE_TRUE, - "Output should be justified"); - setJustified(node); - return false; - } - if (tryGetSatValue(node[1]) != SAT_VALUE_FALSE) { - if (findSplitterRec(node[1], SAT_VALUE_TRUE, litDecision)) { - return true; - } - Assert(litPresent == false || litVal == SAT_VALUE_TRUE, - "Output should be justified"); - setJustified(node); - return false; - } - Assert(false, "No controlling input found (3)"); - } - break; + if (desiredVal == SAT_VALUE_FALSE) + ret = handleBinaryHard(node[0], SAT_VALUE_TRUE, + node[1], SAT_VALUE_FALSE); - case kind::IFF: - //throw GiveUpException(); - { - SatValue val = tryGetSatValue(node[0]); - if (val != SAT_VALUE_UNKNOWN) { - if (findSplitterRec(node[0], val, litDecision)) { - return true; - } - if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val); - - if (findSplitterRec(node[1], val, litDecision)) { - return true; - } - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(node); - return false; - } - else { - val = tryGetSatValue(node[1]); - if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE; - if (desiredVal == SAT_VALUE_FALSE) val = invertValue(val); - if (findSplitterRec(node[0], val, litDecision)) { - return true; - } - Assert(false, "Unable to find controlling input (4)"); - } + else + ret = handleBinaryEasy(node[0], SAT_VALUE_FALSE, + node[1], SAT_VALUE_TRUE); break; - } - - case kind::XOR: - //throw GiveUpException(); - { - SatValue val = tryGetSatValue(node[0]); - if (val != SAT_VALUE_UNKNOWN) { - if (findSplitterRec(node[0], val, litDecision)) { - return true; - } - if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val); - if (findSplitterRec(node[1], val, litDecision)) { - return true; - } - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(node); - return false; - } - else { - SatValue val = tryGetSatValue(node[1]); - if (val == SAT_VALUE_UNKNOWN) val = SAT_VALUE_FALSE; - if (desiredVal == SAT_VALUE_TRUE) val = invertValue(val); - if (findSplitterRec(node[0], val, litDecision)) { - return true; - } - Assert(false, "Unable to find controlling input (5)"); - } + case kind::XOR: + case kind::IFF: { + SatValue desiredVal1 = tryGetSatValue(node[0]); + SatValue desiredVal2 = tryGetSatValue(node[1]); + computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2); + ret = handleBinaryHard(node[0], desiredVal1, + node[1], desiredVal2); break; } - case kind::ITE: { - //[0]: if, [1]: then, [2]: else - SatValue ifVal = tryGetSatValue(node[0]); - if (ifVal == SAT_VALUE_UNKNOWN) { - - // are we better off trying false? if not, try true - SatValue ifDesiredVal = - (tryGetSatValue(node[2]) == desiredVal || - tryGetSatValue(node[1]) == invertValue(desiredVal)) - ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; - - if(findSplitterRec(node[0], ifDesiredVal, litDecision)) { - return true; - } - Assert(false, "No controlling input found (6)"); - } else { - - // Try to justify 'if' - if (findSplitterRec(node[0], ifVal, litDecision)) { - return true; - } - - // If that was successful, we need to go into only one of 'then' - // or 'else' - int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; - int chVal = tryGetSatValue(node[ch]); - if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) - && findSplitterRec(node[ch], desiredVal, litDecision) ) { - return true; - } - } - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(node); - return false; - } + case kind::ITE: + ret = handleITE(node, desiredVal); + break; default: Assert(false, "Unexpected Boolean operator"); break; }//end of switch(k) - Unreachable(); + if(ret == false) { + Assert(litPresent == false || litVal == desiredVal, + "Output should be justified"); + setJustified(node); + } + return ret; }/* findRecSplit method */ + +bool JustificationHeuristic::handleAndOrEasy(TNode node, + SatValue desiredVal) +{ + Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or + (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); + + int numChildren = node.getNumChildren(); + SatValue desiredValInverted = invertValue(desiredVal); + for(int i = 0; i < numChildren; ++i) + if ( tryGetSatValue(node[i]) != desiredValInverted ) + return findSplitterRec(node[i], desiredVal); + Assert(false, "handleAndOrEasy: No controlling input found"); + return false; +} + +bool JustificationHeuristic::handleAndOrHard(TNode node, + SatValue desiredVal) { + Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or + (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); + + int numChildren = node.getNumChildren(); + for(int i = 0; i < numChildren; ++i) + if (findSplitterRec(node[i], desiredVal)) + return true; + return false; +} + +bool JustificationHeuristic::handleBinaryEasy(TNode node1, + SatValue desiredVal1, + TNode node2, + SatValue desiredVal2) +{ + if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) + return findSplitterRec(node1, desiredVal1); + if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) + return findSplitterRec(node2, desiredVal2); + Assert(false, "handleBinaryEasy: No controlling input found"); + return false; +} + +bool JustificationHeuristic::handleBinaryHard(TNode node1, + SatValue desiredVal1, + TNode node2, + SatValue desiredVal2) +{ + if( findSplitterRec(node1, desiredVal1) ) + return true; + return findSplitterRec(node2, desiredVal2); +} + +bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) +{ + Debug("decision::jh") << " handleITE (" << node << ", " + << desiredVal << std::endl; + + //[0]: if, [1]: then, [2]: else + SatValue ifVal = tryGetSatValue(node[0]); + if (ifVal == SAT_VALUE_UNKNOWN) { + + // are we better off trying false? if not, try true [CHOICE] + SatValue ifDesiredVal = + (tryGetSatValue(node[2]) == desiredVal || + tryGetSatValue(node[1]) == invertValue(desiredVal)) + ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; + + if(findSplitterRec(node[0], ifDesiredVal)) return true; + + Assert(false, "No controlling input found (6)"); + } else { + // Try to justify 'if' + if(findSplitterRec(node[0], ifVal)) return true; + + // If that was successful, we need to go into only one of 'then' + // or 'else' + int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; + + // STALE code: remove after tests or mar 2013, whichever earlier + // int chVal = tryGetSatValue(node[ch]); + // Assert(chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal); + // end STALE code: remove + + if( findSplitterRec(node[ch], desiredVal) ) { + return true; + } + }// else (...ifVal...) + return false; +} + +bool JustificationHeuristic::handleEmbeddedITEs(TNode node) +{ + const IteList& l = getITEs(node); + Trace("decision::jh::ite") << " ite size = " << l.size() << std::endl; + + for(IteList::const_iterator i = l.begin(); i != l.end(); ++i) { + if(d_visited.find(i->first) == d_visited.end()) { + d_visited.insert(i->first); + if(findSplitterRec(i->second, SAT_VALUE_TRUE)) + return true; + d_visited.erase(i->first); + } + } + return false; +} diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 5d13d2dd2..91c21d981 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -27,6 +27,8 @@ #include "decision_strategy.h" #include "context/cdhashset.h" +#include "context/cdlist.h" +#include "context/cdhashmap.h" #include "expr/node.h" #include "prop/sat_solver_types.h" @@ -34,20 +36,13 @@ namespace CVC4 { namespace decision { -class GiveUpException : public Exception { -public: - GiveUpException() : - Exception("justification heuristic: giving up") { - } -};/* class GiveUpException */ - class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector<pair<TNode,TNode> > IteList; typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; - typedef hash_map<TNode,TNode,TNodeHashFunction> SkolemMap; + typedef context::CDHashMap<TNode,TNode,TNodeHashFunction> SkolemMap; // being 'justified' is monotonic with respect to decisions - typedef context::CDHashSet<TNode,TNodeHashFunction> JustifiedSet; + typedef context::CDHashSet<Node,NodeHashFunction> JustifiedSet; JustifiedSet d_justified; context::CDO<unsigned> d_prvsIndex; @@ -59,7 +54,7 @@ class JustificationHeuristic : public ITEDecisionStrategy { * A copy of the assertions that need to be justified * directly. Doesn't have ones introduced during during ITE-removal. */ - std::vector<TNode> d_assertions; + context::CDList<TNode> d_assertions; //TNode is fine since decisionEngine has them too /** map from ite-rewrite skolem to a boolean-ite assertion */ @@ -82,127 +77,29 @@ class JustificationHeuristic : public ITEDecisionStrategy { * function */ hash_set<TNode,TNodeHashFunction> d_visitedComputeITE; + + /** current decision for the recursive call */ + SatLiteral d_curDecision; public: - JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *c): - ITEDecisionStrategy(de, c), - d_justified(c), - d_prvsIndex(c, 0), - d_helfulness("decision::jh::helpfulness", 0), - d_giveup("decision::jh::giveup", 0), - d_timestat("decision::jh::time") { - StatisticsRegistry::registerStat(&d_helfulness); - StatisticsRegistry::registerStat(&d_giveup); - StatisticsRegistry::registerStat(&d_timestat); - Trace("decision") << "Justification heuristic enabled" << std::endl; - } - ~JustificationHeuristic() { - StatisticsRegistry::unregisterStat(&d_helfulness); - StatisticsRegistry::unregisterStat(&d_timestat); - } - prop::SatLiteral getNext(bool &stopSearch) { - Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; - TimerStat::CodeTimer codeTimer(d_timestat); - - d_visited.clear(); - - if(Trace.isOn("justified")) { - for(JustifiedSet::iterator i = d_justified.begin(); - i != d_justified.end(); ++i) { - TNode n = *i; - SatLiteral l = d_decisionEngine->hasSatLiteral(n) ? - d_decisionEngine->getSatLiteral(n) : -1; - SatValue v = tryGetSatValue(n); - Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl; - } - } - - for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { - Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl; - - // Sanity check: if it was false, aren't we inconsistent? - Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); - - SatValue desiredVal = SAT_VALUE_TRUE; - SatLiteral litDecision; - try { - litDecision = findSplitter(d_assertions[i], desiredVal); - }catch(GiveUpException &e) { - return prop::undefSatLiteral; - } - - if(litDecision != undefSatLiteral) { - d_prvsIndex = i; - return litDecision; - } - } - - Trace("decision") << "jh: Nothing to split on " << std::endl; - -#if defined CVC4_DEBUG - bool alljustified = true; - for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) { - TNode curass = d_assertions[i]; - while(curass.getKind() == kind::NOT) - curass = curass[0]; - alljustified &= checkJustified(curass); - - if(Debug.isOn("decision")) { - if(!checkJustified(curass)) - Debug("decision") << "****** Not justified [i="<<i<<"]: " - << d_assertions[i] << std::endl; - } - } - Assert(alljustified); -#endif - - // SAT solver can stop... - stopSearch = true; - d_decisionEngine->setResult(SAT_VALUE_TRUE); - return prop::undefSatLiteral; - } + JustificationHeuristic(CVC4::DecisionEngine* de, + context::Context *uc, + context::Context *c); + + ~JustificationHeuristic(); + + prop::SatLiteral getNext(bool &stopSearch); void addAssertions(const std::vector<Node> &assertions, unsigned assertionsEnd, - IteSkolemMap iteSkolemMap) { - Trace("decision") - << "JustificationHeuristic::addAssertions()" - << " size = " << assertions.size() - << " assertionsEnd = " << assertionsEnd - << std::endl; - - // Save the 'real' assertions locally - for(unsigned i = 0; i < assertionsEnd; ++i) - d_assertions.push_back(assertions[i]); - - // Save mapping between ite skolems and ite assertions - for(IteSkolemMap::iterator i = iteSkolemMap.begin(); - i != iteSkolemMap.end(); ++i) { - Trace("jh-ite") << " jh-ite: " << (i->first) << " maps to " - << assertions[(i->second)] << std::endl; - Assert(i->second >= assertionsEnd && i->second < assertions.size()); - d_iteAssertions[i->first] = assertions[i->second]; - } - } + IteSkolemMap iteSkolemMap); private: - SatLiteral findSplitter(TNode node, SatValue desiredVal) - { - bool ret; - SatLiteral litDecision; - ret = findSplitterRec(node, desiredVal, &litDecision); - if(ret == true) { - Debug("decision") << "Yippee!!" << std::endl; - ++d_helfulness; - return litDecision; - } else { - return undefSatLiteral; - } - } + SatLiteral findSplitter(TNode node, SatValue desiredVal); /** * Do all the hard work. */ - bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision); + bool findSplitterRec(TNode node, SatValue value); /* Helper functions */ void setJustified(TNode); @@ -217,6 +114,15 @@ private: /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); + + bool handleAndOrEasy(TNode node, SatValue desiredVal); + bool handleAndOrHard(TNode node, SatValue desiredVal); + bool handleBinaryEasy(TNode node1, SatValue desiredVal1, + TNode node2, SatValue desiredVal2); + bool handleBinaryHard(TNode node1, SatValue desiredVal1, + TNode node2, SatValue desiredVal2); + bool handleITE(TNode node, SatValue desiredVal); + bool handleEmbeddedITEs(TNode node); };/* class JustificationHeuristic */ }/* namespace decision */ diff --git a/src/decision/relevancy.h b/src/decision/relevancy.h index 8a6eb54ef..bfd30ddde 100644 --- a/src/decision/relevancy.h +++ b/src/decision/relevancy.h @@ -60,7 +60,7 @@ class Relevancy : public RelevancyStrategy { typedef hash_map<TNode,SatValue,TNodeHashFunction> PolarityCache; // being 'justified' is monotonic with respect to decisions - context::CDHashSet<TNode,TNodeHashFunction> d_justified; + context::CDHashSet<Node, NodeHashFunction> d_justified; context::CDO<unsigned> d_prvsIndex; IntStat d_helfulness; |