From: Kshitij Bansal Date: Sun, 26 Aug 2012 19:53:14 +0000 (+0000) Subject: minor, lying around in a wd (related to investigating bug 374) X-Git-Tag: cvc5-1.0.0~7842 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1857318ff8b072e07bc0a802960a7b87f119688d;p=cvc5.git minor, lying around in a wd (related to investigating bug 374) --- diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index c7051d570..67000b1ba 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -164,7 +164,12 @@ 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, + // if(not (litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN)) { + // Warning() << "WARNING: IMPORTANT: Please look into this. Sat solver is asking for a decision" << std::endl + // << "when the assertion we are trying to justify is already unsat. OR there is a bug" << std::endl; + // GiveUpException(); + // } + Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, "invariant violated"); /* What type of node is this */ diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index f0ae9fe78..6d9493e89 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -111,13 +111,18 @@ public: } for(unsigned i = d_prvsIndex; i < d_assertions.size(); ++i) { - Debug("decision") << d_assertions[i] << std::endl; + 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); SatValue desiredVal = SAT_VALUE_TRUE; - SatLiteral litDecision = findSplitter(d_assertions[i], desiredVal); + SatLiteral litDecision; + try { + litDecision = findSplitter(d_assertions[i], desiredVal); + }catch(GiveUpException &e) { + return prop::undefSatLiteral; + } if(litDecision != undefSatLiteral) return litDecision; @@ -180,11 +185,7 @@ private: { bool ret; SatLiteral litDecision; - try { - ret = findSplitterRec(node, desiredVal, &litDecision); - }catch(GiveUpException &e) { - return prop::undefSatLiteral; - } + ret = findSplitterRec(node, desiredVal, &litDecision); if(ret == true) { Debug("decision") << "Yippee!!" << std::endl; //d_prvsIndex = i;