From: Kshitij Bansal Date: Tue, 14 Oct 2014 15:50:24 +0000 (-0400) Subject: trace decision-node X-Git-Tag: cvc5-1.0.0~6564 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18f3ed1fb81a3ab168474af9467543dea44c7926;p=cvc5.git trace decision-node --- 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; } }