A mess of changes in the expression manager, simple example still failing due to...

* 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.

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index e88189bcc451170c65e55320444fed370b4a33f5..fa273dfa5665f03bd1111e6e671551c840c939c6 100644 (file)
--- 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 013888baa75728d84bfbfc834e004897b424ac21..7440974d8a89c2dc4740dbfc477dfb0a2a361196 100644 (file)
--- 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 4de22f987fa7a0de6305cf25fe6e2367c47188af..10152a338da6441655b9df836cad72b22f67cc4f 100644 (file)
--- 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 d70acb1fbd7dbbf2320de17904fa22ce9b380dd8..34e34bf6e04bf45fa45cbeddda3092055cdf7340 100644 (file)
--- 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 9b7697e4f348071a8b534dd647778f3e07c2546c..3b534730143deef876531c27b8159ec67e6d1764 100644 (file)
--- 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 d311445f3477fb3094496bd53c7d0dc1eb2251c2..542d1040d820af5ca3e3112f30b1ec35458e9785 100644 (file)
--- 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 250803281618d137ec3902335c589c3bbea936b7..17f3b64c3484f2e829ec9a7810a55514641bfc07 100644 (file)
--- 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 18ad84073ffb8ab16a921ed5fe23d3383a0b80be..b334e1c2da8f318fb18fb1925e0057a167970feb 100644 (file)
--- 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 412c0f3af7e11d737fa750a62b07c8269ae5f408..2e895cdc0762b8ed307bc86cc7ed0d0f830e8315 100644 (file)
--- 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 c78fbc089d69a09c7c0e82ffe8fe3f273acd5a38..ed6b61703861d9820f86c1ad5e93b19540c52028 100644 (file)
--- 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 501aa31e0d213deafc34a9eddd685928d143c7f7..31acbc43baf99bcf4a29163e0014a7dba322b28a 100644 (file)
--- 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: