diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-08-26 18:56:39 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-08-26 19:22:08 -0400 |
commit | 8f9362dcd60e31bbb9300c0f20662afb3dc0c185 (patch) | |
tree | 7328e8b7e67a06f9db8bfb07cc9483ac04b8b9e3 /src/decision/justification_heuristic.cpp | |
parent | 48418b76615dde8d5b472f773358ea1e05890767 (diff) |
bug 374 fix: assert litVal=desiredVal only for leaf nodes1.1.x
Conflicts:
src/decision/justification_heuristic.cpp
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 28d26adb1..6ed331b0a 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -75,7 +75,8 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl; // Sanity check: if it was false, aren't we inconsistent? - Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); + // Commenting out. See bug 374. In short, to do with how CNF stream works. + // Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE); SatValue desiredVal = SAT_VALUE_TRUE; SatLiteral litDecision; @@ -84,6 +85,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) { if(litDecision != undefSatLiteral) { d_prvsIndex = i; + Trace("decision") << "jh: spliting on " << litDecision << std::endl; return litDecision; } } @@ -279,8 +281,9 @@ bool JustificationHeuristic::findSplitterRec(TNode node, Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); /* Good luck, hope you can get what you want */ - Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, - "invariant violated"); + // See bug 374 + // Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, + // "invariant violated"); /* What type of node is this */ Kind k = node.getKind(); @@ -296,12 +299,12 @@ bool JustificationHeuristic::findSplitterRec(TNode node, * If not in theory of booleans, check if this is something to split-on. */ if(tId != theory::THEORY_BOOL) { - // if node has embedded ites, resolve that first if(handleEmbeddedITEs(node)) return true; if(litVal != SAT_VALUE_UNKNOWN) { + Assert(litVal == desiredVal); setJustified(node); return false; } |