diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-11 20:15:32 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-19 20:28:09 -0400 |
commit | c95713d981b513d00f9f665288c574ddc31eaf89 (patch) | |
tree | 99329ff664295ac403cb3feb06b73c8c1f873e29 /src/decision | |
parent | a0c6239f4e6e2e7756922764a4d7bb990043c29f (diff) |
fix statistic in decision engine
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 5 |
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; } |