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

6 files changed, 37 insertions, 35 deletions

diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp
index 37dfedd15..48f5b7b35 100644
--- a/src/theory/sets/cardinality_extension.cpp
+++ b/src/theory/sets/cardinality_extension.cpp
@@ -870,8 +870,8 @@ void CardinalityExtension::mkModelValueElementsFor(
       Node v = val.getModelValue(it->second);
       Trace("sets-model") << "Cardinality of " << eqc << " is " << v
                           << std::endl;
-      Assert(v.getConst<Rational>() <= LONG_MAX,
-             "Exceeded LONG_MAX in sets model");
+      Assert(v.getConst<Rational>() <= LONG_MAX)
+          << "Exceeded LONG_MAX in sets model";
       unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
       Assert(els.size() <= vu);
       NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 1bbbb359b..6354b59e9 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -72,7 +72,7 @@ public:
   } 
   
   static Node reverseTuple( Node tuple ) {
-    Assert( tuple.getType().isTuple() );
+    Assert(tuple.getType().isTuple());
     std::vector<Node> elements;
     std::vector<TypeNode> tuple_types = tuple.getType().getTupleTypes();
     std::reverse( tuple_types.begin(), tuple_types.end() );
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 3b52da338..94fef85f5 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -127,12 +127,14 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
         n_members = (*mem_i1).second;
       }
       for( int i=0; i<(*mem_i2).second; i++ ){
-        Assert( i<(int)d_members_data[t2].size() && d_members_data[t2][i].getKind()==kind::MEMBER );
+        Assert(i < (int)d_members_data[t2].size()
+               && d_members_data[t2][i].getKind() == kind::MEMBER);
         Node m2 = d_members_data[t2][i];
         //check if redundant
         bool add = true;
         for( int j=0; j<n_members; j++ ){
-          Assert( j<(int)d_members_data[t1].size() && d_members_data[t1][j].getKind()==kind::MEMBER );
+          Assert(j < (int)d_members_data[t1].size()
+                 && d_members_data[t1][j].getKind() == kind::MEMBER);
           if (d_state.areEqual(m2[0], d_members_data[t1][j][0]))
           {
             add = false;
@@ -141,7 +143,7 @@ void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
         }
         if( add ){
           if( !s1.isNull() && s2.isNull() ){
-            Assert( m2[1].getType().isComparableTo( s1.getType() ) );
+            Assert(m2[1].getType().isComparableTo(s1.getType()));
             Assert(d_state.areEqual(m2[1], s1));
             Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
             if( s1.getKind()==kind::SINGLETON ){
@@ -213,7 +215,8 @@ bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
 }
 
 bool TheorySetsPrivate::isMember( Node x, Node s ) {
-  Assert( d_equalityEngine.hasTerm( s ) && d_equalityEngine.getRepresentative( s )==s );
+  Assert(d_equalityEngine.hasTerm(s)
+         && d_equalityEngine.getRepresentative(s) == s);
   NodeIntMap::iterator mem_i = d_members.find( s );
   if( mem_i != d_members.end() ) {
     for( int i=0; i<(*mem_i).second; i++ ){
@@ -331,10 +334,10 @@ void TheorySetsPrivate::fullEffortCheck(){
         }
         TypeNode tnn = n.getType();
         if( isSet ){
-          Assert( tnn.isSet() );
+          Assert(tnn.isSet());
           TypeNode tnnel = tnn.getSetElementType();
           tnc = TypeNode::mostCommonTypeNode( tnc, tnnel );
-          Assert( !tnc.isNull() );
+          Assert(!tnc.isNull());
           //update the common type term
           if( tnc==tnnel ){
             tnct = n;
@@ -367,7 +370,7 @@ void TheorySetsPrivate::fullEffortCheck(){
         ++eqc_i;
       }
       if( isSet ){
-        Assert( tnct.getType().getSetElementType()==tnc );
+        Assert(tnct.getType().getSetElementType() == tnc);
         d_most_common_type[eqc] = tnc;
         d_most_common_type_term[eqc] = tnct;
       }
@@ -513,7 +516,7 @@ void TheorySetsPrivate::checkDownwardsClosure()
           {
             Node mem = it2.second;
             Node eq_set = nv;
-            Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
+            Assert(d_equalityEngine.areEqual(mem[1], eq_set));
             if( mem[1]!=eq_set ){
               Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
               if( !options::setsProxyLemmas() ){
@@ -621,7 +624,7 @@ void TheorySetsPrivate::checkUpwardsClosure()
                     }
                   }
                 }else{
-                  Assert( k==kind::SETMINUS );
+                  Assert(k == kind::SETMINUS);
                   std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
                   if (itm == r2mem.end())
                   {
@@ -847,8 +850,8 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
         for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
           TNode x = f1[k];
           TNode y = f2[k];
-          Assert( d_equalityEngine.hasTerm(x) );
-          Assert( d_equalityEngine.hasTerm(y) );
+          Assert(d_equalityEngine.hasTerm(x));
+          Assert(d_equalityEngine.hasTerm(y));
           Assert(!d_state.areDisequal(x, y));
           Assert(!areCareDisequal(x, y));
           if( !d_equalityEngine.areEqual( x, y ) ){
@@ -860,7 +863,7 @@ void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
             }else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){
               //splitting on sets (necessary for handling set of sets properly)
               if( x.getType().isSet() ){
-                Assert( y.getType().isSet() );
+                Assert(y.getType().isSet());
                 if (!d_state.areDisequal(x, y))
                 {
                   Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 65cff2418..5c24cb088 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -522,7 +522,7 @@ void TheorySetsRels::check(Theory::Effort level)
       std::map< Node, std::map< Node, Node > >::iterator tc_exp_it = d_tcr_tcGraph_exps.find( tc_rel );
 
       TC_GRAPH_IT tc_graph_it = (tc_it->second).find( mem_rep_fst );
-      Assert( tc_exp_it != d_tcr_tcGraph_exps.end() );
+      Assert(tc_exp_it != d_tcr_tcGraph_exps.end());
       std::map< Node, Node >::iterator exp_map_it = (tc_exp_it->second).find( mem_rep_tup );
 
       if( exp_map_it == (tc_exp_it->second).end() ) {
@@ -679,7 +679,7 @@ void TheorySetsRels::check(Theory::Effort level)
         std::vector< Node > reasons;
         std::unordered_set<Node, NodeHashFunction> seen;
         Node tuple = RelsUtils::constructPair( tc_rel, getRepresentative( tc_graph_it->first ), getRepresentative( *snd_elements_it) );
-        Assert( rel_tc_graph_exps.find( tuple ) != rel_tc_graph_exps.end() );
+        Assert(rel_tc_graph_exps.find(tuple) != rel_tc_graph_exps.end());
         Node exp   = rel_tc_graph_exps.find( tuple )->second;
 
         reasons.push_back( exp );
@@ -918,7 +918,8 @@ void TheorySetsRels::check(Theory::Effort level)
     Trace("rels-debug") << "[Theory::Rels] ****** Finalizing transitive closure inferences!" << std::endl;
     TC_IT tc_graph_it = d_tcr_tcGraph.begin();
     while( tc_graph_it != d_tcr_tcGraph.end() ) {
-      Assert ( d_tcr_tcGraph_exps.find(tc_graph_it->first) != d_tcr_tcGraph_exps.end() );
+      Assert(d_tcr_tcGraph_exps.find(tc_graph_it->first)
+             != d_tcr_tcGraph_exps.end());
       doTCInference( tc_graph_it->second, d_tcr_tcGraph_exps.find(tc_graph_it->first)->second, tc_graph_it->first );
       ++tc_graph_it;
     }
@@ -992,7 +993,7 @@ void TheorySetsRels::check(Theory::Effort level)
     std::vector<Node>   members = d_rReps_memberReps_cache[rel0_rep];
     std::vector<Node>   exps    = d_rReps_memberReps_exp_cache[rel0_rep];
 
-    Assert( members.size() == exps.size() );
+    Assert(members.size() == exps.size());
 
     for(unsigned int i = 0; i < members.size(); i++) {
       Node reason = exps[i];
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index 5d654e7d5..aa6f4de3f 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -35,8 +35,9 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
     return elementTerm == setTerm[0];
   }
 
-  Assert(setTerm.getKind() == kind::UNION && setTerm[1].getKind() == kind::SINGLETON,
-         "kind was %d, term: %s", setTerm.getKind(), setTerm.toString().c_str());
+  Assert(setTerm.getKind() == kind::UNION
+         && setTerm[1].getKind() == kind::SINGLETON)
+      << "kind was " << setTerm.getKind() << ", term: " << setTerm;
 
   return
     elementTerm == setTerm[1][0] ||
@@ -81,7 +82,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   }//kind::MEMBER
 
   case kind::SUBSET: {
-    Assert(false, "TheorySets::postRrewrite(): Subset is handled in preRewrite.");
+    Assert(false)
+        << "TheorySets::postRrewrite(): Subset is handled in preRewrite.";
 
     // but in off-chance we do end up here, let us do our best
 
diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index 7e6038423..27aa58452 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -48,9 +48,8 @@ public:
 struct SetsBinaryOperatorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::UNION ||
-           n.getKind() == kind::INTERSECTION ||
-           n.getKind() == kind::SETMINUS);
+    Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION
+           || n.getKind() == kind::SETMINUS);
     TypeNode setType = n[0].getType(check);
     if( check ) {
       if(!setType.isSet()) {
@@ -73,9 +72,8 @@ struct SetsBinaryOperatorTypeRule {
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::UNION ||
-           n.getKind() == kind::INTERSECTION ||
-           n.getKind() == kind::SETMINUS);
+    Assert(n.getKind() == kind::UNION || n.getKind() == kind::INTERSECTION
+           || n.getKind() == kind::SETMINUS);
     if(n.getKind() == kind::UNION) {
       return NormalForm::checkNormalConstant(n);
     } else {
@@ -223,7 +221,7 @@ struct InsertTypeRule {
   {
     Assert(n.getKind() == kind::INSERT);
     size_t numChildren = n.getNumChildren();
-    Assert( numChildren >= 2 );
+    Assert(numChildren >= 2);
     TypeNode setType = n[numChildren-1].getType(check);
     if( check ) {
       if(!setType.isSet()) {
@@ -249,8 +247,7 @@ struct InsertTypeRule {
 struct RelBinaryOperatorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
   {
-    Assert(n.getKind() == kind::PRODUCT ||
-           n.getKind() == kind::JOIN);
+    Assert(n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN);
 
     TypeNode firstRelType = n[0].getType(check);
     TypeNode secondRelType = n[1].getType(check);
@@ -286,8 +283,7 @@ struct RelBinaryOperatorTypeRule {
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    Assert(n.getKind() == kind::JOIN ||
-           n.getKind() == kind::PRODUCT);
+    Assert(n.getKind() == kind::JOIN || n.getKind() == kind::PRODUCT);
     return false;
   }
 };/* struct RelBinaryOperatorTypeRule */
@@ -331,8 +327,8 @@ struct RelTransClosureTypeRule {
   }
 
   inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-      Assert(n.getKind() == kind::TCLOSURE);
-      return false;
+    Assert(n.getKind() == kind::TCLOSURE);
+    return false;
     }
 };/* struct RelTransClosureTypeRule */