Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

1 files changed, 22 insertions, 23 deletions

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index e633792d8..0ffd58d5a 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -58,7 +58,7 @@ Base::Base(uint32_t size)
   : d_size(size),
     d_repr(size/32 + (size % 32 == 0? 0 : 1), 0)
 {
-  Assert (d_size > 0); 
+  Assert(d_size > 0);
 }
 
 void Base::sliceAt(Index index)
@@ -73,7 +73,7 @@ void Base::sliceAt(Index index)
 }
 
 void Base::sliceWith(const Base& other) {
-  Assert (d_size == other.d_size);
+  Assert(d_size == other.d_size);
   for (unsigned i = 0; i < d_repr.size(); ++i) {
     d_repr[i] = d_repr[i] | other.d_repr[i]; 
   }
@@ -86,7 +86,7 @@ bool Base::isCutPoint (Index index) const
     return true;
 
   Index vector_index = index / 32;
-  Assert (vector_index < d_size);
+  Assert(vector_index < d_size);
   Index int_index = index % 32;
   uint32_t bit_mask = 1u << int_index;
 
@@ -94,9 +94,9 @@ bool Base::isCutPoint (Index index) const
 }
 
 void Base::diffCutPoints(const Base& other, Base& res) const {
-  Assert (d_size == other.d_size && res.d_size == d_size);
+  Assert(d_size == other.d_size && res.d_size == d_size);
   for (unsigned i = 0; i < d_repr.size(); ++i) {
-    Assert (res.d_repr[i] == 0); 
+    Assert(res.d_repr[i] == 0);
     res.d_repr[i] = d_repr[i] ^ other.d_repr[i]; 
   }
 }
@@ -144,7 +144,7 @@ std::string ExtractTerm::debugPrint() const {
  */
 
 std::pair<TermId, Index> NormalForm::getTerm(Index index, const UnionFind& uf) const {
-  Assert (index < base.getBitwidth()); 
+  Assert(index < base.getBitwidth());
   Index count = 0;
   for (unsigned i = 0; i < decomp.size(); ++i) {
     Index size = uf.getBitwidth(decomp[i]); 
@@ -207,17 +207,17 @@ TermId UnionFind::addTerm(Index bitwidth) {
 void UnionFind::unionTerms(const ExtractTerm& t1, const ExtractTerm& t2) {
   Debug("bv-slicer") << "UnionFind::unionTerms " << t1.debugPrint() << " and \n"
                      << "                      " << t2.debugPrint() << endl;
-  Assert (t1.getBitwidth() == t2.getBitwidth());
-  
+  Assert(t1.getBitwidth() == t2.getBitwidth());
+
   NormalForm nf1(t1.getBitwidth());
   NormalForm nf2(t2.getBitwidth());
   
   getNormalForm(t1, nf1);
   getNormalForm(t2, nf2);
 
-  Assert (nf1.decomp.size() == nf2.decomp.size());
-  Assert (nf1.base == nf2.base);
-  
+  Assert(nf1.decomp.size() == nf2.decomp.size());
+  Assert(nf1.base == nf2.base);
+
   for (unsigned i = 0; i < nf1.decomp.size(); ++i) {
     merge (nf1.decomp[i], nf2.decomp[i]); 
   } 
@@ -239,7 +239,7 @@ void UnionFind::merge(TermId t1, TermId t2) {
   if (t1 == t2)
     return;
 
-  Assert (! hasChildren(t1) && ! hasChildren(t2));
+  Assert(!hasChildren(t1) && !hasChildren(t2));
   setRepr(t1, t2); 
   d_representatives.erase(t1);
   d_statistics.d_numRepresentatives += -1; 
@@ -271,7 +271,7 @@ void UnionFind::split(TermId id, Index i) {
     // nothing to do 
     return;
   }
-  Assert (i < getBitwidth(id));
+  Assert(i < getBitwidth(id));
   if (!hasChildren(id)) {
     // first time we split this term 
     TermId bottom_id = addTerm(i);
@@ -303,13 +303,12 @@ void UnionFind::getNormalForm(const ExtractTerm& term, NormalForm& nf) {
 
 void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp) {
   // making sure the term is aligned
-  TermId id = find(term.id); 
+  TermId id = find(term.id);
 
-  Assert (term.high < getBitwidth(id));
+  Assert(term.high < getBitwidth(id));
   // because we split the node, this must be the whole extract
   if (!hasChildren(id)) {
-    Assert (term.high == getBitwidth(id) - 1 &&
-            term.low == 0);
+    Assert(term.high == getBitwidth(id) - 1 && term.low == 0);
     decomp.push_back(id);
     return; 
   }
@@ -380,9 +379,9 @@ void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposit
 
   if (start2 - start1 < common_size) {
     Index overlap = start1 + common_size - start2;
-    Assert (overlap > 0);
+    Assert(overlap > 0);
     Index diff = common_size - overlap;
-    Assert (diff >= 0);
+    Assert(diff >= 0);
     Index granularity = gcd(diff, overlap);
     // split the common part 
     for (unsigned i = 0; i < common_size; i+= granularity) {
@@ -401,7 +400,7 @@ void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2
   getNormalForm(term1, nf1);
   getNormalForm(term2, nf2);
 
-  Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth());
+  Assert(nf1.base.getBitwidth() == nf2.base.getBitwidth());
 
   // first check if the two have any common slices
   std::vector<TermId> intersection;
@@ -480,8 +479,8 @@ ExtractTerm Slicer::registerTerm(TNode node) {
 
 void Slicer::processEquality(TNode eq) {
   Debug("bv-slicer") << "Slicer::processEquality: " << eq << endl;
-  
-  Assert (eq.getKind() == kind::EQUAL);
+
+  Assert(eq.getKind() == kind::EQUAL);
   TNode a = eq[0];
   TNode b = eq[1];
   ExtractTerm a_ex= registerTerm(a);
@@ -508,7 +507,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
     low = utils::getExtractLow(node);
     top = node[0]; 
   }
-  AlwaysAssert (d_nodeToId.find(top) != d_nodeToId.end()); 
+  AlwaysAssert(d_nodeToId.find(top) != d_nodeToId.end());
   TermId id = d_nodeToId[top];
   NormalForm nf(high-low+1); 
   d_unionFind.getNormalForm(ExtractTerm(id, high, low), nf);