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/expr_template.cpp | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 80 |
1 files changed, 40 insertions, 40 deletions
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() */ |