35 files changed, 266 insertions, 85 deletions

diff --git a/Makefile.am b/Makefile.am
index 451ef0e3a..5b0f8d11a 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -1,3 +1,5 @@
+AM_CXXFLAGS = -Wall
+
 AUTOMAKE_OPTIONS = foreign
 ACLOCAL_AMFLAGS = -I config
 
diff --git a/src/Makefile.am b/src/Makefile.am
index 3f0d0b381..7b2141da3 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,4 +1,4 @@
-INCLUDES = -I@srcdir@/include
+INCLUDES = -I@srcdir@/include -I@srcdir@
 
 SUBDIRS = core parser sat
 
@@ -10,17 +10,5 @@ libcvc4_la_LIBADD = \
 	sat/minisat/libminisat.a
 
 EXTRA_DIST = \
-	include/assert.h \
-	include/attr_type.h \
-	include/command.h
-	include/expr_attribute.h \
-	include/expr_builder.h \
-	include/expr.h \
-	include/expr_manager.h \
-	include/expr_value.h \
-	include/kind.h \
-	include/parser.h \
-	include/sat.h \
-	include/unique_id.h \
-	include/vc.h
-
+	include/cvc4.h \
+	include/cvc4_expr.h
diff --git a/src/core/Makefile.am b/src/core/Makefile.am
index 043882f36..d26a7483d 100644
--- a/src/core/Makefile.am
+++ b/src/core/Makefile.am
@@ -1,7 +1,10 @@
-INCLUDES = -I@srcdir@/../include
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
 
 noinst_LIBRARIES = libcore.a
 
 libcore_a_SOURCES = \
 	expr.cpp \
+	expr_builder.cpp \
+	expr_manager.cpp \
 	expr_value.cpp
diff --git a/src/include/assert.h b/src/core/assert.h
index a66503641..a66503641 100644
--- a/src/include/assert.h
+++ b/src/core/assert.h
diff --git a/src/include/attr_type.h b/src/core/attr_type.h
index d24385f8e..d76bd742d 100644
--- a/src/include/attr_type.h
+++ b/src/core/attr_type.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4_ATTR_TYPE_H
 #define __CVC4_ATTR_TYPE_H
 
-#include "expr_attribute.h"
+#include "core/expr_attribute.h"
 
 namespace CVC4 {
 
diff --git a/src/include/command.h b/src/core/command.h
index 944b9c621..944b9c621 100644
--- a/src/include/command.h
+++ b/src/core/command.h
diff --git a/src/include/context.h b/src/core/context.h
index fce2f0b8d..fce2f0b8d 100644
--- a/src/include/context.h
+++ b/src/core/context.h
diff --git a/src/include/debug.h b/src/core/debug.h
index 36942d1ae..36942d1ae 100644
--- a/src/include/debug.h
+++ b/src/core/debug.h
diff --git a/src/include/decision_engine.h b/src/core/decision_engine.h
index ec0172535..81d820eaa 100644
--- a/src/include/decision_engine.h
+++ b/src/core/decision_engine.h
@@ -12,7 +12,7 @@
 #ifndef __CVC4_DECISION_ENGINE_H
 #define __CVC4_DECISION_ENGINE_H
 
-#include "literal.h"
+#include "core/literal.h"
 
 namespace CVC4 {
 
diff --git a/src/include/exception.h b/src/core/exception.h
index 792a98701..792a98701 100644
--- a/src/include/exception.h
+++ b/src/core/exception.h
diff --git a/src/core/expr.cpp b/src/core/expr.cpp
index cdc7e6775..5e422f349 100644
--- a/src/core/expr.cpp
+++ b/src/core/expr.cpp
@@ -10,9 +10,9 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
-#include "expr.h"
-#include "expr_value.h"
-#include "expr_builder.h"
+#include "cvc4_expr.h"
+#include "core/expr_value.h"
+#include "core/expr_builder.h"
 
 namespace CVC4 {
 
diff --git a/src/include/expr_attribute.h b/src/core/expr_attribute.h
index 77700096e..b00882478 100644
--- a/src/include/expr_attribute.h
+++ b/src/core/expr_attribute.h
@@ -15,9 +15,9 @@
 // TODO WARNING this file needs work !
 
 #include <stdint.h>
-#include "config.h"
-#include "context.h"
-#include "expr.h"
+#include "core/config.h"
+#include "core/context.h"
+#include "core/cvc4_expr.h"
 
 namespace CVC4 {
 
diff --git a/src/core/expr_builder.cpp b/src/core/expr_builder.cpp
new file mode 100644
index 000000000..6491b7d44
--- /dev/null
+++ b/src/core/expr_builder.cpp
@@ -0,0 +1,152 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_builder.cpp
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ **/
+
+#include "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/expr_value.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+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(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 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);
+
+  if(d_nchildren > nchild_thresh) {
+    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));
+  } 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();
+  }
+}
+
+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, const Expr&) : 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() {
+  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
+    }
+  }
+}
+
+// Compound expression constructors
+ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
+  if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
+    collapse();
+  d_kind = EQUAL;
+  return *this;
+}
+
+ExprBuilder& ExprBuilder::notExpr() {
+}
+
+// avoid double-negatives
+ExprBuilder& ExprBuilder::negate() {
+}
+
+ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
+}
+
+ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
+}
+
+ExprBuilder& ExprBuilder::skolemExpr(int i) {
+}
+
+ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
+                                    const std::vector<Expr>& newTerms) {
+}
+
+// "Stream" expression constructor syntax
+ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+}
+
+ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+}
+
+template <class Iterator>
+ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+}
+
+void ExprBuilder::addChild(const Expr& e) {
+  if(d_nchildren == nchild_thresh) {
+    vector<Expr>* v = new vector<Expr>();
+    v->reserve(nchild_thresh + 5);
+    
+  }
+  return *this;
+}
+
+void ExprBuilder::collapse() {
+  if(d_nchildren == nchild_thresh) {
+    vector<Expr>* v = new vector<Expr>();
+    v->reserve(nchild_thresh + 5);
+    
+  }
+  return *this;
+}
+
+// not const
+ExprBuilder::operator Expr() {
+}
+
+AndExprBuilder   ExprBuilder::operator&&(Expr) {
+}
+
+OrExprBuilder    ExprBuilder::operator||(Expr) {
+}
+
+PlusExprBuilder  ExprBuilder::operator+ (Expr) {
+}
+
+PlusExprBuilder  ExprBuilder::operator- (Expr) {
+}
+
+MultExprBuilder  ExprBuilder::operator* (Expr) {
+}
+
+} /* CVC4 namespace */
diff --git a/src/include/expr_builder.h b/src/core/expr_builder.h
index a95ecb2e3..fa08a3149 100644
--- a/src/include/expr_builder.h
+++ b/src/core/expr_builder.h
@@ -13,8 +13,8 @@
 #define __CVC4_EXPR_BUILDER_H
 
 #include <vector>
-#include "expr_manager.h"
-#include "kind.h"
+#include "core/expr_manager.h"
+#include "core/kind.h"
 
 namespace CVC4 {
 
@@ -29,26 +29,35 @@ class ExprBuilder {
 
   Kind d_kind;
 
-  // TODO: store some flags here and install into attribute map when
-  // the expr is created?  (we'd have to do that since we don't know
-  // it's hash code yet)
-
   // initially false, when you extract the Expr this is set and you can't
   // extract another
   bool d_used;
 
+  static const unsigned nchild_thresh = 10;
+
   unsigned d_nchildren;
   union {
-    ExprValue*         u_arr[10];
+    ExprValue*         u_arr[nchild_thresh];
     std::vector<Expr>* u_vec;
   } d_children;
 
+  void addChild();
+  void collapse();
+
 public:
 
   ExprBuilder();
+  ExprBuilder(Kind k);
   ExprBuilder(const Expr&);
   ExprBuilder(const ExprBuilder&);
 
+  ExprBuilder(ExprManager*);
+  ExprBuilder(ExprManager*, Kind k);
+  ExprBuilder(ExprManager*, const Expr&);
+  ExprBuilder(ExprManager*, const ExprBuilder&);
+
+  ~ExprBuilder();
+
   // Compound expression constructors
   ExprBuilder& eqExpr(const Expr& right);
   ExprBuilder& notExpr();
diff --git a/src/core/expr_manager.cpp b/src/core/expr_manager.cpp
index c18fd9652..90f10d8f7 100644
--- a/src/core/expr_manager.cpp
+++ b/src/core/expr_manager.cpp
@@ -10,43 +10,43 @@
  ** Expression manager implementation.
  **/
 
-#include <vector>
-#include "expr.h"
-#include "kind.h"
+#include "core/expr_builder.h"
+#include "core/expr_manager.h"
+#include "core/cvc4_expr.h"
 
 namespace CVC4 {
 
-class ExprManager {
-  static __thread ExprManager* s_current;
-
-public:
-  static ExprManager* currentEM() { return s_current; }
-
-  // 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);
-  // N-ary version
-  Expr mkExpr(Kind kind, std::vector<Expr> children);
-
-  // TODO: these use the current EM (but must be renamed)
-  /*
-  static Expr mkExpr(Kind kind)
-  { currentEM()->mkExpr(kind); }
-  static Expr mkExpr(Kind kind, Expr child1);
-  { currentEM()->mkExpr(kind, child1); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2);
-  { currentEM()->mkExpr(kind, child1, child2); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
-  { currentEM()->mkExpr(kind, child1, child2, child3); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
-  static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
-  */
-};
+__thread ExprManager* ExprManager::s_current = 0;
+
+// general expression-builders
+
+Expr ExprManager::mkExpr(Kind kind) {
+  return ExprBuilder(this, kind);
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1) {
+  return ExprBuilder(this, kind) << child1;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) {
+  return ExprBuilder(this, kind) << child1 << child2;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3) {
+  return ExprBuilder(this, kind) << child1 << child2 << child3;
+}
+
+Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, 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) {
+  return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5;
+}
+
+// N-ary version
+Expr ExprManager::mkExpr(Kind kind, std::vector<Expr> children) {
+  return ExprBuilder(this, kind).append(children);
+}
 
 } /* CVC4 namespace */
diff --git a/src/include/expr_manager.h b/src/core/expr_manager.h
index 59a3eb7a3..048250485 100644
--- a/src/include/expr_manager.h
+++ b/src/core/expr_manager.h
@@ -13,8 +13,8 @@
 #define __CVC4_EXPR_MANAGER_H
 
 #include <vector>
-#include "expr.h"
-#include "kind.h"
+#include "cvc4_expr.h"
+#include "core/kind.h"
 
 namespace CVC4 {
 
diff --git a/src/core/expr_value.cpp b/src/core/expr_value.cpp
index b42773482..ce4177a09 100644
--- a/src/core/expr_value.cpp
+++ b/src/core/expr_value.cpp
@@ -14,7 +14,7 @@
  ** reference count on ExprValue instances and
  **/
 
-#include "expr_value.h"
+#include "core/expr_value.h"
 
 namespace CVC4 {
 
@@ -27,6 +27,23 @@ uint64_t ExprValue::hash() const {
   return hash;
 }
 
+ExprValue* ExprValue::inc() {
+  // FIXME multithreading
+  if(d_rc < MAX_RC)
+    ++d_rc;
+  return this;
+}
+
+ExprValue* ExprValue::dec() {
+  // FIXME multithreading
+  if(d_rc < MAX_RC)
+    if(--d_rc == 0) {
+      // FIXME gc
+      return 0;
+    }
+  return this;
+}
+
 ExprValue::iterator ExprValue::begin() {
   return d_children;
 }
diff --git a/src/include/expr_value.h b/src/core/expr_value.h
index ea14c3fa7..5f90533ed 100644
--- a/src/include/expr_value.h
+++ b/src/core/expr_value.h
@@ -18,7 +18,7 @@
 #define __CVC4_EXPR_VALUE_H
 
 #include <stdint.h>
-#include "expr.h"
+#include "cvc4_expr.h"
 
 namespace CVC4 {
 
@@ -26,6 +26,10 @@ namespace CVC4 {
  * This is an ExprValue.
  */
 class ExprValue {
+  /** Maximum reference count possible.  Used for sticky
+   *  reference-counting.  Should be (1 << num_bits(d_rc)) - 1 */
+  static const unsigned MAX_RC = 255;
+
   // this header fits into one 64-bit word
 
   /** The ID */
diff --git a/src/include/kind.h b/src/core/kind.h
index 5d99330ca..9c4e4d5ab 100644
--- a/src/include/kind.h
+++ b/src/core/kind.h
@@ -19,6 +19,8 @@ namespace CVC4 {
 // placeholder for design & development work.
 
 enum Kind {
+  UNDEFINED_KIND = -1,
+  EQUAL,
   AND,
   OR,
   XOR,
diff --git a/src/include/literal.h b/src/core/literal.h
index 8b147c640..8b147c640 100644
--- a/src/include/literal.h
+++ b/src/core/literal.h
diff --git a/src/include/model.h b/src/core/model.h
index c07b75dfa..c07b75dfa 100644
--- a/src/include/model.h
+++ b/src/core/model.h
diff --git a/src/include/parser.h b/src/core/parser.h
index e30b31b1c..967f20e95 100644
--- a/src/include/parser.h
+++ b/src/core/parser.h
@@ -13,8 +13,8 @@
 #ifndef __CVC4_PARSER_H
 #define __CVC4_PARSER_H
 
-#include "exception.h"
-#include "lang.h"
+#include "core/exception.h"
+#include "core/lang.h"
 
 namespace CVC4 {
 
diff --git a/src/include/parser_exception.h b/src/core/parser_exception.h
index debb75e70..18f027e44 100644
--- a/src/include/parser_exception.h
+++ b/src/core/parser_exception.h
@@ -13,7 +13,7 @@
 #ifndef __CVC4_PARSER_EXCEPTION_H
 #define __CVC4_PARSER_EXCEPTION_H
 
-#include "exception.h"
+#include "core/exception.h"
 #include <string>
 #include <iostream>
 
diff --git a/src/include/prop_engine.h b/src/core/prop_engine.h
index de25c5594..0febd2927 100644
--- a/src/include/prop_engine.h
+++ b/src/core/prop_engine.h
@@ -12,9 +12,9 @@
 #ifndef __CVC4_PROP_ENGINE_H
 #define __CVC4_PROP_ENGINE_H
 
-#include "expr.h"
-#include "decision_engine.h"
-#include "theory_engine.h"
+#include "core/cvc4_expr.h"
+#include "core/decision_engine.h"
+#include "core/theory_engine.h"
 
 namespace CVC4 {
 
diff --git a/src/include/prover.h b/src/core/prover.h
index de29f48c0..14eab7c03 100644
--- a/src/include/prover.h
+++ b/src/core/prover.h
@@ -13,9 +13,9 @@
 #define __CVC4_PROVER_H
 
 #include <vector>
-#include "expr.h"
-#include "result.h"
-#include "model.h"
+#include "core/cvc4_expr.h"
+#include "core/result.h"
+#include "core/model.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
diff --git a/src/include/result.h b/src/core/result.h
index 50f488682..50f488682 100644
--- a/src/include/result.h
+++ b/src/core/result.h
diff --git a/src/include/sat.h b/src/core/sat.h
index 00a94c142..00a94c142 100644
--- a/src/include/sat.h
+++ b/src/core/sat.h
diff --git a/src/include/theory.h b/src/core/theory.h
index 935c23b08..eeaba58d1 100644
--- a/src/include/theory.h
+++ b/src/core/theory.h
@@ -12,8 +12,8 @@
 #ifndef __CVC4_THEORY_H
 #define __CVC4_THEORY_H
 
-#include "expr.h"
-#include "literal.h"
+#include "core/cvc4_expr.h"
+#include "core/literal.h"
 
 namespace CVC4 {
 
diff --git a/src/include/theory_engine.h b/src/core/theory_engine.h
index 2a0841d8d..2a0841d8d 100644
--- a/src/include/theory_engine.h
+++ b/src/core/theory_engine.h
diff --git a/src/include/unique_id.h b/src/core/unique_id.h
index 1a6f3427a..1a6f3427a 100644
--- a/src/include/unique_id.h
+++ b/src/core/unique_id.h
diff --git a/src/include/vc.h b/src/include/cvc4.h
index 845d1eb6d..109496001 100644
--- a/src/include/vc.h
+++ b/src/include/cvc4.h
@@ -13,7 +13,7 @@
 #define __CVC4_VC_H
 
 #include "command.h"
-#include "expr.h"
+#include "cvc4_expr.h"
 
 /* TODO provide way of querying whether you fall into a fragment /
  * returning what fragment you're in */
diff --git a/src/include/expr.h b/src/include/cvc4_expr.h
index e92ece93d..17e7f4f82 100644
--- a/src/include/expr.h
+++ b/src/include/cvc4_expr.h
@@ -71,6 +71,8 @@ public:
                  const std::vector<Expr>& newTerms) const;
 
   static Expr null() { return s_null; }
+
+  friend class ExprBuilder;
 };/* class Expr */
 
 } /* CVC4 namespace */
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index a9560ab93..918ab2fb2 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -1,4 +1,5 @@
-INCLUDES = -I@srcdir@/../include
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
 
 noinst_LIBRARIES = libparser.a
 
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 6ab0ada49..f82980196 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -19,7 +19,7 @@
 
 #include <iostream>
 #include <sstream>
-#include "expr.h"
+#include "cvc4_expr.h"
 #include "exception.h"
 
 namespace CVC4 {
diff --git a/src/sat/Makefile.am b/src/sat/Makefile.am
index 321507609..5051420a2 100644
--- a/src/sat/Makefile.am
+++ b/src/sat/Makefile.am
@@ -1,3 +1,4 @@
-INCLUDES = -I@srcdir@/../include
+INCLUDES = -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall
 
 SUBDIRS = minisat