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

1 files changed, 18 insertions, 16 deletions

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9da9c95b6..79279eb41 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -46,7 +46,8 @@ TermDb::~TermDb(){
 }
 
 void TermDb::registerQuantifier( Node q ) {
-  Assert( q[0].getNumChildren()==d_quantEngine->getTermUtil()->getNumInstantiationConstants( q ) );
+  Assert(q[0].getNumChildren()
+         == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q));
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
     setTermInactive( ic );
@@ -257,7 +258,7 @@ void TermDb::computeArgReps( TNode n ) {
 }
 
 void TermDb::computeUfEqcTerms( TNode f ) {
-  Assert( f==getOperatorRepresentative( f ) );
+  Assert(f == getOperatorRepresentative(f));
   if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
   {
     return;
@@ -291,7 +292,7 @@ void TermDb::computeUfTerms( TNode f ) {
     // already computed
     return;
   }
-  Assert( f==getOperatorRepresentative( f ) );
+  Assert(f == getOperatorRepresentative(f));
   d_op_nonred_count[f] = 0;
   // get the matchable operators in the equivalence class of f
   std::vector<TNode> ops;
@@ -501,8 +502,9 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
     f = getOperatorRepresentative( f );
   }
   computeUfTerms( f );
-  Assert( !d_quantEngine->getActiveEqualityEngine()->hasTerm( r ) || 
-          d_quantEngine->getActiveEqualityEngine()->getRepresentative( r )==r );
+  Assert(!d_quantEngine->getActiveEqualityEngine()->hasTerm(r)
+         || d_quantEngine->getActiveEqualityEngine()->getRepresentative(r)
+                == r);
   std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
   if( it != d_func_map_rel_dom.end() ){
     std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
@@ -712,7 +714,7 @@ Node TermDb::evaluateTerm2(TNode n,
 
 
 TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
-  Assert( !qy->extendsEngine() );
+  Assert(!qy->extendsEngine());
   Trace("term-db-entail") << "get entailed term : " << n << std::endl;
   if( qy->getEngine()->hasTerm( n ) ){
     Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
@@ -723,8 +725,8 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su
       if( it!=subs.end() ){
         Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
         if( subsRep ){
-          Assert( qy->getEngine()->hasTerm( it->second ) );
-          Assert( qy->getEngine()->getRepresentative( it->second )==it->second );
+          Assert(qy->getEngine()->hasTerm(it->second));
+          Assert(qy->getEngine()->getRepresentative(it->second) == it->second);
           return it->second;
         }else{
           return getEntailedTerm2( it->second, subs, subsRep, hasSubs, qy );
@@ -805,9 +807,9 @@ TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
 }
 
 bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
-  Assert( !qy->extendsEngine() );
+  Assert(!qy->extendsEngine());
   Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
-  Assert( n.getType().isBoolean() );
+  Assert(n.getType().isBoolean());
   if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
     TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
@@ -816,8 +818,8 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
         if( n1==n2 ){
           return pol;
         }else{
-          Assert( qy->getEngine()->hasTerm( n1 ) );
-          Assert( qy->getEngine()->hasTerm( n2 ) );
+          Assert(qy->getEngine()->hasTerm(n1));
+          Assert(qy->getEngine()->hasTerm(n2));
           if( pol ){
             return qy->getEngine()->areEqual( n1, n2 );
           }else{
@@ -854,7 +856,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
   }else if( n.getKind()==APPLY_UF ){
     TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
     if( !n1.isNull() ){
-      Assert( qy->hasTerm( n1 ) );
+      Assert(qy->hasTerm(n1));
       if( n1==d_true ){
         return pol;
       }else if( n1==d_false ){
@@ -871,7 +873,7 @@ bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
 
 bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
   if( qy==NULL ){
-    Assert( d_consistent_ee );
+    Assert(d_consistent_ee);
     qy = d_quantEngine->getEqualityQuery();
   }
   std::map< TNode, TNode > subs;
@@ -880,7 +882,7 @@ bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
 
 bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
   if( qy==NULL ){
-    Assert( d_consistent_ee );
+    Assert(d_consistent_ee);
     qy = d_quantEngine->getEqualityQuery();
   }
   return isEntailed2( n, subs, subsRep, true, pol, qy );
@@ -908,7 +910,7 @@ bool TermDb::hasTermCurrent( Node n, bool useMode ) {
     }else if( options::termDbMode()==TERM_DB_RELEVANT ){
       return d_has_map.find( n )!=d_has_map.end();
     }else{
-      Assert( false );
+      Assert(false);
       return false;
     }
   }