Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out.

1 files changed, 12 insertions, 75 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index e9fdc69a8..3561f2119 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -22,88 +22,25 @@ namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
-Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
-  Assert(this != NULL, "Whoops, we have a bad expression manager!");
-  Assert(ev != NULL, "lookup() expects a non-NULL NodeValue!");
-
-  hash_t::iterator i = d_hash.find(hash);
-  if(i == d_hash.end()) {
-    // insert
-    std::vector<Node> v;
-    Node e(ev);
-    v.push_back(e);
-    d_hash.insert(std::make_pair(hash, v));
-    return e;
-  } else {
-    for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
-      if(ev->getKind() != j->getKind()) {
-        continue;
-      }
-
-      if(ev->getNumChildren() != j->getNumChildren()) {
-        continue;
-      }
-
-      NodeValue::const_ev_iterator c1 = ev->ev_begin();
-      NodeValue::ev_iterator c2 = j->d_ev->ev_begin();
-      for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
-        if(*c1 != *c2) {
-          break;
-        }
-      }
-
-      if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) {
-        continue;
-      }
-
-      return *j;
-    }
-
-    // didn't find it, insert
-    Node e(ev);
-    i->second.push_back(e);
-    return e;
-  }
+NodeManager::NodeManager() {
+  poolInsert(&NodeValue::s_null);
 }
 
-NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
-  Assert(this != NULL, "Whoops, we have a bad expression manager!");
-  Assert(ev != NULL, "lookupNoInsert() expects a non-NULL NodeValue!");
-
-  hash_t::iterator i = d_hash.find(hash);
-  if(i == d_hash.end()) {
+NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
+  NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
+  if (find == d_nodeValueSet.end()) {
     return NULL;
   } else {
-    for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) {
-      if(ev->getKind() != j->getKind()) {
-        continue;
-      }
-
-      if(ev->getNumChildren() != j->getNumChildren()) {
-        continue;
-      }
-
-      NodeValue::const_ev_iterator c1 = ev->ev_begin();
-      NodeValue::ev_iterator c2 = j->d_ev->ev_begin();
-      for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
-        Debug("expr") << "comparing " << c1 << " and " << c2 << std::endl;
-        if(*c1 != *c2) {
-          break;
-        }
-      }
-
-      if(c1 != ev->ev_end() || c2 != j->d_ev->ev_end()) {
-        continue;
-      }
-
-      return j->d_ev;
-    }
-
-    // didn't find it, don't insert
-    return 0;
+    return *find;
   }
 }
 
+void NodeManager::poolInsert(NodeValue* nv) {
+  Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in"
+         "the pool!");
+  d_nodeValueSet.insert(nv);
+}
+
 // general expression-builders
 
 Node NodeManager::mkNode(Kind kind) {