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

6 files changed, 36 insertions, 27 deletions

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 0d1095a23..3103f4ecc 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -134,7 +134,7 @@ void ArrayInfo::mergeLists(CTNodeList* la, const CTNodeList* lb) const{
 
 void ArrayInfo::addIndex(const Node a, const TNode i) {
   Assert(a.getType().isArray());
-  Assert(!i.getType().isArray()); // temporary for flat arrays
+  Assert(!i.getType().isArray());  // temporary for flat arrays
 
   Trace("arrays-ind")<<"Arrays::addIndex "<<a<<"["<<i<<"]\n";
   CTNodeList* temp_indices;
@@ -160,7 +160,7 @@ void ArrayInfo::addIndex(const Node a, const TNode i) {
 
 void ArrayInfo::addStore(const Node a, const TNode st){
   Assert(a.getType().isArray());
-  Assert(st.getKind()== kind::STORE); // temporary for flat arrays
+  Assert(st.getKind() == kind::STORE);  // temporary for flat arrays
 
   CTNodeList* temp_store;
   Info* temp_info;
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index 7e18f9ed2..982317350 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -78,7 +78,7 @@ public:
    * prints the information
    */
   void print() const {
-    Assert(indices != NULL && stores!= NULL && in_stores != NULL);
+    Assert(indices != NULL && stores != NULL && in_stores != NULL);
     Trace("arrays-info")<<"  indices   ";
     printList(indices);
     Trace("arrays-info")<<"  stores ";
diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
index 63dfae173..546db649c 100644
--- a/src/theory/arrays/static_fact_manager.cpp
+++ b/src/theory/arrays/static_fact_manager.cpp
@@ -18,7 +18,7 @@
 
 #include <iostream>
 
-#include "base/cvc4_assert.h"
+#include "base/check.h"
 #include "expr/node.h"
 #include "theory/arrays/static_fact_manager.h"
 
@@ -97,7 +97,8 @@ void StaticFactManager::addEq(TNode eq) {
   //   CNodeTNodesMap::iterator deq_ib = d_disequalities.find(b);
   //   if(deq_ib != d_disequalities.end()) {
   //     CTNodeListAlloc* deq = (*deq_ib).second;
-  //     for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end(); j++) {
+  //     for(CTNodeListAlloc::const_iterator j = deq->begin(); j!=deq->end();
+  //     j++) {
   //       TNode deqn = *j;
   //       TNode s = deqn[0];
   //       TNode t = deqn[1];
@@ -120,12 +121,11 @@ void StaticFactManager::addEq(TNode eq) {
   //    */
 
   //   CTNodeListAlloc* deqa = (*deq_ia).second;
-  //   for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end(); i++) {
+  //   for(CTNodeListAlloc::const_iterator i = deqa->begin(); i!= deqa->end();
+  //   i++) {
   //     TNode deqn = (*i);
-  //     Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() == kind::IFF);
-  //     TNode s = deqn[0];
-  //     TNode t = deqn[1];
-  //     TNode sp = find(s);
+  //     Assert(deqn.getKind() == kind::EQUAL || deqn.getKind() ==
+  //     kind::IFF); TNode s = deqn[0]; TNode t = deqn[1]; TNode sp = find(s);
   //     TNode tp = find(t);
 
   //     if(find(s) == find(t)) {
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 003bb0d68..f2beec0b8 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -189,7 +189,8 @@ void TheoryArrays::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 
 bool TheoryArrays::ppDisequal(TNode a, TNode b) {
   bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b);
-  Assert(!termsExist || !a.isConst() || !b.isConst() || a == b || d_ppEqualityEngine.areDisequal(a, b, false));
+  Assert(!termsExist || !a.isConst() || !b.isConst() || a == b
+         || d_ppEqualityEngine.areDisequal(a, b, false));
   return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) ||
           Rewriter::rewrite(a.eqNode(b)) == d_false);
 }
@@ -621,14 +622,17 @@ void TheoryArrays::checkWeakEquiv(bool arraysMerged) {
       Assert(pointer.isNull() == (weakEquivGetRep(n) == n));
       Assert(!pointer.isNull() || secondary.isNull());
       Assert(!index.isNull() || secondary.isNull());
-      Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull() || !secondary.isNull());
+      Assert(d_infoMap.getWeakEquivSecondaryReason(n).isNull()
+             || !secondary.isNull());
       if (!pointer.isNull()) {
         if (index.isNull()) {
           Assert(d_equalityEngine.areEqual(n, pointer));
         }
         else {
-          Assert((n.getKind() == kind::STORE && n[0] == pointer && n[1] == index) ||
-                 (pointer.getKind() == kind::STORE && pointer[0] == n && pointer[1] == index));
+          Assert(
+              (n.getKind() == kind::STORE && n[0] == pointer && n[1] == index)
+              || (pointer.getKind() == kind::STORE && pointer[0] == n
+                  && pointer[1] == index));
         }
       }
     }
@@ -694,7 +698,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
         TNode s = *it;
         if (!d_infoMap.rIntro1Applied(s)) {
           d_infoMap.setRIntro1Applied(s);
-          Assert(s.getKind()==kind::STORE);
+          Assert(s.getKind() == kind::STORE);
           Node ni = nm->mkNode(kind::SELECT, s, s[1]);
           if (ni != node) {
             preRegisterTermInternal(ni);
@@ -823,7 +827,8 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   }
   // Invariant: preregistered terms are exactly the terms in the equality engine
   // Disabled, see comment above for kind::EQUAL
-  // Assert(d_equalityEngine.hasTerm(node) || !d_equalityEngine.consistent());
+  // Assert(d_equalityEngine.hasTerm(node) ||
+  // !d_equalityEngine.consistent());
 }
 
 
@@ -915,7 +920,8 @@ void TheoryArrays::checkPair(TNode r1, TNode r2)
 
   if (r1[0] != r2[0]) {
     // If arrays are known to be disequal, or cannot become equal, we can continue
-    Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0]));
+    Assert(d_mayEqualEqualityEngine.hasTerm(r1[0])
+           && d_mayEqualEqualityEngine.hasTerm(r2[0]));
     if (r1[0].getType() != r2[0].getType() ||
         d_equalityEngine.areDisequal(r1[0], r2[0], false)) {
       Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
@@ -976,7 +982,8 @@ void TheoryArrays::computeCareGraph()
         if (eqStatusArr != EQUALITY_UNKNOWN) {
           continue;
         }
-        Assert(d_valuation.getEqualityStatus((*it1), (*it2)) == EQUALITY_UNKNOWN);
+        Assert(d_valuation.getEqualityStatus((*it1), (*it2))
+               == EQUALITY_UNKNOWN);
         addCarePair((*it1), (*it2));
         ++d_numSharedArrayVarSplits;
         return;
@@ -1133,7 +1140,7 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
           size_t it = 0;
           for(; it < instores->size(); ++it) {
             TNode instore = (*instores)[it];
-            Assert(instore.getKind()==kind::STORE);
+            Assert(instore.getKind() == kind::STORE);
             if (termSet.find(instore) != termSet.end() &&
                 !d_equalityEngine.areEqual(instore[1],n[1])) {
               Node r = nm->mkNode(kind::SELECT, instore, n[1]);
@@ -1203,7 +1210,8 @@ bool TheoryArrays::collectModelInfo(TheoryModel* m)
         TypeNode valueType = nrep.getType().getArrayConstituentType();
         rep = defaultValuesSet.nextTypeEnum(valueType);
         if (rep.isNull()) {
-          Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end());
+          Assert(defaultValuesSet.getSet(valueType)->begin()
+                 != defaultValuesSet.getSet(valueType)->end());
           rep = *(defaultValuesSet.getSet(valueType)->begin());
         }
         Trace("arrays-models") << "New default value = " << rep << endl;
@@ -1558,7 +1566,8 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned
           explained.insert(t);
         } else {
           // EXT lemma
-          Assert(t[1].getKind() == kind::NOT && t[1][0].getKind() == kind::EQUAL);
+          Assert(t[1].getKind() == kind::NOT
+                 && t[1][0].getKind() == kind::EQUAL);
           Assert(t[0].getKind() == kind::EQUAL);
           all.insert(t[0].notNode());
           explained.insert(t);
@@ -1618,7 +1627,7 @@ void TheoryArrays::setNonLinear(TNode a)
   // Propagate non-linearity down chain of stores
   for( ; it < st_a->size(); ++it) {
     TNode store = (*st_a)[it];
-    Assert(store.getKind()==kind::STORE);
+    Assert(store.getKind() == kind::STORE);
     setNonLinear(store[0]);
   }
 
@@ -1847,7 +1856,7 @@ void TheoryArrays::checkStore(TNode a) {
     d_infoMap.getInfo(a)->print();
   }
   Assert(a.getType().isArray());
-  Assert(a.getKind()==kind::STORE);
+  Assert(a.getKind() == kind::STORE);
   TNode b = a[0];
   TNode i = a[1];
 
@@ -1898,7 +1907,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 
   for(; it < stores->size(); ++it) {
     TNode store = (*stores)[it];
-    Assert(store.getKind()==kind::STORE);
+    Assert(store.getKind() == kind::STORE);
     TNode j = store[1];
     if (i == j) continue;
     lem = std::make_tuple(store, store[0], j, i);
@@ -1910,7 +1919,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     it = 0;
     for(; it < instores->size(); ++it) {
       TNode instore = (*instores)[it];
-      Assert(instore.getKind()==kind::STORE);
+      Assert(instore.getKind() == kind::STORE);
       TNode j = instore[1];
       if (i == j) continue;
       lem = std::make_tuple(instore, instore[0], j, i);
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 78756176d..223d742eb 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -218,7 +218,8 @@ struct ArraysProperties {
 struct ArrayPartialSelectTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::PARTIAL_SELECT_0 || n.getKind() == kind::PARTIAL_SELECT_1);
+    Assert(n.getKind() == kind::PARTIAL_SELECT_0
+           || n.getKind() == kind::PARTIAL_SELECT_1);
     return nodeManager->integerType();
   }
 };/* struct ArrayPartialSelectTypeRule */
diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp
index af2cf3c3f..0afa94a8e 100644
--- a/src/theory/arrays/union_find.cpp
+++ b/src/theory/arrays/union_find.cpp
@@ -18,7 +18,6 @@
 
 #include <iostream>
 
-#include "base/cvc4_assert.h"
 #include "expr/node.h"
 #include "theory/arrays/union_find.h"