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

1 files changed, 30 insertions, 26 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index bc3d450d0..09555da1b 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -578,7 +578,7 @@ FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
 /** Make a function type with input types from argTypes. */
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( argTypes.size() >= 1 );
+  Assert(argTypes.size() >= 1);
   std::vector<TypeNode> argTypeNodes;
   for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) {
     argTypeNodes.push_back(*argTypes[i].d_typeNode);
@@ -588,7 +588,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type
 
 FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( sorts.size() >= 2 );
+  Assert(sorts.size() >= 2);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
@@ -598,7 +598,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) {
 
 FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   NodeManagerScope nms(d_nodeManager);
-  Assert( sorts.size() >= 1 );
+  Assert(sorts.size() >= 1);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) {
      sortNodes.push_back(*sorts[i].d_typeNode);
@@ -735,7 +735,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
     if( (*i).isSort() ) {
       name = SortType(*i).getName();
     } else {
-      Assert( (*i).isSortConstructor() );
+      Assert((*i).isSortConstructor());
       name = SortConstructorType(*i).getName();
     }
     std::map<std::string, DatatypeType>::const_iterator resolver =
@@ -753,7 +753,7 @@ std::vector<DatatypeType> ExprManager::mkMutualDatatypeTypes(
       placeholders.push_back(*i);
       replacements.push_back( (*resolver).second );
     } else {
-      Assert( (*i).isSortConstructor() );
+      Assert((*i).isSortConstructor());
       paramTypes.push_back( SortConstructorType(*i) );
       paramReplacements.push_back( (*resolver).second );
     }
@@ -794,31 +794,31 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
       ++i) {
     const DatatypeConstructor& c = *i;
     Type testerType CVC4_UNUSED = c.getTester().getType();
-    Assert(c.isResolved() &&
-           testerType.isTester() &&
-           TesterType(testerType).getDomain() == dtt &&
-           TesterType(testerType).getRangeType() == booleanType(),
-           "malformed tester in datatype post-resolution");
+    Assert(c.isResolved() && testerType.isTester()
+           && TesterType(testerType).getDomain() == dtt
+           && TesterType(testerType).getRangeType() == booleanType())
+        << "malformed tester in datatype post-resolution";
     Type ctorType CVC4_UNUSED = c.getConstructor().getType();
-    Assert(ctorType.isConstructor() &&
-           ConstructorType(ctorType).getArity() == c.getNumArgs() &&
-           ConstructorType(ctorType).getRangeType() == dtt,
-           "malformed constructor in datatype post-resolution");
+    Assert(ctorType.isConstructor()
+           && ConstructorType(ctorType).getArity() == c.getNumArgs()
+           && ConstructorType(ctorType).getRangeType() == dtt)
+        << "malformed constructor in datatype post-resolution";
     // for all selectors...
     for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
         j != j_end;
         ++j) {
       const DatatypeConstructorArg& a = *j;
       Type selectorType = a.getType();
-      Assert(a.isResolved() &&
-             selectorType.isSelector() &&
-             SelectorType(selectorType).getDomain() == dtt,
-             "malformed selector in datatype post-resolution");
+      Assert(a.isResolved() && selectorType.isSelector()
+             && SelectorType(selectorType).getDomain() == dtt)
+          << "malformed selector in datatype post-resolution";
       // This next one's a "hard" check, performed in non-debug builds
       // as well; the other ones should all be guaranteed by the
       // CVC4::Datatype class, but this actually needs to be checked.
-      AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
-                   "cannot put function-like things in datatypes");
+      AlwaysAssert(!SelectorType(selectorType)
+                        .getRangeType()
+                        .d_typeNode->isFunctionLike())
+          << "cannot put function-like things in datatypes";
     }
   }
 }
@@ -892,7 +892,9 @@ Type ExprManager::getType(Expr e, bool check)
 }
 
 Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
+  Assert(NodeManager::currentNM() == NULL)
+      << "ExprManager::mkVar() should only be called externally, not from "
+         "within CVC4 code.  Please use mkSkolem().";
   NodeManagerScope nms(d_nodeManager);
   Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, flags);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
@@ -901,7 +903,9 @@ Expr ExprManager::mkVar(const std::string& name, Type type, uint32_t flags) {
 }
 
 Expr ExprManager::mkVar(Type type, uint32_t flags) {
-  Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
+  Assert(NodeManager::currentNM() == NULL)
+      << "ExprManager::mkVar() should only be called externally, not from "
+         "within CVC4 code.  Please use mkSkolem().";
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
   return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, flags));
@@ -974,8 +978,8 @@ Expr ExprManager::mkAssociative(Kind kind,
 
   /* It would be really weird if this happened (it would require
    * min > 2, for one thing), but let's make sure. */
-  AlwaysAssert( newChildren.size() >= min,
-                "Too few new children in mkAssociative" );
+  AlwaysAssert(newChildren.size() >= min)
+      << "Too few new children in mkAssociative";
 
   // recurse
   return mkAssociative(kind, newChildren);
@@ -1085,8 +1089,8 @@ TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, Expr
 }/* CVC4::expr namespace */
 
 Type ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) {
-  Assert(t.d_nodeManager != em->d_nodeManager,
-         "Can't export a Type to the same ExprManager");
+  Assert(t.d_nodeManager != em->d_nodeManager)
+      << "Can't export a Type to the same ExprManager";
   NodeManagerScope ems(t.d_nodeManager);
   return Type(em->d_nodeManager,
               new TypeNode(expr::exportTypeInternal(*t.d_typeNode, t.d_nodeManager, em->d_nodeManager, vmap)));