1 files changed, 58 insertions, 18 deletions

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8da87c9eb..ab52b9f40 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr_manager.cpp
+/** node_manager.cpp
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -18,76 +18,116 @@ namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
-Node NodeManager::lookup(uint64_t hash, const Node& e) {
-  Assert(this != NULL, "Woops, we have a bad expression manager!");
+Node NodeManager::lookup(uint64_t hash, NodeValue* ev) {
+  Assert(this != NULL, "Whoops, we have a bad expression manager!");
   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(e.getKind() != j->getKind())
+      if(ev->getKind() != j->getKind()) {
         continue;
+      }
 
-      if(e.numChildren() != j->numChildren())
+      if(ev->numChildren() != j->numChildren()) {
         continue;
+      }
 
-      Node::const_iterator c1 = e.begin();
-      Node::iterator c2 = j->begin();
-      for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
-        if(c1->d_ev != c2->d_ev)
+      NodeValue::const_iterator c1 = ev->ev_begin();
+      NodeValue::iterator c2 = j->d_ev->ev_begin();
+      for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
+        if((*c1).d_ev != (*c2).d_ev) {
           break;
+        }
       }
 
-      if(c1 != e.end() || c2 != j->end())
+      if(c1 != ev->ev_end() || c2 != j->end()) {
         continue;
+      }
 
       return *j;
     }
     // didn't find it, insert
     std::vector<Node> v;
+    Node e(ev);
     v.push_back(e);
     d_hash.insert(std::make_pair(hash, v));
     return e;
   }
 }
 
+NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) {
+  Assert(this != NULL, "Whoops, we have a bad expression manager!");
+  hash_t::iterator i = d_hash.find(hash);
+  if(i == d_hash.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->numChildren() != j->numChildren()) {
+        continue;
+      }
+
+      NodeValue::const_iterator c1 = ev->ev_begin();
+      NodeValue::iterator c2 = j->d_ev->ev_begin();
+      for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) {
+        if((*c1).d_ev != (*c2).d_ev) {
+          break;
+        }
+      }
+
+      if(c1 != ev->ev_end() || c2 != j->end()) {
+        continue;
+      }
+
+      return j->d_ev;
+    }
+    // didn't find it
+    return 0;
+  }
+}
+
 // general expression-builders
 
 Node NodeManager::mkExpr(Kind kind) {
-  return NodeBuilder(this, kind);
+  return NodeBuilder<>(this, kind);
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1) {
-  return NodeBuilder(this, kind) << child1;
+  return NodeBuilder<>(this, kind) << child1;
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
-  return NodeBuilder(this, kind) << child1 << child2;
+  return NodeBuilder<>(this, kind) << child1 << child2;
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
-  return NodeBuilder(this, kind) << child1 << child2 << child3;
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3;
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
-  return NodeBuilder(this, kind) << child1 << child2 << child3 << child4;
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
 }
 
 Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
-  return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
+  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
 }
 
 // N-ary version
 Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
-  return NodeBuilder(this, kind).append(children);
+  return NodeBuilder<>(this, kind).append(children);
 }
 
 Node NodeManager::mkVar() {
-  return NodeBuilder(this, VARIABLE);
+  return NodeBuilder<>(this, VARIABLE);
 }
 
 }/* CVC4 namespace */