various fixes and updates to use and support parser

5 files changed, 118 insertions, 71 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index e25cf8595..f94a3c438 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -86,13 +86,4 @@ Expr Expr::xorExpr(const Expr& right) const {
   return ExprBuilder(*this).xorExpr(right);
 }
 
-Expr Expr::skolemExpr(int i) const {
-  return ExprBuilder(*this).skolemExpr(i);
-}
-
-Expr Expr::substExpr(const std::vector<Expr>& oldTerms,
-                     const std::vector<Expr>& newTerms) const {
-  return ExprBuilder(*this).substExpr(oldTerms, newTerms);
-}
-
 }/* CVC4 namespace */
diff --git a/src/expr/expr.h b/src/expr/expr.h
index d99708991..19f02650e 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -10,8 +10,8 @@
  ** Reference-counted encapsulation of a pointer to an expression.
  **/
 
-#ifndef __CVC4_EXPR_H
-#define __CVC4_EXPR_H
+#ifndef __CVC4__EXPR_H
+#define __CVC4__EXPR_H
 
 #include <vector>
 #include <stdint.h>
@@ -74,9 +74,6 @@ public:
   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;
@@ -100,4 +97,4 @@ inline Kind Expr::getKind() const {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4_EXPR_H */
+#endif /* __CVC4__EXPR_H */
diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp
index bf572cfbc..be9c60199 100644
--- a/src/expr/expr_builder.cpp
+++ b/src/expr/expr_builder.cpp
@@ -157,14 +157,6 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) {
   return *this;
 }
 
-ExprBuilder& ExprBuilder::skolemExpr(int i) {
-  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;
@@ -217,37 +209,13 @@ void ExprBuilder::addChild(ExprValue* ev) {
   }
 }
 
-void ExprBuilder::collapse() {
+ExprBuilder& ExprBuilder::collapse() {
   if(d_nchildren == nchild_thresh) {
     vector<Expr>* v = new vector<Expr>();
     v->reserve(nchild_thresh + 5);
-    
+    //
   }
-}
-
-// not const
-ExprBuilder::operator Expr() {
-  // FIXME
-}
-
-AndExprBuilder   ExprBuilder::operator&&(Expr e) {
-  return AndExprBuilder(*this) && e;
-}
-
-OrExprBuilder    ExprBuilder::operator||(Expr e) {
-  return OrExprBuilder(*this) || e;
-}
-
-PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
-  return PlusExprBuilder(*this) + e;
-}
-
-PlusExprBuilder  ExprBuilder::operator- (Expr e) {
-  return PlusExprBuilder(*this) - e;
-}
-
-MultExprBuilder  ExprBuilder::operator* (Expr e) {
-  return MultExprBuilder(*this) * e;
+  return *this;
 }
 
 }/* CVC4 namespace */
diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h
index 97f18ca6d..13f196dd0 100644
--- a/src/expr/expr_builder.h
+++ b/src/expr/expr_builder.h
@@ -43,7 +43,7 @@ class ExprBuilder {
 
   void addChild(const Expr&);
   void addChild(ExprValue*);
-  void collapse();
+  ExprBuilder& collapse();
 
   typedef ExprValue** ev_iterator;
   typedef ExprValue const** const_ev_iterator;
@@ -74,12 +74,6 @@ public:
   ExprBuilder& iffExpr(const Expr& right);
   ExprBuilder& impExpr(const Expr& right);
   ExprBuilder& xorExpr(const Expr& right);
-  ExprBuilder& skolemExpr(int i);
-  ExprBuilder& substExpr(const std::vector<Expr>& oldTerms,
-                         const std::vector<Expr>& newTerms);
-  /*
-  ExprBuilder& substExpr(const ExprHashMap<Expr>& oldToNew);
-  */
 
   /* TODO design: these modify ExprBuilder */
   ExprBuilder& operator!() { return notExpr(); }
@@ -92,6 +86,7 @@ public:
 
   // For pushing sequences of children
   ExprBuilder& append(const std::vector<Expr>& children) { return append(children.begin(), children.end()); }
+  ExprBuilder& append(Expr child) { return append(&child, &(child)+1); }
   template <class Iterator> ExprBuilder& append(const Iterator& begin, const Iterator& end);
 
   operator Expr();// not const
@@ -102,71 +97,167 @@ public:
   PlusExprBuilder  operator- (Expr);
   MultExprBuilder  operator* (Expr);
 
+  friend class AndExprBuilder;
+  friend class OrExprBuilder;
+  friend class PlusExprBuilder;
+  friend class MultExprBuilder;
 };/* class ExprBuilder */
 
 class AndExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  AndExprBuilder(const ExprBuilder&);
+  AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != AND) {
+      d_eb.collapse();
+      d_eb.d_kind = AND;
+    }
+  }
 
   AndExprBuilder&   operator&&(Expr);
   OrExprBuilder     operator||(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class AndExprBuilder */
 
 class OrExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  OrExprBuilder(const ExprBuilder&);
+  OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != OR) {
+      d_eb.collapse();
+      d_eb.d_kind = OR;
+    }
+  }
 
   AndExprBuilder    operator&&(Expr);
   OrExprBuilder&    operator||(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class OrExprBuilder */
 
 class PlusExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  PlusExprBuilder(const ExprBuilder&);
+  PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != PLUS) {
+      d_eb.collapse();
+      d_eb.d_kind = PLUS;
+    }
+  }
 
   PlusExprBuilder&  operator+(Expr);
   PlusExprBuilder&  operator-(Expr);
   MultExprBuilder   operator*(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class PlusExprBuilder */
 
 class MultExprBuilder {
-  ExprManager* d_em;
+  ExprBuilder d_eb;
 
 public:
 
-  MultExprBuilder(const ExprBuilder&);
+  MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) {
+    if(d_eb.d_kind != MULT) {
+      d_eb.collapse();
+      d_eb.d_kind = MULT;
+    }
+  }
 
   PlusExprBuilder   operator+(Expr);
   PlusExprBuilder   operator-(Expr);
   MultExprBuilder&  operator*(Expr);
 
-  operator ExprBuilder();
+  operator ExprBuilder() { return d_eb; }
 
 };/* class MultExprBuilder */
 
 template <class Iterator>
-ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) {
+  return *this;
+}
+
+// not const
+inline ExprBuilder::operator Expr() {
+  // FIXME
+  return Expr::s_null;
+}
+
+inline AndExprBuilder   ExprBuilder::operator&&(Expr e) {
+  return AndExprBuilder(*this) && e;
+}
+
+inline OrExprBuilder    ExprBuilder::operator||(Expr e) {
+  return OrExprBuilder(*this) || e;
+}
+
+inline PlusExprBuilder  ExprBuilder::operator+ (Expr e) {
+  return PlusExprBuilder(*this) + e;
+}
+
+inline PlusExprBuilder  ExprBuilder::operator- (Expr e) {
+  return PlusExprBuilder(*this) - e;
+}
+
+inline MultExprBuilder  ExprBuilder::operator* (Expr e) {
+  return MultExprBuilder(*this) * e;
+}
+
+inline AndExprBuilder&  AndExprBuilder::operator&&(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+inline OrExprBuilder    AndExprBuilder::operator||(Expr e) {
+  return OrExprBuilder(d_eb.collapse()) || e;
+}
+
+inline AndExprBuilder   OrExprBuilder::operator&&(Expr e) {
+  return AndExprBuilder(d_eb.collapse()) && e;
+}
+
+inline OrExprBuilder&   OrExprBuilder::operator||(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) {
+  d_eb.append(e.negate());
   return *this;
 }
 
+inline MultExprBuilder  PlusExprBuilder::operator*(Expr e) {
+  return MultExprBuilder(d_eb.collapse()) * e;
+}
+
+inline PlusExprBuilder  MultExprBuilder::operator+(Expr e) {
+  return MultExprBuilder(d_eb.collapse()) + e;
+}
+
+inline PlusExprBuilder  MultExprBuilder::operator-(Expr e) {
+  return MultExprBuilder(d_eb.collapse()) - e;
+}
+
+inline MultExprBuilder& MultExprBuilder::operator*(Expr e) {
+  d_eb.append(e);
+  return *this;
+}
+
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__EXPR_BUILDER_H */
diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index a65a2f3cd..3aeab8049 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -12,7 +12,7 @@
 
 #include "expr_builder.h"
 #include "expr_manager.h"
-#include "cvc4_expr.h"
+#include "expr/expr.h"
 
 namespace CVC4 {