parsing/expr/command/result/various other fixes

9 files changed, 419 insertions, 291 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 256ebef0e..800afc990 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -2,12 +2,14 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@
 AM_CXXFLAGS = -Wall -fvisibility=hidden
 AM_CPPFLAGS = -D__BUILDING_CVC4LIB
 
-noinst_LTLIBRARIES = libparser.la
+nobase_lib_LTLIBRARIES = libcvc4parser.la
 
-libparser_la_SOURCES = \
+libcvc4parser_la_SOURCES = \
 	parser.cpp \
 	parser_state.cpp \
 	symbol_table.cpp \
+	pl_scanner.lpp \
+	pl.ypp \
 	smtlib_scanner.lpp \
 	smtlib.ypp
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 1bf0341f2..89276872c 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -10,17 +10,51 @@
  ** Parser implementation.
  **/
 
-#include "parser.h"
-#include "parser_state.h"
-#include "parser_exception.h"
+#include <iostream>
 
-namespace CVC4 {
+#include "parser/parser.h"
+#include "util/command.h"
+#include "util/assert.h"
+#include "parser/parser_state.h"
+#include "parser/parser_exception.h"
+
+int CVC4_PUBLIC smtlibparse();
+int CVC4_PUBLIC PLparse();
+extern "C" int smtlibdebug, PLdebug;
 
+using namespace std;
+using namespace CVC4;
+
+namespace CVC4 {
 namespace parser {
 
-ParserState *_global_parser_state;
+ParserState CVC4_PUBLIC *_global_parser_state = 0;
+
+bool Parser::done() const {
+  return _global_parser_state->done();
+}
+
+Command* Parser::parseNextCommand(bool verbose) {
+  switch(d_lang) {
+  case PL:
+    PLdebug = verbose;
+    PLparse();
+    cout << "getting command" << endl;
+    return _global_parser_state->getCommand();
+  case SMTLIB:
+    smtlibdebug = verbose;
+    smtlibparse();
+    return _global_parser_state->getCommand();
+  default:
+    Unhandled();
+  }
+  return new EmptyCommand;
+}
 
+Parser::~Parser() {
+  //delete d_data;
 }
 
+}/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 765fb0553..411e7760c 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -16,83 +16,84 @@
 #include <string>
 #include <iostream>
 
-namespace CVC4
-{
-namespace parser
-{
+#include "parser/language.h"
+#include "parser/parser_state.h"
+
+namespace CVC4 {
 
 // Forward declarations
 class Expr;
 class Command;
 class ExprManager;
-class ParserState;
+class SmtEngine;
+class Options;
+
+namespace parser {
 
 /**
- * The parser.
+ * The global pointer to ParserTemp.  Each instance of class Parser sets this pointer
+ * before any calls to the lexer.  We do it this way because flex and bison use global
+ * vars, and we want each Parser object to appear independent.
  */
-class Parser
-{
-  private:
+extern ParserState CVC4_PUBLIC *_global_parser_state;
 
-    /** Internal parser state we are keeping */
-    ParserState* d_data;
+/**
+ * The parser.
+ */
+class CVC4_PUBLIC Parser {
+ private:
 
-    /** Initialize the parser */
-    void initParser();
+  /** Internal parser state we are keeping */
+  //ParserState* d_data;
 
-    /** Remove the parser components */
-    void deleteParser();
+  /** Initialize the parser */
+  void initParser();
 
-  public:
+  /** Remove the parser components */
+  void deleteParser();
 
-    /** The supported input languages */
-    enum InputLanguage {
-      /** SMT-LIB language */
-      INPUT_SMTLIB,
-      /** CVC language */
-      INPUT_CVC
-    };
+  Language d_lang;
+  std::istream &d_in;
+  Options *d_opts;
 
-    /**
-     * Constructor for parsing out of a file.
-     * @param em the expression manager to use
-     * @param lang the language syntax to use
-     * @param file_name the file to parse
-     */
-    Parser(ExprManager* em, InputLanguage lang, const std::string& file_name);
+ public:
 
-    /**
-     * Destructor.
-     */
-    ~Parser();
+  /**
+   * Constructor for parsing out of a file.
+   * @param em the expression manager to use
+   * @param lang the language syntax to use
+   * @param file_name the file to parse
+   */
+  Parser(SmtEngine* smt, ExprManager* em, Language lang, std::istream& in, Options* opts) :
+    d_lang(lang), d_in(in), d_opts(opts) {
+    _global_parser_state = new ParserState(smt, em);
+    _global_parser_state->setInputStream(in);
+  }
 
-    /** Parse a command */
-    Command parseNextCommand();
+  /**
+   * Destructor.
+   */
+  ~Parser();
 
-    /** Parse an expression of the stream */
-    Expr parseNextExpression();
+  /** Parse a command */
+  Command* parseNextCommand(bool verbose = false);
 
-    // Check if we are done (end of input has been reached)
-    bool done() const;
+  /** Parse an expression of the stream */
+  Expr parseNextExpression();
 
-    // The same check can be done by using the class Parser's value as a Boolean
-    operator bool() const { return done(); }
+  // Check if we are done (end of input has been reached)
+  bool done() const;
 
-    /** Prints the location to the output stream */
-    void printLocation(std::ostream& out) const;
+  // The same check can be done by using the class Parser's value as a Boolean
+  operator bool() const { return done(); }
 
-    /** Reset any local data */
-    void reset();
+  /** Prints the location to the output stream */
+  void printLocation(std::ostream& out) const;
 
+  /** Reset any local data */
+  void reset();
 }; // end of class Parser
 
-/**
- * The global pointer to ParserTemp.  Each instance of class Parser sets this pointer
- * before any calls to the lexer.  We do it this way because flex and bison use global
- * vars, and we want each Parser object to appear independent.
- */
-extern ParserState* _global_parser_state;
-
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 25f1cfd78..db64107e1 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -11,14 +11,10 @@
 
 using namespace std;
 
-namespace CVC4
-{
+namespace CVC4 {
+namespace parser {
 
-namespace parser
-{
-
-int ParserState::read(char* buffer, int size)
-{
+int ParserState::read(char* buffer, int size) {
   if (d_input_stream) {
     // Read the characters and count them in result
     d_input_stream->read(buffer, size);
@@ -26,41 +22,29 @@ int ParserState::read(char* buffer, int size)
   } else return 0;
 }
 
-ParserState::ParserState() :
-  d_uid(0), d_prompt_main("CVC>"), d_prompt_continue("- "), d_prompt("CVC"), d_input_line(0), d_done(false)
-{
-
-}
-
-int ParserState::parseError(const std::string& s)
-{
+int ParserState::parseError(const std::string& s) {
   throw new ParserException(s);
 }
 
-string ParserState::getNextUniqueID()
-{
+string ParserState::getNextUniqueID() {
   ostringstream ss;
   ss << d_uid++;
   return ss.str();
 }
 
-string ParserState::getCurrentPrompt() const
-{
+string ParserState::getCurrentPrompt() const {
   return d_prompt;
 }
 
-void ParserState::setPromptMain()
-{
+void ParserState::setPromptMain() {
   d_prompt = d_prompt_main;
 }
 
-void ParserState::setPromptNextLine()
-{
+void ParserState::setPromptNextLine() {
   d_prompt = d_prompt_continue;
 }
 
-void ParserState::increaseLineNumber()
-{
+void ParserState::increaseLineNumber() {
   ++d_input_line;
   if (d_interactive) {
     std::cout << getCurrentPrompt();
@@ -68,17 +52,13 @@ void ParserState::increaseLineNumber()
   }
 }
 
-int ParserState::getLineNumber() const
-{
+int ParserState::getLineNumber() const {
   return d_input_line;
 }
 
-std::string ParserState::getFileName() const
-{
+std::string ParserState::getFileName() const {
   return d_file_name;
 }
 
-} // End namespace parser
-
-} // End namespace CVC3
-
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 8b18ff22f..cb4ee6834 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -19,169 +19,237 @@
 
 #include <vector>
 #include <iostream>
-#include "cvc4.h"
+#include <map>
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
 
-namespace CVC4
-{
-
-namespace parser
-{
+namespace CVC4 {
+namespace parser {
 
 /**
  * The state of the parser.
  */
-class ParserState
-{
-  public:
-
-    /** Possible status values of a benchmark */
-    enum BenchmarkStatus {
-      SATISFIABLE,
-      UNSATISFIABLE,
-      UNKNOWN
-    };
-
-    /** The default constructor. */
-    ParserState();
-
-    /** Parser error handling */
-    int parseError(const std::string& s);
-
-    /** Get the next uniqueID as a string */
-    std::string getNextUniqueID();
-
-    /** Get the current prompt */
-    std::string getCurrentPrompt() const;
-
-    /** Set the prompt to the main one */
-    void setPromptMain();
-
-    /** Set the prompt to the secondary one */
-    void setPromptNextLine();
-
-    /** Increases the current line number */
-    void increaseLineNumber();
-
-    /** Gets the line number */
-    int getLineNumber() const;
-
-    /** Gets the file we are parsing, if any */
-    std::string getFileName() const;
-
-    /**
-     * Parses the next chunk of input from the stream. Reads at most size characters
-     * from the input stream and copies them into the buffer.
-     * @param the buffer to put the read characters into
-     * @param size the max numer of character
-     */
-    int read(char* buffer, int size);
-
-    /**
-     * Makes room for a new string literal (empties the buffer).
-     */
-    void newStringLiteral();
-
-    /**
-     * Returns the current string literal.
-     */
-    std::string getStringLiteral() const;
-
-    /**
-     * Appends the first character of str to the string literal buffer. If
-     * is_escape is true, the first character should be '\' and second character
-     * is examined to determine the escaped character.
-     */
-    void appendCharToStringLiteral(const char* str, bool is_escape = false);
-
-    /**
-     * Sets the name of the benchmark.
-     */
-    void setBenchmarkName(const std::string bench_name);
-
-    /**
-     * Returns the benchmark name.
-     */
-    std::string getBenchmarkName() const;
-
-    /**
-     * Set the status of the parsed benchmark.
-     */
-    void setBenchmarkStatus(BenchmarkStatus status);
-
-    /**
-     * Get the status of the parsed benchmark.
-     */
-    BenchmarkStatus getBenchmarkStatus() const;
-
-    /**
-     * Set the logic of the benchmark.
-     */
-    void setBenchmarkLogic(const std::string logic);
-
-    /**
-     * Declare a unary predicate (Boolean variable).
-     */
-    void declareNewPredicate(const std::string pred_name);
-
-    /**
-     * Creates a new expression, given the kind and the children
-     */
-    CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr>& children);
-
-    /**
-     * Returns a new TRUE Boolean constant.
-     */
-    CVC4::Expr* getNewTrue() const;
-
-    /**
-     * Returns a new TRUE Boolean constant.
-     */
-    CVC4::Expr* getNewFalse() const;
-
-    /**
-     * Retruns a variable, given the name.
-     */
-    CVC4::Expr* getNewVariableByName(const std::string var_name) const;
-
-    /**
-     * Sets the command that is the result of the parser.
-     */
-    void setCommand(CVC4::Command* cmd);
-
-    /**
-     * Sets the interactive flag on/off. If on, every time we go to a new line
-     * (via increaseLineNumber()) the prompt will be printed to stdout.
-     */
-    void setInteractive(bool interactive = true);
-
-  private:
-
-    /** Counter for uniqueID of bound variables */
-    int d_uid;
-    /** The main prompt when running interactive */
-    std::string d_prompt_main;
-    /** The interactive prompt in the middle of a multiline command */
-    std::string d_prompt_continue;
-    /** The currently used prompt */
-    std::string d_prompt;
-    /** The expression manager we will be using */
-    ExprManager* d_expression_manager;
-    /** The stream we are reading off */
-    std::istream* d_input_stream;
-    /** The current input line */
-    unsigned d_input_line;
-    /** File we are parsing */
-    std::string d_file_name;
-    /** Whether we are done or not */
-    bool d_done;
-    /** Whether we are running in interactive mode */
-    bool d_interactive;
-
-    /** String to buffer the string literals */
-    std::string d_string_buffer;
-
-    /** The name of the benchmark if any */
-    std::string d_benchmark_name;
+class ParserState {
+public:
+
+  /** Possible status values of a benchmark */
+  enum BenchmarkStatus {
+    SATISFIABLE,
+    UNSATISFIABLE,
+    UNKNOWN
+  };
+
+  /** The default constructor. */
+  ParserState(SmtEngine* smt, ExprManager* em) : d_uid(0), d_prompt_main("CVC>"), d_prompt_continue("- "), d_prompt("CVC"), d_expressionManager(em), d_smtEngine(smt), d_input_line(0), d_done(false) {}
+
+  /** Parser error handling */
+  int parseError(const std::string& s);
+
+  /** Get the next uniqueID as a string */
+  std::string getNextUniqueID();
+
+  /** Get the current prompt */
+  std::string getCurrentPrompt() const;
+
+  /** Set the prompt to the main one */
+  void setPromptMain();
+
+  /** Set the prompt to the secondary one */
+  void setPromptNextLine();
+
+  /** Increases the current line number */
+  void increaseLineNumber();
+
+  /** Gets the line number */
+  int getLineNumber() const;
+
+  /** Gets the file we are parsing, if any */
+  std::string getFileName() const;
+
+  /**
+   * Are we done yet?
+   */
+  bool done() const { return d_done; }
+
+  /**
+   * We are done.
+   */
+  void setDone() { d_done = true; }
+
+  /**
+   * Parses the next chunk of input from the stream. Reads at most size characters
+   * from the input stream and copies them into the buffer.
+   * @param the buffer to put the read characters into
+   * @param size the max numer of character
+   */
+  int read(char* buffer, int size);
+
+  /**
+   * Makes room for a new string literal (empties the buffer).
+   */
+  void newStringLiteral() { d_string_buffer.clear(); }
+
+  /**
+   * Returns the current string literal.
+   */
+  std::string getStringLiteral() const { return d_string_buffer; }
+
+  /**
+   * Appends the first character of str to the string literal buffer. If
+   * is_escape is true, the first character should be '\' and second character
+   * is examined to determine the escaped character.
+   */
+  void appendCharToStringLiteral(const char* str, bool is_escape = false) {
+    if(is_escape) {
+      // fixme
+    } else d_string_buffer += str[0];
+  }
+
+  /**
+   * Sets the name of the benchmark.
+   */
+  void setBenchmarkName(const std::string bench_name) { d_benchmark_name = bench_name; }
+
+  /**
+   * Returns the benchmark name.
+   */
+  std::string getBenchmarkName() const { return d_benchmark_name; }
+
+  /**
+   * Set the status of the parsed benchmark.
+   */
+  void setBenchmarkStatus(BenchmarkStatus status) { d_status = status; }
+
+  /**
+   * Get the status of the parsed benchmark.
+   */
+  BenchmarkStatus getBenchmarkStatus() const { return d_status; }
+
+  /**
+   * Set the logic of the benchmark.
+   */
+  void setBenchmarkLogic(const std::string logic) { d_logic = logic; }
+
+  /**
+   * Declare a unary predicate (Boolean variable).
+   */
+  void declareNewPredicate(const std::string pred_name) {
+    d_preds.insert( make_pair(pred_name, d_expressionManager->mkExpr(VARIABLE)) );
+  }
+
+  /**
+   * Creates a new expression, given the kind and the children
+   */
+  CVC4::Expr* newExpression(CVC4::Kind kind, std::vector<CVC4::Expr>& children) {
+    return new Expr(d_expressionManager->mkExpr(kind, children));
+  }
+
+  /**
+   * Returns a new TRUE Boolean constant.
+   */
+  CVC4::Expr* getNewTrue() { return new Expr(d_expressionManager->mkExpr(TRUE)); }
+
+  /**
+   * Returns a new TRUE Boolean constant.
+   */
+  CVC4::Expr* getNewFalse() { return new Expr(d_expressionManager->mkExpr(FALSE)); }
+
+  /**
+   * Returns a variable, given the name.
+   */
+  CVC4::Expr* getNewVariableByName(const std::string var_name) const {
+    std::map<std::string, Expr>::const_iterator i = d_preds.find(var_name);
+    return (i == d_preds.end()) ? 0 : new Expr(i->second);
+  }
+
+  /**
+   * Sets the command that is the result of the parser.
+   */
+  void setCommand(CVC4::Command* cmd) { d_command = cmd; }
+
+  /**
+   * Gets the command that is the result of the parser.
+   */
+  CVC4::Command* getCommand() { return d_command; }
+
+  /**
+   * Sets the interactive flag on/off. If on, every time we go to a new line
+   * (via increaseLineNumber()) the prompt will be printed to stdout.
+   */
+  void setInteractive(bool interactive = true);
+
+  /**
+   * Gets the value of the interactive flag.
+   */
+  bool interactive() { return d_interactive; }
+
+  /**
+   * Gets the SMT Engine
+   */
+  CVC4::SmtEngine* getSmtEngine() { return d_smtEngine; }
+
+  /**
+   * Sets the SMT Engine
+   */
+  void setSmtEngine(CVC4::SmtEngine* smtEngine) { d_smtEngine = smtEngine; }
+
+  /**
+   * Gets the Expression Manager
+   */
+  CVC4::ExprManager* getExpressionManager() { return d_expressionManager; }
+
+  /**
+   * Sets the Expression Manager
+   */
+  void setExpressionManager(CVC4::ExprManager* exprMgr) { d_expressionManager = exprMgr; }
+
+  /**
+   * Sets the input stream
+   */
+  void setInputStream(std::istream& in) { d_input_stream = &in; }
+
+private:
+
+  /** Counter for uniqueID of bound variables */
+  int d_uid;
+  /** The main prompt when running interactive */
+  std::string d_prompt_main;
+  /** The interactive prompt in the middle of a multiline command */
+  std::string d_prompt_continue;
+  /** The currently used prompt */
+  std::string d_prompt;
+  /** The expression manager we will be using */
+  ExprManager* d_expressionManager;
+  /** The smt engine we will be using */
+  SmtEngine* d_smtEngine;
+  /** The stream we are reading off */
+  std::istream* d_input_stream;
+  /** The current input line */
+  unsigned d_input_line;
+  /** File we are parsing */
+  std::string d_file_name;
+  /** Whether we are done or not */
+  bool d_done;
+  /** Whether we are running in interactive mode */
+  bool d_interactive;
+
+  /** String to buffer the string literals */
+  std::string d_string_buffer;
+
+  /** The name of the benchmark if any */
+  std::string d_benchmark_name;
+
+  /** The benchmark's status */
+  BenchmarkStatus d_status;
+
+  /** The benchmark's logic */
+  std::string d_logic;
+
+  /** declared predicates */
+  std::map<std::string, Expr> d_preds;
+
+  /** result of parser */
+  Command* d_command;
 };
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index 2668eabb8..f0bc21942 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -1,4 +1,4 @@
-/*********************                                           -*- C++ -*-  */
+%{/*******************                                           -*- C++ -*-  */
 /** pl.ypp
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
@@ -11,12 +11,13 @@
  ** commands in the presentation language (hence "PL").
  **/
 
-%{
-
+#define YYDEBUG 1
 
 #include <list>
 #include <vector>
 #include <string>
+#include <ostream>
+#include <sstream>
 
 #include "smt/smt_engine.h"
 #include "parser/parser_exception.h"
@@ -30,16 +31,15 @@
 // Exported shared data
 namespace CVC4 {
   namespace parser {
-    extern ParserState* parserState;
+    extern ParserState* _global_parser_state;;
   }/* CVC4::parser namespace */
-}/* CVC4 hnamespace */
+}/* CVC4 namespace */
 
 // Define shortcuts for various things
-// #define TMP CVC4::parser::parserState
-// #define EXPR CVC4::parser::parserState->expr
-#define SMT_ENGINE (CVC4::parser::parserState->smtEngine)
-#define EXPR_MANAGER (CVC4::parser::parserState->exprManager)
-#define SYMBOL_TABLE (CVC4::parser::parserState->symbolTable)
+// #define TMP CVC4::parser::_global_parser_state
+// #define EXPR CVC4::parser::_global_parser_state->expr
+#define SMT_ENGINE (CVC4::parser::_global_parser_state->getSmtEngine())
+#define EXPR_MANAGER (CVC4::parser::_global_parser_state->getExpressionManager())
 // #define RAT(args) CVC4::newRational args
 
 // Suppress the bogus warning suppression in bison (it generates
@@ -49,15 +49,17 @@ namespace CVC4 {
 /* stuff that lives in PL.lex */
 extern int PLlex(void);
 
-int PLerror(const char *s)
-{
+int PLerror(const char *s) {
   std::ostringstream ss;
-  ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum
-     << ": " << s;
-  CVC4::parser::parserState->error(ss.str());
+  ss << CVC4::parser::_global_parser_state->getFileName() << ":"
+     << CVC4::parser::_global_parser_state->getLineNumber() << ": " << s;
+  CVC4::parser::_global_parser_state->parseError(ss.str());
   return 0;// dead code; error() above throws an exception
 }
 
+// make the entry point public
+int CVC4_PUBLIC PLparse(void *YYPARSE_PARAM);
+
 #define YYLTYPE_IS_TRIVIAL 1
 #define YYMAXDEPTH 10485760
 /* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */
@@ -297,27 +299,40 @@ using namespace CVC4;
 cmd:       
     ASSERT_TOK Expr { 
       $$ = new AssertCommand(*$2);
+      CVC4::parser::_global_parser_state->setCommand($$);
       delete $2;
     } 
   | QUERY_TOK Expr { 
       $$ = new QueryCommand(*$2);
+      CVC4::parser::_global_parser_state->setCommand($$);
       delete $2;
     }
   | CHECKSAT_TOK Expr {
       $$ = new CheckSatCommand(*$2);
+      CVC4::parser::_global_parser_state->setCommand($$);
       delete $2;
     }
   | CHECKSAT_TOK {
       $$ = new CheckSatCommand();
+      CVC4::parser::_global_parser_state->setCommand($$);
     } 
   | IdentifierList ':' Type { // variable/constant declaration
       // FIXME: assuming Type is BOOLEAN
-      SYMBOL_TABLE->defineVarList($1, (const void *)0);
+      for(std::list<std::string>::iterator i = $1->begin(); i != $1->end(); ++i)
+        CVC4::parser::_global_parser_state->declareNewPredicate(*i);
+      delete $1;
+      CVC4::parser::_global_parser_state->setCommand(new EmptyCommand());
+    }
+  | DONE_TOK {
+      CVC4::parser::_global_parser_state->setCommand(new EmptyCommand());
+      CVC4::parser::_global_parser_state->setDone();
+      YYACCEPT;
     }
 
 Expr:	
     Identifier { 
-      $$ = new Expr(SYMBOL_TABLE->lookupVar($1)); 
+      $$ = CVC4::parser::_global_parser_state->getNewVariableByName(*$1);
+      delete $1;
     }
   | TRUELIT_TOK {
       $$ = new Expr(EXPR_MANAGER->mkExpr(TRUE));
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index 3b0f79a42..b7b27c4b0 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -32,7 +32,7 @@
 
 namespace CVC4 {
   namespace parser {
-    extern ParserState* parserState;
+    extern ParserState* _global_parser_state;
   }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
@@ -46,23 +46,27 @@ 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::parser::parserState->interactive) {
+    if(CVC4::parser::_global_parser_state->interactive()) {
       // Print the current prompt
-      std::cout << CVC4::parser::parserState->getPrompt() << std::flush;
+      std::cout << CVC4::parser::_global_parser_state->getCurrentPrompt() << std::flush;
       // Set the prompt to "middle of the command" one
-      CVC4::parser::parserState->setPrompt2();
+      CVC4::parser::_global_parser_state->setPromptNextLine();
       // Read the line
-      is.getline(buf, size-1);
+      is.getline(buf, size - 1);
     } else // Set the terminator char to 0
-      is.getline(buf, size-1, 0);
+      is.getline(buf, size - 1, 0);
     // If failbit is set, but eof is not, it means the line simply
     // didn't fit; so we clear the state and keep on reading.
     bool partialStr = is.fail() && !is.eof();
     if(partialStr)
       is.clear();
 
-    for(res = 0; res<size && buf[res] != 0; res++);
-    if(res == size) PLerror("Lexer bug: overfilled the buffer");
+    for(res = 0; res < size && buf[res] != 0; ++res)
+      ;
+
+    if(res == size)
+      PLerror("Lexer bug: overfilled the buffer");
+
     if(!partialStr) { // Insert \n into the buffer
       buf[res++] = '\n';
       buf[res] = '\0';
@@ -74,8 +78,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::parser::parserState->is, buf, max_size);
+#define YY_INPUT(buffer, result, max_size) result = CVC4::parser::_global_parser_state->read(buffer, max_size);
 
 int PL_bufSize() { return YY_BUF_SIZE; }
 YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; }
@@ -129,7 +132,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 %%
 
-[\n]            { CVC4::parser::parserState->lineNum++; }
+[\n]            { CVC4::parser::_global_parser_state->increaseLineNumber(); }
 
 [ \t\r\f]	{ /* skip whitespace */ }
 
@@ -142,7 +145,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
 
 "%"		{ BEGIN COMMENT; }
 <COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC4::parser::parserState->lineNum++; }
+                  CVC4::parser::_global_parser_state->increaseLineNumber(); }
 <COMMENT>.	{ /* stay in comment mode */ }
 
 <INITIAL>"\""		{ BEGIN STRING_LITERAL; 
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index b1aeaa570..1210d8817 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,15 +11,23 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "cvc4.h"
+#define YYDEBUG 1
+
+#include <string>
+#include <ostream>
+#include <sstream>
+
 #include "parser_state.h"
+#include "smt/smt_engine.h"
+#include "util/command.h"
+#include "smtlib.hpp"
 
 // Exported shared data
 namespace CVC4 {
 namespace parser {
   extern ParserState* _global_parser_state;
-}
-}
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
 using namespace std;
 using namespace CVC4;
@@ -32,7 +40,16 @@ using namespace CVC4::parser;
 extern int smtliblex(void);
 
 /** Error call */ 
-int smtliberror(const char *s) { return _global_parser_state->parseError(s); }
+int smtliberror(const char *s) {
+  std::ostringstream ss;
+  ss << CVC4::parser::_global_parser_state->getFileName() << ":"
+     << CVC4::parser::_global_parser_state->getLineNumber() << ": " << s;
+  CVC4::parser::_global_parser_state->parseError(ss.str());
+  return 0;// dead code; error() above throws an exception
+}
+
+// make the entry point public
+int CVC4_PUBLIC smtlibparse(void *YYPARSE_PARAM);
 
 #define YYLTYPE_IS_TRIVIAL 1
 #define YYMAXDEPTH 10485760
@@ -112,8 +129,14 @@ benchmark:
     LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK {
       _global_parser_state->setBenchmarkName(*$3);
       _global_parser_state->setCommand($4);
-    }    
-  | EOF_TOK { _global_parser_state->setCommand(new EmptyCommand()); }
+      _global_parser_state->setDone();
+      YYACCEPT;
+    }
+  | EOF_TOK {
+      _global_parser_state->setCommand(new EmptyCommand());
+      _global_parser_state->setDone();
+      YYACCEPT;
+    }
 ; 
 
 bench_name: SYM_TOK;
@@ -160,7 +183,7 @@ an_formulas:
 
 an_formula:
     an_atom
-  | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; } 
+    | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); std::cout << "we have an expr: " << *$$ << std::endl; delete $3; } 
 ;
 
 connective:
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index 70026bd4c..e9a58b1a9 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -22,12 +22,14 @@
 
 #include <iostream>
 #include "parser_state.h"
+#include "smt/smt_engine.h"
+#include "util/command.h"
 #include "smtlib.hpp"
 
 namespace CVC4 {
-namespace parser {
-  extern ParserState* _global_parser_state;
-}
+  namespace parser {
+    extern ParserState* _global_parser_state;
+  }
 }
 
 using CVC4::parser::_global_parser_state;
@@ -42,7 +44,7 @@ extern char *smtlibtext;
 
 %x COMMENT
 %x STRING_LITERAL
-%x SYM_TOK
+ //%x SYM_TOK
 %x USER_VALUE
 
 LETTER	([a-zA-Z])