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/symbol_table.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/symbol_table.cpp')
-rw-r--r-- | src/expr/symbol_table.cpp | 25 |
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")) { |