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.
 
 
   

1 files changed, 30 insertions, 17 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 */