Extracted the public Expr and ExprManager interface to encapsulate the optimized expressions and the internal expression manager.

15 files changed, 625 insertions, 47 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 6ca68d35c..b8606e051 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -9,11 +9,16 @@ libexpr_la_SOURCES = \
 	attr_var_name.h \
 	node.h \
 	node_builder.h \
+	expr.h \
 	expr_value.h \
 	node_manager.h \
+	expr_manager.h \
 	node_attribute.h \
 	kind.h \
 	node.cpp \
 	node_builder.cpp \
 	node_manager.cpp \
-	expr_value.cpp
+	expr_manager.cpp \
+	expr_value.cpp \
+	expr.cpp
+
diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in
index a668e8876..6b1555e6c 100644
--- a/src/expr/Makefile.in
+++ b/src/expr/Makefile.in
@@ -53,7 +53,7 @@ CONFIG_CLEAN_VPATH_FILES =
 LTLIBRARIES = $(noinst_LTLIBRARIES)
 libexpr_la_LIBADD =
 am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \
-	expr_value.lo
+	expr_manager.lo expr_value.lo expr.lo
 libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS)
 DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
 depcomp = $(SHELL) $(top_srcdir)/config/depcomp
@@ -225,14 +225,18 @@ libexpr_la_SOURCES = \
 	attr_var_name.h \
 	node.h \
 	node_builder.h \
+	expr.h \
 	expr_value.h \
 	node_manager.h \
+	expr_manager.h \
 	node_attribute.h \
 	kind.h \
 	node.cpp \
 	node_builder.cpp \
 	node_manager.cpp \
-	expr_value.cpp
+	expr_manager.cpp \
+	expr_value.cpp \
+	expr.cpp
 
 all: all-am
 
@@ -286,6 +290,8 @@ mostlyclean-compile:
 distclean-compile:
 	-rm -f *.tab.c
 
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@
+@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@
 @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
new file mode 100644
index 000000000..af685aced
--- /dev/null
+++ b/src/expr/expr.cpp
@@ -0,0 +1,154 @@
+/*
+ * expr.cpp
+ *
+ *  Created on: Dec 10, 2009
+ *      Author: dejan
+ */
+
+#include "expr/expr.h"
+#include "expr/node.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const Expr& e) {
+  e.toStream(out);
+  return out;
+}
+
+Expr::Expr() :
+  d_node(new Node()), d_em(NULL) {
+}
+
+Expr::Expr(ExprManager* em, Node* node) :
+  d_node(node), d_em(em) {
+}
+
+Expr::Expr(const Expr& e) :
+  d_node(new Node(*e.d_node)), d_em(e.d_em) {
+}
+
+ExprManager* Expr::getExprManager() const {
+  return d_em;
+}
+
+Expr::~Expr() {
+  delete d_node;
+}
+
+Expr& Expr::operator=(const Expr& e) {
+  if(this != &e) {
+    delete d_node;
+    d_node = new Node(*e.d_node);
+    d_em = e.d_em;
+  }
+  return *this;
+}
+
+bool Expr::operator==(const Expr& e) const {
+  if(d_em != e.d_em)
+    return false;Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  return *d_node == *e.d_node;
+}
+
+bool Expr::operator!=(const Expr& e) const {
+  return !(*this == e);
+}
+
+bool Expr::operator<(const Expr& e) const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");Assert(e.d_node != NULL, "Unexpected NULL expression pointer!");
+  if(d_em != e.d_em)
+    return false;
+  return *d_node < *e.d_node;
+}
+
+uint64_t Expr::hash() const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return (d_node->isNull());
+}
+
+Kind Expr::getKind() const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->getKind();
+}
+
+size_t Expr::numChildren() const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->numChildren();
+}
+
+std::string Expr::toString() const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->toString();
+}
+
+bool Expr::isNull() const {
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->isNull();
+}
+
+void Expr::toStream(std::ostream& out) const {
+  d_node->toStream(out);
+}
+
+Node Expr::getNode() const {
+  return *d_node;
+}
+
+BoolExpr::BoolExpr() {
+}
+
+BoolExpr::BoolExpr(const Expr& e) :
+  Expr(e) {
+}
+
+BoolExpr BoolExpr::notExpr() const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  return d_em->mkExpr(NOT, *this);
+}
+
+BoolExpr BoolExpr::andExpr(const BoolExpr& e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == e.d_em, "Different expression managers!");
+  return d_em->mkExpr(AND, *this, e);
+}
+
+BoolExpr BoolExpr::orExpr(const BoolExpr& e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == e.d_em, "Different expression managers!");
+  return d_em->mkExpr(OR, *this, e);
+}
+
+BoolExpr BoolExpr::xorExpr(const BoolExpr& e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == e.d_em, "Different expression managers!");
+  return d_em->mkExpr(XOR, *this, e);
+}
+
+BoolExpr BoolExpr::iffExpr(const BoolExpr& e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == e.d_em, "Different expression managers!");
+  return d_em->mkExpr(IFF, *this, e);
+}
+
+BoolExpr BoolExpr::impExpr(const BoolExpr& e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == e.d_em, "Different expression managers!");
+  return d_em->mkExpr(IMPLIES, *this, e);
+}
+
+BoolExpr BoolExpr::iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == then_e.d_em, "Different expression managers!");
+  Assert(d_em == else_e.d_em, "Different expression managers!");
+  return d_em->mkExpr(ITE, *this, then_e, else_e);
+}
+
+Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
+  Assert(d_em != NULL, "Don't have an expression manager for this expression!");
+  Assert(d_em == then_e.getExprManager(), "Different expression managers!");
+  Assert(d_em == else_e.getExprManager(), "Different expression managers!");
+  return d_em->mkExpr(ITE, *this, then_e, else_e);
+}
+
+} // End namespace CVC4
diff --git a/src/expr/expr.h b/src/expr/expr.h
new file mode 100644
index 000000000..dc1926ce7
--- /dev/null
+++ b/src/expr/expr.h
@@ -0,0 +1,233 @@
+/*
+ * expr.h
+ *
+ *  Created on: Dec 10, 2009
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__EXPR_H
+#define __CVC4__EXPR_H
+
+#include "cvc4_config.h"
+#include "expr/expr_manager.h"
+
+#include <string>
+#include <iostream>
+#include <stdint.h>
+
+namespace CVC4 {
+
+// The internal expression representation
+class Node;
+
+/**
+ * Class encapsulating CVC4 expressions and methods for constructing new
+ * expressions.
+ */
+class CVC4_PUBLIC Expr {
+
+public:
+
+  /** Default constructor, makes a null expression. */
+  Expr();
+
+  /**
+   * Copy constructor, makes a copy of a given expression
+   * @param the expression to copy
+   */
+  Expr(const Expr& e);
+
+  /** Destructor */
+  ~Expr();
+
+  /**
+   * Assignment operator, makes a copy of the given expression. If the
+   * expression managers of the two expressions differ, the expression of
+   * the given expression will be used.
+   * @param e the expression to assign
+   * @return the reference to this expression after assignment
+   */
+  Expr& operator=(const Expr& e);
+
+  /**
+   * Syntactic comparison operator. Returns true if expressions belong to the
+   * same expression manager and are syntactically identical.
+   * @param e the expression to compare to
+   * @return true if expressions are syntactically the same, false otherwise
+   */
+  bool operator==(const Expr& e) const;
+
+  /**
+   * Syntactic dis-equality operator.
+   * @param e the expression to compare to
+   * @return true if expressions differ syntactically, false otherwise
+   */
+  bool operator!=(const Expr& e) const;
+
+  /**
+   * Order comparison operator. The only invariant on the order of expressions
+   * is that the expressions that were created sooner will be smaller in the
+   * ordering than all the expressions created later. Null expression is the
+   * smallest element of the ordering. The behavior of the operator is
+   * undefined if the expressions come from two different expression managers.
+   * @param e the expression to compare to
+   * @return true if this expression is smaller than the given one
+   */
+  bool operator<(const Expr& e) const;
+
+  /**
+   * Returns the hash value of the expression. Equal expression will have the
+   * same hash value.
+   */
+  uint64_t hash() const;
+
+  /**
+   * Returns the kind of the expression (AND, PLUS ...).
+   * @return the kind of the expression
+   */
+  Kind getKind() const;
+
+  /**
+   * Returns the number of children of this expression.
+   * @return the number of children
+   */
+  size_t numChildren() const;
+
+  /**
+   * Returns the string representation of the expression.
+   */
+  std::string toString() const;
+
+  /**
+   * Outputs the string representation of the expression to the stream.
+   * @param the output stream
+   */
+  void toStream(std::ostream& out) const;
+
+  /**
+   * Check if this is a null expression.
+   * @return true if a null expression
+   */
+  bool isNull() const;
+
+  /**
+   * Returns the expression reponsible for this expression.
+   */
+  ExprManager* getExprManager() const;
+
+protected:
+
+  /**
+   * Constructor for internal purposes.
+   * @param em the expression manager that handles this expression
+   * @param node the actuall expression node pointer
+   */
+  Expr(ExprManager* em, Node* node);
+
+  /** The internal expression representation */
+  Node* d_node;
+
+  /** The responsible expression manager */
+  ExprManager* d_em;
+
+  /**
+   * Returns the actual internal node.
+   * @return the internal node
+   */
+  Node getNode() const;
+
+  // Friend to access the actual internal node information and private methods*/
+  friend class SmtEngine;
+  friend class ExprManager;
+};
+
+/**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
+/**
+ * Extending the expression with the capability to construct Boolean
+ * expressions.
+ */
+class CVC4_PUBLIC BoolExpr : public Expr {
+
+public:
+
+  /** Default constructor, makes a null expression */
+  BoolExpr();
+
+  /**
+   * Convert an expression to a Boolean expression
+   */
+  BoolExpr(const Expr& e);
+
+  /**
+   * Negate this expression.
+   * @return the logical negation of this expression.
+   */
+  BoolExpr notExpr() const;
+
+  /**
+   * Conjunct the given expression to this expression.
+   * @param e the expression to conjunct
+   * @return the conjunction of this expression and e
+   */
+  BoolExpr andExpr(const BoolExpr& e) const;
+
+  /**
+   * Disjunct the given expression to this expression.
+   * @param e the expression to disjunct
+   * @return the disjunction of this expression and e
+   */
+  BoolExpr orExpr(const BoolExpr& e) const;
+
+  /**
+   * Make an exclusive or expression out of this expression and the given
+   * expression.
+   * @param e the right side of the xor
+   * @return the xor of this expression and e
+   */
+  BoolExpr xorExpr(const BoolExpr& e) const;
+
+  /**
+   * Make an equivalence expression out of this expression and the given
+   * expression.
+   * @param e the right side of the equivalence
+   * @return the equivalence expression
+   */
+  BoolExpr iffExpr(const BoolExpr& e) const;
+
+  /**
+   * Make an implication expression out of this expression and the given
+   * expression.
+   * @param e the right side of the equivalence
+   * @return the equivalence expression
+   */
+  BoolExpr impExpr(const BoolExpr& e) const;
+
+  /**
+   * Make a Boolean if-then-else expression using this expression as the
+   * condition, and given the then and else parts
+   * @param then_e the then branch expression
+   * @param else_e the else branch expression
+   * @return the if-then-else expression
+   */
+  BoolExpr iteExpr(const BoolExpr& then_e, const BoolExpr& else_e) const;
+
+  /**
+   * Make a term if-then-else expression using this expression as the
+   * condition, and given the then and else parts
+   * @param then_e the then branch expression
+   * @param else_e the else branch expression
+   * @return the if-then-else expression
+   */
+  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;
+};
+
+}
+
+#endif /* __CVC4__EXPR_H */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
new file mode 100644
index 000000000..877ba9d3c
--- /dev/null
+++ b/src/expr/expr_manager.cpp
@@ -0,0 +1,78 @@
+/*
+ * expr_manager.cpp
+ *
+ *  Created on: Dec 10, 2009
+ *      Author: dejan
+ */
+
+#include "expr/node.h"
+#include "expr/expr.h"
+#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+ExprManager::ExprManager()
+: d_nm(new NodeManager()) {
+}
+
+ExprManager::~ExprManager() {
+  delete d_nm;
+}
+
+Expr ExprManager::mkExpr(Kind kind) {
+  return Expr(this, new Node(d_nm->mkExpr(kind)));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
+  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
+  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+                                          child2.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+                         const Expr& child3) {
+  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+                                          child2.getNode(), child3.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+                         const Expr& child3, const Expr& child4) {
+  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+                                          child2.getNode(), child3.getNode(),
+                                          child4.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+                         const Expr& child3, const Expr& child4,
+                         const Expr& child5) {
+  return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+                                          child2.getNode(), child3.getNode(),
+                                          child5.getNode())));
+}
+
+Expr ExprManager::mkExpr(Kind kind, const vector<Expr>& children) {
+  vector<Node> nodes;
+  vector<Expr>::const_iterator it = children.begin();
+  vector<Expr>::const_iterator it_end = children.end();
+  while(it != it_end) {
+    nodes.push_back(it->getNode());
+    ++it;
+  }
+  return Expr(this, new Node(d_nm->mkExpr(kind, nodes)));
+}
+
+Expr ExprManager::mkVar() {
+  return Expr(this, new Node(d_nm->mkVar()));
+}
+
+NodeManager* ExprManager::getNodeManager() const {
+  return d_nm;
+}
+
+} // End namespace CVC4
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
new file mode 100644
index 000000000..4a7f359e9
--- /dev/null
+++ b/src/expr/expr_manager.h
@@ -0,0 +1,93 @@
+/*
+ * expr_manager.h
+ *
+ *  Created on: Dec 10, 2009
+ *      Author: dejan
+ */
+
+#ifndef __CVC4__EXPR_MANAGER_H
+#define __CVC4__EXPR_MANAGER_H
+
+#include "cvc4_config.h"
+#include "expr/kind.h"
+#include <vector>
+
+namespace CVC4 {
+
+class Expr;
+class NodeManager;
+class SmtEngine;
+
+class CVC4_PUBLIC ExprManager {
+
+public:
+
+  /**
+   * Creates an expressio manager.
+   */
+  ExprManager();
+
+  /**
+   * Destroys the expression manager. No will be deallocated at this point, so
+   * any expression references that used to be managed by this expression
+   * manager and are left-over are bad.
+   */
+  ~ExprManager();
+
+  /**
+   * Make a unary expression of a given kind (TRUE, FALSE,...).
+   * @param kind the kind of expression
+   * @return the expression
+   */
+  Expr mkExpr(Kind kind);
+
+  /**
+   * Make a unary expression of a given kind (NOT, BVNOT, ...).
+   * @param kind the kind of expression
+   * @return the expression
+   */
+  Expr mkExpr(Kind kind, const Expr& child1);
+
+  /**
+   * Make a ternary expression of a given kind (AND, PLUS, ...).
+   * @param kind the kind of expression
+   * @return the expression
+   */
+  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
+
+  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+              const Expr& child3);
+  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+              const Expr& child3, const Expr& child4);
+  Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
+              const Expr& child3, const Expr& child4, const Expr& child5);
+
+  /**
+   * Make an n-ary expression of given kind given a vector of it's children
+   * @param kind the kind of expression to build
+   * @param children the subexpressions
+   * @return the n-ary expression
+   */
+  Expr mkExpr(Kind kind, const std::vector<Expr>& children);
+
+  // variables are special, because duplicates are permitted
+  Expr mkVar();
+
+private:
+
+  /** The internal node manager */
+  NodeManager* d_nm;
+
+  /**
+   * Returns the internal node manager. This should only be used by internal
+   * users, i.e. the friend classes.
+   */
+  NodeManager* getNodeManager() const;
+
+  /** SmtEngine will use all the internals, so it will grab the node manager */
+  friend class SmtEngine;
+};
+
+}
+
+#endif /* __CVC4__EXPR_MANAGER_H */
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index 9ce7c3e12..af064f43d 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -15,6 +15,9 @@
  **/
 
 #include "expr_value.h"
+#include <sstream>
+
+using namespace std;
 
 namespace CVC4 {
 
@@ -77,7 +80,13 @@ ExprValue::const_iterator ExprValue::rend() const {
   return d_children - 1;
 }
 
-void ExprValue::toString(std::ostream& out) const {
+string ExprValue::toString() const {
+  stringstream ss;
+  toStream(ss);
+  return ss.str();
+}
+
+void ExprValue::toStream(std::ostream& out) const {
   out << "(" << Kind(d_kind);
   if(d_kind == VARIABLE) {
     out << ":" << this;
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 10f09e565..25fada4af 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -25,6 +25,8 @@
 #include <stdint.h>
 #include "kind.h"
 
+#include <string>
+
 namespace CVC4 {
 
 class Node;
@@ -112,7 +114,8 @@ public:
 
   unsigned getId() const { return d_id; }
   unsigned getKind() const { return (Kind) d_kind; }
-  void CVC4_PUBLIC toString(std::ostream& out) const;
+  std::string toString() const;
+  void toStream(std::ostream& out) const;
 };
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 22a905470..be9ac995c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -15,7 +15,10 @@
 #include "expr/node_builder.h"
 #include "util/Assert.h"
 
+#include <sstream>
+
 using namespace CVC4::expr;
+using namespace std;
 
 namespace CVC4 {
 
@@ -23,6 +26,11 @@ ExprValue ExprValue::s_null;
 
 Node Node::s_null(&ExprValue::s_null);
 
+Node Node::null() {
+  return s_null;
+}
+
+
 bool Node::isNull() const {
   return d_ev == &ExprValue::s_null;
 }
@@ -82,12 +90,6 @@ Node Node::notExpr() const {
   return NodeManager::currentEM()->mkExpr(NOT, *this);
 }
 
-// FIXME: What does this do and why?
-Node Node::negate() const { // avoid double-negatives
-  return NodeBuilder(*this).negate();
-}
-
-
 Node Node::andExpr(const Node& right) const {
   return NodeManager::currentEM()->mkExpr(AND, *this, right);
 }
diff --git a/src/expr/node.h b/src/expr/node.h
index aec50000e..98847e428 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -10,10 +10,11 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
-#ifndef __CVC4__EXPR_H
-#define __CVC4__EXPR_H
+#ifndef __CVC4__NODE_H
+#define __CVC4__NODE_H
 
 #include <vector>
+#include <string>
 #include <iostream>
 #include <stdint.h>
 
@@ -26,7 +27,7 @@ namespace CVC4 {
 
 namespace CVC4 {
 
-inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Node&);
 
 class NodeManager;
 
@@ -40,7 +41,7 @@ using CVC4::expr::ExprValue;
  * Encapsulation of an ExprValue pointer.  The reference count is
  * maintained in the ExprValue.
  */
-class CVC4_PUBLIC Node {
+class Node {
 
   friend class ExprValue;
 
@@ -99,7 +100,6 @@ public:
 
   Node eqExpr(const Node& right) const;
   Node notExpr() const;
-  Node negate() const; // avoid double-negatives
   Node andExpr(const Node& right) const;
   Node orExpr(const Node& right) const;
   Node iteExpr(const Node& thenpart, const Node& elsepart) const;
@@ -115,7 +115,7 @@ public:
 
   inline size_t numChildren() const;
 
-  static Node null() { return s_null; }
+  static Node null();
 
   typedef Node* iterator;
   typedef Node const* const_iterator;
@@ -125,7 +125,8 @@ public:
   inline const_iterator begin() const;
   inline const_iterator end() const;
 
-  void toString(std::ostream&) const;
+  inline std::string toString() const;
+  inline void toStream(std::ostream&) const;
 
   bool isNull() const;
 
@@ -142,7 +143,7 @@ inline bool Node::operator<(const Node& e) const {
 }
 
 inline std::ostream& operator<<(std::ostream& out, const Node& e) {
-  e.toString(out);
+  e.toStream(out);
   return out;
 }
 
@@ -150,10 +151,12 @@ inline Kind Node::getKind() const {
   return Kind(d_ev->d_kind);
 }
 
-inline void Node::toString(std::ostream& out) const {
-  if(d_ev)
-    d_ev->toString(out);
-  else out << "null";
+inline std::string Node::toString() const {
+  return d_ev->toString();
+}
+
+inline void Node::toStream(std::ostream& out) const {
+  d_ev->toStream(out);
 }
 
 inline Node::iterator Node::begin() {
@@ -178,4 +181,4 @@ inline size_t Node::numChildren() const {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__EXPR_H */
+#endif /* __CVC4__NODE_H */
diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h
index b978f097d..0b759efb4 100644
--- a/src/expr/node_attribute.h
+++ b/src/expr/node_attribute.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H
-#define __CVC4__EXPR__EXPR_ATTRIBUTE_H
+#ifndef __CVC4__EXPR__NODE_ATTRIBUTE_H
+#define __CVC4__EXPR__NODE_ATTRIBUTE_H
 
 #include <stdint.h>
 #include "config.h"
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
index 83d2ae41d..7d30ff4e3 100644
--- a/src/expr/node_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -104,15 +104,6 @@ NodeBuilder& NodeBuilder::notExpr() {
   return *this;
 }
 
-// avoid double-negatives
-NodeBuilder& NodeBuilder::negate() {
-  if(EXPECT_FALSE( d_kind == NOT ))
-    return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND );
-  collapse();
-  d_kind = NOT;
-  return *this;
-}
-
 NodeBuilder& NodeBuilder::andExpr(const Node& right) {
   Assert( d_kind != UNDEFINED_KIND );
   if(d_kind != AND) {
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index be96c2e77..5be3c284d 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4__EXPR_BUILDER_H
-#define __CVC4__EXPR_BUILDER_H
+#ifndef __CVC4__NODE_BUILDER_H
+#define __CVC4__NODE_BUILDER_H
 
 #include <vector>
 #include <cstdlib>
@@ -78,7 +78,6 @@ public:
   // Compound expression constructors
   NodeBuilder& eqExpr(const Node& right);
   NodeBuilder& notExpr();
-  NodeBuilder& negate(); // avoid double-negatives
   NodeBuilder& andExpr(const Node& right);
   NodeBuilder& orExpr(const Node& right);
   NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart);
@@ -209,7 +208,9 @@ inline NodeBuilder::operator Node() {
   // variables are permitted to be duplicates (from POV of the expression manager)
   if(d_kind == VARIABLE) {
     ev = new ExprValue;
-    hash = reinterpret_cast<uint64_t>(ev);
+    ev->d_kind = d_kind;
+    ev->d_id = ExprValue::next_id++;// FIXME multithreading
+    return Node(ev);
   } else {
     if(d_nchildren <= nchild_thresh) {
       hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end());
@@ -220,7 +221,7 @@ inline NodeBuilder::operator Node() {
       ev_iterator i_end = ev_end();
       for(; i != i_end; ++i) {
         // The expressions in the allocated children are all 0, so we must
-        // construct it withouth using an assignment operator
+        // construct it without using an assignment operator
         ev->d_children[nc++].assignExprValue(*i);
       }
     } else {
@@ -286,7 +287,7 @@ inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) {
 }
 
 inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) {
-  d_eb.append(e.negate());
+  d_eb.append(e.uMinusExpr());
   return *this;
 }
 
@@ -310,4 +311,4 @@ inline MultExprBuilder& MultExprBuilder::operator*(Node e) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__EXPR_BUILDER_H */
+#endif /* __CVC4__NODE_BUILDER_H */
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3c15aa9c4..8da87c9eb 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -82,7 +82,7 @@ Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, cons
 }
 
 // N-ary version
-Node NodeManager::mkExpr(Kind kind, std::vector<Node> children) {
+Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
   return NodeBuilder(this, kind).append(children);
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ca15d88b4..6c20b29e8 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -9,8 +9,8 @@
  **
  **/
 
-#ifndef __CVC4__EXPR_MANAGER_H
-#define __CVC4__EXPR_MANAGER_H
+#ifndef __CVC4__NODE_MANAGER_H
+#define __CVC4__NODE_MANAGER_H
 
 #include <vector>
 #include <map>
@@ -24,7 +24,7 @@ namespace expr {
   class ExprBuilder;
 }/* CVC4::expr namespace */
 
-class CVC4_PUBLIC NodeManager {
+class NodeManager {
   static __thread NodeManager* s_current;
 
   friend class CVC4::NodeBuilder;
@@ -45,7 +45,7 @@ public:
   Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
   Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
   // N-ary version
-  Node mkExpr(Kind kind, std::vector<Node> children);
+  Node mkExpr(Kind kind, const std::vector<Node>& children);
 
   // variables are special, because duplicates are permitted
   Node mkVar();