diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-04-04 19:36:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-04-04 19:36:56 +0000 |
commit | 73be7b6b5a9c98cc5a32dcfb3050b9656bf10243 (patch) | |
tree | 5421477844240ad71493ee01a85a4a8a5369d92d /src/expr/expr_template.cpp | |
parent | 3e27983545a25f3acc3bf7c7dbdf0ec1fe3219ca (diff) |
Recommit revision 365 (undoing revision 375, which reverted revision 365).
Fix the case in NodeBuilderBlack that triggered bug #82. (Fixes bug #82.)
This also fixes regression failures from this morning (2010 Apr 4), in
the optimized builds, for which a fix was included in 365 and reverted
in 375. They looked like this:
In ExprBlack::testGetConst:
/usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:377: Error: Expected (a->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
/usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:378: Error: Expected (b->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
[etc..]
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 57 |
1 files changed, 38 insertions, 19 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 4d4061bd0..7c723d338 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -123,13 +123,14 @@ bool Expr::hasOperator() const { Expr Expr::getOperator() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); - CheckArgument(d_node->hasOperator(), + CheckArgument(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() const { ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); return d_node->getType(); } @@ -178,51 +179,69 @@ BoolExpr::BoolExpr(const Expr& e) : } BoolExpr BoolExpr::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); } BoolExpr BoolExpr::andExpr(const BoolExpr& e) const { - Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - Assert(d_exprManager == e.d_exprManager, "Different expression managers!"); + Assert(d_exprManager != NULL, + "Don't have an expression manager for this expression!"); + CheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(AND, *this, e); } BoolExpr BoolExpr::orExpr(const BoolExpr& e) const { - Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - Assert(d_exprManager == e.d_exprManager, "Different expression managers!"); + Assert(d_exprManager != NULL, + "Don't have an expression manager for this expression!"); + CheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(OR, *this, e); } BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const { - Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - Assert(d_exprManager == e.d_exprManager, "Different expression managers!"); + Assert(d_exprManager != NULL, + "Don't have an expression manager for this expression!"); + CheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(XOR, *this, e); } BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const { - Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - Assert(d_exprManager == e.d_exprManager, "Different expression managers!"); + Assert(d_exprManager != NULL, + "Don't have an expression manager for this expression!"); + CheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(IFF, *this, e); } BoolExpr BoolExpr::impExpr(const BoolExpr& e) const { - Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - Assert(d_exprManager == e.d_exprManager, "Different expression managers!"); + Assert(d_exprManager != NULL, + "Don't have an expression manager for this expression!"); + CheckArgument(d_exprManager == e.d_exprManager, e, + "Different expression managers!"); return d_exprManager->mkExpr(IMPLIES, *this, e); } -BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const { - Assert(d_exprManager != NULL, "Don't have an expression manager for this expression!"); - Assert(d_exprManager == then_e.d_exprManager, "Different expression managers!"); - Assert(d_exprManager == else_e.d_exprManager, "Different expression managers!"); +BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, + const BoolExpr& 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!"); return d_exprManager->mkExpr(ITE, *this, then_e, else_e); } Expr BoolExpr::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 == then_e.getExprManager(), "Different expression managers!"); - Assert(d_exprManager == else_e.getExprManager(), "Different expression managers!"); + Assert(d_exprManager != NULL, + "Don't have an expression manager for this expression!"); + CheckArgument(d_exprManager == then_e.getExprManager(), then_e, + "Different expression managers!"); + CheckArgument(d_exprManager == else_e.getExprManager(), else_e, + "Different expression managers!"); return d_exprManager->mkExpr(ITE, *this, then_e, else_e); } |