diff options
author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
tree | ed40cb371c41ac285ca2bf41a82254a36134e132 /src/expr/expr_template.cpp | |
parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
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); } |