fixes and additions

19 files changed, 512 insertions, 351 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 90efb9cab..3f0d0b381 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -1,10 +1,11 @@
 INCLUDES = -I@srcdir@/include
 
-SUBDIRS = parser sat
+SUBDIRS = core parser sat
 
 lib_LTLIBRARIES = libcvc4.la
 
 libcvc4_la_LIBADD = \
+	core/libcore.a
 	parser/libparser.a
 	sat/minisat/libminisat.a
 
diff --git a/src/core/Makefile.am b/src/core/Makefile.am
new file mode 100644
index 000000000..043882f36
--- /dev/null
+++ b/src/core/Makefile.am
@@ -0,0 +1,7 @@
+INCLUDES = -I@srcdir@/../include
+
+noinst_LIBRARIES = libcore.a
+
+libcore_a_SOURCES = \
+	expr.cpp \
+	expr_value.cpp
diff --git a/src/core/expr.cpp b/src/core/expr.cpp
new file mode 100644
index 000000000..1af197f27
--- /dev/null
+++ b/src/core/expr.cpp
@@ -0,0 +1,103 @@
+/*********************                                           -*- C++ -*-  */
+/** expr.cpp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#include "expr.h"
+#include "expr_value.h"
+#include "expr_builder.h"
+
+namespace CVC4 {
+
+Expr Expr::s_null(0);
+
+Expr::Expr(ExprValue* ev)
+  : d_ev(ev) {
+  // FIXME: thread-safety
+  ++d_ev->d_rc;
+}
+
+Expr::Expr(const Expr& e) {
+  // FIXME: thread-safety
+  if((d_ev = e.d_ev))
+    ++d_ev->d_rc;
+}
+
+Expr::~Expr() {
+  // FIXME: thread-safety
+  --d_ev->d_rc;
+}
+
+Expr& Expr::operator=(const Expr& e) {
+  // FIXME: thread-safety
+  if(d_ev)
+    --d_ev->d_rc;
+  if((d_ev = e.d_ev))
+    ++d_ev->d_rc;
+  return *this;
+}
+
+ExprValue* Expr::operator->() {
+  return d_ev;
+}
+
+const ExprValue* Expr::operator->() const {
+  return d_ev;
+}
+
+uint64_t Expr::hash() const {
+  return d_ev->hash();
+}
+
+Expr Expr::eqExpr(const Expr& right) const {
+  return ExprBuilder(*this).eqExpr(right);
+}
+
+Expr Expr::notExpr() const {
+  return ExprBuilder(*this).notExpr();
+}
+
+Expr Expr::negate() const { // avoid double-negatives
+  return ExprBuilder(*this).negate();
+}
+
+Expr Expr::andExpr(const Expr& right) const {
+  return ExprBuilder(*this).andExpr(right);
+}
+
+Expr Expr::orExpr(const Expr& right) const {
+  return ExprBuilder(*this).orExpr(right);
+}
+
+Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const {
+  return ExprBuilder(*this).iteExpr(thenpart, elsepart);
+}
+
+Expr Expr::iffExpr(const Expr& right) const {
+  return ExprBuilder(*this).iffExpr(right);
+}
+
+Expr Expr::impExpr(const Expr& right) const {
+  return ExprBuilder(*this).impExpr(right);
+}
+
+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/core/expr_manager.cpp b/src/core/expr_manager.cpp
new file mode 100644
index 000000000..93903c3aa
--- /dev/null
+++ b/src/core/expr_manager.cpp
@@ -0,0 +1,49 @@
+/*********************                                           -*- C++ -*-  */
+/** expr_manager.cpp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#include <vector>
+#include "expr.h"
+#include "kind.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); }
+  */
+};
+
+} /* CVC4 namespace */
diff --git a/src/core/expr_value.cpp b/src/core/expr_value.cpp
new file mode 100644
index 000000000..b7c65023e
--- /dev/null
+++ b/src/core/expr_value.cpp
@@ -0,0 +1,61 @@
+/*********************
+/** expr_value.cpp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** An expression node.
+ **
+ ** Instances of this class are generally referenced through
+ ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the
+ ** reference count on ExprValue instances and
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#include "expr_value.h"
+
+namespace CVC4 {
+
+uint64_t ExprValue::hash() const {
+  uint64_t hash = d_kind;
+
+  for(const_iterator i = begin(); i != end(); ++i)
+    hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ i->hash();
+
+  return hash;
+}
+
+ExprValue::iterator ExprValue::begin() {
+  return d_children;
+}
+
+ExprValue::iterator ExprValue::end() {
+  return d_children + d_nchildren;
+}
+
+ExprValue::iterator ExprValue::rbegin() {
+  return d_children + d_nchildren - 1;
+}
+
+ExprValue::iterator ExprValue::rend() {
+  return d_children - 1;
+}
+
+ExprValue::const_iterator ExprValue::begin() const {
+  return d_children;
+}
+
+ExprValue::const_iterator ExprValue::end() const {
+  return d_children + d_nchildren;
+}
+
+ExprValue::const_iterator ExprValue::rbegin() const {
+  return d_children + d_nchildren - 1;
+}
+
+ExprValue::const_iterator ExprValue::rend() const {
+  return d_children - 1;
+}
+
+} /* CVC4 namespace */
diff --git a/src/include/debug.h b/src/include/debug.h
new file mode 100644
index 000000000..95e705bcb
--- /dev/null
+++ b/src/include/debug.h
@@ -0,0 +1,24 @@
+/*********************                                           -*- C++ -*-  */
+/** debug.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_DEBUG_H
+#define __CVC4_DEBUG_H
+
+#include <cassert>
+
+#ifdef DEBUG
+// the __builtin_expect() helps us if assert is built-in or a macro
+# define cvc4assert(x) assert(__builtin_expect((x), 1))
+#else
+// TODO: use a compiler annotation when assertions are off ?
+// (to improve optimization)
+# define cvc4assert(x)
+#endif /* DEBUG */
+
+#endif /* __CVC4_DEBUG_H */
diff --git a/src/include/exception.h b/src/include/exception.h
index 3502fdf0c..ce19b0d68 100644
--- a/src/include/exception.h
+++ b/src/include/exception.h
@@ -10,7 +10,7 @@
  **/
 
 #ifndef __CVC4_EXCEPTION_H
-#ifndef __CVC4_EXCEPTION_H
+#define __CVC4_EXCEPTION_H
 
 #include <string>
 #include <iostream>
diff --git a/src/include/expr.h b/src/include/expr.h
index 5e3559fd7..9ca449ce7 100644
--- a/src/include/expr.h
+++ b/src/include/expr.h
@@ -12,6 +12,9 @@
 #ifndef __CVC4_EXPR_H
 #define __CVC4_EXPR_H
 
+#include <vector>
+#include <stdint.h>
+
 namespace CVC4 {
 
 class ExprValue;
@@ -34,19 +37,39 @@ class Expr {
    *  Increments the reference count. */
   explicit Expr(ExprValue*);
 
+public:
+  Expr(const Expr&);
+
   /** Destructor.  Decrements the reference count and, if zero,
    *  collects the ExprValue. */
   ~Expr();
 
-public:
+  Expr& operator=(const Expr&);
+
   /** Access to the encapsulated expression.
    *  @return the encapsulated expression. */
   ExprValue* operator->();
 
-  /** Const access to the encapsulated expressoin.
+  /** Const access to the encapsulated expression.
    *  @return the encapsulated expression [const]. */
   const ExprValue* operator->() const;
 
+  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;
+
+  static Expr null() { return s_null; }
 };/* class Expr */
 
 } /* CVC4 namespace */
diff --git a/src/include/expr_builder.h b/src/include/expr_builder.h
index 59503aa4f..342834e37 100644
--- a/src/include/expr_builder.h
+++ b/src/include/expr_builder.h
@@ -43,6 +43,10 @@ class ExprBuilder {
 
 public:
 
+  ExprBuilder();
+  ExprBuilder(const Expr&);
+  ExprBuilder(const ExprBuilder&);
+
   // Compound expression constructors
   ExprBuilder& eqExpr(const Expr& right);
   ExprBuilder& notExpr();
diff --git a/src/include/expr_manager.h b/src/include/expr_manager.h
index 0c265f57f..5dae5b854 100644
--- a/src/include/expr_manager.h
+++ b/src/include/expr_manager.h
@@ -23,47 +23,29 @@ public:
   static ExprManager* currentEM() { return s_current; }
 
   // general expression-builders
-  Expr build(Kind kind);
-  Expr build(Kind kind, Expr child1);
-  Expr build(Kind kind, Expr child1, Expr child2);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9);
-  Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10);
+  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 build(Kind kind, std::vector<Expr> children);
+  Expr mkExpr(Kind kind, std::vector<Expr> children);
 
   // TODO: these use the current EM (but must be renamed)
   /*
-  static Expr build(Kind kind)
-  { currentEM()->build(kind); }
-  static Expr build(Kind kind, Expr child1);
-  { currentEM()->build(kind, child1); }
-  static Expr build(Kind kind, Expr child1, Expr child2);
-  { currentEM()->build(kind, child1, child2); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3);
-  { currentEM()->build(kind, child1, child2, child3); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
-  { currentEM()->build(kind, child1, child2, child3, child4); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9); }
-  static Expr build(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5, Expr child6, Expr child7, Expr child8, Expr child9, Expr child10);
-  { currentEM()->build(kind, child1, child2, child3, child4, child5, child6, child7, child8, child9, child10); }
-  // N-ary version
-  static Expr build(Kind kind, vector<Expr> children)
-  { currentEM()->build(kind, children); }
+  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); }
   */
 
   // do we want a varargs one?  perhaps not..
diff --git a/src/include/expr_value.h b/src/include/expr_value.h
index ca12b8e03..c15241ebf 100644
--- a/src/include/expr_value.h
+++ b/src/include/expr_value.h
@@ -16,6 +16,7 @@
 #ifndef __CVC4_EXPR_VALUE_H
 #define __CVC4_EXPR_VALUE_H
 
+#include <stdint.h>
 #include "expr.h"
 
 namespace CVC4 {
@@ -41,14 +42,12 @@ class ExprValue {
   /** Variable number of child nodes */
   Expr     d_children[0];
 
+  friend class Expr;
+
 public:
   /** Hash this expression.
    *  @return the hash value of this expression. */
-  unsigned hash() const;
-
-  /** Convert to (wrap in) an Expr.
-   *  @return an Expr pointing to this expression. */
-  operator Expr();
+  uint64_t hash() const;
 
   // Iterator support
 
diff --git a/src/include/kind.h b/src/include/kind.h
index 9307cc677..a015a6b71 100644
--- a/src/include/kind.h
+++ b/src/include/kind.h
@@ -22,7 +22,11 @@ enum Kind {
   XOR,
   NOT,
   PLUS,
-  MINUS
+  MINUS,
+  ITE,
+  IFF,
+  SKOLEM,
+  SUBST
 };/* enum Kind */
 
 }/* CVC4 namespace */
diff --git a/src/include/parser_temp.h b/src/include/parser_temp.h
deleted file mode 100644
index d64a770e4..000000000
--- a/src/include/parser_temp.h
+++ /dev/null
@@ -1,76 +0,0 @@
-/*********************                                           -*- C++ -*-  */
-/** parser_temp.h
- ** This file is part of the CVC4 prototype.
- **
- ** A temporary holder for data used with the parser.
- **
- ** The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- **/
-
-#ifndef __CVC4_PARSER_TEMP_H
-#define __CVC4_PARSER_TEMP_H
-
-#include <iostream>
-
-#include "expr.h"
-#include "exception.h"
-
-namespace CVC4 {
-
-  class ValidityChecker;
-
-  class ParserTemp {
-  private:
-    // Counter for uniqueID of bound variables
-    int d_uid;
-    // The main prompt when running interactive
-    std::string prompt1;
-    // The interactive prompt in the middle of a multi-line command
-    std::string prompt2;
-    // The currently used prompt
-    std::string prompt;
-  public:
-    ValidityChecker* vc;
-    std::istream* is;
-    // The current input line
-    int lineNum;
-    // File name
-    std::string fileName;
-    // The last parsed Expr
-    Expr expr;
-    // Whether we are done or not
-    bool done;
-    // Whether we are running interactive
-    bool interactive;
-    // Whether arrays are enabled for smt-lib format
-    bool arrFlag;
-    // Whether bit-vectors are enabled for smt-lib format
-    bool bvFlag;
-    // Size of bit-vectors for smt-lib format
-    int bvSize;
-    // Did we encounter a formula query (smtlib)
-    bool queryParsed;
-    // Default constructor
-    ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "),
-      prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { }
-    // Parser error handling (implemented in parser.cpp)
-    int error(const std::string& s);
-    // Get the next uniqueID as a string
-    std::string uniqueID() {
-      std::ostringstream ss;
-      ss << d_uid++;
-      return ss.str();
-    }
-    // Get the current prompt
-    std::string getPrompt() { return prompt; }
-    // Set the prompt to the main one
-    void setPrompt1() { prompt = prompt1; }
-    // Set the prompt to the secondary one
-    void setPrompt2() { prompt = prompt2; }
-  };
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4_PARSER_TEMP_H */
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 0ebcad8c7..8cf9f4a6d 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -10,9 +10,26 @@ libparser_a_SOURCES = \
 	parser.cpp
 
 BUILT_SOURCES = \
-	pl_scanner.lpp \
-	pl.ypp \
-	smtlib_scanner.lpp \
-	smtlib.ypp
+	pl_scanner.cpp \
+	pl.cpp \
+	pl.h \
+	smtlib_scanner.cpp \
+	smtlib.cpp \
+	smtlib.h
+
+# produce headers too
+AM_YFLAGS = -d
+
+pl_scanner.cpp: pl_scanner.lpp
+	$(LEX) $(AM_LFLAGS) $(LFLAGS) -P PL -o $@ $<
+smtlib_scanner.cpp: smtlib_scanner.lpp
+	$(LEX) $(AM_LFLAGS) $(LFLAGS) -P smtlib -o $@ $<
+
+pl_scanner.o: pl.h
+pl.cpp: pl.ypp
+	$(YACC) $(AM_YFLAGS) $(YFLAGS) -p PL -o $@ $<
 
 
+smtlib_scanner.o: smtlib.h
+smtlib.cpp: smtlib.ypp
+	$(YACC) $(AM_YFLAGS) $(YFLAGS) -p smtlib -o $@ $<
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
new file mode 100644
index 000000000..4444925e2
--- /dev/null
+++ b/src/parser/parser_state.h
@@ -0,0 +1,89 @@
+/*********************                                           -*- C++ -*-  */
+/** parser_state.h
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Extra state of the parser shared by the lexer and parser.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#ifndef __CVC4_PARSER_STATE_H
+#define __CVC4_PARSER_STATE_H
+
+#include <iostream>
+#include <sstream>
+#include "expr.h"
+#include "exception.h"
+
+namespace CVC4 {
+
+class ValidityChecker;
+
+class ParserState {
+private:
+  // Counter for uniqueID of bound variables
+  int d_uid;
+  // The main prompt when running interactive
+  std::string prompt1;
+  // The interactive prompt in the middle of a multi-line command
+  std::string prompt2;
+  // The currently used prompt
+  std::string prompt;
+public:
+  ValidityChecker* vc;
+  std::istream* is;
+  // The current input line
+  int lineNum;
+  // File name
+  std::string fileName;
+  // The last parsed Expr
+  Expr expr;
+  // Whether we are done or not
+  bool done;
+  // Whether we are running interactive
+  bool interactive;
+  // Whether arrays are enabled for smt-lib format
+  bool arrFlag;
+  // Whether bit-vectors are enabled for smt-lib format
+  bool bvFlag;
+  // Size of bit-vectors for smt-lib format
+  int bvSize;
+  // Did we encounter a formula query (smtlib)
+  bool queryParsed;
+  // Default constructor
+  ParserState() : d_uid(0),
+                  prompt1("CVC> "),
+                  prompt2("- "),
+                  prompt("CVC> "),
+                  vc(0),
+                  is(0),
+                  lineNum(1),
+                  fileName(),
+                  expr(Expr::null()),
+                  done(false),
+                  interactive(false),
+                  arrFlag(false),
+                  bvFlag(false),
+                  bvSize(0),
+                  queryParsed(false) { }
+  // Parser error handling (implemented in parser.cpp)
+  int error(const std::string& s);
+  // Get the next uniqueID as a string
+  std::string uniqueID() {
+    std::ostringstream ss;
+    ss << d_uid++;
+    return ss.str();
+  }
+  // Get the current prompt
+  std::string getPrompt() { return prompt; }
+  // Set the prompt to the main one
+  void setPrompt1() { prompt = prompt1; }
+  // Set the prompt to the secondary one
+  void setPrompt2() { prompt = prompt2; }
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4_PARSER_STATE_H */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index dfed55dbb..e9aeab78e 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -1,43 +1,32 @@
+/*********************                                           -*- C++ -*-  */
+/** smtlib.ypp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **
+ ** This file contains the bison code for the parser that reads in CVC
+ ** commands in the presentation language (hence "PL").
+ **/
+
 %{
-/*****************************************************************************/
-/*!
- * \file PL.y
- * 
- * Author: Sergey Berezin
- * 
- * Created: Feb 06 03:00:43 GMT 2003
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-/* PL.y
-   Aaron Stump, 4/14/01
-
-   This file contains the bison code for the parser that reads in CVC
-   commands in the presentation language (hence "PL").
-*/
 
 #include "vc.h"
 #include "parser_exception.h"
-#include "parser_temp.h"
-#include "rational.h"
+#include "parser_state.h"
+//#include "rational.h"
 
 // Exported shared data
 namespace CVC4 {
-  extern ParserTemp* parserTemp;
+  extern ParserState* parserState;
 }
 // Define shortcuts for various things
-#define TMP CVC4::parserTemp
-#define EXPR CVC4::parserTemp->expr
-#define VC (CVC4::parserTemp->vc)
+#define TMP CVC4::parserState
+#define EXPR CVC4::parserState->expr
+#define VC (CVC4::parserState->vc)
 #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -50,9 +39,9 @@ extern int PLlex(void);
 int PLerror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum
+  ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum
      << ": " << s;
-  return CVC4::parserTemp->error(ss.str());
+  return CVC4::parserState->error(ss.str());
 }
 
 
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index d203a1e9a..d70937e34 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -1,76 +1,34 @@
+/*********************                                           -*- C++ -*-  */
+/** pl_scanner.lpp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+%option interactive
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+%option prefix="PL"
+
 %{
-/*****************************************************************************/
-/*!
- * \file PL.lex
- * 
- * Author: Sergey Berezin
- * 
- * Created: Feb 06 03:00:43 GMT 2003
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
 
 #include <iostream>
-#include "parser_temp.h"
 #include "expr_manager.h" /* for the benefit of parsePL_defs.h */
-#include "parsePL_defs.h"
+#include "parser_state.h"
+#include "pl.h"
 #include "debug.h"
 
 namespace CVC4 {
-  extern ParserTemp* parserTemp;
+  extern ParserState* parserState;
 }
 
-/* prefixing hack from gdb (via automake docs) */
-#define	yymaxdepth PL_maxdepth
-#define	yyparse	PL_parse
-#define	yylex	PL_lex
-#define	yyerror	PL_error
-#define	yylval	PL_lval
-#define	yychar	PL_char
-#define	yydebug	PL_debug
-#define	yypact	PL_pact	
-#define	yyr1	PL_r1			
-#define	yyr2	PL_r2			
-#define	yydef	PL_def		
-#define	yychk	PL_chk		
-#define	yypgo	PL_pgo		
-#define	yyact	PL_act		
-#define	yyexca	PL_exca
-#define yyerrflag PL_errflag
-#define yynerrs	PL_nerrs
-#define	yyps	PL_ps
-#define	yypv	PL_pv
-#define	yys	PL_s
-#define	yy_yys	PL_yys
-#define	yystate	PL_state
-#define	yytmp	PL_tmp
-#define	yyv	PL_v
-#define	yy_yyv	PL_yyv
-#define	yyval	PL_val
-#define	yylloc	PL_lloc
-#define yyreds	PL_reds
-#define yytoks	PL_toks
-#define yylhs	PL_yylhs
-#define yylen	PL_yylen
-#define yydefred PL_yydefred
-#define yydgoto	PL_yydgoto
-#define yysindex PL_yysindex
-#define yyrindex PL_yyrindex
-#define yygindex PL_yygindex
-#define yytable	 PL_yytable
-#define yycheck	 PL_yycheck
-#define yyname   PL_yyname
-#define yyrule   PL_yyrule
-
 extern int PL_inputLine;
 extern char *PLtext;
 
@@ -81,11 +39,11 @@ static int PLinput(std::istream& is, char* buf, int size) {
   if(is) {
     // If interactive, read line by line; otherwise read as much as we
     // can gobble
-    if(CVC4::parserTemp->interactive) {
+    if(CVC4::parserState->interactive) {
       // Print the current prompt
-      std::cout << CVC4::parserTemp->getPrompt() << std::flush;
+      std::cout << CVC4::parserState->getPrompt() << std::flush;
       // Set the prompt to "middle of the command" one
-      CVC4::parserTemp->setPrompt2();
+      CVC4::parserState->setPrompt2();
       // Read the line
       is.getline(buf, size-1);
     } else // Set the terminator char to 0
@@ -110,7 +68,7 @@ static int PLinput(std::istream& is, char* buf, int size) {
 
 // Redefine the input buffer function to read from an istream
 #define YY_INPUT(buf,result,max_size) \
-  result = PLinput(*CVC4::parserTemp->is, buf, max_size);
+  result = PLinput(*CVC4::parserState->is, buf, max_size);
 
 int PL_bufSize() { return YY_BUF_SIZE; }
 YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; }
@@ -152,13 +110,6 @@ static std::string _string_lit;
 
 %}
 
-%option interactive
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
 %x	COMMENT
 %x	STRING_LITERAL
 
@@ -171,7 +122,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
 
-[\n]            { CVC4::parserTemp->lineNum++; }
+[\n]            { CVC4::parserState->lineNum++; }
 
 [ \t\r\f]	{ /* skip whitespace */ }
 
@@ -184,7 +135,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 "%"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC4::parserTemp->lineNum++; }
+                  CVC4::parserState->lineNum++; }
 <COMMENT>.	{ /* stay in comment mode */ }
 
 <INITIAL>"\""		{ BEGIN STRING_LITERAL; 
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index 1bc22675a..97f61e715 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -1,45 +1,34 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.y
- * 
- * Author: Clark Barrett
- * 
- * Created: Apr 30 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
-/* 
-   This file contains the bison code for the parser that reads in CVC
-   commands in SMT-LIB language.
-*/
+%{/*******************                                           -*- C++ -*-  */
+/** smtlib.ypp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **
+ ** This file contains the bison code for the parser that reads in CVC
+ ** commands in SMT-LIB language.
+ **/
 
 #include "vc.h"
 #include "parser_exception.h"
-#include "parser_temp.h"
+#include "parser_state.h"
 
 // Exported shared data
-namespace CVC4 {
+namespace CVC3 {
   extern ParserTemp* parserTemp;
 }
 // Define shortcuts for various things
-#define TMP CVC4::parserTemp
-#define EXPR CVC4::parserTemp->expr
-#define VC (CVC4::parserTemp->vc)
-#define ARRAYSENABLED (CVC4::parserTemp->arrFlag)
-#define BVENABLED (CVC4::parserTemp->bvFlag)
-#define BVSIZE (CVC4::parserTemp->bvSize)
-#define RAT(args) CVC4::newRational args
-#define QUERYPARSED CVC4::parserTemp->queryParsed
+#define TMP CVC3::parserTemp
+#define EXPR CVC3::parserTemp->expr
+#define VC (CVC3::parserTemp->vc)
+#define ARRAYSENABLED (CVC3::parserTemp->arrFlag)
+#define BVENABLED (CVC3::parserTemp->bvFlag)
+#define BVSIZE (CVC3::parserTemp->bvSize)
+#define RAT(args) CVC3::newRational args
+#define QUERYPARSED CVC3::parserTemp->queryParsed
 
 // Suppress the bogus warning suppression in bison (it generates
 // compile error)
@@ -51,9 +40,9 @@ extern int smtliblex(void);
 int smtliberror(const char *s)
 {
   std::ostringstream ss;
-  ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum
+  ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
      << ": " << s;
-  return CVC4::parserTemp->error(ss.str());
+  return CVC3::parserTemp->error(ss.str());
 }
 
 
@@ -66,9 +55,9 @@ int smtliberror(const char *s)
 %union {
   std::string *str;
   std::vector<std::string> *strvec;
-  CVC4::Expr *node;
-  std::vector<CVC4::Expr> *vec;
-  std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann;
+  CVC3::Expr *node;
+  std::vector<CVC3::Expr> *vec;
+  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
 };
 
 
@@ -1548,6 +1537,4 @@ fun_pred_symb:
     }
 ;
 
-
-
 %%
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index d5bdaaf26..b78b27a0d 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -1,76 +1,31 @@
-%{
-/*****************************************************************************/
-/*!
- * \file smtlib.lex
- * 
- * Author: Clark Barrett
- * 
- * Created: 2005
- *
- * <hr>
- *
- * License to use, copy, modify, sell and/or distribute this software
- * and its documentation for any purpose is hereby granted without
- * royalty, subject to the terms and conditions defined in the \ref
- * LICENSE file provided with this distribution.
- * 
- * <hr>
- * 
- */
-/*****************************************************************************/
+/*********************                                           -*- C++ -*-  */
+/** smtlib_scanner.lpp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Reference-counted encapsulation of a pointer to an expression.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
 
+%option interactive
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+%option prefix="smtlib"
+
+%{
 #include <iostream>
-#include "parser_temp.h"
-#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
-#include "parsesmtlib_defs.h"
+#include "smtlib.h"
 #include "debug.h"
 
 namespace CVC4 {
   extern ParserTemp* parserTemp;
 }
 
-/* prefixing hack from gdb (via automake docs) */
-#define	yymaxdepth smtlib_maxdepth
-#define	yyparse	smtlib_parse
-#define	yylex	smtlib_lex
-#define	yyerror	smtlib_error
-#define	yylval	smtlib_lval
-#define	yychar	smtlib_char
-#define	yydebug	smtlib_debug
-#define	yypact	smtlib_pact	
-#define	yyr1	smtlib_r1			
-#define	yyr2	smtlib_r2			
-#define	yydef	smtlib_def		
-#define	yychk	smtlib_chk		
-#define	yypgo	smtlib_pgo		
-#define	yyact	smtlib_act		
-#define	yyexca	smtlib_exca
-#define yyerrflag smtlib_errflag
-#define yynerrs	smtlib_nerrs
-#define	yyps	smtlib_ps
-#define	yypv	smtlib_pv
-#define	yys	smtlib_s
-#define	yy_yys	smtlib_yys
-#define	yystate	smtlib_state
-#define	yytmp	smtlib_tmp
-#define	yyv	smtlib_v
-#define	yy_yyv	smtlib_yyv
-#define	yyval	smtlib_val
-#define	yylloc	smtlib_lloc
-#define yyreds	smtlib_reds
-#define yytoks	smtlib_toks
-#define yylhs	smtlib_yylhs
-#define yylen	smtlib_yylen
-#define yydefred smtlib_yydefred
-#define yydgoto	smtlib_yydgoto
-#define yysindex smtlib_yysindex
-#define yyrindex smtlib_yyrindex
-#define yygindex smtlib_yygindex
-#define yytable	 smtlib_yytable
-#define yycheck	 smtlib_yycheck
-#define yyname   smtlib_yyname
-#define yyrule   smtlib_yyrule
-
 extern int smtlib_inputLine;
 extern char *smtlibtext;
 
@@ -152,13 +107,6 @@ static std::string _string_lit;
 
 %}
 
-%option interactive
-%option noyywrap
-%option nounput
-%option noreject
-%option noyymore
-%option yylineno
-
 %x	COMMENT
 %x	STRING_LITERAL
 %x      USER_VALUE
@@ -257,4 +205,3 @@ IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
 
 . { smtliberror("Illegal input character."); }
 %%
-