diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-09-09 16:24:15 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-07 18:33:12 -0400 |
commit | 461a416e254095f4bdb4b3f5f4f3258b52722e23 (patch) | |
tree | 261ca25ed7e4e15b6922e158d95aa6fb6f0c2b41 /src/decision/justification_heuristic.cpp | |
parent | b976f4da9bf79670226d7fa55e02d4c0e4c7e8ba (diff) |
whitespace fixes
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index ffff6952f..84f4d5074 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -124,7 +124,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D if(Debug.isOn("decision")) { if(!checkJustified(curass)) - Debug("decision") << "****** Not justified [i="<<i<<"]: " + Debug("decision") << "****** Not justified [i="<<i<<"]: " << d_assertions[i] << std::endl; } } @@ -169,7 +169,7 @@ void JustificationHeuristic::addAssertions IteSkolemMap iteSkolemMap) { Trace("decision") - << "JustificationHeuristic::addAssertions()" + << "JustificationHeuristic::addAssertions()" << " size = " << assertions.size() << " assertionsEnd = " << assertionsEnd << std::endl; @@ -182,7 +182,7 @@ void JustificationHeuristic::addAssertions for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) { - Trace("decision::jh::ite") + Trace("decision::jh::ite") << " jh-ite: " << (i->first) << " maps to " << assertions[(i->second)] << std::endl; Assert(i->second >= assertionsEnd && i->second < assertions.size()); @@ -199,7 +199,7 @@ SatLiteral JustificationHeuristic::findSplitter(TNode node, d_curDecision = undefSatLiteral; if(findSplitterRec(node, desiredVal)) { ++d_helfulness; - } + } return d_curDecision; } @@ -405,9 +405,9 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) * children to be true. this is done recursively. */ - Trace("decision::jh") - << "findSplitterRec(" << node << ", " - << desiredVal << ", .. )" << std::endl; + Trace("decision::jh") + << "findSplitterRec(" << node << ", " + << desiredVal << ", .. )" << std::endl; /* Handle NOT as a special case */ while (node.getKind() == kind::NOT) { @@ -417,7 +417,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) /* Base case */ if (checkJustified(node)) { - Debug("decision::jh") << " justified, returning" << std::endl; + Debug("decision::jh") << " justified, returning" << std::endl; return NO_SPLITTER; } if (getExploredThreshold(node) < d_curThreshold) { @@ -449,7 +449,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) // "invariant violated"); /* What type of node is this */ - Kind k = node.getKind(); + Kind k = node.getKind(); theory::TheoryId tId = theory::kindToTheoryId(k); /* Some debugging stuff */ @@ -470,7 +470,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) Assert(litVal == desiredVal); setJustified(node); return NO_SPLITTER; - } + } else { Assert(d_decisionEngine->hasSatLiteral(node)); if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold) @@ -548,7 +548,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) { - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or + Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); int numChildren = node.getNumChildren(); @@ -575,7 +575,7 @@ void JustificationHeuristic::saveStartIndex(TNode node, int val) { JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node, SatValue desiredVal) { - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or + Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); int numChildren = node.getNumChildren(); @@ -671,7 +671,7 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER) return FOUND_SPLITTER; - + Assert(d_curThreshold != 0, "No controlling input found (6)"); return DONT_KNOW; } else { |