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

1 files changed, 24 insertions, 12 deletions

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 131fcd3b6..ec2f85829 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -152,7 +152,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         out << ss.str();
         out << ") (pred_eq_f _ " << ProofManager::getLitName(n2[0]) << ")) t_t_neq_f))" << std::endl;
       } else {
-        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1]) || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
+        Assert((n1[0] == n2[0][0] && n1[1] == n2[0][1])
+               || (n1[1] == n2[0][0] && n1[0] == n2[0][1]));
         if(n1[1] == n2[0][0]) {
           out << "(symm _ _ _ " << ss.str() << ")";
         } else {
@@ -166,7 +167,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     } else {
       Node n2 = pf.d_node;
       Assert(n2.getKind() == kind::EQUAL);
-      Assert((n1[0] == n2[0] && n1[1] == n2[1]) || (n1[1] == n2[0] && n1[0] == n2[1]));
+      Assert((n1[0] == n2[0] && n1[1] == n2[1])
+             || (n1[1] == n2[0] && n1[0] == n2[1]));
 
       out << ss.str();
       out << " ";
@@ -323,10 +325,15 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
       b2 << n2[1-side];
       out << ss.str();
     } else {
-      Assert(pf2->d_node[b1.getNumChildren() +
-                         (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0) +
-                         (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0) -
-                         (pf2->d_node.getMetaKind() == kind::metakind::PARAMETERIZED ? 0 : 1)] == n2[1-side]);
+      Assert(
+          pf2->d_node[b1.getNumChildren()
+                      + (n1[side].getKind() == kind::PARTIAL_SELECT_0 ? 1 : 0)
+                      + (n1[side].getKind() == kind::PARTIAL_SELECT_1 ? 1 : 0)
+                      - (pf2->d_node.getMetaKind()
+                                 == kind::metakind::PARAMETERIZED
+                             ? 0
+                             : 1)]
+          == n2[1 - side]);
       b1 << n2[1-side];
       b2 << n2[side];
       out << "(symm _ _ _ " << ss.str() << ")";
@@ -359,7 +366,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
         b2 << n2[1-side];
         out << ss.str();
       } else {
-        Assert(pf2->d_node[b1.getNumChildren()] == n2[1-side]);
+        Assert(pf2->d_node[b1.getNumChildren()] == n2[1 - side]);
         b1 << n2[1-side];
         b2 << n2[side];
         out << "(symm _ _ _ " << ss.str() << ")";
@@ -383,7 +390,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Debug("mgd") << "n1.getNumChildren() + 1 = "
                  << n1.getNumChildren() + 1 << std::endl;
 
-    Assert(!((n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2)));
+    Assert(!(
+        (n1.getKind() == kind::PARTIAL_SELECT_0 && n1.getNumChildren() == 2)));
     if (n1.getKind() == kind::PARTIAL_SELECT_1 && n1.getNumChildren() == 2) {
       Debug("mgd") << "Finished a SELECT. Updating.." << std::endl;
       b1.clear(kind::SELECT);
@@ -410,7 +418,8 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
     Debug("mgd") << "n2.getNumChildren() + 1 = "
                  << n2.getNumChildren() + 1 << std::endl;
 
-    Assert(!((n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2)));
+    Assert(!(
+        (n2.getKind() == kind::PARTIAL_SELECT_0 && n2.getNumChildren() == 2)));
     if (n2.getKind() == kind::PARTIAL_SELECT_1 && n2.getNumChildren() == 2) {
       Debug("mgd") << "Finished a SELECT. Updating.." << std::endl;
       b2.clear(kind::SELECT);
@@ -1115,7 +1124,7 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) {
 }
 
 void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
-  Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
+  Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS);
 
   if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) {
     // We can get here, for instance, if there's a (select ite ...), e.g. a non-array term
@@ -1129,7 +1138,10 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
     return;
   }
 
-  Assert ((term.getKind() == kind::SELECT) || (term.getKind() == kind::PARTIAL_SELECT_0) || (term.getKind() == kind::PARTIAL_SELECT_1) || (term.getKind() == kind::STORE));
+  Assert((term.getKind() == kind::SELECT)
+         || (term.getKind() == kind::PARTIAL_SELECT_0)
+         || (term.getKind() == kind::PARTIAL_SELECT_1)
+         || (term.getKind() == kind::STORE));
 
   switch (term.getKind()) {
   case kind::SELECT: {
@@ -1196,7 +1208,7 @@ void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM
 
 void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
   Debug("pf::array") << std::endl << "(pf::array) LFSCArrayProof::printOwnedSort: type is: " << type << std::endl;
-  Assert (type.isArray() || type.isSort());
+  Assert(type.isArray() || type.isSort());
   if (type.isArray()){
     ArrayType array_type(type);