* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"

  (etc.) now work for Nodes a, b, c, d, e.  Also refcounting fixes for
  NodeBuilder in certain cases

* (various places) don't overload __gnu_cxx::hash<>, instead provide
  an explicit hash function to hash_maps and hash_sets.

* add a new kind of assert, DtorAssert(), which doesn't throw
  exceptions (right now it operates like a usual C assert()).  For use
  in destructors.

* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).

* fix some Make rule dependencies

* reformat node.h as per code formatting policy

* added Theory and NodeBuilder unit tests

1 files changed, 8 insertions, 14 deletions

diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h
index bfa38ec28..5838790a8 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -23,18 +23,15 @@
 
 #include <ext/hash_map>
 
-namespace __gnu_cxx {
-template<>
-  struct hash<std::string> {
-    size_t operator()(const std::string& str) const {
-      return hash<const char*>()(str.c_str());
-    }
-  };
-}/* __gnu_cxx namespace */
-
 namespace CVC4 {
 namespace parser {
 
+struct StringHashFcn {
+  size_t operator()(const std::string& str) const {
+    return __gnu_cxx::hash<const char*>()(str.c_str());
+  }
+};
+
 /**
  * Generic symbol table for looking up variables by name.
  */
@@ -44,12 +41,9 @@ class SymbolTable {
 private:
 
   /** The name to expression bindings */
-  typedef __gnu_cxx::hash_map<std::string, ObjectType>
+  typedef __gnu_cxx::hash_map<std::string, ObjectType, StringHashFcn>
   LookupTable;
-/*
-  typedef __gnu_cxx::hash_map<std::string, std::stack<ObjectType> >
-  LookupTable;
-*/
+
   /** The table iterator */
   typedef typename LookupTable::iterator table_iterator;
   /** The table iterator */