diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:58:07 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:58:07 -0500 |
commit | 3e495881142c623d9099869dba1147b6ea5ebae5 (patch) | |
tree | b214a2ad56a9a9a108969dc9a748aea79b66b7d5 /src | |
parent | 8f341b6dc401a780f4a84fd4c51063242e885149 (diff) |
decision/ : jh: refactor embedded ITE, other minor
other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.
Diffstat (limited to 'src')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 44 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 15 |
2 files changed, 29 insertions, 30 deletions
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; i<n.getNumChildren(); ++i) { SkolemMap::iterator it2 = d_iteAssertions.find(n[i]); @@ -138,27 +138,13 @@ bool JustificationHeuristic::findSplitterRec(TNode node, << "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) { // if node has embedded ites, 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)) - 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<pair<TNode,TNode> > IteList; typedef hash_map<TNode,IteList,TNodeHashFunction> 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 */ |