configure option adjustments as per 11/24 meeting; various fixes and improvements

8 files changed, 186 insertions, 22 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index f1b334ff8..e25cf8595 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -10,7 +10,7 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "expr_value.h"
 #include "expr_builder.h"
 
diff --git a/src/expr/expr.h b/src/expr/expr.h
new file mode 100644
index 000000000..d99708991
--- /dev/null
+++ b/src/expr/expr.h
@@ -0,0 +1,103 @@
+/*********************                                           -*- C++ -*-  */
+/** cvc4_expr.h
+ ** 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.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **/
+
+#ifndef __CVC4_EXPR_H
+#define __CVC4_EXPR_H
+
+#include <vector>
+#include <stdint.h>
+
+#include "cvc4_config.h"
+#include "expr/kind.h"
+
+namespace CVC4 {
+
+namespace expr {
+  class ExprValue;
+}/* CVC4::expr namespace */
+
+using CVC4::expr::ExprValue;
+
+/**
+ * Encapsulation of an ExprValue pointer.  The reference count is
+ * maintained in the ExprValue.
+ */
+class CVC4_PUBLIC Expr {
+  /** A convenient null-valued encapsulated pointer */
+  static Expr s_null;
+
+  /** The referenced ExprValue */
+  ExprValue* d_ev;
+
+  /** This constructor is reserved for use by the Expr package; one
+   *  must construct an Expr using one of the build mechanisms of the
+   *  Expr package.
+   *
+   *  Increments the reference count. */
+  explicit Expr(ExprValue*);
+
+  typedef Expr* iterator;
+  typedef Expr const* const_iterator;
+
+  friend class ExprBuilder;
+
+public:
+  CVC4_PUBLIC Expr(const Expr&);
+
+  /** Destructor.  Decrements the reference count and, if zero,
+   *  collects the ExprValue. */
+  CVC4_PUBLIC ~Expr();
+
+  Expr& operator=(const Expr&) CVC4_PUBLIC;
+
+  /** Access to the encapsulated expression.
+   *  @return the encapsulated expression. */
+  ExprValue* operator->() const CVC4_PUBLIC;
+
+  uint64_t hash() const;
+
+  Expr eqExpr(const Expr& right) const;
+  Expr notExpr() const;
+  Expr negate() const; // avoid double-negatives
+  Expr andExpr(const Expr& right) const;
+  Expr orExpr(const Expr& right) const;
+  Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const;
+  Expr iffExpr(const Expr& right) const;
+  Expr impExpr(const Expr& right) const;
+  Expr xorExpr(const Expr& right) const;
+  Expr skolemExpr(int i) const;
+  Expr substExpr(const std::vector<Expr>& oldTerms,
+                 const std::vector<Expr>& newTerms) const;
+
+  Expr plusExpr(const Expr& right) const;
+  Expr uMinusExpr() const;
+  Expr multExpr(const Expr& right) const;
+
+  inline Kind getKind() const;
+
+  static Expr null() { return s_null; }
+
+};/* class Expr */
+
+}/* CVC4 namespace */
+
+#include "expr/expr_value.h"
+
+namespace CVC4 {
+
+inline Kind Expr::getKind() const {
+  return Kind(d_ev->d_kind);
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_EXPR_H */
diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h
index b44c9af6f..03140c4eb 100644
--- a/src/expr/expr_attribute.h
+++ b/src/expr/expr_attribute.h
@@ -17,7 +17,7 @@
 #include <stdint.h>
 #include "config.h"
 #include "context/context.h"
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 namespace CVC4 {
 namespace expr {
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index c5f366654..bf572cfbc 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -38,7 +38,7 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
 }
 
 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);
+  Assert( !d_used );
 
   if(d_nchildren > nchild_thresh) {
     d_children.u_vec = new vector<Expr>();
@@ -74,59 +74,104 @@ ExprBuilder::~ExprBuilder() {
 
 // Compound expression constructors
 ExprBuilder& ExprBuilder::eqExpr(const Expr& right) {
-  if(d_kind != UNDEFINED_KIND && d_kind != EQUAL)
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != EQUAL )) {
     collapse();
-  d_kind = EQUAL;
+    d_kind = EQUAL;
+  }
+  addChild(right);
   return *this;
 }
 
 ExprBuilder& ExprBuilder::notExpr() {
-  if(d_kind != UNDEFINED_KIND)
-    collapse();
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
   d_kind = NOT;
   return *this;
 }
 
 // avoid double-negatives
 ExprBuilder& ExprBuilder::negate() {
-  if(d_kind == NOT)
+  if(EXPECT_FALSE( d_kind == NOT ))
     return reset(d_children.u_arr[0]);
-  if(d_kind != UNDEFINED_KIND)
-    collapse();
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
   d_kind = NOT;
   return *this;
 }
 
 ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(d_kind != AND) {
+    collapse();
+    d_kind = AND;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::orExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != OR )) {
+    collapse();
+    d_kind = OR;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) {
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
+  d_kind = ITE;
+  addChild(thenpart);
+  addChild(elsepart);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::iffExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != IFF )) {
+    collapse();
+    d_kind = IFF;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::impExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
+  d_kind = IMPLIES;
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
+  Assert( d_kind != UNDEFINED_KIND );
+  if(EXPECT_TRUE( d_kind != XOR )) {
+    collapse();
+    d_kind = XOR;
+  }
+  addChild(right);
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::skolemExpr(int i) {
-}
-
-ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms,
-                                    const std::vector<Expr>& newTerms) {
+  Assert( d_kind != UNDEFINED_KIND );
+  collapse();
+  d_kind = SKOLEM;
+  //addChild(i);//FIXME: int constant
+  return *this;
 }
 
 // "Stream" expression constructor syntax
 ExprBuilder& ExprBuilder::operator<<(const Kind& op) {
+  return *this;
 }
 
 ExprBuilder& ExprBuilder::operator<<(const Expr& child) {
+  return *this;
 }
 
 void ExprBuilder::addChild(const Expr& e) {
@@ -182,21 +227,27 @@ void ExprBuilder::collapse() {
 
 // not const
 ExprBuilder::operator Expr() {
+  // FIXME
 }
 
-AndExprBuilder   ExprBuilder::operator&&(Expr) {
+AndExprBuilder   ExprBuilder::operator&&(Expr e) {
+  return AndExprBuilder(*this) && e;
 }
 
-OrExprBuilder    ExprBuilder::operator||(Expr) {
+OrExprBuilder    ExprBuilder::operator||(Expr e) {
+  return OrExprBuilder(*this) || e;
 }
 
-PlusExprBuilder  ExprBuilder::operator+ (Expr) {
+PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
+  return PlusExprBuilder(*this) + e;
 }
 
-PlusExprBuilder  ExprBuilder::operator- (Expr) {
+PlusExprBuilder  ExprBuilder::operator- (Expr e) {
+  return PlusExprBuilder(*this) - e;
 }
 
-MultExprBuilder  ExprBuilder::operator* (Expr) {
+MultExprBuilder  ExprBuilder::operator* (Expr e) {
+  return MultExprBuilder(*this) * e;
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 07d069a9e..97f18ca6d 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -109,6 +109,8 @@ class AndExprBuilder {
 
 public:
 
+  AndExprBuilder(const ExprBuilder&);
+
   AndExprBuilder&   operator&&(Expr);
   OrExprBuilder     operator||(Expr);
 
@@ -121,6 +123,8 @@ class OrExprBuilder {
 
 public:
 
+  OrExprBuilder(const ExprBuilder&);
+
   AndExprBuilder    operator&&(Expr);
   OrExprBuilder&    operator||(Expr);
 
@@ -133,6 +137,8 @@ class PlusExprBuilder {
 
 public:
 
+  PlusExprBuilder(const ExprBuilder&);
+
   PlusExprBuilder&  operator+(Expr);
   PlusExprBuilder&  operator-(Expr);
   MultExprBuilder   operator*(Expr);
@@ -146,6 +152,8 @@ class MultExprBuilder {
 
 public:
 
+  MultExprBuilder(const ExprBuilder&);
+
   PlusExprBuilder   operator+(Expr);
   PlusExprBuilder   operator-(Expr);
   MultExprBuilder&  operator*(Expr);
diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h
index 802cfe9c0..e3fbd91bf 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -13,7 +13,7 @@
 #define __CVC4__EXPR_MANAGER_H
 
 #include <vector>
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 #include "kind.h"
 
 namespace CVC4 {
diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h
index e0451f7a6..0b97dfdae 100644
--- a/src/expr/expr_value.h
+++ b/src/expr/expr_value.h
@@ -16,7 +16,7 @@
 
 /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */
 /* to resolve a circular dependency */
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 #ifndef __CVC4__EXPR__EXPR_VALUE_H
 #define __CVC4__EXPR__EXPR_VALUE_H
diff --git a/src/expr/kind.h b/src/expr/kind.h
index 98cc7e2e3..db25d914e 100644
--- a/src/expr/kind.h
+++ b/src/expr/kind.h
@@ -36,12 +36,14 @@ enum Kind {
 
   AND,
   IFF,
+  IMPLIES,
   OR,
   XOR,
 
   /* from arith */
   PLUS,
-  MINUS
+  MINUS,
+  MULT
 
 };/* enum Kind */