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/theory/bv/bv_inequality_graph.cpp | 54 ++++++++++++++++++----------------- 1 file changed, 28 insertions(+), 26 deletions(-) (limited to 'src/theory/bv/bv_inequality_graph.cpp') diff --git a/src/theory/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp index 89d5e1883..ed8756456 100644 --- a/src/theory/bv/bv_inequality_graph.cpp +++ b/src/theory/bv/bv_inequality_graph.cpp @@ -36,7 +36,7 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) TermId id_b = registerTerm(b); ReasonId id_reason = registerReason(reason); - Assert (!(isConst(id_a) && isConst(id_b))); + Assert(!(isConst(id_a) && isConst(id_b))); BitVector a_val = getValue(id_a); BitVector b_val = getValue(id_b); @@ -73,7 +73,7 @@ bool InequalityGraph::addInequality(TNode a, TNode b, bool strict, TNode reason) // add the inequality edge addEdge(id_a, id_b, strict, id_reason); BFSQueue queue(&d_modelValues); - Assert (hasModelValue(id_a)); + Assert(hasModelValue(id_a)); queue.push(id_a); return processQueue(queue, id_a); } @@ -141,7 +141,7 @@ bool InequalityGraph::processQueue(BFSQueue& queue, TermId start) { // it means we have an overflow and hence a conflict std::vector conflict; conflict.push_back(it->reason); - Assert (hasModelValue(start)); + Assert(hasModelValue(start)); ReasonId start_reason = getModelValue(start).reason; if (start_reason != UndefinedReasonId) { conflict.push_back(start_reason); @@ -193,9 +193,9 @@ void InequalityGraph::computeExplanation(TermId from, TermId to, std::vector() : BitVector(size, 0u); @@ -248,10 +248,10 @@ TermId InequalityGraph::registerTerm(TNode term) { bool isConst = term.getKind() == kind::CONST_BITVECTOR; InequalityNode ineq = InequalityNode(id, size, isConst); - Assert (d_ineqNodes.size() == id); + Assert(d_ineqNodes.size() == id); d_ineqNodes.push_back(ineq); - - Assert (d_ineqEdges.size() == id); + + Assert(d_ineqEdges.size() == id); d_ineqEdges.push_back(Edges()); initializeModelValue(term); @@ -272,22 +272,22 @@ ReasonId InequalityGraph::registerReason(TNode reason) { } TNode InequalityGraph::getReasonNode(ReasonId id) const { - Assert (d_reasonNodes.size() > id); + Assert(d_reasonNodes.size() > id); return d_reasonNodes[id]; } TNode InequalityGraph::getTermNode(TermId id) const { - Assert (d_termNodes.size() > id); + Assert(d_termNodes.size() > id); return d_termNodes[id]; } TermId InequalityGraph::getTermId(TNode node) const { - Assert (d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end()); + Assert(d_termNodeToIdMap.find(node) != d_termNodeToIdMap.end()); return d_termNodeToIdMap.find(node)->second; } void InequalityGraph::setConflict(const std::vector& conflict) { - Assert (!d_inConflict); + Assert(!d_inConflict); d_inConflict = true; d_conflict.clear(); for (unsigned i = 0; i < conflict.size(); ++i) { @@ -314,7 +314,7 @@ void InequalityGraph::setModelValue(TermId term, const ModelValue& mv) { } InequalityGraph::ModelValue InequalityGraph::getModelValue(TermId term) const { - Assert (d_modelValues.find(term) != d_modelValues.end()); + Assert(d_modelValues.find(term) != d_modelValues.end()); return (*(d_modelValues.find(term))).second; } @@ -323,7 +323,7 @@ bool InequalityGraph::hasModelValue(TermId id) const { } BitVector InequalityGraph::getValue(TermId id) const { - Assert (hasModelValue(id)); + Assert(hasModelValue(id)); return (*(d_modelValues.find(id))).second.value; } @@ -387,10 +387,12 @@ bool InequalityGraph::addDisequality(TNode a, TNode b, TNode reason) { } // void InequalityGraph::splitDisequality(TNode diseq) { -// Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << diseq <<"\n"; -// Assert (diseq.getKind() == kind::NOT && diseq[0].getKind() == kind::EQUAL); -// if (d_disequalitiesAlreadySplit.find(diseq) == d_disequalitiesAlreadySplit.end()) { -// d_disequalitiesToSplit.push_back(diseq); +// Debug("bv-inequality-internal")<<"InequalityGraph::splitDisequality " << +// diseq <<"\n"; Assert (diseq.getKind() == kind::NOT && +// diseq[0].getKind() == kind::EQUAL); if +// (d_disequalitiesAlreadySplit.find(diseq) == +// d_disequalitiesAlreadySplit.end()) { +// d_disequalitiesToSplit.push_back(diseq); // } // } @@ -398,7 +400,7 @@ void InequalityGraph::backtrack() { Debug("bv-inequality-internal") << "InequalityGraph::backtrack()\n"; int size = d_undoStack.size(); for (int i = size - 1; i >= (int)d_undoStackIndex.get(); --i) { - Assert (!d_undoStack.empty()); + Assert(!d_undoStack.empty()); TermId id = d_undoStack.back().first; InequalityEdge edge = d_undoStack.back().second; d_undoStack.pop_back(); @@ -409,8 +411,8 @@ void InequalityGraph::backtrack() { for (Edges::const_iterator it = edges.begin(); it!= edges.end(); ++it) { Debug("bv-inequality-internal") << getTermNode(it->next) <<" " << it->strict << "\n"; } - Assert (!edges.empty()); - Assert (edges.back() == edge); + Assert(!edges.empty()); + Assert(edges.back() == edge); edges.pop_back(); } } @@ -444,7 +446,7 @@ void InequalityGraph::checkDisequalities(std::vector& lemmas) { } bool InequalityGraph::isLessThan(TNode a, TNode b) { - Assert (isRegistered(a) && isRegistered(b)); + Assert(isRegistered(a) && isRegistered(b)); Unimplemented(); } @@ -457,8 +459,8 @@ bool InequalityGraph::hasValueInModel(TNode node) const { } BitVector InequalityGraph::getValueInModel(TNode node) const { - TermId id = getTermId(node); - Assert (hasModelValue(id)); + TermId id = getTermId(node); + Assert(hasModelValue(id)); return getValue(id); } -- cgit v1.2.3