1 files changed, 1 insertions, 58 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 556b577e5..b11361827 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -13,11 +13,7 @@
  ** Expression manager implementation.
  **/
 
-#include "node_builder.h"
 #include "node_manager.h"
-#include "expr/node.h"
-#include "expr/attribute.h"
-#include "util/output.h"
 
 using namespace std;
 using namespace CVC4::expr;
@@ -28,64 +24,11 @@ __thread NodeManager* NodeManager::s_current = 0;
 
 NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
   NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
-  if (find == d_nodeValueSet.end()) {
+  if(find == d_nodeValueSet.end()) {
     return NULL;
   } else {
     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) {
-  return NodeBuilder<>(this, kind);
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1) {
-  return NodeBuilder<>(this, kind) << child1;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
-  return NodeBuilder<>(this, kind) << child1 << child2;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3;
-}
-
-Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
-  return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
-}
-
-Node NodeManager::mkNode(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;
-}
-
-// N-ary version
-Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
-  return NodeBuilder<>(this, kind).append(children);
-}
-
-Node NodeManager::mkVar(const Type* type, const std::string& name) {
-  Node n = mkVar(type);
-  n.setAttribute(VarNameAttr(), name);
-  return n;
-}
-
-Node NodeManager::mkVar(const Type* type) {
-  Node n = NodeBuilder<>(this, VARIABLE);
-  n.setAttribute(TypeAttr(), type);
-  return n;
-}
-
-Node NodeManager::mkVar() {
-  return NodeBuilder<>(this, VARIABLE);
-}
-
 }/* CVC4 namespace */