From 25ab6d676ad3be1e0426adb8846e7f4277b5149e Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sat, 16 Feb 2013 20:52:03 -0500 Subject: [PATCH] decision: jh: more refactoring (.h->.cpp, xor/iff) --- src/decision/justification_heuristic.cpp | 262 ++++++++++++++++------- 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") <<"{ "<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 &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") <<"{ "<setResult(SAT_VALUE_TRUE); - return prop::undefSatLiteral; - } + context::Context *c); + + ~JustificationHeuristic(); + + prop::SatLiteral getNext(bool &stopSearch); void addAssertions(const std::vector &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. -- 2.30.2