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, 13 insertions, 12 deletions

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 3d53f2e44..c0a80b7ce 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -17,17 +17,18 @@
  **/
 
 #include "expr/symbol_table.h"
-#include "expr/expr.h"
-#include "expr/type.h"
-#include "expr/expr_manager_scope.h"
+
+#include <string>
+#include <utility>
+
 #include "context/cdhashmap.h"
 #include "context/cdhashset.h"
 #include "context/context.h"
+#include "expr/expr.h"
+#include "expr/expr_manager_scope.h"
+#include "expr/type.h"
 
-#include <string>
-#include <utility>
 
-using namespace CVC4;
 using namespace CVC4::context;
 using namespace std;
 
@@ -49,7 +50,7 @@ SymbolTable::~SymbolTable() {
 
 void SymbolTable::bind(const std::string& name, Expr obj,
                        bool levelZero) throw() {
-  CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+  PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj);
   else d_exprMap->insert(name, obj);
@@ -57,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj,
 
 void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj,
                                       bool levelZero) throw() {
-  CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
+  PrettyCheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr");
   ExprManagerScope ems(obj);
   if(levelZero){
     d_exprMap->insertAtContextLevelZero(name, obj);
@@ -121,7 +122,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() {
 
 Type SymbolTable::lookupType(const std::string& name) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
-  CheckArgument(p.first.size() == 0, name,
+  PrettyCheckArgument(p.first.size() == 0, name,
                 "type constructor arity is wrong: "
                 "`%s' requires %u parameters but was provided 0",
                 name.c_str(), p.first.size());
@@ -131,12 +132,12 @@ Type SymbolTable::lookupType(const std::string& name) const throw() {
 Type SymbolTable::lookupType(const std::string& name,
                              const std::vector<Type>& params) const throw() {
   pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
-  CheckArgument(p.first.size() == params.size(), params,
+  PrettyCheckArgument(p.first.size() == params.size(), params,
                 "type constructor arity is wrong: "
                 "`%s' requires %u parameters but was provided %u",
          name.c_str(), p.first.size(), params.size());
   if(p.first.size() == 0) {
-    CheckArgument(p.second.isSort(), name);
+    PrettyCheckArgument(p.second.isSort(), name.c_str());
     return p.second;
   }
   if(p.second.isSortConstructor()) {
@@ -161,7 +162,7 @@ Type SymbolTable::lookupType(const std::string& name,
 
     return instantiation;
   } else if(p.second.isDatatype()) {
-    CheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
+    PrettyCheckArgument(DatatypeType(p.second).isParametric(), name, "expected parametric datatype");
     return DatatypeType(p.second).instantiate(params);
   } else {
     if(Debug.isOn("sort")) {