projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
a0c6239
)
fix statistic in decision engine
author
Kshitij Bansal
<kshitij@cs.nyu.edu>
Sun, 12 Oct 2014 00:15:32 +0000
(20:15 -0400)
committer
Kshitij Bansal
<kshitij@cs.nyu.edu>
Mon, 20 Oct 2014 00:28:09 +0000
(20:28 -0400)
src/decision/justification_heuristic.cpp
patch
|
blob
|
history
diff --git
a/src/decision/justification_heuristic.cpp
b/src/decision/justification_heuristic.cpp
index 891d89cc5aff91c0313bce99003572a236dcaa66..c9a6b7e1b9ad934d4d375307c2111bbdddabc14c 100644
(file)
--- 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;
}