From: Kshitij Bansal Date: Sun, 17 Feb 2013 00:58:07 +0000 (-0500) Subject: decision/ : jh: refactor embedded ITE, other minor X-Git-Tag: cvc5-1.0.0~7407^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e495881142c623d9099869dba1147b6ea5ebae5;p=cvc5.git decision/ : jh: refactor embedded ITE, other minor other minor: cleanup some remaning fragments of GiveUpException(), hopefully all is gone now. --- diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 4e924de9e..f2e5feee5 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -48,7 +48,7 @@ SatValue JustificationHeuristic::tryGetSatValue(Node 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; ifirst << std::endl; - if(findSplitterRec(i->second, SAT_VALUE_TRUE)) - 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(handleEmbeddedITEs(node)) + return true; if(litVal != SAT_VALUE_UNKNOWN) { setJustified(node); @@ -353,3 +339,25 @@ bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) }// 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); + 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 a1a39cd6a..4be436351 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -36,13 +36,6 @@ namespace CVC4 { namespace decision { -class GiveUpException : public Exception { -public: - GiveUpException() : - Exception("justification heuristic: giving up") { - } -};/* class GiveUpException */ - class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector > IteList; typedef hash_map IteCache; @@ -138,11 +131,8 @@ public: SatValue desiredVal = SAT_VALUE_TRUE; SatLiteral litDecision; - try { - litDecision = findSplitter(d_assertions[i], desiredVal); - }catch(GiveUpException &e) { - return prop::undefSatLiteral; - } + + litDecision = findSplitter(d_assertions[i], desiredVal); if(litDecision != undefSatLiteral) { d_prvsIndex = i; @@ -234,6 +224,7 @@ private: bool handleBinaryHard(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2); bool handleITE(TNode node, SatValue desiredVal); + bool handleEmbeddedITEs(TNode node); };/* class JustificationHeuristic */ }/* namespace decision */