diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 20:52:03 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 20:52:03 -0500 |
commit | 25ab6d676ad3be1e0426adb8846e7f4277b5149e (patch) | |
tree | 5f3c3223d816ab96bda2268d3ecb1067a63055a6 /src/decision | |
parent | 3e495881142c623d9099869dba1147b6ea5ebae5 (diff) |
decision: jh: more refactoring (.h->.cpp, xor/iff)
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 262 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 116 |
2 files changed, 195 insertions, 183 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index f2e5feee5..0b63dfbe1 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -24,6 +24,159 @@ #include "theory/rewriter.h" #include "util/ite_removal.h" + +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) { d_justified.insert(n); @@ -46,6 +199,22 @@ 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("decision::jh::ite") << " computeITEs( " << n << ", &l)\n"; @@ -63,21 +232,6 @@ 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) { @@ -85,7 +239,7 @@ bool JustificationHeuristic::findSplitterRec(TNode node, * 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 AND + * 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. */ @@ -149,13 +303,12 @@ bool JustificationHeuristic::findSplitterRec(TNode node, if(litVal != SAT_VALUE_UNKNOWN) { setJustified(node); return false; - } else { + } + else { Assert(d_decisionEngine->hasSatLiteral(node)); SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); - d_curDecision = - SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); - Trace("decision") << "decision " << d_curDecision << std::endl; + d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); return true; } } @@ -192,51 +345,11 @@ bool JustificationHeuristic::findSplitterRec(TNode node, node[1], SAT_VALUE_TRUE); break; + case kind::XOR: case kind::IFF: { SatValue desiredVal1 = tryGetSatValue(node[0]); SatValue desiredVal2 = tryGetSatValue(node[1]); - - 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 = - desiredVal == SAT_VALUE_TRUE ? - desiredVal1 : invertValue(desiredVal1); - } else if(desiredVal1 == SAT_VALUE_UNKNOWN) { - desiredVal1 = - desiredVal == SAT_VALUE_TRUE ? - desiredVal2 : invertValue(desiredVal2); - } - - ret = handleBinaryHard(node[0], desiredVal1, - node[1], desiredVal2); - break; - } - - case kind::XOR:{ - SatValue desiredVal1 = tryGetSatValue(node[0]); - SatValue desiredVal2 = tryGetSatValue(node[1]); - - 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 = - desiredVal == SAT_VALUE_FALSE ? - desiredVal1 : invertValue(desiredVal1); - } else if(desiredVal1 == SAT_VALUE_UNKNOWN) { - desiredVal1 = - desiredVal == SAT_VALUE_FALSE ? - desiredVal2 : invertValue(desiredVal2); - } - + computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2); ret = handleBinaryHard(node[0], desiredVal1, node[1], desiredVal2); break; @@ -259,7 +372,9 @@ bool JustificationHeuristic::findSplitterRec(TNode node, return ret; }/* findRecSplit method */ -bool JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) { +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) ); @@ -272,7 +387,8 @@ bool JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) { return false; } -bool JustificationHeuristic::handleAndOrHard(TNode node, SatValue desiredVal) { +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) ); @@ -283,8 +399,10 @@ bool JustificationHeuristic::handleAndOrHard(TNode node, SatValue desiredVal) { return false; } -bool JustificationHeuristic::handleBinaryEasy -(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2) +bool JustificationHeuristic::handleBinaryEasy(TNode node1, + SatValue desiredVal1, + TNode node2, + SatValue desiredVal2) { if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) return findSplitterRec(node1, desiredVal1); @@ -294,8 +412,10 @@ bool JustificationHeuristic::handleBinaryEasy return false; } -bool JustificationHeuristic::handleBinaryHard -(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2) +bool JustificationHeuristic::handleBinaryHard(TNode node1, + SatValue desiredVal1, + TNode node2, + SatValue desiredVal2) { if( findSplitterRec(node1, desiredVal1) ) return true; @@ -348,15 +468,9 @@ bool JustificationHeuristic::handleEmbeddedITEs(TNode 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("decision::jh::ite") << "jh-ite: adding visited " - << i->first << std::endl; if(findSplitterRec(i->second, SAT_VALUE_TRUE)) return true; - Debug("decision::jh::ite") << "jh-ite: removing visited " - << i->first << std::endl; d_visited.erase(i->first); - } else { - Debug("decision::jh::ite") << "jh-ite: already visited " << i->first << std::endl; } } return false; diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 4be436351..91c21d981 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -83,120 +83,18 @@ class JustificationHeuristic : public ITEDecisionStrategy { public: 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() { - StatisticsRegistry::unregisterStat(&d_helfulness); - StatisticsRegistry::unregisterStat(&d_giveup); - 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::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; - } + 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) - { - d_curDecision = undefSatLiteral; - if(findSplitterRec(node, desiredVal)) { - ++d_helfulness; - } - return d_curDecision; - } + SatLiteral findSplitter(TNode node, SatValue desiredVal); /** * Do all the hard work. |