1 files changed, 18 insertions, 5 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3561f2119..12a6d1732 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -16,16 +16,16 @@
 #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;
+
 namespace CVC4 {
 
 __thread NodeManager* NodeManager::s_current = 0;
 
-NodeManager::NodeManager() {
-  poolInsert(&NodeValue::s_null);
-}
-
 NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
   NodeValueSet::const_iterator find = d_nodeValueSet.find(nv);
   if (find == d_nodeValueSet.end()) {
@@ -68,10 +68,23 @@ Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, cons
 }
 
 // N-ary version
-Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
+Node NodeManager::mkNode(Kind kind, const vector<Node>& children) {
   return NodeBuilder<>(this, kind).append(children);
 }
 
+Node NodeManager::mkVar(const Type* type, string name) {
+  Node n = NodeBuilder<>(this, VARIABLE);
+  n.setAttribute(TypeAttr(), 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);
 }