summaryrefslogtreecommitdiff
path: root/src/expr/expr_template.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r--src/expr/expr_template.cpp80
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() */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback