1 files changed, 22 insertions, 19 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index be9ac995c..1a549973f 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,5 +1,5 @@
 /*********************                                           -*- C++ -*-  */
-/** expr.cpp
+/** node.cpp
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
@@ -11,7 +11,7 @@
  **/
 
 #include "expr/node.h"
-#include "expr/expr_value.h"
+#include "expr/node_value.h"
 #include "expr/node_builder.h"
 #include "util/Assert.h"
 
@@ -22,26 +22,29 @@ using namespace std;
 
 namespace CVC4 {
 
-ExprValue ExprValue::s_null;
+NodeValue NodeValue::s_null;
 
-Node Node::s_null(&ExprValue::s_null);
+Node Node::s_null(&NodeValue::s_null);
 
 Node Node::null() {
   return s_null;
 }
 
-
 bool Node::isNull() const {
-  return d_ev == &ExprValue::s_null;
+  return d_ev == &NodeValue::s_null;
 }
 
 Node::Node() :
-  d_ev(&ExprValue::s_null) {
+  d_ev(&NodeValue::s_null) {
   // No refcount needed
 }
 
-Node::Node(ExprValue* ev)
-  : d_ev(ev) {
+// FIXME: escape from type system convenient but is there a better
+// way?  Nodes conceptually don't change their expr values but of
+// course they do modify the refcount.  But it's nice to be able to
+// support node_iterators over const NodeValue*.  So.... hm.
+Node::Node(const NodeValue* ev)
+  : d_ev(const_cast<NodeValue*>(ev)) {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
   d_ev->inc();
 }
@@ -57,7 +60,7 @@ Node::~Node() {
   d_ev->dec();
 }
 
-void Node::assignExprValue(ExprValue* ev) {
+void Node::assignNodeValue(NodeValue* ev) {
   d_ev = ev;
   d_ev->inc();
 }
@@ -72,7 +75,7 @@ Node& Node::operator=(const Node& e) {
   return *this;
 }
 
-ExprValue const* Node::operator->() const {
+NodeValue const* Node::operator->() const {
   Assert(d_ev != NULL, "Expecting a non-NULL expression value!");
   return d_ev;
 }
@@ -83,35 +86,35 @@ uint64_t Node::hash() const {
 }
 
 Node Node::eqExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(EQUAL, *this, right);
+  return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
 }
 
 Node Node::notExpr() const {
-  return NodeManager::currentEM()->mkExpr(NOT, *this);
+  return NodeManager::currentNM()->mkExpr(NOT, *this);
 }
 
 Node Node::andExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(AND, *this, right);
+  return NodeManager::currentNM()->mkExpr(AND, *this, right);
 }
 
 Node Node::orExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(OR, *this, right);
+  return NodeManager::currentNM()->mkExpr(OR, *this, right);
 }
 
 Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
-  return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
+  return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
 }
 
 Node Node::iffExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(IFF, *this, right);
+  return NodeManager::currentNM()->mkExpr(IFF, *this, right);
 }
 
 Node Node::impExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right);
+  return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
 }
 
 Node Node::xorExpr(const Node& right) const {
-  return NodeManager::currentEM()->mkExpr(XOR, *this, right);
+  return NodeManager::currentNM()->mkExpr(XOR, *this, right);
 }
 
 }/* CVC4 namespace */