A mess of changes in the expression manager, simple example still failing due to some problems in the prop_engine

* default null expr and expr value and reorganisation/rewrite of some methods
* fixed some bugs
* expressions should always be passed as const Expr& to methods, otherwise copy constructors are called

Problematic code:
* Expr class has a bunch of methods that return Exprs, such as a.andExpr(b). None of these know what is their expression manager. We should
 (a) Not allow this, all expression construction should go through the ExprBuilder or directly thorugh the expression manager
 (b) Allow this, as it is now, but the have the default expression manager be setup in every entry into the smt solver + these construction methods shouldn't be available to the user (oterwise a mess ensues)
* We have to decide how to construct ExprBuilders:
 (a) constructing ExprBuilders with em = ExprBuilder(e).andExpr(b) is problematic as at construction we can't know the expression manager, and the kind of em will be UNDEFINED, so when adding b we can't assume its not UNDEFINED
 (b) constructing it with ExprBuilder(em) << AND << a << b or ExprBuilder(em, AND) << a << b seems like a nicer approach
 
 I am still confused about these expression builders so we should talk about this.
 
 
   

11 files changed, 162 insertions, 112 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index e88189bcc..fa273dfa5 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -13,6 +13,7 @@
 #include "expr/expr.h"
 #include "expr_value.h"
 #include "expr_builder.h"
+#include "util/Assert.h"
 
 using namespace CVC4::expr;
 
@@ -33,70 +34,82 @@ Expr::Expr() :
 
 Expr::Expr(ExprValue* ev)
   : d_ev(ev) {
-  if(d_ev != 0)
-    d_ev->inc();
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
+  d_ev->inc();
 }
 
 Expr::Expr(const Expr& e) {
-  if((d_ev = e.d_ev) && d_ev != 0)
-    d_ev->inc();
+  Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!");
+  d_ev = e.d_ev;
+  d_ev->inc();
 }
 
 Expr::~Expr() {
-  if(d_ev)
-    d_ev->dec();
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
+  d_ev->dec();
+}
+
+void Expr::assignExprValue(ExprValue* ev) {
+  d_ev = ev;
+  d_ev->inc();
 }
 
 Expr& Expr::operator=(const Expr& e) {
-  if(d_ev)
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
+  if(this != &e && d_ev != e.d_ev) {
     d_ev->dec();
-  if((d_ev = e.d_ev))
+    d_ev = e.d_ev;
     d_ev->inc();
+  }
   return *this;
 }
 
-ExprValue* Expr::operator->() const {
+ExprValue const* Expr::operator->() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
   return d_ev;
 }
 
 uint64_t Expr::hash() const {
+  Assert(d_ev != NULL, "Expecting a non-NULL evpression value!");
   return d_ev->hash();
 }
 
 Expr Expr::eqExpr(const Expr& right) const {
-  return ExprBuilder(*this).eqExpr(right);
+  return ExprManager::currentEM()->mkExpr(EQUAL, *this, right);
 }
 
 Expr Expr::notExpr() const {
-  return ExprBuilder(*this).notExpr();
+  return ExprManager::currentEM()->mkExpr(NOT, *this);
 }
 
+// FIXME: What does this do and why?
 Expr Expr::negate() const { // avoid double-negatives
   return ExprBuilder(*this).negate();
 }
 
+
 Expr Expr::andExpr(const Expr& right) const {
-  return ExprBuilder(*this).andExpr(right);
+  return ExprManager::currentEM()->mkExpr(AND, *this, right);
 }
 
 Expr Expr::orExpr(const Expr& right) const {
-  return ExprBuilder(*this).orExpr(right);
+  return ExprManager::currentEM()->mkExpr(OR, *this, right);
 }
 
 Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
-  return ExprBuilder(*this).iteExpr(thenpart, elsepart);
+  return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart);
 }
 
 Expr Expr::iffExpr(const Expr& right) const {
-  return ExprBuilder(*this).iffExpr(right);
+  return ExprManager::currentEM()->mkExpr(IFF, *this, right);
 }
 
 Expr Expr::impExpr(const Expr& right) const {
-  return ExprBuilder(*this).impExpr(right);
+  return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right);
 }
 
 Expr Expr::xorExpr(const Expr& right) const {
-  return ExprBuilder(*this).xorExpr(right);
+  return ExprManager::currentEM()->mkExpr(XOR, *this, right);
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr.h b/src/expr/expr.h
index 013888baa..7440974d8 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -26,7 +26,7 @@ namespace CVC4 {
 
 namespace CVC4 {
 
-inline std::ostream& operator<<(std::ostream&, CVC4::Expr) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC;
 
 class ExprManager;
 
@@ -41,6 +41,9 @@ using CVC4::expr::ExprValue;
  * maintained in the ExprValue.
  */
 class CVC4_PUBLIC Expr {
+
+  friend class ExprValue;
+
   /** A convenient null-valued encapsulated pointer */
   static Expr s_null;
 
@@ -57,6 +60,19 @@ class CVC4_PUBLIC Expr {
   friend class ExprBuilder;
   friend class ExprManager;
 
+  /** Access to the encapsulated expression.
+   *  @return the encapsulated expression. */
+  ExprValue const* operator->() const;
+
+  /**
+   * Assigns the expression value and does reference counting. No assumptions are
+   * made on the expression, and should only be used if we know what we are
+   * doing.
+   *
+   * @param ev the expression value to assign
+   */
+  void assignExprValue(ExprValue* ev);
+
 public:
 
   /** Default constructor, makes a null expression. */
@@ -70,13 +86,14 @@ public:
 
   bool operator==(const Expr& e) const { return d_ev == e.d_ev; }
   bool operator!=(const Expr& e) const { return d_ev != e.d_ev; }
-  bool operator<(const Expr& e) const { return d_ev < e.d_ev; }// for map key
 
-  Expr& operator=(const Expr&);
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   */
+  inline bool operator<(const Expr& e) const;
 
-  /** Access to the encapsulated expression.
-   *  @return the encapsulated expression. */
-  ExprValue* operator->() const;
+  Expr& operator=(const Expr&);
 
   uint64_t hash() const;
 
@@ -105,8 +122,8 @@ public:
 
   inline iterator begin();
   inline iterator end();
-  inline iterator begin() const;
-  inline iterator end() const;
+  inline const_iterator begin() const;
+  inline const_iterator end() const;
 
   void toString(std::ostream&) const;
 
@@ -120,7 +137,11 @@ public:
 
 namespace CVC4 {
 
-inline std::ostream& operator<<(std::ostream& out, CVC4::Expr e) {
+inline bool Expr::operator<(const Expr& e) const {
+  return d_ev->d_id < e.d_ev->d_id;
+}
+
+inline std::ostream& operator<<(std::ostream& out, const Expr& e) {
   e.toString(out);
   return out;
 }
@@ -143,11 +164,11 @@ inline Expr::iterator Expr::end() {
   return d_ev->end();
 }
 
-inline Expr::iterator Expr::begin() const {
+inline Expr::const_iterator Expr::begin() const {
   return d_ev->begin();
 }
 
-inline Expr::iterator Expr::end() const {
+inline Expr::const_iterator Expr::end() const {
   return d_ev->end();
 }
 
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index 4de22f987..10152a338 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -12,20 +12,24 @@
 #include "expr_builder.h"
 #include "expr_manager.h"
 #include "expr_value.h"
-#include "util/Assert.h"
 #include "util/output.h"
 
 using namespace std;
 
 namespace CVC4 {
 
-ExprBuilder::ExprBuilder() : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {}
+ExprBuilder::ExprBuilder() :
+  d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false),
+      d_nchildren(0) {
+}
 
-ExprBuilder::ExprBuilder(Kind k) : d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {}
+ExprBuilder::ExprBuilder(Kind k) :
+  d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) {
+}
 
-ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
-  ExprValue *v = e->inc();
-  d_children.u_arr[0] = v;
+ExprBuilder::ExprBuilder(const Expr& e) :
+  d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+  d_children.u_arr[0] = e.d_ev->inc();;
 }
 
 ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
@@ -38,36 +42,45 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
   return *this;
 }
 
-ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) {
+ExprBuilder::ExprBuilder(const ExprBuilder& eb) :
+  d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used),
+      d_nchildren(eb.d_nchildren) {
   Assert( !d_used );
 
   if(d_nchildren > nchild_thresh) {
-    d_children.u_vec = new vector<Expr>();
+    d_children.u_vec = new vector<Expr> ();
     d_children.u_vec->reserve(d_nchildren + 5);
-    copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec));
+    copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(),
+         back_inserter(*d_children.u_vec));
   } else {
     ev_iterator j = d_children.u_arr;
-    for(ExprValue* const* i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
+    ExprValue* const * i = eb.d_children.u_arr;
+    ExprValue* const * i_end = i + eb.d_nchildren;
+    for(; i != i_end; ++i, ++j)
       *j = (*i)->inc();
   }
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
+ExprBuilder::ExprBuilder(ExprManager* em) :
+  d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
+ExprBuilder::ExprBuilder(ExprManager* em, Kind k) :
+  d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
-  ExprValue *v = e->inc();
-  d_children.u_arr[0] = v;
+ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) :
+  d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+  d_children.u_arr[0] = e.d_ev->inc();
 }
 
 ExprBuilder::~ExprBuilder() {
   if(d_nchildren > nchild_thresh) {
     delete d_children.u_vec;
   } else {
-    for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
+    ev_iterator i = d_children.u_arr;
+    ev_iterator i_end = d_children.u_arr + d_nchildren;
+    for(; i != i_end ; ++i) {
       (*i)->dec();
     }
   }
@@ -94,8 +107,7 @@ ExprBuilder& ExprBuilder::notExpr() {
 // avoid double-negatives
 ExprBuilder& ExprBuilder::negate() {
   if(EXPECT_FALSE( d_kind == NOT ))
-    return reset(d_children.u_arr[0]);
-  Assert( d_kind != UNDEFINED_KIND );
+    return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND );
   collapse();
   d_kind = NOT;
   return *this;
@@ -169,39 +181,27 @@ ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
   return *this;
 }
 
-void ExprBuilder::addChild(const Expr& e) {
-  Debug("expr") << "adding child E " << e << endl;
-  if(d_nchildren == nchild_thresh) {
-    Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
-    vector<Expr>* v = new vector<Expr>();
-    v->reserve(nchild_thresh + 5);
-    for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
-      v->push_back(Expr(*i));
-      (*i)->dec();
-    }
-    v->push_back(e);
-    d_children.u_vec = v;
-    ++d_nchildren;
-  } else if(d_nchildren > nchild_thresh) {
-    Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl;
-    d_children.u_vec->push_back(e);
-    ++d_nchildren;
-  } else {
-    Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl;
-    ExprValue *ev = e.d_ev;
-    d_children.u_arr[d_nchildren] = ev;
-    ev->inc();
-    ++d_nchildren;
-  }
-}
-
+/**
+ * We keep the children either:
+ * (a) In the array of expression values if the number of children is less than
+ *     nchild_thresh. Hence (last else) we increase the reference count.
+ * (b) If the number of children reaches the nchild_thresh, we allocate a vector
+ *     for the children. Children are now expressions, so we also decrement the
+ *     reference count for each child.
+ * (c) Otherwise we just add to the end of the vector.
+ */
 void ExprBuilder::addChild(ExprValue* ev) {
+  Assert(d_nchildren <= nchild_thresh ||
+         d_nchildren == d_children.u_vec->size(),
+         "children count doesn't reflect the size of the vector!");
   Debug("expr") << "adding child ev " << ev << endl;
   if(d_nchildren == nchild_thresh) {
     Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl;
-    vector<Expr>* v = new vector<Expr>();
+    vector<Expr>* v = new vector<Expr> ();
     v->reserve(nchild_thresh + 5);
-    for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) {
+    ExprValue** i = d_children.u_arr;
+    ExprValue** i_end = i + nchild_thresh;
+    for(;i != i_end; ++ i) {
       v->push_back(Expr(*i));
       (*i)->dec();
     }
@@ -209,20 +209,20 @@ void ExprBuilder::addChild(ExprValue* ev) {
     d_children.u_vec = v;
     ++d_nchildren;
   } else if(d_nchildren > nchild_thresh) {
-    Debug("expr") << "over thresh " << d_nchildren << " > " << nchild_thresh << endl;
+    Debug("expr") << "over thresh " << d_nchildren
+                  << " > " << nchild_thresh << endl;
     d_children.u_vec->push_back(Expr(ev));
-    ++d_nchildren;
+    // ++d_nchildren; no need for this
   } else {
-    Debug("expr") << "under thresh " << d_nchildren << " < " << nchild_thresh << endl;
-    d_children.u_arr[d_nchildren] = ev;
-    ev->inc();
-    ++d_nchildren;
+    Debug("expr") << "under thresh " << d_nchildren
+                  << " < " << nchild_thresh << endl;
+    d_children.u_arr[d_nchildren ++] = ev->inc();
   }
 }
 
 ExprBuilder& ExprBuilder::collapse() {
   if(d_nchildren == nchild_thresh) {
-    vector<Expr>* v = new vector<Expr>();
+    vector<Expr>* v = new vector<Expr> ();
     v->reserve(nchild_thresh + 5);
     //
     Unreachable();// unimplemented
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index d70acb1fb..34e34bf6e 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -17,6 +17,7 @@
 
 #include "expr_manager.h"
 #include "kind.h"
+#include "util/Assert.h"
 
 namespace CVC4 {
 
@@ -43,7 +44,7 @@ class ExprBuilder {
     std::vector<Expr>* u_vec;
   } d_children;
 
-  void addChild(const Expr&);
+  void addChild(const Expr& e) { addChild(e.d_ev); }
   void addChild(ExprValue*);
   ExprBuilder& collapse();
 
@@ -203,26 +204,27 @@ inline ExprBuilder::operator Expr() {
   ExprValue *ev;
   uint64_t hash;
 
+  Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!");
+
   // 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);
   } else {
-    hash = d_kind;
-
     if(d_nchildren <= nchild_thresh) {
-      for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
-        hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
-
+      hash = ExprValue::computeHash<ev_iterator>(d_kind, ev_begin(), ev_end());
       void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
       ev = new (space) ExprValue;
       size_t nc = 0;
-      for(ev_iterator i = ev_begin(); i != ev_end(); ++i)
-        ev->d_children[nc++] = Expr(*i);
+      ev_iterator i = ev_begin();
+      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
+        ev->d_children[nc++].assignExprValue(*i);
+      }
     } else {
-      for(std::vector<Expr>::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i)
-        hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->hash();
-
+      hash = ExprValue::computeHash<std::vector<Expr>::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end());
       void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr));
       ev = new (space) ExprValue;
       size_t nc = 0;
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 9b7697e4f..3b5347301 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -19,6 +19,7 @@ namespace CVC4 {
 __thread ExprManager* ExprManager::s_current = 0;
 
 Expr ExprManager::lookup(uint64_t hash, const Expr& e) {
+  Assert(this != NULL, "Woops, we have a bad expression manager!");
   hash_t::iterator i = d_hash.find(hash);
   if(i == d_hash.end()) {
     // insert
@@ -34,7 +35,7 @@ Expr ExprManager::lookup(uint64_t hash, const Expr& e) {
       if(e.numChildren() != j->numChildren())
         continue;
 
-      Expr::iterator c1 = e.begin();
+      Expr::const_iterator c1 = e.begin();
       Expr::iterator c2 = j->begin();
       for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) {
         if(c1->d_ev != c2->d_ev)
@@ -60,23 +61,23 @@ Expr ExprManager::mkExpr(Kind kind) {
   return ExprBuilder(this, kind);
 }
 
-Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
   return ExprBuilder(this, kind) << child1;
 }
 
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
   return ExprBuilder(this, kind) << child1 << child2;
 }
 
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3) {
   return ExprBuilder(this, kind) << child1 << child2 << child3;
 }
 
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4) {
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4) {
   return ExprBuilder(this, kind) << child1 << child2 << child3 << child4;
 }
 
-Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5) {
+Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) {
   return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
 }
 
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index d311445f3..542d1040d 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -39,11 +39,11 @@ public:
 
   // general expression-builders
   Expr mkExpr(Kind kind);
-  Expr mkExpr(Kind kind, Expr child1);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
+  Expr mkExpr(Kind kind, const Expr& child1);
+  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);
   // N-ary version
   Expr mkExpr(Kind kind, std::vector<Expr> children);
 
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index 250803281..17f3b64c3 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -25,12 +25,7 @@ ExprValue::ExprValue() :
 }
 
 uint64_t ExprValue::hash() const {
-  uint64_t hash = d_kind;
-
-  for(const_iterator i = begin(); i != end(); ++i)
-    hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ i->hash();
-
-  return hash;
+  return computeHash<const_iterator>(d_kind, begin(), end());
 }
 
 ExprValue* ExprValue::inc() {
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 18ad84073..b334e1c2d 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -74,6 +74,22 @@ class ExprValue {
   /** Private default constructor for the null value. */
   ExprValue();
 
+  /**
+   * Computes the hash over the given iterator span of children, and the
+   * root hash. The iterator should be either over a range of Expr or pointers
+   * to ExprValue.
+   * @param hash the initial value for the hash
+   * @param begin the begining of the range
+   * @param end the end of the range
+   * @return the hash value
+   */
+  template<typename const_iterator_type>
+  static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) {
+    for(const_iterator_type i = begin; i != end; ++i)
+      hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->getId();
+    return hash;
+  }
+
 public:
   /** Hash this expression.
    *  @return the hash value of this expression. */
@@ -94,6 +110,8 @@ public:
   const_iterator rbegin() const;
   const_iterator rend() const;
 
+  unsigned getId() const { return d_id; }
+  unsigned getKind() const { return (Kind) d_kind; }
   void CVC4_PUBLIC toString(std::ostream& out) const;
 };
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 412c0f3af..2e895cdc0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -27,7 +27,7 @@ void SmtEngine::processAssertionList() {
   for(std::vector<Expr>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
+    d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i);
 }
 
 Result SmtEngine::check() {
diff --git a/src/util/command.cpp b/src/util/command.cpp
index c78fbc089..ed6b61703 100644
--- a/src/util/command.cpp
+++ b/src/util/command.cpp
@@ -14,7 +14,7 @@ using namespace std;
 
 namespace CVC4 {
 
-ostream& operator<<(ostream& out, const CVC4::Command& c) {
+ostream& operator<<(ostream& out, const Command& c) {
   c.toString(out);
   return out;
 }
diff --git a/src/util/command.h b/src/util/command.h
index 501aa31e0..31acbc43b 100644
--- a/src/util/command.h
+++ b/src/util/command.h
@@ -25,7 +25,7 @@ namespace CVC4 {
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream&, const CVC4::Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
 
 class CVC4_PUBLIC Command {
 public: