diff options
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 45 |
1 files changed, 23 insertions, 22 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index dbd7c049b..dfbe179be 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -13,18 +13,18 @@ ** ** Public-facing expression interface, implementation. **/ +#include "expr/expr.h" + +#include <iterator> +#include <utility> +#include <vector> #include "base/cvc4_assert.h" -#include "expr/expr.h" #include "expr/node.h" #include "expr/expr_manager_scope.h" #include "expr/variable_type_map.h" #include "expr/node_manager_attributes.h" -#include <vector> -#include <iterator> -#include <utility> - ${includes} // This is a hack, but an important one: if there's an error, the @@ -326,15 +326,16 @@ bool Expr::hasOperator() const { Expr Expr::getOperator() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - CheckArgument(d_node->hasOperator(), *this, - "Expr::getOperator() called on an Expr with no operator"); + PrettyCheckArgument(d_node->hasOperator(), *this, + "Expr::getOperator() called on an Expr with no operator"); return Expr(d_exprManager, new Node(d_node->getOperator())); } Type Expr::getType(bool check) const throw (TypeCheckingException) { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - CheckArgument(!d_node->isNull(), this, "Can't get type of null expression!"); + PrettyCheckArgument(!d_node->isNull(), this, + "Can't get type of null expression!"); return d_exprManager->getType(*this, check); } @@ -509,40 +510,40 @@ Expr Expr::notExpr() const { Expr Expr::andExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + 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!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + 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!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(XOR, *this, e); } Expr Expr::iffExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(IFF, *this, e); } Expr Expr::impExpr(const Expr& e) const { Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - CheckArgument(d_exprManager == e.d_exprManager, e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(IMPLIES, *this, e); } @@ -550,10 +551,10 @@ 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!"); - CheckArgument(d_exprManager == then_e.d_exprManager, then_e, - "Different expression managers!"); - CheckArgument(d_exprManager == else_e.d_exprManager, else_e, - "Different expression managers!"); + PrettyCheckArgument(d_exprManager == then_e.d_exprManager, then_e, + "Different expression managers!"); + PrettyCheckArgument(d_exprManager == else_e.d_exprManager, else_e, + "Different expression managers!"); return d_exprManager->mkExpr(ITE, *this, then_e, else_e); } |