diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-14 11:50:24 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-10-14 11:50:24 -0400 |
| commit | 18f3ed1fb81a3ab168474af9467543dea44c7926 (patch) | |
| tree | 1e9337919de2b729c2c3078f5bc405853ab7d9db /src | |
| parent | f77be2a9c94ba26d134ae978542ce9858314fc24 (diff) | |
trace decision-node
Diffstat (limited to 'src')
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 84f4d5074..72dea907c 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -477,7 +477,10 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) return DONT_KNOW; SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); - d_curDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); + d_curDecision = SatLiteral(v, /* negated = */ desiredVal != SAT_VALUE_TRUE ); + Trace("decision-node") << "[decision-node] requesting split on " << d_curDecision + << ", node: " << node + << ", polarity: " << (desiredVal ? "true" : "false") << std::endl; return FOUND_SPLITTER; } } |