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.

3 files changed, 94 insertions, 79 deletions

diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
index 6dca5c81d..6b47de8cc 100644
--- a/src/base/cvc4_assert.h
+++ b/src/base/cvc4_assert.h
@@ -282,11 +282,15 @@ void debugAssertionFailed(const AssertionException& thisException, const char* l
 #define InternalError(msg...) \
   throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
 #define IllegalArgument(arg, msg...) \
-  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
-#define CheckArgument(cond, arg, msg...)         \
+  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, \
+                                         ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str());
+// This cannot use check argument directly as this forces
+// CheckArgument to use a va_list. This is unsupported in Swig.
+#define PrettyCheckArgument(cond, arg, msg...)         \
   do { \
     if(__builtin_expect( ( ! (cond) ), false )) { \
-      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
+      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, \
+                                             ::CVC4::IllegalArgumentException::formatVariadic(msg).c_str()); \
     } \
   } while(0)
 #define AlwaysAssertArgument(cond, arg, msg...)  \
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index d8eee50bc..87bdfcfa5 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -15,6 +15,7 @@
  **/
 
 #include "base/exception.h"
+
 #include <string>
 #include <cstdio>
 #include <cstdlib>
@@ -24,12 +25,58 @@
 
 using namespace std;
 
-#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument."
-
 namespace CVC4 {
+
+char* IllegalArgumentException::s_header = "Illegal argument detected";
+
+std::string IllegalArgumentException::formatVariadic() {
+  return std::string();
+}
+
+std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
+  va_list args;
+  va_start(args, format);
+
+  int n = 512;
+  char* buf = NULL;
+
+  for (int i = 0; i < 2; ++i){
+    Assert(n > 0);
+    if(buf != NULL){
+      delete [] buf;
+    }
+    buf = new char[n];
+
+    va_list args_copy;
+    va_copy(args_copy, args);
+    int size = vsnprintf(buf, n, format, args);
+    va_end(args_copy);
+
+    if(size >= n){
+      buf[n-1] = '\0';
+      n = size + 1;
+    } else {
+      break;
+    }
+  }
+  // buf is not NULL is an invariant.
+  // buf is also 0 terminated.
+  Assert(buf != NULL);
+  std::string result(buf);
+  delete [] buf;
+  va_end(args);
+  return result;
+}
+
+std::string IllegalArgumentException::format_extra(const char* condStr, const char* argDesc){
+  return ( std::string("`") + argDesc + "' is a bad argument"
+           + (*condStr == '\0' ? std::string() :
+              ( std::string("; expected ") +
+                condStr + " to hold" )) );
+}
+
 void IllegalArgumentException::construct(const char* header, const char* extra,
-                                         const char* function, const char* fmt,
-                                         va_list args) {
+                                         const char* function, const char* tail) {
   // try building the exception msg with a smallish buffer first,
   // then with a larger one if sprintf tells us to.
   int n = 512;
@@ -40,25 +87,17 @@ void IllegalArgumentException::construct(const char* header, const char* extra,
 
     int size;
     if(extra == NULL) {
-      size = snprintf(buf, n, "%s\n%s\n",
-                      header, function);
+      size = snprintf(buf, n, "%s\n%s\n%s",
+                      header, function, tail);
     } else {
-      size = snprintf(buf, n, "%s\n%s\n\n  %s\n",
-                      header, function, extra);
+      size = snprintf(buf, n, "%s\n%s\n\n  %s\n%s",
+                      header, function, extra, tail);
     }
 
     if(size < n) {
-      va_list args_copy;
-      va_copy(args_copy, args);
-      size += vsnprintf(buf + size, n - size, fmt, args_copy);
-      va_end(args_copy);
-
-      if(size < n) {
-        break;
-      }
-    }
-
-    if(size >= n) {
+      break;
+    } else {
+      // size >= n
       // try again with a buffer that's large enough
       n = size + 1;
       delete [] buf;
diff --git a/src/base/exception.h b/src/base/exception.h
index 78bb160cc..84872b9b1 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -19,13 +19,13 @@
 #ifndef __CVC4__EXCEPTION_H
 #define __CVC4__EXCEPTION_H
 
-#include <iostream>
-#include <string>
+#include <cstdarg>
+#include <cstdlib>
+#include <exception>
+#include <iosfwd>
 #include <sstream>
 #include <stdexcept>
-#include <exception>
-#include <cstdlib>
-#include <cstdarg>
+#include <string>
 
 namespace CVC4 {
 
@@ -81,44 +81,37 @@ protected:
   IllegalArgumentException() : Exception() {}
 
   void construct(const char* header, const char* extra,
-                 const char* function, const char* fmt, ...) {
-    va_list args;
-    va_start(args, fmt);
-    construct(header, extra, function, fmt, args);
-    va_end(args);
-  }
-
-  void construct(const char* header, const char* extra,
-                 const char* function, const char* fmt, va_list args);
+                 const char* function, const char* tail);
 
   void construct(const char* header, const char* extra,
                  const char* function);
 
+  static std::string format_extra(const char* condStr, const char* argDesc);
+
+  static char* s_header;
+
 public:
+
   IllegalArgumentException(const char* condStr, const char* argDesc,
-                           const char* function, const char* fmt, ...) :
+                           const char* function, const char* tail) :
     Exception() {
-    va_list args;
-    va_start(args, fmt);
-    construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument"
-                + (*condStr == '\0' ? std::string() :
-                    ( std::string("; expected ") +
-                        condStr + " to hold" )) ).c_str(),
-              function, fmt, args);
-    va_end(args);
+    construct(s_header, format_extra(condStr, argDesc).c_str(), function, tail);
   }
 
   IllegalArgumentException(const char* condStr, const char* argDesc,
                            const char* function) :
     Exception() {
-    construct("Illegal argument detected",
-              ( std::string("`") + argDesc + "' is a bad argument"
-                + (*condStr == '\0' ? std::string() :
-                    ( std::string("; expected ") +
-                        condStr + " to hold" )) ).c_str(),
-              function);
+    construct(s_header, format_extra(condStr, argDesc).c_str(), function);
   }
+
+  /**
+   * This is a convenience function for building usages that are variadic.
+   *
+   * Having IllegalArgumentException itself be variadic is problematic for
+   * making sure calls to IllegalArgumentException clean up memory.
+   */
+  static std::string formatVariadic();
+  static std::string formatVariadic(const char* format, ...);
 };/* class IllegalArgumentException */
 
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
@@ -127,43 +120,22 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
   return os;
 }
 
-}/* CVC4 namespace */
-
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
-#  include "base/cvc4_assert.h"
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */
-
-namespace CVC4 {
-
-#ifndef CheckArgument
-template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
-template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
+template <class T> inline void CheckArgument(bool cond, const T& arg,
+                                             const char* tail) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg,
+                                             const char* tail) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
-template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg)
+  CVC4_PUBLIC;
 template <class T> inline void CheckArgument(bool cond, const T& arg) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
-#endif /* CheckArgument */
 
-#ifndef DebugCheckArgument
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
-  if(__builtin_expect( ( !cond ), false )) { \
-    throw ::CVC4::IllegalArgumentException("", "", ""); \
-  } \
-}
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
-template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
-  if(__builtin_expect( ( !cond ), false )) { \
-    throw ::CVC4::IllegalArgumentException("", "", ""); \
-  } \
-}
-#endif /* DebugCheckArgument */
 
 }/* CVC4 namespace */