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.

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);
 }