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, 2 insertions, 2 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 17524a3c0..c9e6866d4 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -393,8 +393,8 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
     sorts.push_back(sort);
   }
   Debug("datatypes") << "ctor range: " << range << endl;
-  CheckArgument(!range.isFunctionLike(), range,
-                "cannot create higher-order function types");
+  PrettyCheckArgument(!range.isFunctionLike(), range,
+                      "cannot create higher-order function types");
   sorts.push_back(range);
   return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts);
 }