diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 15:15:53 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-12 15:15:53 +0000 |
commit | e67d573de13e4421036d7de9559d8ace39571492 (patch) | |
tree | f6f02f51b829f77e65c022e80884c87f68c01b64 /src/expr/declaration_scope.h | |
parent | 46e4487c37628217ec64a2b325b287acfb0ae8c5 (diff) |
Adding class Smt2 to handle declaration of logic and theory symbols
Diffstat (limited to 'src/expr/declaration_scope.h')
-rw-r--r-- | src/expr/declaration_scope.h | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 7d0f2b787..e33aa25fa 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -15,6 +15,7 @@ #define DECLARATION_SCOPE_H_ #include "expr.h" +#include "util/hash.h" #include <ext/hash_map> @@ -31,15 +32,6 @@ class CDMap; } //namespace context -/** A basic hash function for std::string - * TODO: Does this belong somewhere else (like util/)? - */ -struct StringHashFunction { - size_t operator()(const std::string& str) const { - return __gnu_cxx::hash<const char*>()(str.c_str()); - } -}; - class CVC4_PUBLIC ScopeException : public Exception { }; |