From 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Wed, 30 Oct 2019 15:27:10 -0700 Subject: Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) --- src/decision/decision_engine.h | 10 +++++----- src/decision/justification_heuristic.cpp | 34 +++++++++++++++----------------- 2 files changed, 21 insertions(+), 23 deletions(-) (limited to 'src/decision') diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 73d7e2a31..41d439d4f 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -118,10 +118,10 @@ public: /** Gets the next decision based on strategies that are enabled */ SatLiteral getNext(bool &stopSearch) { NodeManager::currentResourceManager()->spendResource(options::decisionStep()); - Assert(d_cnfStream != NULL, - "Forgot to set cnfStream for decision engine?"); - Assert(d_satSolver != NULL, - "Forgot to set satSolver for decision engine?"); + Assert(d_cnfStream != NULL) + << "Forgot to set cnfStream for decision engine?"; + Assert(d_satSolver != NULL) + << "Forgot to set satSolver for decision engine?"; SatLiteral ret = undefSatLiteral; for(unsigned i = 0; @@ -157,7 +157,7 @@ public: case SAT_VALUE_TRUE: return Result(Result::SAT); case SAT_VALUE_FALSE: return Result(Result::UNSAT); case SAT_VALUE_UNKNOWN: return Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON); - default: Assert(false, "d_result is garbage"); + default: Assert(false) << "d_result is garbage"; } return Result(); } diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 043ec10f2..f7e5b84fc 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -68,8 +68,8 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch) bool stopSearchTmp = false; SatLiteral lit = getNextThresh(stopSearchTmp, options::decisionThreshold()); if(lit != undefSatLiteral) { - Assert(stopSearchTmp == false); - return lit; + Assert(stopSearchTmp == false); + return lit; } Assert(stopSearchTmp == true); } @@ -441,12 +441,12 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) SatValue litVal = tryGetSatValue(node); /* You'd better know what you want */ - Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); + Assert(desiredVal != SAT_VALUE_UNKNOWN) << "expected known value"; /* Good luck, hope you can get what you want */ // See bug 374 - // Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, - // "invariant violated"); + // Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN) << + // "invariant violated"; /* What type of node is this */ Kind k = node.getKind(); @@ -494,7 +494,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) case kind::CONST_BOOLEAN: Assert(node.getConst() == false || desiredVal == SAT_VALUE_TRUE); - Assert(node.getConst() == true || desiredVal == SAT_VALUE_FALSE); + Assert(node.getConst() == true || desiredVal == SAT_VALUE_FALSE); break; case kind::AND: @@ -535,9 +535,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) ret = handleITE(node, desiredVal); break; - default: - Assert(false, "Unexpected Boolean operator"); - break; + default: Assert(false) << "Unexpected Boolean operator"; break; }//end of switch(k) if(ret == DONT_KNOW) { @@ -545,8 +543,8 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) } if(ret == NO_SPLITTER) { - Assert( litPresent == false || litVal == desiredVal, - "Output should be justified"); + Assert(litPresent == false || litVal == desiredVal) + << "Output should be justified"; setJustified(node); } return ret; @@ -555,8 +553,8 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) { - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) or - (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE) ); + Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE) + or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE)); int numChildren = node.getNumChildren(); SatValue desiredValInverted = invertValue(desiredVal); @@ -569,7 +567,7 @@ JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal) } } } - Assert(d_curThreshold != 0, "handleAndOrEasy: No controlling input found"); + Assert(d_curThreshold != 0) << "handleAndOrEasy: No controlling input found"; return DONT_KNOW; } @@ -582,8 +580,8 @@ void JustificationHeuristic::saveStartIndex(TNode node, int val) { JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node, SatValue desiredVal) { - Assert( (node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) or - (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE) ); + Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE) + or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE)); int numChildren = node.getNumChildren(); bool noSplitter = true; @@ -621,7 +619,7 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TN if(ret != DONT_KNOW) return ret; } - Assert(d_curThreshold != 0, "handleBinaryEasy: No controlling input found"); + Assert(d_curThreshold != 0) << "handleBinaryEasy: No controlling input found"; return DONT_KNOW; } @@ -679,7 +677,7 @@ JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode nod if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER) return FOUND_SPLITTER; - Assert(d_curThreshold != 0, "No controlling input found (6)"); + Assert(d_curThreshold != 0) << "No controlling input found (6)"; return DONT_KNOW; } else { // Try to justify 'if' -- cgit v1.2.3