summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-10-11 20:15:32 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-10-19 20:28:09 -0400
commitc95713d981b513d00f9f665288c574ddc31eaf89 (patch)
tree99329ff664295ac403cb3feb06b73c8c1f873e29 /src
parenta0c6239f4e6e2e7756922764a4d7bb990043c29f (diff)
fix statistic in decision engine
Diffstat (limited to 'src')
-rw-r--r--src/decision/justification_heuristic.cpp5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index 891d89cc5..c9a6b7e1b 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -108,6 +108,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D
if(litDecision != undefSatLiteral) {
setPrvsIndex(i);
Trace("decision") << "jh: splitting on " << litDecision << std::endl;
+ ++d_helfulness;
return litDecision;
}
}
@@ -197,9 +198,7 @@ SatLiteral JustificationHeuristic::findSplitter(TNode node,
SatValue desiredVal)
{
d_curDecision = undefSatLiteral;
- if(findSplitterRec(node, desiredVal)) {
- ++d_helfulness;
- }
+ findSplitterRec(node, desiredVal);
return d_curDecision;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback