diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/expr | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/array_store_all.cpp | 2 | ||||
-rw-r--r-- | src/expr/attribute.cpp | 5 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 5 | ||||
-rw-r--r-- | src/expr/datatype.cpp | 47 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 56 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 80 | ||||
-rw-r--r-- | src/expr/kind_map.h | 2 | ||||
-rw-r--r-- | src/expr/matcher.h | 1 | ||||
-rw-r--r-- | src/expr/metakind_template.cpp | 30 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 2 | ||||
-rwxr-xr-x | src/expr/mkkind | 4 | ||||
-rw-r--r-- | src/expr/node.h | 105 | ||||
-rw-r--r-- | src/expr/node_algorithm.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_builder.h | 291 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 44 | ||||
-rw-r--r-- | src/expr/node_manager.h | 18 | ||||
-rw-r--r-- | src/expr/node_self_iterator.h | 10 | ||||
-rw-r--r-- | src/expr/node_value.h | 18 | ||||
-rw-r--r-- | src/expr/record.cpp | 2 | ||||
-rw-r--r-- | src/expr/type_checker_template.cpp | 18 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 18 | ||||
-rw-r--r-- | src/expr/type_node.h | 48 | ||||
-rw-r--r-- | src/expr/type_properties_template.h | 104 | ||||
-rw-r--r-- | src/expr/uninterpreted_constant.cpp | 2 |
24 files changed, 456 insertions, 460 deletions
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp index eff2c2151..f2d9a35a9 100644 --- a/src/expr/array_store_all.cpp +++ b/src/expr/array_store_all.cpp @@ -20,7 +20,7 @@ #include <iostream> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/expr.h" #include "expr/type.h" diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index b9234883b..553c19f6e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -79,7 +79,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) { switch(tableId) { case AttrTableBool: - Unimplemented("delete attributes is unimplemented for bools"); + Unimplemented() << "delete attributes is unimplemented for bools"; break; case AttrTableUInt64: deleteAttributesFromTable(d_ints, ids); @@ -103,7 +103,8 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids) { case AttrTableCDNode: case AttrTableCDString: case AttrTableCDPointer: - Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired."); + Unimplemented() << "CDAttributes cannot be deleted. Contact Tim/Morgan " + "if this behavior is desired."; break; case LastAttrTable: diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index e47dce434..bc34324b0 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -463,9 +463,8 @@ public: */ static inline uint64_t registerAttribute() { const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId(); - AlwaysAssert( id <= 63, - "Too many boolean node attributes registered " - "during initialization !" ); + AlwaysAssert(id <= 63) << "Too many boolean node attributes registered " + "during initialization !"; return id; } };/* class Attribute<..., bool, ...> */ diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 4ec6ac36a..2356f74bc 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -19,7 +19,7 @@ #include <string> #include <sstream> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/attribute.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" @@ -67,7 +67,7 @@ const Datatype& Datatype::datatypeOf(Expr item) { case kind::TESTER_TYPE: return DatatypeType(t[0].toType()).getDatatype(); default: - Unhandled("arg must be a datatype constructor, selector, or tester"); + Unhandled() << "arg must be a datatype constructor, selector, or tester"; } } @@ -242,7 +242,7 @@ void Datatype::setRecord() { Cardinality Datatype::getCardinality(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); + Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); std::vector< Type > processing; computeCardinality( t, processing ); return d_card; @@ -275,10 +275,10 @@ Cardinality Datatype::computeCardinality(Type t, bool Datatype::isRecursiveSingleton(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); + Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){ if( isCodatatype() ){ - Assert( d_card_u_assume[t].empty() ); + Assert(d_card_u_assume[t].empty()); std::vector< Type > processing; if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){ d_card_rec_singleton[t] = 1; @@ -307,8 +307,8 @@ bool Datatype::isRecursiveSingleton() const unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const { - Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() ); - Assert( isRecursiveSingleton( t ) ); + Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end()); + Assert(isRecursiveSingleton(t)); return d_card_u_assume[t].size(); } @@ -320,8 +320,8 @@ unsigned Datatype::getNumRecursiveSingletonArgTypes() const Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const { - Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() ); - Assert( isRecursiveSingleton( t ) ); + Assert(d_card_rec_singleton.find(t) != d_card_rec_singleton.end()); + Assert(isRecursiveSingleton(t)); return d_card_u_assume[t][i]; } @@ -384,7 +384,7 @@ bool Datatype::computeCardinalityRecSingleton(Type t, bool Datatype::isFinite(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); + Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); @@ -413,7 +413,7 @@ bool Datatype::isFinite() const bool Datatype::isInterpretedFinite(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); - Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this ); + Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this); // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_self); TypeNode self = TypeNode::fromType(d_self); @@ -596,10 +596,10 @@ bool Datatype::operator==(const Datatype& other) const // testing equivalence of constructors and testers is harder b/c // this constructor might not be resolved yet; only compare them // if they are both resolved - Assert(isResolved() == !(*i).d_constructor.isNull() && - isResolved() == !(*i).d_tester.isNull() && - (*i).d_constructor.isNull() == (*j).d_constructor.isNull() && - (*i).d_tester.isNull() == (*j).d_tester.isNull()); + Assert(isResolved() == !(*i).d_constructor.isNull() + && isResolved() == !(*i).d_tester.isNull() + && (*i).d_constructor.isNull() == (*j).d_constructor.isNull() + && (*i).d_tester.isNull() == (*j).d_tester.isNull()); if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) { return false; } @@ -613,8 +613,8 @@ bool Datatype::operator==(const Datatype& other) const } // testing equivalence of selectors is harder b/c args might not // be resolved yet - Assert(isResolved() == (*k).isResolved() && - (*k).isResolved() == (*l).isResolved()); + Assert(isResolved() == (*k).isResolved() + && (*k).isResolved() == (*l).isResolved()); if((*k).isResolved()) { // both are resolved, so simply compare the selectors directly if((*k).d_selector != (*l).d_selector) { @@ -1121,7 +1121,7 @@ Expr DatatypeConstructor::computeGroundTerm(Type t, Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); if( groundTerm.getType()!=t ){ - Assert( Datatype::datatypeOf( d_constructor ).isParametric() ); + Assert(Datatype::datatypeOf(d_constructor).isParametric()); //type is ambiguous, must apply type ascription Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl; groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION, @@ -1140,8 +1140,8 @@ void DatatypeConstructor::computeSharedSelectors( Type domainType ) const { }else{ ctype = TypeNode::fromType( d_constructor.getType() ); } - Assert( ctype.isConstructor() ); - Assert( ctype.getNumChildren()-1==getNumArgs() ); + Assert(ctype.isConstructor()); + Assert(ctype.getNumChildren() - 1 == getNumArgs()); //compute the shared selectors const Datatype& dt = Datatype::datatypeOf(d_constructor); std::map< TypeNode, unsigned > counter; @@ -1149,7 +1149,8 @@ void DatatypeConstructor::computeSharedSelectors( Type domainType ) const { TypeNode t = ctype[j]; Expr ss = dt.getSharedSelector( domainType, t.toType(), counter[t] ); d_shared_selectors[domainType].push_back( ss ); - Assert( d_shared_selector_index[domainType].find( ss )==d_shared_selector_index[domainType].end() ); + Assert(d_shared_selector_index[domainType].find(ss) + == d_shared_selector_index[domainType].end()); d_shared_selector_index[domainType][ss] = j; counter[t]++; } @@ -1226,7 +1227,7 @@ Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) c PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); if( options::dtSharedSelectors() ){ computeSharedSelectors( domainType ); - Assert( d_shared_selectors[domainType].size()==getNumArgs() ); + Assert(d_shared_selectors[domainType].size() == getNumArgs()); return d_shared_selectors[domainType][index]; }else{ return d_args[index].getSelector(); @@ -1236,7 +1237,7 @@ Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) c int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const { PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor"); if( options::dtSharedSelectors() ){ - Assert( sel.getType().isSelector() ); + Assert(sel.getType().isSelector()); Type domainType = ((SelectorType)sel.getType()).getDomain(); computeSharedSelectors( domainType ); std::map< Expr, unsigned >::iterator its = d_shared_selector_index[domainType].find( sel ); 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))); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 2338a7320..998f58d0c 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -20,7 +20,7 @@ #include <utility> #include <vector> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/expr_manager_scope.h" #include "expr/node.h" #include "expr/node_algorithm.h" @@ -306,15 +306,15 @@ public: Expr Expr::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags /* = 0 */) const { - Assert(d_exprManager != exprManager, - "No sense in cloning an Expr in the same ExprManager"); + Assert(d_exprManager != exprManager) + << "No sense in cloning an Expr in the same ExprManager"; ExprManagerScope ems(*this); return Expr(exprManager, new Node(expr::ExportPrivate(d_exprManager, exprManager, variableMap, flags).exportInternal(*d_node))); } Expr& Expr::operator=(const Expr& e) { - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; + Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; if(this != &e) { if(d_exprManager == e.d_exprManager) { @@ -342,8 +342,8 @@ bool Expr::operator==(const Expr& e) const { return false; } ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; + Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; return *d_node == *e.d_node; } @@ -352,8 +352,8 @@ bool Expr::operator!=(const Expr& e) const { } bool Expr::operator<(const Expr& e) const { - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; + Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; if(isNull() && !e.isNull()) { return true; } @@ -362,8 +362,8 @@ bool Expr::operator<(const Expr& e) const { } bool Expr::operator>(const Expr& e) const { - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; + Assert(e.d_node != NULL) << "Unexpected NULL expression pointer!"; if(isNull() && !e.isNull()) { return true; } @@ -374,38 +374,38 @@ bool Expr::operator>(const Expr& e) const { uint64_t Expr::getId() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->getId(); } Kind Expr::getKind() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->getKind(); } size_t Expr::getNumChildren() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->getNumChildren(); } Expr Expr::operator[](unsigned i) const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - Assert(i >= 0 && i < d_node->getNumChildren(), "Child index out of bounds"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; + Assert(i >= 0 && i < d_node->getNumChildren()) << "Child index out of bounds"; return Expr(d_exprManager, new Node((*d_node)[i])); } bool Expr::hasOperator() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->hasOperator(); } Expr Expr::getOperator() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; PrettyCheckArgument(d_node->hasOperator(), *this, "Expr::getOperator() called on an Expr with no operator"); return Expr(d_exprManager, new Node(d_node->getOperator())); @@ -414,14 +414,14 @@ Expr Expr::getOperator() const { bool Expr::isParameterized() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->getMetaKind() == kind::metakind::PARAMETERIZED; } Type Expr::getType(bool check) const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; PrettyCheckArgument(!d_node->isNull(), this, "Can't get type of null expression!"); return d_exprManager->getType(*this, check); @@ -553,32 +553,32 @@ Expr::const_iterator Expr::end() const { std::string Expr::toString() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->toString(); } bool Expr::isNull() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->isNull(); } bool Expr::isVariable() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->getMetaKind() == kind::metakind::VARIABLE; } bool Expr::isConst() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return d_node->isConst(); } bool Expr::hasFreeVariable() const { ExprManagerScope ems(*this); - Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + Assert(d_node != NULL) << "Unexpected NULL expression pointer!"; return expr::hasFreeVar(*d_node); } @@ -591,30 +591,30 @@ void Expr::toStream(std::ostream& out, int depth, bool types, size_t dag, Node Expr::getNode() const { return *d_node; } TNode Expr::getTNode() const { return *d_node; } Expr Expr::notExpr() const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; return d_exprManager->mkExpr(NOT, *this); } Expr Expr::andExpr(const Expr& e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); return d_exprManager->mkExpr(AND, *this, e); } Expr Expr::orExpr(const Expr& e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); return d_exprManager->mkExpr(OR, *this, e); } Expr Expr::xorExpr(const Expr& e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); return d_exprManager->mkExpr(XOR, *this, e); @@ -622,16 +622,16 @@ Expr Expr::xorExpr(const Expr& e) const { Expr Expr::eqExpr(const Expr& e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); return d_exprManager->mkExpr(EQUAL, *this, e); } Expr Expr::impExpr(const Expr& e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; PrettyCheckArgument(d_exprManager == e.d_exprManager, e, "Different expression managers!"); return d_exprManager->mkExpr(IMPLIES, *this, e); @@ -639,8 +639,8 @@ Expr Expr::impExpr(const Expr& e) const { Expr Expr::iteExpr(const Expr& then_e, const Expr& else_e) const { - Assert(d_exprManager != NULL, - "Don't have an expression manager for this expression!"); + Assert(d_exprManager != NULL) + << "Don't have an expression manager for this expression!"; PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e, "Different expression managers!"); PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e, @@ -684,7 +684,7 @@ static Node exportConstant(TNode n, NodeManager* to, ExprManagerMapCollection& v switch(n.getKind()) { ${exportConstant_cases} - default: Unhandled(n.getKind()); +default: Unhandled() << n.getKind(); } }/* exportConstant() */ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h index a5ae73802..3b49ad51a 100644 --- a/src/expr/kind_map.h +++ b/src/expr/kind_map.h @@ -23,7 +23,7 @@ #include <stdint.h> #include <iterator> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/kind.h" namespace CVC4 { diff --git a/src/expr/matcher.h b/src/expr/matcher.h index 95ece7d23..9a2dad7d0 100644 --- a/src/expr/matcher.h +++ b/src/expr/matcher.h @@ -24,7 +24,6 @@ #include <vector> #include <map> -#include "base/cvc4_assert.h" #include "expr/node.h" #include "expr/type_node.h" diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 5116392cb..83c7e6e2c 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -52,13 +52,14 @@ ${metakind_constantMaps} namespace kind { namespace metakind { -size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) { +size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) +{ Assert(nv->getMetaKind() == kind::metakind::CONSTANT); - switch(nv->d_kind) { + switch (nv->d_kind) + { ${metakind_constHashes} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind); } } @@ -69,11 +70,12 @@ bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1, return false; } - if(nv1->getMetaKind() == kind::metakind::CONSTANT) { - switch(nv1->d_kind) { + if (nv1->getMetaKind() == kind::metakind::CONSTANT) + { + switch (nv1->d_kind) + { ${metakind_compares} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind)); + default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind); } } @@ -105,10 +107,10 @@ void NodeValueConstPrinter::toStream(std::ostream& out, const ::CVC4::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); - switch(nv->d_kind) { + switch (nv->d_kind) + { ${metakind_constPrinters} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind); } } @@ -135,10 +137,10 @@ void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); - switch(nv->d_kind) { + switch (nv->d_kind) + { ${metakind_constDeleters} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + default: Unhandled() << ::CVC4::expr::NodeValue::dKindToKind(nv->d_kind); } } diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 1615d461b..c4d35b7dc 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -21,7 +21,7 @@ #include <iosfwd> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/kind.h" namespace CVC4 { diff --git a/src/expr/mkkind b/src/expr/mkkind index a8a74b5a6..8e45b94ba 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -274,7 +274,7 @@ function register_sort { fi else type_constant_groundterms="${type_constant_groundterms}#line $lineno \"$kf\" - case $id: Unhandled(tc); + case $id: Unhandled() << tc; " fi } @@ -323,7 +323,7 @@ function register_wellfoundedness { " else type_groundterms="${type_groundterms}#line $lineno \"$kf\" - case $id: Unhandled(typeNode); + case $id: Unhandled() << typeNode; " fi if [ -n "$header" ]; then diff --git a/src/expr/node.h b/src/expr/node.h index e0231bef6..cd3c99a78 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -33,15 +33,15 @@ #include <utility> #include <vector> +#include "base/check.h" #include "base/configuration.h" -#include "base/cvc4_assert.h" #include "base/exception.h" #include "base/output.h" -#include "expr/type.h" -#include "expr/kind.h" -#include "expr/metakind.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" +#include "expr/kind.h" +#include "expr/metakind.h" +#include "expr/type.h" #include "options/language.h" #include "options/set_language.h" #include "util/hash.h" @@ -226,7 +226,7 @@ class NodeTemplate { inline void assertTNodeNotExpired() const { if(!ref_count) { - Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); + Assert(d_nv->d_rc > 0) << "TNode pointing to an expired NodeValue"; } } @@ -1022,9 +1022,9 @@ template <bool ref_count> template <class AttrKind> inline typename AttrKind::value_type NodeTemplate<ref_count>:: getAttribute(const AttrKind&) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1035,9 +1035,9 @@ template <bool ref_count> template <class AttrKind> inline bool NodeTemplate<ref_count>:: hasAttribute(const AttrKind&) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1048,9 +1048,9 @@ template <bool ref_count> template <class AttrKind> inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1061,9 +1061,9 @@ template <bool ref_count> template <class AttrKind> inline void NodeTemplate<ref_count>:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1080,12 +1080,12 @@ NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::null() template <bool ref_count> NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) : d_nv(const_cast<expr::NodeValue*> (ev)) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; if(ref_count) { d_nv->inc(); } else { - Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null(), - "TNode constructed from NodeValue with rc == 0"); + Assert(d_nv->d_rc > 0 || d_nv == &expr::NodeValue::null()) + << "TNode constructed from NodeValue with rc == 0"; } } @@ -1095,37 +1095,37 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) : template <bool ref_count> NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) { - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!"; d_nv = e.d_nv; if(ref_count) { - Assert(d_nv->d_rc > 0, "Node constructed from TNode with rc == 0"); + Assert(d_nv->d_rc > 0) << "Node constructed from TNode with rc == 0"; d_nv->inc(); } else { // shouldn't ever fail - Assert(d_nv->d_rc > 0, "TNode constructed from Node with rc == 0"); + Assert(d_nv->d_rc > 0) << "TNode constructed from Node with rc == 0"; } } template <bool ref_count> NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) { - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value!"; d_nv = e.d_nv; if(ref_count) { // shouldn't ever fail - Assert(d_nv->d_rc > 0, "Node constructed from Node with rc == 0"); + Assert(d_nv->d_rc > 0) << "Node constructed from Node with rc == 0"; d_nv->inc(); } else { - Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0"); + Assert(d_nv->d_rc > 0) << "TNode constructed from TNode with rc == 0"; } } template <bool ref_count> NodeTemplate<ref_count>::NodeTemplate(const Expr& e) { - Assert(e.d_node != NULL, "Expecting a non-NULL expression value!"); - Assert(e.d_node->d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(e.d_node != NULL) << "Expecting a non-NULL expression value!"; + Assert(e.d_node->d_nv != NULL) << "Expecting a non-NULL expression value!"; d_nv = e.d_node->d_nv; // shouldn't ever fail - Assert(d_nv->d_rc > 0, "Node constructed from Expr with rc == 0"); + Assert(d_nv->d_rc > 0) << "Node constructed from Expr with rc == 0"; if(ref_count) { d_nv->inc(); } @@ -1133,10 +1133,10 @@ NodeTemplate<ref_count>::NodeTemplate(const Expr& e) { template <bool ref_count> NodeTemplate<ref_count>::~NodeTemplate() { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; if(ref_count) { // shouldn't ever fail - Assert(d_nv->d_rc > 0, "Node reference count would be negative"); + Assert(d_nv->d_rc > 0) << "Node reference count would be negative"; d_nv->dec(); } } @@ -1147,29 +1147,28 @@ void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) { if(ref_count) { d_nv->inc(); } else { - Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0"); + Assert(d_nv->d_rc > 0) << "TNode assigned to NodeValue with rc == 0"; } } template <bool ref_count> NodeTemplate<ref_count>& NodeTemplate<ref_count>:: operator=(const NodeTemplate& e) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; + Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!"; if(__builtin_expect( ( d_nv != e.d_nv ), true )) { if(ref_count) { // shouldn't ever fail - Assert(d_nv->d_rc > 0, - "Node reference count would be negative"); + Assert(d_nv->d_rc > 0) << "Node reference count would be negative"; d_nv->dec(); } d_nv = e.d_nv; if(ref_count) { // shouldn't ever fail - Assert(d_nv->d_rc > 0, "Node assigned from Node with rc == 0"); + Assert(d_nv->d_rc > 0) << "Node assigned from Node with rc == 0"; d_nv->inc(); } else { - Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0"); + Assert(d_nv->d_rc > 0) << "TNode assigned from TNode with rc == 0"; } } return *this; @@ -1178,21 +1177,21 @@ operator=(const NodeTemplate& e) { template <bool ref_count> NodeTemplate<ref_count>& NodeTemplate<ref_count>:: operator=(const NodeTemplate<!ref_count>& e) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; + Assert(e.d_nv != NULL) << "Expecting a non-NULL expression value on RHS!"; if(__builtin_expect( ( d_nv != e.d_nv ), true )) { if(ref_count) { // shouldn't ever fail - Assert(d_nv->d_rc > 0, "Node reference count would be negative"); + Assert(d_nv->d_rc > 0) << "Node reference count would be negative"; d_nv->dec(); } d_nv = e.d_nv; if(ref_count) { - Assert(d_nv->d_rc > 0, "Node assigned from TNode with rc == 0"); + Assert(d_nv->d_rc > 0) << "Node assigned from TNode with rc == 0"; d_nv->inc(); } else { // shouldn't ever happen - Assert(d_nv->d_rc > 0, "TNode assigned from Node with rc == 0"); + Assert(d_nv->d_rc > 0) << "TNode assigned from Node with rc == 0"; } } return *this; @@ -1273,9 +1272,9 @@ NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const { */ template <bool ref_count> NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1301,8 +1300,7 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { case kind::metakind::NULLARY_OPERATOR: IllegalArgument(*this, "getOperator() called on Node with NULLARY_OPERATOR-kinded kind"); - default: - Unhandled(mk); + default: Unhandled() << mk; } } @@ -1319,9 +1317,9 @@ inline bool NodeTemplate<ref_count>::hasOperator() const { template <bool ref_count> TypeNode NodeTemplate<ref_count>::getType(bool check) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; assertTNodeNotExpired(); @@ -1409,8 +1407,9 @@ NodeTemplate<ref_count>::substitute(Iterator1 nodesBegin, } // otherwise compute - Assert( std::distance(nodesBegin, nodesEnd) == std::distance(replacementsBegin, replacementsEnd), - "Substitution iterator ranges must be equal size" ); + Assert(std::distance(nodesBegin, nodesEnd) + == std::distance(replacementsBegin, replacementsEnd)) + << "Substitution iterator ranges must be equal size"; Iterator1 j = find(nodesBegin, nodesEnd, TNode(*this)); if(j != nodesEnd) { Iterator2 b = replacementsBegin; diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 59e3d3b03..eda4dadd2 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -436,8 +436,8 @@ Node substituteCaptureAvoiding(TNode n, std::vector<TNode> visit; TNode curr; visit.push_back(n); - Assert(src.size() == dest.size(), - "Substitution domain and range must be equal size"); + Assert(src.size() == dest.size()) + << "Substitution domain and range must be equal size"; do { curr = visit.back(); diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index b5e99c6fd..b6594a933 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -170,13 +170,12 @@ namespace CVC4 { class NodeManager; }/* CVC4 namespace */ -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" - namespace CVC4 { // Sometimes it's useful for debugging to output a NodeBuilder that @@ -231,10 +230,9 @@ class NodeBuilder { * Set this NodeBuilder to the `used' state. */ inline void setUsed() { - Assert(!isUsed(), "Internal error: bad `used' state in NodeBuilder!"); - Assert(d_inlineNv.d_nchildren == 0 && - d_nvMaxChildren == nchild_thresh, - "Internal error: bad `inline' state in NodeBuilder!"); + Assert(!isUsed()) << "Internal error: bad `used' state in NodeBuilder!"; + Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh) + << "Internal error: bad `inline' state in NodeBuilder!"; d_nv = NULL; } @@ -243,10 +241,9 @@ class NodeBuilder { * from clear(). */ inline void setUnused() { - Assert(isUsed(), "Internal error: bad `used' state in NodeBuilder!"); - Assert(d_inlineNv.d_nchildren == 0 && - d_nvMaxChildren == nchild_thresh, - "Internal error: bad `inline' state in NodeBuilder!"); + Assert(isUsed()) << "Internal error: bad `used' state in NodeBuilder!"; + Assert(d_inlineNv.d_nchildren == 0 && d_nvMaxChildren == nchild_thresh) + << "Internal error: bad `inline' state in NodeBuilder!"; d_nv = &d_inlineNv; } @@ -381,9 +378,8 @@ public: d_nv(&d_inlineNv), d_nm(NodeManager::currentNM()), d_nvMaxChildren(nchild_thresh) { - - Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND, - "illegal Node-building kind"); + Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND) + << "illegal Node-building kind"; d_inlineNv.d_id = 1; // have a kind already d_inlineNv.d_rc = 0; @@ -406,9 +402,8 @@ public: d_nv(&d_inlineNv), d_nm(nm), d_nvMaxChildren(nchild_thresh) { - - Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND, - "illegal Node-building kind"); + Assert(k != kind::NULL_EXPR && k != kind::UNDEFINED_KIND) + << "illegal Node-building kind"; d_inlineNv.d_id = 1; // have a kind already d_inlineNv.d_rc = 0; @@ -461,48 +456,48 @@ public: /** Get the begin-const-iterator of this Node-under-construction. */ inline const_iterator begin() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "Iterators over NodeBuilder<> are undefined " - "until a Kind is set"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "Iterators over NodeBuilder<> are undefined " + "until a Kind is set"; return d_nv->begin< NodeTemplate<true> >(); } /** Get the end-const-iterator of this Node-under-construction. */ inline const_iterator end() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "Iterators over NodeBuilder<> are undefined " - "until a Kind is set"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "Iterators over NodeBuilder<> are undefined " + "until a Kind is set"; return d_nv->end< NodeTemplate<true> >(); } /** Get the kind of this Node-under-construction. */ inline Kind getKind() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; return d_nv->getKind(); } /** Get the kind of this Node-under-construction. */ inline kind::MetaKind getMetaKind() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "The metakind of a NodeBuilder<> is undefined " - "until a Kind is set"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "The metakind of a NodeBuilder<> is undefined " + "until a Kind is set"; return d_nv->getMetaKind(); } /** Get the current number of children of this Node-under-construction. */ inline unsigned getNumChildren() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "The number of children of a NodeBuilder<> is undefined " - "until a Kind is set"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "The number of children of a NodeBuilder<> is undefined " + "until a Kind is set"; return d_nv->getNumChildren(); } @@ -512,15 +507,15 @@ public: * that is of PARAMETERIZED metakind. */ inline Node getOperator() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "NodeBuilder<> operator access is not permitted " - "until a Kind is set"); - Assert(getMetaKind() == kind::metakind::PARAMETERIZED, - "NodeBuilder<> operator access is only permitted " - "on parameterized kinds, not `%s'", - kind::kindToString(getKind()).c_str()); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "NodeBuilder<> operator access is not permitted " + "until a Kind is set"; + Assert(getMetaKind() == kind::metakind::PARAMETERIZED) + << "NodeBuilder<> operator access is only permitted " + "on parameterized kinds, not `" + << getKind() << "'"; return Node(d_nv->getOperator()); } @@ -529,13 +524,13 @@ public: * if this NodeBuilder is unused and has a defined kind. */ inline Node getChild(int i) const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "NodeBuilder<> child access is not permitted " - "until a Kind is set"); - Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(), - "index out of range for NodeBuilder::getChild()"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "NodeBuilder<> child access is not permitted " + "until a Kind is set"; + Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren()) + << "index out of range for NodeBuilder::getChild()"; return Node(d_nv->getChild(i)); } @@ -562,12 +557,12 @@ public: /** Set the Kind of this Node-under-construction. */ inline NodeBuilder<nchild_thresh>& operator<<(const Kind& k) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0, - "can't redefine the Kind of a NodeBuilder"); - Assert(d_nv->d_id == 0, - "internal inconsistency with NodeBuilder: d_id != 0"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0) + << "can't redefine the Kind of a NodeBuilder"; + Assert(d_nv->d_id == 0) + << "internal inconsistency with NodeBuilder: d_id != 0"; AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR && k < kind::LAST_KIND, @@ -592,8 +587,8 @@ public: * append the given Node as a child. Otherwise, simply append. */ NodeBuilder<nchild_thresh>& operator<<(TNode n) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; // This test means: we didn't have a Kind at the beginning (on // NodeBuilder construction or at the last clear()), but we do // now. That means we appended a Kind with operator<<(Kind), @@ -611,8 +606,8 @@ public: * append the given Node as a child. Otherwise, simply append. */ NodeBuilder<nchild_thresh>& operator<<(TypeNode n) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; // This test means: we didn't have a Kind at the beginning (on // NodeBuilder construction or at the last clear()), but we do // now. That means we appended a Kind with operator<<(Kind), @@ -628,8 +623,8 @@ public: /** Append a sequence of children to this TypeNode-under-construction. */ inline NodeBuilder<nchild_thresh>& append(const std::vector<TypeNode>& children) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; return append(children.begin(), children.end()); } @@ -637,16 +632,16 @@ public: template <bool ref_count> inline NodeBuilder<nchild_thresh>& append(const std::vector<NodeTemplate<ref_count> >& children) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; return append(children.begin(), children.end()); } /** Append a sequence of children to this Node-under-construction. */ template <class Iterator> NodeBuilder<nchild_thresh>& append(const Iterator& begin, const Iterator& end) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; for(Iterator i = begin; i != end; ++i) { append(*i); } @@ -655,9 +650,9 @@ public: /** Append a child to this Node-under-construction. */ NodeBuilder<nchild_thresh>& append(TNode n) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(!n.isNull()) << "Cannot use NULL Node as a child of a Node"; if(n.getKind() == kind::BUILTIN) { return *this << NodeManager::operatorToKind(n); } @@ -671,9 +666,9 @@ public: /** Append a child to this Node-under-construction. */ NodeBuilder<nchild_thresh>& append(const TypeNode& typeNode) { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(!typeNode.isNull(), "Cannot use NULL Node as a child of a Node"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(!typeNode.isNull()) << "Cannot use NULL Node as a child of a Node"; allocateNvIfNecessaryForAppend(); expr::NodeValue* nv = typeNode.d_nv; nv->inc(); @@ -751,7 +746,7 @@ namespace CVC4 { template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::clear(Kind k) { - Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind"); + Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind"; if(__builtin_expect( ( nvIsAllocated() ), false )) { dealloc(); @@ -774,13 +769,11 @@ void NodeBuilder<nchild_thresh>::clear(Kind k) { template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { - AlwaysAssert(toSize > d_nvMaxChildren, - "attempt to realloc() a NodeBuilder to a smaller/equal size!"); - Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN), - "attempt to realloc() a NodeBuilder to size %lu (beyond hard limit of " - "%u)", - toSize, - expr::NodeValue::MAX_CHILDREN); + AlwaysAssert(toSize > d_nvMaxChildren) + << "attempt to realloc() a NodeBuilder to a smaller/equal size!"; + Assert(toSize < (static_cast<size_t>(1) << expr::NodeValue::NBITS_NCHILDREN)) + << "attempt to realloc() a NodeBuilder to size " << toSize + << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")"; if(__builtin_expect( ( nvIsAllocated() ), false )) { // Ensure d_nv is not modified on allocation failure @@ -793,7 +786,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { throw std::bad_alloc(); } d_nvMaxChildren = toSize; - Assert(d_nvMaxChildren == toSize);//overflow check + Assert(d_nvMaxChildren == toSize); // overflow check // Here, the copy (between two heap-allocated buffers) has already // been done for us by the std::realloc(). d_nv = newBlock; @@ -806,7 +799,7 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { throw std::bad_alloc(); } d_nvMaxChildren = toSize; - Assert(d_nvMaxChildren == toSize);//overflow check + Assert(d_nvMaxChildren == toSize); // overflow check d_nv = newBlock; d_nv->d_id = d_inlineNv.d_id; @@ -825,9 +818,9 @@ void NodeBuilder<nchild_thresh>::realloc(size_t toSize) { template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::dealloc() { - Assert( nvIsAllocated(), - "Internal error: NodeBuilder: dealloc() called without a " - "private NodeBuilder-allocated buffer" ); + Assert(nvIsAllocated()) + << "Internal error: NodeBuilder: dealloc() called without a " + "private NodeBuilder-allocated buffer"; for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); @@ -842,9 +835,9 @@ void NodeBuilder<nchild_thresh>::dealloc() { template <unsigned nchild_thresh> void NodeBuilder<nchild_thresh>::decrRefCounts() { - Assert( !nvIsAllocated(), - "Internal error: NodeBuilder: decrRefCounts() called with a " - "private NodeBuilder-allocated buffer" ); + Assert(!nvIsAllocated()) + << "Internal error: NodeBuilder: decrRefCounts() called with a " + "private NodeBuilder-allocated buffer"; for(expr::NodeValue::nv_iterator i = d_inlineNv.nv_begin(); i != d_inlineNv.nv_end(); @@ -918,10 +911,10 @@ NodeBuilder<nchild_thresh>::operator TypeNode() const { template <unsigned nchild_thresh> expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "Can't make an expression of an undefined kind!"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "Can't make an expression of an undefined kind!"; // NOTE: The comments in this function refer to the cases in the // file comments at the top of this file. @@ -933,12 +926,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { * and we don't keep VARIABLE-kinded Nodes in the NodeManager * pool. */ - Assert( ! nvIsAllocated(), - "internal NodeBuilder error: " - "VARIABLE-kinded NodeBuilder is heap-allocated !?" ); - Assert( d_inlineNv.d_nchildren == 0, - "improperly-formed VARIABLE-kinded NodeBuilder: " - "no children permitted" ); + Assert(!nvIsAllocated()) + << "internal NodeBuilder error: " + "VARIABLE-kinded NodeBuilder is heap-allocated !?"; + Assert(d_inlineNv.d_nchildren == 0) + << "improperly-formed VARIABLE-kinded NodeBuilder: " + "no children permitted"; // we have to copy the inline NodeValue out expr::NodeValue* nv = (expr::NodeValue*) @@ -963,20 +956,20 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { } // check that there are the right # of children for this kind - Assert(getMetaKind() != kind::metakind::CONSTANT, - "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"); - Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()), - "Nodes with kind %s must have at least %u children (the one under " - "construction has %u)", - kind::kindToString(getKind()).c_str(), - kind::metakind::getLowerBoundForKind(getKind()), - getNumChildren()); - Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()), - "Nodes with kind %s must have at most %u children (the one under " - "construction has %u)", - kind::kindToString(getKind()).c_str(), - kind::metakind::getUpperBoundForKind(getKind()), - getNumChildren()); + Assert(getMetaKind() != kind::metakind::CONSTANT) + << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"; + Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind())) + << "Nodes with kind " << getKind() << " must have at least " + << kind::metakind::getLowerBoundForKind(getKind()) + << " children (the one under " + "construction has " + << getNumChildren() << ")"; + Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind())) + << "Nodes with kind " << getKind() << " must have at most " + << kind::metakind::getUpperBoundForKind(getKind()) + << " children (the one under " + "construction has " + << getNumChildren() << ")"; // Implementation differs depending on whether the NodeValue was // malloc'ed or not and whether or not it's in the already-been-seen @@ -1098,10 +1091,10 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { // CONST VERSION OF NODE EXTRACTOR template <unsigned nchild_thresh> expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - Assert(getKind() != kind::UNDEFINED_KIND, - "Can't make an expression of an undefined kind!"); + Assert(!isUsed()) << "NodeBuilder is one-shot only; " + "attempt to access it after conversion"; + Assert(getKind() != kind::UNDEFINED_KIND) + << "Can't make an expression of an undefined kind!"; // NOTE: The comments in this function refer to the cases in the // file comments at the top of this file. @@ -1113,12 +1106,12 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { * and we don't keep VARIABLE-kinded Nodes in the NodeManager * pool. */ - Assert( ! nvIsAllocated(), - "internal NodeBuilder error: " - "VARIABLE-kinded NodeBuilder is heap-allocated !?" ); - Assert( d_inlineNv.d_nchildren == 0, - "improperly-formed VARIABLE-kinded NodeBuilder: " - "no children permitted" ); + Assert(!nvIsAllocated()) + << "internal NodeBuilder error: " + "VARIABLE-kinded NodeBuilder is heap-allocated !?"; + Assert(d_inlineNv.d_nchildren == 0) + << "improperly-formed VARIABLE-kinded NodeBuilder: " + "no children permitted"; // we have to copy the inline NodeValue out expr::NodeValue* nv = (expr::NodeValue*) @@ -1138,29 +1131,27 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const { } // check that there are the right # of children for this kind - Assert(getMetaKind() != kind::metakind::CONSTANT, - "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"); - Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()), - "Nodes with kind %s must have at least %u children (the one under " - "construction has %u)", - kind::kindToString(getKind()).c_str(), - kind::metakind::getLowerBoundForKind(getKind()), - getNumChildren()); - Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()), - "Nodes with kind %s must have at most %u children (the one under " - "construction has %u)", - kind::kindToString(getKind()).c_str(), - kind::metakind::getUpperBoundForKind(getKind()), - getNumChildren()); + Assert(getMetaKind() != kind::metakind::CONSTANT) + << "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds"; + Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind())) + << "Nodes with kind " << getKind() << " must have at least " + << kind::metakind::getLowerBoundForKind(getKind()) + << " children (the one under " + "construction has " + << getNumChildren() << ")"; + Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind())) + << "Nodes with kind " << getKind() << " must have at most " + << kind::metakind::getUpperBoundForKind(getKind()) + << " children (the one under " + "construction has " + << getNumChildren() << ")"; #if 0 // if the kind is PARAMETERIZED, check that the operator is correctly-kinded Assert(kind::metaKindOf(getKind()) != kind::metakind::PARAMETERIZED || - NodeManager::operatorToKind(getOperator()) == getKind(), - "Attempted to construct a parameterized kind `%s' with " - "incorrectly-kinded operator `%s'", - kind::kindToString(getKind()).c_str(), - kind::kindToString(getOperator().getKind()).c_str()); + NodeManager::operatorToKind(getOperator()) == getKind()) << + "Attempted to construct a parameterized kind `"<< getKind() <<"' with " + "incorrectly-kinded operator `"<< getOperator().getKind() <<"'"; #endif /* 0 */ // Implementation differs depending on whether the NodeValue was @@ -1298,10 +1289,12 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { Assert(nb.d_nvMaxChildren <= d_nvMaxChildren); Assert(nb.d_nv->nv_end() >= nb.d_nv->nv_begin()); - Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren, "realloced:%s, d_nvMax:%u, size:%u, nc:%u", realloced ? "true" : "false", d_nvMaxChildren, nb.d_nv->nv_end() - nb.d_nv->nv_begin(), nb.d_nv->getNumChildren()); - std::copy(nb.d_nv->nv_begin(), - nb.d_nv->nv_end(), - d_nv->nv_begin()); + Assert((size_t)(nb.d_nv->nv_end() - nb.d_nv->nv_begin()) <= d_nvMaxChildren) + << "realloced:" << (realloced ? "true" : "false") + << ", d_nvMax:" << d_nvMaxChildren + << ", size:" << nb.d_nv->nv_end() - nb.d_nv->nv_begin() + << ", nc:" << nb.d_nv->getNumChildren(); + std::copy(nb.d_nv->nv_begin(), nb.d_nv->nv_end(), d_nv->nv_begin()); d_nv->d_nchildren = nb.d_nv->d_nchildren; diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 66d597a36..d66225961 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -21,7 +21,7 @@ #include <stack> #include <utility> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/listener.h" #include "expr/attribute.h" #include "expr/node_manager_attributes.h" @@ -29,8 +29,8 @@ #include "expr/type_checker.h" #include "options/options.h" #include "options/smt_options.h" -#include "util/statistics_registry.h" #include "util/resource_manager.h" +#include "util/statistics_registry.h" using namespace std; using namespace CVC4::expr; @@ -195,7 +195,7 @@ NodeManager::~NodeManager() { } d_ownedDatatypes.clear(); - Assert(!d_attrManager->inGarbageCollection() ); + Assert(!d_attrManager->inGarbageCollection()); std::vector<NodeValue*> order = TopologicalSort(d_maxedOut); d_maxedOut.clear(); @@ -253,7 +253,7 @@ unsigned NodeManager::registerDatatype(Datatype* dt) { } const Datatype & NodeManager::getDatatypeForIndex( unsigned index ) const{ - Assert( index<d_ownedDatatypes.size() ); + Assert(index < d_ownedDatatypes.size()); return *d_ownedDatatypes[index]; } @@ -264,7 +264,8 @@ void NodeManager::reclaimZombies() { Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; // during reclamation, reclaimZombies() is never supposed to be called - Assert(! d_inReclaimZombies, "NodeManager::reclaimZombies() not re-entrant!"); + Assert(!d_inReclaimZombies) + << "NodeManager::reclaimZombies() not re-entrant!"; // whether exit is normal or exceptional, the Reclaim dtor is called // and ensures that d_inReclaimZombies is set back to false. @@ -446,7 +447,7 @@ TypeNode NodeManager::getType(TNode n, bool check) } if( readyToCompute ) { - Assert( check || m.getMetaKind()!=kind::metakind::NULLARY_OPERATOR ); + Assert(check || m.getMetaKind() != kind::metakind::NULLARY_OPERATOR); /* All the children have types, time to compute */ typeNode = TypeChecker::computeType(this, m, check); worklist.pop(); @@ -454,18 +455,18 @@ TypeNode NodeManager::getType(TNode n, bool check) } // end while /* Last type computed in loop should be the type of n */ - Assert( typeNode == getAttribute(n, TypeAttr()) ); + Assert(typeNode == getAttribute(n, TypeAttr())); } else if( !hasType || needsCheck ) { /* We can compute the type top-down, without worrying about deep recursion. */ - Assert( check || n.getMetaKind()!=kind::metakind::NULLARY_OPERATOR ); + Assert(check || n.getMetaKind() != kind::metakind::NULLARY_OPERATOR); typeNode = TypeChecker::computeType(this, n, check); } /* The type should be have been computed and stored. */ - Assert( hasAttribute(n, TypeAttr()) ); + Assert(hasAttribute(n, TypeAttr())); /* The check should have happened, if we asked for it. */ - Assert( !check || getAttribute(n, TypeCheckedAttr()) ); + Assert(!check || getAttribute(n, TypeCheckedAttr())); Debug("getType") << "type of " << &n << " " << n << " is " << typeNode << endl; return typeNode; @@ -628,16 +629,17 @@ TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { TypeNode NodeManager::mkSort(TypeNode constructor, const std::vector<TypeNode>& children, uint32_t flags) { - Assert(constructor.getKind() == kind::SORT_TYPE && - constructor.getNumChildren() == 0, - "expected a sort constructor"); - Assert(children.size() > 0, "expected non-zero # of children"); - Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) && - hasAttribute(constructor.d_nv, expr::VarNameAttr()), - "expected a sort constructor" ); + Assert(constructor.getKind() == kind::SORT_TYPE + && constructor.getNumChildren() == 0) + << "expected a sort constructor"; + Assert(children.size() > 0) << "expected non-zero # of children"; + Assert(hasAttribute(constructor.d_nv, expr::SortArityAttr()) + && hasAttribute(constructor.d_nv, expr::VarNameAttr())) + << "expected a sort constructor"; std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); - Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(), - "arity mismatch in application of sort constructor"); + Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) + == children.size()) + << "arity mismatch in application of sort constructor"; NodeBuilder<> nb(this, kind::SORT_TYPE); Node sortTag = Node(constructor.d_nv->d_children[0]); nb << sortTag; @@ -706,7 +708,7 @@ Node* NodeManager::mkBoundVarPtr(const std::string& name, } Node NodeManager::getBoundVarListForFunctionType( TypeNode tn ) { - Assert( tn.isFunction() ); + Assert(tn.isFunction()); Node bvl = tn.getAttribute(LambdaBoundVarListAttr()); if( bvl.isNull() ){ std::vector< Node > vars; @@ -777,7 +779,7 @@ Node NodeManager::mkNullaryOperator(const TypeNode& type, Kind k) { setAttribute(n, TypeAttr(), type); //setAttribute(n, TypeCheckedAttr(), true); d_unique_vars[k][type] = n; - Assert( n.getMetaKind() == kind::metakind::NULLARY_OPERATOR ); + Assert(n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); return n; }else{ return it->second; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 510e6d585..a3fd50d8c 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -32,6 +32,7 @@ #include <string> #include <unordered_set> +#include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" #include "expr/node_value.h" @@ -411,14 +412,16 @@ public: /** Subscribe to NodeManager events */ void subscribeEvents(NodeManagerListener* listener) { - Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) == d_listeners.end(), "listener already subscribed"); + Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) + == d_listeners.end()) + << "listener already subscribed"; d_listeners.push_back(listener); } /** Unsubscribe from NodeManager events */ void unsubscribeEvents(NodeManagerListener* listener) { std::vector<NodeManagerListener*>::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener); - Assert(elt != d_listeners.end(), "listener not subscribed"); + Assert(elt != d_listeners.end()) << "listener not subscribed"; d_listeners.erase(elt); } @@ -1177,14 +1180,14 @@ inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { } inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), - "NodeValue already in the pool!"); + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end()) + << "NodeValue already in the pool!"; d_nodeValuePool.insert(nv);// FIXME multithreading } inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), - "NodeValue is not in the pool!"); + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end()) + << "NodeValue is not in the pool!"; d_nodeValuePool.erase(nv);// FIXME multithreading } @@ -1240,8 +1243,7 @@ inline bool NodeManager::hasOperator(Kind k) { case kind::metakind::CONSTANT: return false; - default: - Unhandled(mk); + default: Unhandled() << mk; } } diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h index 7e0478acc..79df7691c 100644 --- a/src/expr/node_self_iterator.h +++ b/src/expr/node_self_iterator.h @@ -21,7 +21,7 @@ #include <iterator> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/node.h" namespace CVC4 { @@ -53,12 +53,12 @@ public: };/* class NodeSelfIterator */ inline NodeSelfIterator NodeSelfIterator::self(TNode n) { - Assert(!n.isNull(), "Self-iteration over null nodes not permitted."); + Assert(!n.isNull()) << "Self-iteration over null nodes not permitted."; return NodeSelfIterator(n); } inline NodeSelfIterator NodeSelfIterator::selfEnd(TNode n) { - Assert(!n.isNull(), "Self-iteration over null nodes not permitted."); + Assert(!n.isNull()) << "Self-iteration over null nodes not permitted."; return NodeSelfIterator(n.end()); } @@ -70,13 +70,13 @@ inline NodeSelfIterator::NodeSelfIterator() : inline NodeSelfIterator::NodeSelfIterator(Node node) : d_node(node), d_child() { - Assert(!node.isNull(), "Self-iteration over null nodes not permitted."); + Assert(!node.isNull()) << "Self-iteration over null nodes not permitted."; } inline NodeSelfIterator::NodeSelfIterator(TNode node) : d_node(node), d_child() { - Assert(!node.isNull(), "Self-iteration over null nodes not permitted."); + Assert(!node.isNull()) << "Self-iteration over null nodes not permitted."; } inline NodeSelfIterator::NodeSelfIterator(const NodeSelfIterator& i) : diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 9d1a4f98e..2c52c46be 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -421,18 +421,18 @@ inline void NodeValue::decrRefCounts() { } inline void NodeValue::inc() { - Assert(!isBeingDeleted(), - "NodeValue is currently being deleted " - "and increment is being called on it. Don't Do That!"); + Assert(!isBeingDeleted()) + << "NodeValue is currently being deleted " + "and increment is being called on it. Don't Do That!"; // FIXME multithreading if (__builtin_expect((d_rc < MAX_RC - 1), true)) { ++d_rc; } else if (__builtin_expect((d_rc == MAX_RC - 1), false)) { ++d_rc; - Assert(NodeManager::currentNM() != NULL, - "No current NodeManager on incrementing of NodeValue: " + Assert(NodeManager::currentNM() != NULL) + << "No current NodeManager on incrementing of NodeValue: " "maybe a public CVC4 interface function is missing a " - "NodeManagerScope ?"); + "NodeManagerScope ?"; NodeManager::currentNM()->markRefCountMaxedOut(this); } } @@ -442,10 +442,10 @@ inline void NodeValue::dec() { if(__builtin_expect( ( d_rc < MAX_RC ), true )) { --d_rc; if(__builtin_expect( ( d_rc == 0 ), false )) { - Assert(NodeManager::currentNM() != NULL, - "No current NodeManager on destruction of NodeValue: " + Assert(NodeManager::currentNM() != NULL) + << "No current NodeManager on destruction of NodeValue: " "maybe a public CVC4 interface function is missing a " - "NodeManagerScope ?"); + "NodeManagerScope ?"; NodeManager::currentNM()->markForDeletion(this); } } diff --git a/src/expr/record.cpp b/src/expr/record.cpp index 0303ff705..074205d04 100644 --- a/src/expr/record.cpp +++ b/src/expr/record.cpp @@ -16,7 +16,7 @@ #include "expr/record.h" -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" #include "expr/expr.h" #include "expr/type.h" diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 9ca5f00cc..375fbd515 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -48,7 +48,7 @@ ${typerules} default: Debug("getType") << "FAILURE" << std::endl; - Unhandled(n.getKind()); + Unhandled() << n.getKind(); } nodeManager->setAttribute(n, TypeAttr(), typeNode); @@ -61,14 +61,16 @@ ${typerules} bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); + Assert(n.getMetaKind() == kind::metakind::OPERATOR + || n.getMetaKind() == kind::metakind::PARAMETERIZED + || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); switch(n.getKind()) { ${construles} -#line 70 "${template}" +#line 72 "${template}" - default:; + default:; } return false; @@ -77,14 +79,16 @@ ${construles} bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n) { - Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); + Assert(n.getMetaKind() == kind::metakind::OPERATOR + || n.getMetaKind() == kind::metakind::PARAMETERIZED + || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); switch(n.getKind()) { ${neverconstrules} -#line 86 "${template}" +#line 90 "${template}" - default:; + default:; } return true; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 9db29f115..b3c8592ed 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -377,14 +377,14 @@ bool TypeNode::isRecord() const { size_t TypeNode::getTupleLength() const { Assert(isTuple()); const Datatype& dt = getDatatype(); - Assert(dt.getNumConstructors()==1); + Assert(dt.getNumConstructors() == 1); return dt[0].getNumArgs(); } vector<TypeNode> TypeNode::getTupleTypes() const { Assert(isTuple()); const Datatype& dt = getDatatype(); - Assert(dt.getNumConstructors()==1); + Assert(dt.getNumConstructors() == 1); vector<TypeNode> types; for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) { types.push_back(TypeNode::fromType(dt[0][i].getRangeType())); @@ -444,9 +444,9 @@ TypeNode TypeNode::mostCommonTypeNode(TypeNode t0, TypeNode t1){ } TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; Assert(!t0.isNull()); Assert(!t1.isNull()); @@ -506,15 +506,17 @@ TypeNode TypeNode::commonTypeNode(TypeNode t0, TypeNode t1, bool isLeast) { } } case kind::SEXPR_TYPE: - Unimplemented("haven't implemented leastCommonType for symbolic expressions yet"); + Unimplemented() + << "haven't implemented leastCommonType for symbolic expressions yet"; default: - Unimplemented("don't have a commonType for types `%s' and `%s'", t0.toString().c_str(), t1.toString().c_str()); + Unimplemented() << "don't have a commonType for types `" << t0 << "' and `" + << t1 << "'"; } } Node TypeNode::getEnsureTypeCondition( Node n, TypeNode tn ) { TypeNode ntn = n.getType(); - Assert( ntn.isComparableTo( tn ) ); + Assert(ntn.isComparableTo(tn)); if( !ntn.isSubtypeOf( tn ) ){ if( tn.isInteger() ){ if( tn.isSubtypeOf( ntn ) ){ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index c5e1f400c..1fcd64fc7 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -29,7 +29,7 @@ #include <unordered_map> #include <vector> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "expr/kind.h" #include "expr/metakind.h" #include "util/cardinality.h" @@ -752,8 +752,8 @@ TypeNode TypeNode::substitute(Iterator1 typesBegin, } // otherwise compute - Assert( typesEnd - typesBegin == replacementsEnd - replacementsBegin, - "Substitution iterator ranges must be equal size" ); + Assert(typesEnd - typesBegin == replacementsEnd - replacementsBegin) + << "Substitution iterator ranges must be equal size"; Iterator1 j = find(typesBegin, typesEnd, *this); if(j != typesEnd) { TypeNode tn = *(replacementsBegin + (j - typesBegin)); @@ -792,18 +792,18 @@ inline const T& TypeNode::getConst() const { inline TypeNode::TypeNode(const expr::NodeValue* ev) : d_nv(const_cast<expr::NodeValue*> (ev)) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; d_nv->inc(); } inline TypeNode::TypeNode(const TypeNode& typeNode) { - Assert(typeNode.d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(typeNode.d_nv != NULL) << "Expecting a non-NULL expression value!"; d_nv = typeNode.d_nv; d_nv->inc(); } inline TypeNode::~TypeNode() { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; d_nv->dec(); } @@ -813,9 +813,9 @@ inline void TypeNode::assignNodeValue(expr::NodeValue* ev) { } inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) { - Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); - Assert(typeNode.d_nv != NULL, - "Expecting a non-NULL expression value on RHS!"); + Assert(d_nv != NULL) << "Expecting a non-NULL expression value!"; + Assert(typeNode.d_nv != NULL) + << "Expecting a non-NULL expression value on RHS!"; if(__builtin_expect( ( d_nv != typeNode.d_nv ), true )) { d_nv->dec(); d_nv = typeNode.d_nv; @@ -827,35 +827,35 @@ inline TypeNode& TypeNode::operator=(const TypeNode& typeNode) { template <class AttrKind> inline typename AttrKind::value_type TypeNode:: getAttribute(const AttrKind&) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->getAttribute(d_nv, AttrKind()); } template <class AttrKind> inline bool TypeNode:: hasAttribute(const AttrKind&) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->hasAttribute(d_nv, AttrKind()); } template <class AttrKind> inline bool TypeNode::getAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; return NodeManager::currentNM()->getAttribute(d_nv, AttrKind(), ret); } template <class AttrKind> inline void TypeNode:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + Assert(NodeManager::currentNM() != NULL) + << "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?"; NodeManager::currentNM()->setAttribute(d_nv, AttrKind(), value); } @@ -1022,7 +1022,7 @@ inline const Datatype& TypeNode::getDatatype() const { DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>(); return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() ); }else{ - Assert( getKind() == kind::PARAMETRIC_DATATYPE ); + Assert(getKind() == kind::PARAMETRIC_DATATYPE); return (*this)[0].getDatatype(); } } @@ -1035,8 +1035,8 @@ inline unsigned TypeNode::getFloatingPointExponentSize() const { /** Get the significand size of this floating-point type */ inline unsigned TypeNode::getFloatingPointSignificandSize() const { - Assert(isFloatingPoint()); - return getConst<FloatingPointSize>().significand(); + Assert(isFloatingPoint()); + return getConst<FloatingPointSize>().significand(); } /** Get the size of this bit-vector type */ diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 88447a125..6f1297f16 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -23,15 +23,15 @@ #include <sstream> -#include "base/cvc4_assert.h" -#include "options/language.h" -#include "expr/type_node.h" -#include "expr/kind.h" +#include "base/check.h" #include "expr/expr.h" +#include "expr/kind.h" +#include "expr/type_node.h" +#include "options/language.h" ${type_properties_includes} -#line 35 "${template}" +#line 36 "${template}" namespace CVC4 { namespace kind { @@ -42,17 +42,15 @@ namespace kind { * "kinds" files, so includes contributions from each theory regarding * that theory's types. */ -inline Cardinality getCardinality(TypeConstant tc) { - switch(tc) { +inline Cardinality getCardinality(TypeConstant tc) +{ + switch (tc) + { ${type_constant_cardinalities} -#line 49 "${template}" - default: { - std::stringstream ss; - ss << "No cardinality known for type constant " << tc; - InternalError(ss.str()); - } +#line 51 "${template}" + default: InternalError() << "No cardinality known for type constant " << tc; } -}/* getCardinality(TypeConstant) */ +} /* getCardinality(TypeConstant) */ /** * Return the cardinality of the type represented by the TypeNode @@ -66,26 +64,21 @@ inline Cardinality getCardinality(TypeNode typeNode) { case TYPE_CONSTANT: return getCardinality(typeNode.getConst<TypeConstant>()); ${type_cardinalities} -#line 70 "${template}" - default: { - std::stringstream ss; - ss << "A theory kinds file did not provide a cardinality " - << "or cardinality computer for type:\n" << typeNode - << "\nof kind " << k; - InternalError(ss.str()); - } +#line 68 "${template}" + default: + InternalError() << "A theory kinds file did not provide a cardinality " + << "or cardinality computer for type:\n" + << typeNode << "\nof kind " << k; } }/* getCardinality(TypeNode) */ inline bool isWellFounded(TypeConstant tc) { switch(tc) { ${type_constant_wellfoundednesses} -#line 84 "${template}" - default: { - std::stringstream ss; - ss << "No well-foundedness status known for type constant: " << tc; - InternalError(ss.str()); - } +#line 79 "${template}" +default: + InternalError() << "No well-foundedness status known for type constant: " + << tc; } }/* isWellFounded(TypeConstant) */ @@ -95,45 +88,40 @@ inline bool isWellFounded(TypeNode typeNode) { case TYPE_CONSTANT: return isWellFounded(typeNode.getConst<TypeConstant>()); ${type_wellfoundednesses} -#line 99 "${template}" - default: { - std::stringstream ss; - ss << "A theory kinds file did not provide a well-foundedness " - << "or well-foundedness computer for type:\n" << typeNode - << "\nof kind " << k; - InternalError(ss.str()); - } +#line 92 "${template}" + default: + InternalError() << "A theory kinds file did not provide a well-foundedness " + << "or well-foundedness computer for type:\n" + << typeNode << "\nof kind " << k; } }/* isWellFounded(TypeNode) */ -inline Node mkGroundTerm(TypeConstant tc) { - switch(tc) { +inline Node mkGroundTerm(TypeConstant tc) +{ + switch (tc) + { ${type_constant_groundterms} -#line 113 "${template}" - default: { - std::stringstream ss; - ss << "No ground term known for type constant: " << tc; - InternalError(ss.str()); +#line 105 "${template}" + default: + InternalError() << "No ground term known for type constant: " << tc; } - } -}/* mkGroundTerm(TypeConstant) */ +} /* mkGroundTerm(TypeConstant) */ -inline Node mkGroundTerm(TypeNode typeNode) { +inline Node mkGroundTerm(TypeNode typeNode) +{ AssertArgument(!typeNode.isNull(), typeNode); - switch(Kind k = typeNode.getKind()) { - case TYPE_CONSTANT: - return mkGroundTerm(typeNode.getConst<TypeConstant>()); + switch (Kind k = typeNode.getKind()) + { + case TYPE_CONSTANT: + return mkGroundTerm(typeNode.getConst<TypeConstant>()); ${type_groundterms} -#line 128 "${template}" - default: { - std::stringstream ss; - ss << "A theory kinds file did not provide a ground term " - << "or ground term computer for type:\n" << typeNode - << "\nof kind " << k; - InternalError(ss.str()); - } +#line 119 "${template}" + default: + InternalError() << "A theory kinds file did not provide a ground term " + << "or ground term computer for type:\n" + << typeNode << "\nof kind " << k; } -}/* mkGroundTerm(TypeNode) */ +} /* mkGroundTerm(TypeNode) */ }/* CVC4::kind namespace */ }/* CVC4 namespace */ diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index 64180c377..574580259 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -21,7 +21,7 @@ #include <sstream> #include <string> -#include "base/cvc4_assert.h" +#include "base/check.h" using namespace std; |