work on exprs, driver, util

9 files changed, 92 insertions, 29 deletions

diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h
index d76bd742d..d24385f8e 100644
--- a/src/expr/attr_type.h
+++ b/src/expr/attr_type.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4_ATTR_TYPE_H
 #define __CVC4_ATTR_TYPE_H
 
-#include "core/expr_attribute.h"
+#include "expr_attribute.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 5e422f349..b6484ef25 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -11,8 +11,8 @@
  **/
 
 #include "cvc4_expr.h"
-#include "core/expr_value.h"
-#include "core/expr_builder.h"
+#include "expr_value.h"
+#include "expr_builder.h"
 
 namespace CVC4 {
 
@@ -44,11 +44,7 @@ Expr& Expr::operator=(const Expr& e) {
   return *this;
 }
 
-ExprValue* Expr::operator->() {
-  return d_ev;
-}
-
-const ExprValue* Expr::operator->() const {
+ExprValue* Expr::operator->() const {
   return d_ev;
 }
 
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index b00882478..3525a8370 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -15,9 +15,9 @@
 // TODO WARNING this file needs work !
 
 #include <stdint.h>
-#include "core/config.h"
-#include "core/context.h"
-#include "core/cvc4_expr.h"
+#include "config.h"
+#include "context/context.h"
+#include "cvc4_expr.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index 6491b7d44..2f7114a9b 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -9,9 +9,10 @@
  **
  **/
 
-#include "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/expr_value.h"
+#include "expr_builder.h"
+#include "expr_manager.h"
+#include "expr_value.h"
+#include "util/assert.h"
 
 using namespace std;
 
@@ -26,6 +27,16 @@ ExprBuilder::ExprBuilder(const Expr& e) : d_em(ExprManager::currentEM()), d_kind
   d_children.u_arr[0] = v;
 }
 
+ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
+  this->~ExprBuilder();
+  d_kind = Kind(ev->d_kind);
+  d_used = false;
+  d_nchildren = ev->d_nchildren;
+  for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i)
+    addChild(i->d_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) {
   cvc4assert(!d_used);
 
@@ -34,9 +45,9 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kin
     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));
   } else {
-    iterator j = d_children.u_arr;
-    for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
-      *j = i->inc();
+    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)
+      *j = (*i)->inc();
   }
 }
 
@@ -46,7 +57,7 @@ ExprBuilder::ExprBuilder(ExprManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_
 ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
 }
 
-ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+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;
 }
@@ -55,8 +66,8 @@ ExprBuilder::~ExprBuilder() {
   if(d_nchildren > nchild_thresh) {
     delete d_children.u_vec;
   } else {
-    for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
-      *i
+    for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
+      (*i)->dec();
     }
   }
 }
@@ -70,10 +81,20 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
 }
 
 ExprBuilder& ExprBuilder::notExpr() {
+  if(d_kind != UNDEFINED_KIND)
+    collapse();
+  d_kind = NOT;
+  return *this;
 }
 
 // avoid double-negatives
 ExprBuilder& ExprBuilder::negate() {
+  if(d_kind == NOT)
+    return reset(d_children.u_arr[0]);
+  if(d_kind != UNDEFINED_KIND)
+    collapse();
+  d_kind = NOT;
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
@@ -116,7 +137,43 @@ void ExprBuilder::addChild(const Expr& e) {
   if(d_nchildren == nchild_thresh) {
     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) {
+    d_children.u_vec.push_back(e);
+    ++d_nchildren;
+  } else {
+    ExprValue *ev = e->d_ev;
+    d_children.u_arr[d_nchildren] = ev;
+    ev->inc();
+    ++d_nchildren;
+  }
+  return *this;
+}
+
+void ExprBuilder::addChild(const ExprValue* ev) {
+  if(d_nchildren == nchild_thresh) {
+    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(Expr(ev));
+    d_children.u_vec = v;
+    ++d_nchildren;
+  } else if(d_nchildren > nchild_thresh) {
+    d_children.u_vec.push_back(Expr(ev));
+    ++d_nchildren;
+  } else {
+    d_children.u_arr[d_nchildren] = ev;
+    ev->inc();
+    ++d_nchildren;
   }
   return *this;
 }
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index fa08a3149..1104c17f5 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -13,8 +13,8 @@
 #define __CVC4_EXPR_BUILDER_H
 
 #include <vector>
-#include "core/expr_manager.h"
-#include "core/kind.h"
+#include "expr_manager.h"
+#include "kind.h"
 
 namespace CVC4 {
 
@@ -41,9 +41,15 @@ class ExprBuilder {
     std::vector<Expr>* u_vec;
   } d_children;
 
-  void addChild();
+  void addChild(const Expr&);
+  void addChild(const ExprValue*);
   void collapse();
 
+  typedef ExprValue** ev_iterator;
+  typedef ExprValue const** const_ev_iterator;
+
+  void reset(const ExprValue*);
+
 public:
 
   ExprBuilder();
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 90f10d8f7..80091bef6 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -10,9 +10,9 @@
  ** Expression manager implementation.
  **/
 
-#include "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/cvc4_expr.h"
+#include "expr_builder.h"
+#include "expr_manager.h"
+#include "cvc4_expr.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 048250485..7e0da01c6 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -14,7 +14,7 @@
 
 #include <vector>
 #include "cvc4_expr.h"
-#include "core/kind.h"
+#include "kind.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp
index ce4177a09..451538f3f 100644
--- a/src/expr/expr_value.cpp
+++ b/src/expr/expr_value.cpp
@@ -14,7 +14,7 @@
  ** reference count on ExprValue instances and
  **/
 
-#include "core/expr_value.h"
+#include "expr_value.h"
 
 namespace CVC4 {
 
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index 5f90533ed..4b4b4f612 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -48,6 +48,10 @@ class ExprValue {
   Expr     d_children[0];
 
   friend class Expr;
+  friend class ExprBuilder;
+
+  ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; }
+  ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; }
 
 public:
   /** Hash this expression.