From 86aa93a619e4697b92c719f478399965ccb96d2d Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 15 Jun 2012 22:15:43 +0000 Subject: [PATCH] Bug fix in justification heuristic. Had to do with how a "visited" node in the recursive findSplitter method was handled (which would lead to infinite loop). Earlier, they were ignored assuming the ancestor would split on it later. The right thing to do is to split on it right away. (Fixes errors from the fuzzer, not the ones from last night's regression) --- src/decision/justification_heuristic.cpp | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index cd69eeb74..93ff65e6d 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -141,8 +141,23 @@ bool JustificationHeuristic::findSplitterRec(TNode node, } /* Base case */ - if (checkJustified(node) || d_visited.find(node) != d_visited.end()) + if (checkJustified(node)) return false; + if(d_visited.find(node) != d_visited.end()) { + + if(tryGetSatValue(node) != SAT_VALUE_UNKNOWN) { + setJustified(node); + return false; + } else { + Assert(d_decisionEngine->hasSatLiteral(node)); + SatVariable v = d_decisionEngine->getSatLiteral(node).getSatVariable(); + *litDecision = SatLiteral(v, desiredVal != SAT_VALUE_TRUE ); + Trace("decision") << "decision " << *litDecision << std::endl; + Trace("decision") << "Found something to split. Glad to be able to serve you." << std::endl; + return true; + } + + } #if defined CVC4_ASSERTIONS || defined CVC4_TRACING // We don't always have a sat literal, so remember that. Will need -- 2.30.2