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

30 files changed, 798 insertions, 204 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();
diff --git a/src/main/main.cpp b/src/main/main.cpp
index c7e23aee2..d9d3988f1 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -22,7 +22,7 @@
 #include "parser/parser.h"
 #include "parser/smt/smt_parser.h"
 #include "parser/cvc/cvc_parser.h"
-#include "expr/node_manager.h"
+#include "expr/expr_manager.h"
 #include "smt/smt_engine.h"
 #include "util/command.h"
 #include "util/output.h"
@@ -53,7 +53,7 @@ int main(int argc, char *argv[]) {
       throw new Exception("Too many input files specified.");
 
     // Create the expression manager
-    NodeManager exprMgr;
+    ExprManager exprMgr;
 
     // Create the SmtEngine
     SmtEngine smt(&exprMgr, &options);
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index d81336b53..a50b1f18f 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -65,29 +65,29 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
   antlr::LLkParser(lexer, k) {
 }
 
-Node AntlrParser::getVariable(std::string var_name) {
-  Node e = d_var_symbol_table.getObject(var_name);
+Expr AntlrParser::getVariable(std::string var_name) {
+  Expr e = d_var_symbol_table.getObject(var_name);
   Debug("parser") << "getvar " << var_name << " gives " << e << endl;
   return e;
 }
 
-Node AntlrParser::getTrueExpr() const {
+Expr AntlrParser::getTrueExpr() const {
   return d_expr_manager->mkExpr(TRUE);
 }
 
-Node AntlrParser::getFalseExpr() const {
+Expr AntlrParser::getFalseExpr() const {
   return d_expr_manager->mkExpr(FALSE);
 }
 
-Node AntlrParser::newExpression(Kind kind, const Node& child) {
+Expr AntlrParser::newExpression(Kind kind, const Expr& child) {
   return d_expr_manager->mkExpr(kind, child);
 }
 
-Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) {
+Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) {
   return d_expr_manager->mkExpr(kind, child_1, child_2);
 }
 
-Node AntlrParser::newExpression(Kind kind, const std::vector<Node>& children) {
+Expr AntlrParser::newExpression(Kind kind, const std::vector<Expr>& children) {
   return d_expr_manager->mkExpr(kind, children);
 }
 
@@ -112,7 +112,7 @@ void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) {
 void AntlrParser::addExtraSorts(const std::vector<std::string>& extra_sorts) {
 }
 
-void AntlrParser::setExpressionManager(NodeManager* em) {
+void AntlrParser::setExpressionManager(ExprManager* em) {
   d_expr_manager = em;
 }
 
@@ -132,7 +132,7 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message)
                                  LT(0).get()->getColumn());
 }
 
-Node AntlrParser::createPrecedenceExpr(const vector<Node>& exprs, const vector<
+Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector<
     Kind>& kinds) {
   return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1);
 }
@@ -154,7 +154,7 @@ unsigned AntlrParser::findPivot(const std::vector<Kind>& kinds,
   return pivot;
 }
 
-Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs,
+Expr AntlrParser::createPrecedenceExpr(const std::vector<Expr>& exprs,
                                        const std::vector<Kind>& kinds,
                                        unsigned start_index, unsigned end_index) {
   if(start_index == end_index)
@@ -162,8 +162,8 @@ Node AntlrParser::createPrecedenceExpr(const std::vector<Node>& exprs,
 
   unsigned pivot = findPivot(kinds, start_index, end_index - 1);
 
-  Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
-  Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
+  Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot);
+  Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index);
   return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2);
 }
 
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 26f206e43..ad23d45f8 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -15,8 +15,8 @@
 #include <antlr/LLkParser.hpp>
 #include <antlr/SemanticException.hpp>
 
-#include "expr/node.h"
-#include "expr/node_manager.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "util/command.h"
 #include "util/Assert.h"
 #include "parser/symbol_table.h"
@@ -48,7 +48,7 @@ public:
    * Set's the expression manager to use when creating/managing expression.
    * @param expr_manager the expression manager
    */
-  void setExpressionManager(NodeManager* expr_manager);
+  void setExpressionManager(ExprManager* expr_manager);
 
 protected:
 
@@ -89,7 +89,7 @@ protected:
    * @param var_name the name of the variable
    * @return the variable expression
    */
-  Node getVariable(std::string var_name);
+  Expr getVariable(std::string var_name);
 
   /**
    * Types of symbols.
@@ -113,40 +113,40 @@ protected:
    * Returns the true expression.
    * @return the true expression
    */
-  Node getTrueExpr() const;
+  Expr getTrueExpr() const;
 
   /**
    * Returns the false expression.
    * @return the false expression
    */
-  Node getFalseExpr() const;
+  Expr getFalseExpr() const;
 
   /**
    * Creates a new unary CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param child the child
    */
-  Node newExpression(Kind kind, const Node& child);
+  Expr newExpression(Kind kind, const Expr& child);
 
   /**
    * Creates a new binary CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param children the children of the expression
    */
-  Node newExpression(Kind kind, const Node& child_1, const Node& child_2);
+  Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2);
 
   /**
    * Creates a new CVC4 expression using the expression manager.
    * @param kind the kind of the expression
    * @param children the children of the expression
    */
-  Node newExpression(Kind kind, const std::vector<Node>& children);
+  Expr newExpression(Kind kind, const std::vector<Expr>& children);
 
   /**
    * Creates a new expression based on the given string of expressions and kinds.
    * The expression is created so that it respects the kinds precedence table.
    */
-  Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds);
+  Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds);
 
   /**
    * Creates a new predicated over the given sorts.
@@ -193,16 +193,16 @@ private:
    * Creates a new expression based on the given string of expressions and kinds.
    * The expression is created so that it respects the kinds precedence table.
    */
-  Node createPrecedenceExpr(const std::vector<Node>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
+  Expr createPrecedenceExpr(const std::vector<Expr>& exprs, const std::vector<Kind>& kinds, unsigned start_index, unsigned end_index);
 
   /** The status of the benchmark */
   BenchmarkStatus d_benchmark_status;
 
   /** The expression manager */
-  NodeManager* d_expr_manager;
+  ExprManager* d_expr_manager;
 
   /** The symbol table lookup */
-  SymbolTable<Node> d_var_symbol_table;
+  SymbolTable<Expr> d_var_symbol_table;
 };
 
 std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status);
diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp
index 2bb01007a..adeb5761d 100644
--- a/src/parser/cvc/cvc_parser.cpp
+++ b/src/parser/cvc/cvc_parser.cpp
@@ -44,8 +44,8 @@ Command* CvcParser::parseNextCommand() throw(ParserException) {
   return cmd;
 }
 
-Node CvcParser::parseNextExpression() throw(ParserException) {
-  Node result;
+Expr CvcParser::parseNextExpression() throw(ParserException) {
+  Expr result;
   if(!done()) {
     try {
       result = d_antlr_parser->formula();
@@ -62,7 +62,7 @@ CvcParser::~CvcParser() {
   delete d_antlr_lexer;
 }
 
-CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) :
+CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) :
   Parser(em), d_input(input) {
   if(!d_input) {
     throw ParserException(string("Read error") +
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 812925b0b..625f2c381 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -34,7 +34,7 @@ options {
  */
 command returns [CVC4::Command* cmd = 0]
 {
-  Node f;
+  Expr f;
   vector<string> ids;
 }
   : ASSERT   f = formula  { cmd = new AssertCommand(f);   }
@@ -60,15 +60,15 @@ type
   : BOOLEAN
   ;
 
-formula returns [CVC4::Node formula]
+formula returns [CVC4::Expr formula]
   :  formula = bool_formula
   ;
 
-bool_formula returns [CVC4::Node formula] 
+bool_formula returns [CVC4::Expr formula] 
 {
-  vector<Node> formulas;
+  vector<Expr> formulas;
   vector<Kind> kinds;
-  Node f1, f2;
+  Expr f1, f2;
   Kind k;
 }
   : f1 = primary_bool_formula { formulas.push_back(f1); } 
@@ -79,7 +79,7 @@ bool_formula returns [CVC4::Node formula]
     }
   ;
   
-primary_bool_formula returns [CVC4::Node formula]
+primary_bool_formula returns [CVC4::Expr formula]
   : formula = bool_atom
   | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); }
   | LPAREN formula = bool_formula RPAREN
@@ -93,7 +93,7 @@ bool_operator returns [CVC4::Kind kind]
   | IFF      { kind = CVC4::IFF;     }
   ;
     
-bool_atom returns [CVC4::Node atom]
+bool_atom returns [CVC4::Expr atom]
 {
   string p;
 }
diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h
index 07699916f..9cb6b7594 100644
--- a/src/parser/cvc/cvc_parser.h
+++ b/src/parser/cvc/cvc_parser.h
@@ -37,7 +37,7 @@ public:
    * @param input the input stream to parse
    * @param file_name the name of the file (for diagnostic output)
    */
-  CvcParser(NodeManager* em, std::istream& input, const char* file_name = "");
+  CvcParser(ExprManager* em, std::istream& input, const char* file_name = "");
 
   /**
    * Destructor.
@@ -57,7 +57,7 @@ public:
    * Parses the next complete expression of the stream.
    * @return the expression parsed
    */
-  Node parseNextExpression() throw(ParserException);
+  Expr parseNextExpression() throw(ParserException);
 
 protected:
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index c6d5bcb5c..8d4af5ba1 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -28,7 +28,7 @@ using namespace std;
 namespace CVC4 {
 namespace parser {
 
-Parser::Parser(NodeManager* em) :
+Parser::Parser(ExprManager* em) :
   d_expr_manager(em), d_done(false) {
 }
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 7f63261c7..7755d65f0 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -22,9 +22,9 @@
 namespace CVC4 {
 
 // Forward declarations
-class Node;
+class Expr;
 class Command;
-class NodeManager;
+class ExprManager;
 
 namespace parser {
 
@@ -44,7 +44,7 @@ public:
    * Construct the parser that uses the given expression manager.
    * @param em the expression manager.
    */
-  Parser(NodeManager* em);
+  Parser(ExprManager* em);
 
   /**
    * Destructor.
@@ -60,7 +60,7 @@ public:
   /**
    * Parse the next expression of the stream
    */
-  virtual Node parseNextExpression() throw (ParserException) = 0;
+  virtual Expr parseNextExpression() throw (ParserException) = 0;
 
   /**
    * Check if we are done -- either the end of input has been reached.
@@ -73,7 +73,7 @@ protected:
   void setDone(bool done = true);
 
   /** Expression manager the parser will be using */
-  NodeManager* d_expr_manager;
+  ExprManager* d_expr_manager;
 
   /** Are we done */
   bool d_done;
diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp
index 411866540..65d36690c 100644
--- a/src/parser/smt/smt_parser.cpp
+++ b/src/parser/smt/smt_parser.cpp
@@ -41,8 +41,8 @@ Command* SmtParser::parseNextCommand() throw(ParserException) {
   return cmd;
 }
 
-Node SmtParser::parseNextExpression() throw(ParserException) {
-  Node result;
+Expr SmtParser::parseNextExpression() throw(ParserException) {
+  Expr result;
   if(!done()) {
     try {
       result = d_antlr_parser->an_formula();
@@ -59,7 +59,7 @@ SmtParser::~SmtParser() {
   delete d_antlr_lexer;
 }
 
-SmtParser::SmtParser(NodeManager* em, istream& input, const char* file_name) :
+SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) :
   Parser(em), d_input(input) {
   if(!d_input) {
     throw ParserException(string("Read error") +
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index c2f5c145b..b1bb35e6f 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -60,7 +60,7 @@ pred_symb returns [std::string p]
 /**
  * Matches a propositional atom from the input. 
  */
-prop_atom returns [CVC4::Node atom]
+prop_atom returns [CVC4::Expr atom]
 {
   std::string p;
 } 
@@ -78,14 +78,14 @@ prop_atom returns [CVC4::Node atom]
  * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined
  * here in order to get rid of the ugly antlr non-determinism warrnings. 
  */
-an_atom returns [CVC4::Node atom] 
+an_atom returns [CVC4::Expr atom] 
   : atom = prop_atom  
   ;
   
 /**
  * Matches on of the unary Boolean conectives.  
  */
-connective returns [CVC4::Kind kind]
+bool_connective returns [CVC4::Kind kind]
   : NOT      { kind = CVC4::NOT;     } 
   | IMPLIES  { kind = CVC4::IMPLIES; }
   | AND      { kind = CVC4::AND;     }
@@ -97,18 +97,18 @@ connective returns [CVC4::Kind kind]
 /** 
  * Matches an annotated formula. 
  */
-an_formula returns [CVC4::Node formula] 
+an_formula returns [CVC4::Expr formula] 
 { 
   Kind kind; 
-  vector<Node> children;
+  vector<Expr> children;
 }
   :  formula = an_atom 
-  |  LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children);  }    
+  |  LPAREN kind = bool_connective an_formulas[children] RPAREN { formula = newExpression(kind, children);  }    
   ;
   
-an_formulas[std::vector<Node>& formulas]
+an_formulas[std::vector<Expr>& formulas]
 {
-  Node f;
+  Expr f;
 }
   : ( f = an_formula { formulas.push_back(f); } )+
   ;
@@ -149,7 +149,7 @@ status returns [ AntlrParser::BenchmarkStatus status ]
 bench_attribute returns [ Command* smt_command = 0]
 {
   BenchmarkStatus b_status = SMT_UNKNOWN;
-  Node formula;  
+  Expr formula;  
   vector<string> sorts;
 }
   : C_LOGIC       IDENTIFIER      
diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h
index 7dedcd5b4..a68f0e783 100644
--- a/src/parser/smt/smt_parser.h
+++ b/src/parser/smt/smt_parser.h
@@ -37,7 +37,7 @@ public:
    * @param input the input stream to parse
    * @param file_name the name of the file (for diagnostic output)
    */
-  SmtParser(NodeManager* em, std::istream& input, const char* file_name = "");
+  SmtParser(ExprManager* em, std::istream& input, const char* file_name = "");
 
   /**
    * Destructor.
@@ -57,7 +57,7 @@ public:
    * Parses the next complete expression of the stream.
    * @return the expression parsed
    */
-  Node parseNextExpression() throw(ParserException);
+  Expr parseNextExpression() throw(ParserException);
 
 protected:
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4ccdd07d0..723263177 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -15,24 +15,39 @@
 
 namespace CVC4 {
 
+SmtEngine::SmtEngine(ExprManager* em, Options* opts) throw() :
+    d_public_em(em),
+    d_em(em->getNodeManager()),
+    d_opts(opts),
+    d_de(),
+    d_te(),
+    d_prop(d_de, d_te) {
+  }
+
+SmtEngine::~SmtEngine() {
+
+}
+
 void SmtEngine::doCommand(Command* c) {
   c->invoke(this);
 }
 
-Node SmtEngine::preprocess(Node e) {
+Node SmtEngine::preprocess(const Node& e) {
   return e;
 }
 
-void SmtEngine::processAssertionList() {
+Node SmtEngine::processAssertionList() {
+  Node asserts;
   for(std::vector<Node>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i);
+    asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i);
+  return asserts;
 }
 
 Result SmtEngine::check() {
-  processAssertionList();
-  d_prop.solve(d_expr);
+  Node asserts = processAssertionList();
+  d_prop.solve(asserts);
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
@@ -41,25 +56,25 @@ Result SmtEngine::quickCheck() {
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
-void SmtEngine::addFormula(Node e) {
+void SmtEngine::addFormula(const Node& e) {
   d_assertions.push_back(e);
 }
 
-Result SmtEngine::checkSat(Node e) {
-  e = preprocess(e);
-  addFormula(e);
+Result SmtEngine::checkSat(const BoolExpr& e) {
+  Node node_e = preprocess(e.getNode());
+  addFormula(node_e);
   return check();
 }
 
-Result SmtEngine::query(Node e) {
-  e = preprocess(e);
-  addFormula(e);
+Result SmtEngine::query(const BoolExpr& e) {
+  Node node_e = preprocess(e.getNode());
+  addFormula(node_e);
   return check();
 }
 
-Result SmtEngine::assertFormula(Node e) {
-  e = preprocess(e);
-  addFormula(e);
+Result SmtEngine::assertFormula(const BoolExpr& e) {
+  Node node_e = preprocess(e.getNode());
+  addFormula(node_e);
   return quickCheck();
 }
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c4addc7dd..edcbdcca3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -16,7 +16,9 @@
 
 #include "cvc4_config.h"
 #include "expr/node.h"
+#include "expr/expr.h"
 #include "expr/node_manager.h"
+#include "expr/expr_manager.h"
 #include "util/result.h"
 #include "util/model.h"
 #include "util/options.h"
@@ -42,73 +44,19 @@ class Command;
 //
 // The CNF conversion can go on in PropEngine.
 
-class SmtEngine {
-  /** Current set of assertions. */
-  // TODO: make context-aware to handle user-level push/pop.
-  std::vector<Node> d_assertions;
-
-  /** Our expression manager */
-  NodeManager *d_em;
-
-  /** User-level options */
-  Options *d_opts;
-
-  /** Expression built-up for handing off to the propagation engine */
-  Node d_expr;
-
-  /** The decision engine */
-  DecisionEngine d_de;
-
-  /** The decision engine */
-  TheoryEngine d_te;
-
-  /** The propositional engine */
-  PropEngine d_prop;
-
-  /**
-   * Pre-process an Node.  This is expected to be highly-variable,
-   * with a lot of "source-level configurability" to add multiple
-   * passes over the Node.  TODO: may need to specify a LEVEL of
-   * preprocessing (certain contexts need more/less ?).
-   */
-  Node preprocess(Node);
+class CVC4_PUBLIC SmtEngine {
 
-  /**
-   * Adds a formula to the current context.
-   */
-  void addFormula(Node);
-
-  /**
-   * Full check of consistency in current context.  Returns true iff
-   * consistent.
-   */
-  Result check();
+public:
 
   /**
-   * Quick check of consistency in current context: calls
-   * processAssertionList() then look for inconsistency (based only on
-   * that).
+   * Construct an SmtEngine with the given expression manager and user options.
    */
-  Result quickCheck();
+  SmtEngine(ExprManager* em, Options* opts) throw();
 
   /**
-   * Process the assertion list: for literals and conjunctions of
-   * literals, assert to T-solver.
-   */
-  void processAssertionList();
-
-public:
-  /*
-   * Construct an SmtEngine with the given expression manager and user options.
+   * Destruct the smt engine.
    */
-  SmtEngine(NodeManager* em, Options* opts) throw() :
-    d_em(em),
-    d_opts(opts),
-    d_expr(Node::null()),
-    d_de(),
-    d_te(),
-    d_prop(d_de, d_te) {
-  }
+  ~SmtEngine();
 
   /**
    * Execute a command.
@@ -121,25 +69,25 @@ public:
    * literals and conjunction of literals.  Returns false iff
    * inconsistent.
    */
-  Result assertFormula(Node);
+  Result assertFormula(const BoolExpr& e);
 
   /**
    * Add a formula to the current context and call check().  Returns
    * true iff consistent.
    */
-  Result query(Node);
+  Result query(const BoolExpr& e);
 
   /**
    * Add a formula to the current context and call check().  Returns
    * true iff consistent.
    */
-  Result checkSat(Node);
+  Result checkSat(const BoolExpr& e);
 
   /**
    * Simplify a formula without doing "much" work.  Requires assist
    * from the SAT Engine.
    */
-  Node simplify(Node);
+  Expr simplify(const Expr& e);
 
   /**
    * Get a (counter)model (only if preceded by a SAT or INVALID query.
@@ -155,6 +103,64 @@ public:
    * Pop a user-level context.  Throws an exception if nothing to pop.
    */
   void pop();
+
+private:
+
+  /** Current set of assertions. */
+  // TODO: make context-aware to handle user-level push/pop.
+  std::vector<Node> d_assertions;
+
+  /** Our expression manager */
+  ExprManager *d_public_em;
+
+  /** Out internal expression/node manager */
+  NodeManager *d_em;
+
+  /** User-level options */
+  Options *d_opts;
+
+  /** The decision engine */
+  DecisionEngine d_de;
+
+  /** The decision engine */
+  TheoryEngine d_te;
+
+  /** The propositional engine */
+  PropEngine d_prop;
+
+  /**
+   * Pre-process an Node.  This is expected to be highly-variable,
+   * with a lot of "source-level configurability" to add multiple
+   * passes over the Node.  TODO: may need to specify a LEVEL of
+   * preprocessing (certain contexts need more/less ?).
+   */
+  Node preprocess(const Node& e);
+
+  /**
+   * Adds a formula to the current context.
+   */
+  void addFormula(const Node& e);
+
+  /**
+   * Full check of consistency in current context.  Returns true iff
+   * consistent.
+   */
+  Result check();
+
+  /**
+   * Quick check of consistency in current context: calls
+   * processAssertionList() then look for inconsistency (based only on
+   * that).
+   */
+  Result quickCheck();
+
+  /**
+   * Process the assertion list: for literals and conjunctions of
+   * literals, assert to T-solver.
+   */
+  Node processAssertionList();
+
+
 };/* class SmtEngine */
 
 }/* CVC4 namespace */
diff --git a/src/util/command.cpp b/src/util/command.cpp
index 0953a2ba2..3911897f5 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -5,10 +5,9 @@
  *      Author: dejan
  */
 
+#include <map>
 #include "util/command.h"
 #include "smt/smt_engine.h"
-#include "expr/node.h"
-#include "util/result.h"
 
 using namespace std;
 
@@ -26,7 +25,7 @@ EmptyCommand::EmptyCommand(string name) :
 void EmptyCommand::invoke(SmtEngine* smt_engine) {
 }
 
-AssertCommand::AssertCommand(const Node& e) :
+AssertCommand::AssertCommand(const BoolExpr& e) :
   d_expr(e) {
 }
 
@@ -37,7 +36,7 @@ void AssertCommand::invoke(SmtEngine* smt_engine) {
 CheckSatCommand::CheckSatCommand() {
 }
 
-CheckSatCommand::CheckSatCommand(const Node& e) :
+CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
   d_expr(e) {
 }
 
@@ -45,7 +44,7 @@ void CheckSatCommand::invoke(SmtEngine* smt_engine) {
   smt_engine->checkSat(d_expr);
 }
 
-QueryCommand::QueryCommand(const Node& e) :
+QueryCommand::QueryCommand(const BoolExpr& e) :
   d_expr(e) {
 }
 
@@ -73,10 +72,6 @@ void CommandSequence::addCommand(Command* cmd) {
   d_command_sequence.push_back(cmd);
 }
 
-// Printout methods
-
-using namespace std;
-
 void EmptyCommand::toString(ostream& out) const {
   out << "EmptyCommand(" << d_name << ")";
 }
@@ -98,8 +93,9 @@ void QueryCommand::toString(ostream& out) const {
 
 void CommandSequence::toString(ostream& out) const {
   out << "CommandSequence[" << endl;
-  for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i)
+  for(unsigned i = d_last_index; i < d_command_sequence.size(); ++i) {
     out << *d_command_sequence[i] << endl;
+  }
   out << "]";
 }
 
diff --git a/src/util/command.h b/src/util/command.h
index 189872220..221c513f0 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -15,12 +15,11 @@
 #include <iostream>
 
 #include "cvc4_config.h"
-#include "expr/node.h"
+#include "expr/expr.h"
 
 namespace CVC4 {
   class SmtEngine;
   class Command;
-  class Node;
 }/* CVC4 namespace */
 
 namespace CVC4 {
@@ -45,33 +44,33 @@ private:
 
 
 class CVC4_PUBLIC AssertCommand : public Command {
-protected:
-  Node d_expr;
 public:
-  AssertCommand(const Node& e);
+  AssertCommand(const BoolExpr& e);
   void invoke(CVC4::SmtEngine* smt_engine);
   void toString(std::ostream& out) const;
+protected:
+  BoolExpr d_expr;
 };/* class AssertCommand */
 
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
 public:
   CheckSatCommand();
-  CheckSatCommand(const Node& e);
+  CheckSatCommand(const BoolExpr& e);
   void invoke(SmtEngine* smt);
   void toString(std::ostream& out) const;
 protected:
-  Node d_expr;
+  BoolExpr d_expr;
 };/* class CheckSatCommand */
 
 
 class CVC4_PUBLIC QueryCommand : public Command {
 public:
-  QueryCommand(const Node& e);
+  QueryCommand(const BoolExpr& e);
   void invoke(SmtEngine* smt);
   void toString(std::ostream& out) const;
 protected:
-  Node d_expr;
+  BoolExpr d_expr;
 };/* class QueryCommand */