Enough parsing for tonight. Added:

* Everything goes through the ParserState instead of coding in lex/yacc files
* Bare Boolean SMT lexer/parser
* Basic commands
To be completed: ParserState method implementations, parser.h/parser.cpp, make it compile and run...

9 files changed, 509 insertions, 1808 deletions

diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index 8d8730d68..256ebef0e 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -8,10 +8,8 @@ libparser_la_SOURCES = \
 	parser.cpp \
 	parser_state.cpp \
 	symbol_table.cpp \
-	pl_scanner.lpp \
-	pl.ypp
-#	smtlib_scanner.lpp \
-#	smtlib.ypp
+	smtlib_scanner.lpp \
+	smtlib.ypp
 
 BUILT_SOURCES = \
 	pl_scanner.cpp \
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 42ff506fa..1bf0341f2 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -10,85 +10,17 @@
  ** Parser implementation.
  **/
 
-#include "parser/parser.h"
-#include "parser/parser_state.h"
-#include "parser/parser_exception.h"
-#include "parser/pl.hpp"
-//#include "parser/smtlib.hpp"
-
-// The communication entry points of the actual parsers
-
-// for presentation language (PL.y and PL.lex)
-extern int PLparse(); 
-extern void *PL_createBuffer(int);
-extern void PL_deleteBuffer(void *);
-extern void PL_switchToBuffer(void *);
-extern int PL_bufSize();
-extern void *PL_bufState();
-void PL_setInteractive(bool);
-
-// for smtlib language (smtlib.y and smtlib.lex)
-extern int smtlibparse(); 
-extern void *smtlib_createBuffer(int);
-extern void smtlib_deleteBuffer(void *);
-extern void smtlib_switchToBuffer(void *);
-extern int smtlib_bufSize();
-extern void *smtlibBufState();
-void smtlib_setInteractive(bool);
+#include "parser.h"
+#include "parser_state.h"
+#include "parser_exception.h"
 
 namespace CVC4 {
-namespace parser {
-
-ParserState *parserState;
 
-Parser::Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive) throw()
-  : d_smt(smt),
-    d_is(is),
-    d_opts(opts),
-    d_lang(lang),
-    d_interactive(interactive),
-    d_buffer(0) {
-
-  parserState->lineNum = 1;
-  switch(d_lang) {
-  case PL:
-    d_buffer = ::PL_createBuffer(::PL_bufSize());
-    break;
-  case SMTLIB:
-    //d_buffer = ::smtlib_createBuffer(::smtlib_bufSize());
-    break;
-  default:
-    Unhandled();
-  }
-}
-
-Parser::~Parser() throw() {
-  switch(d_lang) {
-  case PL:
-    ::PL_deleteBuffer(d_buffer);
-    break;
-  case SMTLIB:
-    //::smtlib_deleteBuffer(d_buffer);
-    break;
-  default:
-    Unhandled();
-  }
-}
-
-CVC4::Command* Parser::next() throw() {
-  return 0;
-}
-
-bool Parser::done() const throw() {
-  return false;
-}
+namespace parser {
 
-void Parser::printLocation(std::ostream & out) const throw() {
-}
+ParserState *_global_parser_state;
 
-void Parser::reset() throw() {
 }
 
-
-}/* CVC4::parser namespace */
 }/* CVC4 namespace */
+
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8103238b3..765fb0553 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -13,46 +13,86 @@
 #ifndef __CVC4__PARSER__PARSER_H
 #define __CVC4__PARSER__PARSER_H
 
+#include <string>
 #include <iostream>
 
-#include "util/exception.h"
-#include "parser/language.h"
-#include "parser/parser_state.h"
-#include "util/command.h"
-#include "util/options.h"
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
-#include "util/assert.h"
-
-namespace CVC4 {
-namespace parser {
-
-class Parser {
-
-  CVC4::SmtEngine *d_smt;
-  std::istream &d_is;
-  CVC4::Options *d_opts;
-  Language d_lang;
-  bool d_interactive;
-  void *d_buffer;
-
-public:
-  // Constructors
-  Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw();
-  // Destructor
-  ~Parser() throw();
-  // Read the next command.
-  CVC4::Command* next() throw();
-  // Check if we are done (end of input has been reached)
-  bool done() const throw();
-  // The same check can be done by using the class Parser's value as
-  // a Boolean
-  operator bool() const throw() { return done(); }
-  void printLocation(std::ostream & out) const throw();
-  // Reset any local data that depends on SmtEngine
-  void reset() throw();
+namespace CVC4
+{
+namespace parser
+{
+
+// Forward declarations
+class Expr;
+class Command;
+class ExprManager;
+class ParserState;
+
+/**
+ * The parser.
+ */
+class Parser
+{
+  private:
+
+    /** Internal parser state we are keeping */
+    ParserState* d_data;
+
+    /** Initialize the parser */
+    void initParser();
+
+    /** Remove the parser components */
+    void deleteParser();
+
+  public:
+
+    /** The supported input languages */
+    enum InputLanguage {
+      /** SMT-LIB language */
+      INPUT_SMTLIB,
+      /** CVC language */
+      INPUT_CVC
+    };
+
+    /**
+     * 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);
+
+    /**
+     * Destructor.
+     */
+    ~Parser();
+
+    /** Parse a command */
+    Command parseNextCommand();
+
+    /** Parse an expression of the stream */
+    Expr parseNextExpression();
+
+    // Check if we are done (end of input has been reached)
+    bool done() const;
+
+    // The same check can be done by using the class Parser's value as a Boolean
+    operator bool() const { return done(); }
+
+    /** 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 654fbfe32..74def84cb 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -1,25 +1,86 @@
-/*********************                                           -*- C++ -*-  */
-/** parser_state.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.
- **
- ** Parser state implementation.
- **/
-
-#include <string>
-#include "parser/parser_state.h"
-#include "parser/parser_exception.h"
-
-namespace CVC4 {
-namespace parser {
-
-void ParserState::error(const std::string& s) throw(ParserException*) {
+/*
+ * parser_state.cpp
+ *
+ *  Created on: Nov 20, 2009
+ *      Author: dejan
+ */
+
+#include "parser_state.h"
+#include "parser_exception.h"
+#include <sstream>
+
+using namespace std;
+
+namespace CVC4
+{
+
+namespace parser
+{
+
+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);
+    return d_input_stream->gcount();
+  } 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)
+{
   throw new ParserException(s);
 }
 
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+string ParserState::getNextUniqueID()
+{
+  ostringstream ss;
+  ss << d_uid++;
+  return ss.str();
+}
+
+string ParserState::getCurrentPrompt() const
+{
+  return d_prompt;
+}
+
+void ParserState::setPromptMain()
+{
+  d_prompt = d_prompt_main;
+}
+
+void ParserState::setPromptNextLine()
+{
+  d_prompt = d_prompt_continue;
+}
+
+void ParserState::increaseLineNumber()
+{
+  ++d_input_line;
+}
+
+int ParserState::getLineNumber() const
+{
+  return d_input_line;
+}
+
+std::string ParserState::getFileName() const
+{
+  return d_file_name;
+}
+
+void ParserState::getParsedCommands(vector<Command*>& commands_vector)
+{
+  d_commands.swap(commands_vector);
+  d_commands.clear();
+}
+
+} // End namespace parser
+
+} // End namespace CVC3
+
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 2bcc08bef..fbb0afe70 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -17,86 +17,182 @@
 #ifndef __CVC4__PARSER__PARSER_STATE_H
 #define __CVC4__PARSER__PARSER_STATE_H
 
+#include <vector>
 #include <iostream>
-#include <sstream>
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
-#include "parser/symbol_table.h"
-#include "parser/parser_exception.h"
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class SmtEngine;
-
-namespace parser {
-
-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:
-  CVC4::SmtEngine* smtEngine;
-  CVC4::ExprManager* exprManager;
-  SymbolTable* symbolTable;
-  std::istream* is;
-  // The current input line
-  int lineNum;
-  // File name
-  std::string fileName;
-  // The last parsed Expr
-  CVC4::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() throw()
-    : d_uid(0),
-      prompt1("CVC> "),
-      prompt2("- "),
-      prompt("CVC> "),
-      smtEngine(0),
-      exprManager(0),
-      symbolTable(0),
-      is(0),
-      lineNum(1),
-      fileName(),
-      expr(CVC4::Expr::null()),
-      done(false),
-      interactive(false),
-      arrFlag(false),
-      bvFlag(false),
-      bvSize(0),
-      queryParsed(false) { }
-  // Parser error handling (implemented in parser.cpp)
-  void error(const std::string& s) throw(ParserException*) __attribute__((noreturn));
-  // Get the next uniqueID as a string
-  std::string uniqueID() throw() {
-    std::ostringstream ss;
-    ss << d_uid++;
-    return ss.str();
-  }
-  // Get the current prompt
-  std::string getPrompt() throw() { return prompt; }
-  // Set the prompt to the main one
-  void setPrompt1() throw() { prompt = prompt1; }
-  // Set the prompt to the secondary one
-  void setPrompt2() throw() { prompt = prompt2; }
+#include <util/command.h>
+
+namespace CVC4
+{
+
+class Expr;
+class ExprManager;
+
+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);
+
+    /**
+     * Returns the vector of parsed commands in the given vector (and forgets
+     * about them in the local state.
+     */
+    void getParsedCommands(std::vector<CVC4::Command*>& commands_vector);
+
+    /**
+     * Adds the commands in the given vector.
+     */
+    void addCommands(std::vector<CVC4::Command*>& commands_vector);
+
+    /**
+     * 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;
+
+    /**
+     * Add the command to the list of commands.
+     */
+    void addCommand(const Command* cmd);
+
+    /**
+     * 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;
+
+  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;
+
+    /** The vector of parsed commands if parsed as a whole */
+    std::vector<CVC4::Command*> d_commands;
 };
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
index a4aa7ef70..2668eabb8 100644
--- a/src/parser/pl.ypp
+++ b/src/parser/pl.ypp
@@ -14,8 +14,8 @@
 %{
 
 
-#include <vector>
 #include <list>
+#include <vector>
 #include <string>
 
 #include "smt/smt_engine.h"
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
index f3b866f2d..3b0f79a42 100644
--- a/src/parser/pl_scanner.lpp
+++ b/src/parser/pl_scanner.lpp
@@ -20,9 +20,9 @@
 
 %{
 
-#include <iostream>
-#include <vector>
 #include <list>
+#include <vector>
+#include <iostream>
 
 #include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */
 #include "util/command.h"
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
index e616b3a65..8e6d99f6e 100644
--- a/src/parser/smtlib.ypp
+++ b/src/parser/smtlib.ypp
@@ -11,42 +11,29 @@
  ** commands in SMT-LIB language.
  **/
 
-#include "smt/smt_engine.h"
-#include "parser/parser_exception.h"
+#include "cvc4_expr.h"
 #include "parser/parser_state.h"
-
-#include <vector>
+#include "util/command.h"
 
 // Exported shared data
 namespace CVC4 {
-  extern ParserState* parserState;
+namespace parser {
+  extern ParserState* _global_parser_state;
+}
 }
-// Define shortcuts for various things
-#define TMP CVC4::parserState
-#define EXPR CVC4::parserState->expr
-#define VC (CVC4::parserState->vc)
-#define ARRAYSENABLED (CVC4::parserState->arrFlag)
-#define BVENABLED (CVC4::parserState->bvFlag)
-#define BVSIZE (CVC4::parserState->bvSize)
-#define RAT(args) CVC4::newRational args
-#define QUERYPARSED CVC4::parserState->queryParsed
 
-// Suppress the bogus warning suppression in bison (it generates
-// compile error)
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+
+// Suppress the bogus warning suppression in bison (it generates compile error)
 #undef __GNUC_MINOR__
 
-/* stuff that lives in smtlib.lex */
+/** stuff that lives in smtlib_scanner.lpp */
 extern int smtliblex(void);
 
-int smtliberror(const char *s)
-{
-  std::ostringstream ss;
-  ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum
-     << ": " << s;
-  return CVC4::parserState->error(ss.str());
-}
-
-
+/** Error call */ 
+int smtliberror(const char *s) { return _global_parser_state->parseError(s); }
 
 #define YYLTYPE_IS_TRIVIAL 1
 #define YYMAXDEPTH 10485760
@@ -54,36 +41,29 @@ 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;
-};
 
+  std::string *p_string;
+  std::vector<std::string*> *p_string_vector;
+
+  CVC4::Expr *p_expression;
+  std::vector<CVC4::Expr*> *p_expression_vector;
+
+  CVC4::Command *p_command;
+  std::vector<CVC4::Command*> *p_command_vector;
 
-%start cmd
+  CVC4::parser::ParserState::BenchmarkStatus d_bench_status;
+  
+  CVC4::Kind d_kind;
+  
+};
 
-/* strings are for better error messages.  
-   "_TOK" is so macros don't conflict with kind names */
+%start benchmark
 
-%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls
-%type <vec> an_exprs an_formulas quant_vars an_terms fun_symb fun_pred_symb
-%type <node> pattern
-%type <node> benchmark bench_name bench_attribute
-%type <node> status fun_symb_decl fun_sig pred_symb_decl pred_sig
-%type <node> an_expr an_formula quant_var an_atom prop_atom
-%type <node> an_term basic_term sort_symb pred_symb
-%type <node> var fvar
-%type <str> logic_name quant_symb connective user_value attribute annotation
-%type <strvec> annotations
-%type <pat_ann> patterns_annotations
+%token <p_string> NUMERAL_TOK
+%token <p_string> SYM_TOK
+%token <p_string> STRING_TOK
+%token <p_string> USER_VAL_TOK
 
-%token <str> NUMERAL_TOK
-%token <str> SYM_TOK
-%token <str> STRING_TOK
-%token <str> AR_SYMB
-%token <str> USER_VAL_TOK
 %token TRUE_TOK
 %token FALSE_TOK
 %token ITE_TOK
@@ -94,20 +74,10 @@ int smtliberror(const char *s)
 %token OR_TOK
 %token XOR_TOK
 %token IFF_TOK
-%token EXISTS_TOK
-%token FORALL_TOK
 %token LET_TOK
 %token FLET_TOK
 %token NOTES_TOK
-%token CVC_COMMAND_TOK
 %token LOGIC_TOK
-%token COLON_TOK
-%token LBRACKET_TOK
-%token RBRACKET_TOK
-%token LCURBRACK_TOK
-%token RCURBRACK_TOK
-%token LPAREN_TOK
-%token RPAREN_TOK
 %token SAT_TOK
 %token UNSAT_TOK
 %token UNKNOWN_TOK
@@ -118,1424 +88,113 @@ int smtliberror(const char *s)
 %token EXTRASORTS_TOK
 %token EXTRAFUNS_TOK
 %token EXTRAPREDS_TOK
+%token DISTINCT_TOK
+%token COLON_TOK
+%token LBRACKET_TOK
+%token RBRACKET_TOK
+%token LPAREN_TOK
+%token RPAREN_TOK
 %token DOLLAR_TOK
 %token QUESTION_TOK
-%token DISTINCT_TOK
+
 %token EOF_TOK
-%token PAT_TOK
-%%
 
-cmd:
-    benchmark
-    {
-      EXPR = *$1;
-      delete $1;
-      YYACCEPT;
-    }
-;
+%type <p_string> bench_name logic_name pred_symb attribute user_value  
+%type <d_bench_status> status
+%type <p_expression> an_formula an_atom prop_atom
+%type <p_expression_vector> an_formulas;
+%type <d_kind> connective;
+
+%%
 
 benchmark:
-    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
-    {
-      if (!QUERYPARSED)
-        $4->push_back(CVC4::Expr(VC->listExpr("_CHECKSAT", CVC4::Expr(VC->idExpr("_TRUE_EXPR")))));
-      $$ = new CVC4::Expr(VC->listExpr("_SEQ",*$4));
-      delete $4;
-    }
+    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK {
+      _global_parser_state->setBenchmarkName(*$3);
+    }    
   | EOF_TOK
-    { 
-      TMP->done = true;
-      $$ = new CVC4::Expr();
-    }
-;
+; 
 
-bench_name:
-    SYM_TOK
-    {
-      $$ = NULL;
-      delete $1;
-    }
-;
+bench_name: SYM_TOK;
 
 bench_attributes:
     bench_attribute
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if ($1) {
-	$$->push_back(*$1);
-	delete $1;
-      }
-    }
   | bench_attributes bench_attribute
-    {
-      $$ = $1;
-      if ($2) {
-	$$->push_back(*$2);
-	delete $2;
-      }
-    }
 ;
 
 bench_attribute:
-    COLON_TOK ASSUMPTION_TOK an_formula
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_ASSERT", *$3));
-      delete $3;
-    }
-  | COLON_TOK FORMULA_TOK an_formula 
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_CHECKSAT", *$3));
-      QUERYPARSED = true;
-      delete $3;
-    }
-  | COLON_TOK STATUS_TOK status 
-    {
-      $$ = NULL;
-    }
-  | COLON_TOK LOGIC_TOK logic_name 
-    {
-      ARRAYSENABLED = false;
-      BVENABLED = false;
-      CVC4::Expr cmd;
-      if (*$3 == "QF_UF") {
-        cmd = CVC4::Expr(VC->listExpr("_TYPE", VC->idExpr("U")));
-      }
-      else if (*$3 == "QF_A" ||
-               *$3 == "QF_AX") {
-        ARRAYSENABLED = true;
-        std::vector<CVC4::Expr> tmp;
-        tmp.push_back(VC->listExpr("_TYPE", VC->idExpr("Index")));
-        tmp.push_back(VC->listExpr("_TYPE", VC->idExpr("Element")));
-        tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"),
-                                   VC->listExpr("_ARRAY",
-                                                VC->idExpr("Index"),
-                                                VC->idExpr("Element"))));
-        cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp));
-      }
-      else if (*$3 == "QF_AUFLIA" ||
-               *$3 == "AUFLIA") {
-        ARRAYSENABLED = true;
-        std::vector<CVC4::Expr> tmp;
-        tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"),
-                                   VC->listExpr("_ARRAY",
-                                                VC->idExpr("_INT"),
-                                                VC->idExpr("_INT"))));
-        cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp));
-      }
-      else if (*$3 == "QF_AUFLIRA" ||
-               *$3 == "AUFLIRA" ||
-               *$3 == "QF_AUFNIRA" ||
-               *$3 == "AUFNIRA") {
-        ARRAYSENABLED = true;
-        std::vector<CVC4::Expr> tmp;
-        tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array1"),
-                                   VC->listExpr("_ARRAY",
-                                                VC->idExpr("_INT"),
-                                                VC->idExpr("_REAL"))));
-        tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array2"),
-                                   VC->listExpr("_ARRAY",
-                                                VC->idExpr("_INT"),
-                                                VC->idExpr("Array1"))));
-        cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp));
-      }
-      else if (*$3 == "QF_AUFBV" ||
-               *$3 == "QF_ABV") {
-        ARRAYSENABLED = true;
-        BVENABLED = true;
-//         $$ = new CVC4::Expr(VC->listExpr("_TYPEDEF", VC->idExpr("Array"),
-//                                          VC->listExpr("_ARRAY",
-//                                                       VC->listExpr("_BITVECTOR", VC->ratExpr(32)),
-//                                                       VC->listExpr("_BITVECTOR", VC->ratExpr(8)))));
-      }
-      else if (*$3 == "QF_BV" ||
-               *$3 == "QF_UFBV") {
-        BVENABLED = true;
-      }
-    // This enables the new arith for QF_LRA, but this results in assertion failures in DEBUG mode
-//       else if (*$3 == "QF_LRA") {
-//         cmd = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("arith-new"), VC->ratExpr(1)));
-//       }
-
-      CVC4::Expr cmd2;
-      if (*$3 == "AUFLIA" ||
-          *$3 == "AUFLIRA" ||
-          *$3 == "AUFNIRA" ||
-          *$3 == "LRA" ||
-          *$3 == "UFNIA") {
-        cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("quant-complete-inst"), VC->ratExpr(1)));
-      }
-//    else if (*$3 == "QF_NIA" ||
-//             *$3 == "QF_UFNRA") {
-//      cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("unknown-check-model"), VC->ratExpr(1)));
-//    }
-//       else if (*$3 == "QF_LIA" ||
-//                *$3 == "QF_AUFLIA" ||
-//                *$3 == "QF_AX") {
-//         cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("pp-budget"), VC->ratExpr(5000)));
-//       }
-
-      if (cmd.isNull()) {
-        if (cmd2.isNull()) {
-          $$ = NULL;
-        }
-        else $$ = new CVC4::Expr(cmd2);
-      }
-      else {
-        if (!cmd2.isNull()) {
-          cmd = CVC4::Expr(VC->listExpr("_SEQ", cmd, cmd2));
-        }
-        $$ = new CVC4::Expr(cmd);
-      }
-      delete $3;
-    }
-  | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_TYPE", *$4));
-      delete $4;
-    }
-  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_SEQ", *$4));
-      delete $4;
-    }
+  | COLON_TOK FORMULA_TOK an_formula  { _global_parser_state->addCommand(new CheckSatCommand(*$3)); delete $3; }  
+  | COLON_TOK STATUS_TOK status       { _global_parser_state->setBenchmarkStatus($3); } 
+  | COLON_TOK LOGIC_TOK logic_name    { _global_parser_state->setBenchmarkLogic(*$3); delete $3; } 
   | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_SEQ", *$4));
-      delete $4;
-    }
-  | COLON_TOK NOTES_TOK STRING_TOK
-    {
-      $$ = NULL;
-      delete $3;
-    }
-  | COLON_TOK CVC_COMMAND_TOK STRING_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_"+*$3)));
-      delete $3;
-    }
   | annotation
-    {
-      $$ = NULL;
-      delete $1;
-    }
-;
-
-logic_name:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      BVSIZE = atoi($3->c_str());
-      delete $3;
-      $$ = $1;
-    }
-  | SYM_TOK
-    {
-      $$ = $1;
-    }
-;
-
-status:
-    SAT_TOK { $$ = NULL; }
-  | UNSAT_TOK { $$ = NULL; }
-  | UNKNOWN_TOK { $$ = NULL; }
-;
-
-sort_symbs:
-    sort_symb 
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  | sort_symbs sort_symb
-    { 
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-fun_symb_decls:
-    fun_symb_decl
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    fun_symb_decls fun_symb_decl
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-fun_symb_decl:
-    LPAREN_TOK fun_sig annotations RPAREN_TOK
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK fun_sig RPAREN_TOK
-    {
-      $$ = $2;
-    }
-;
+;  
+ 
+logic_name: SYM_TOK;
 
-fun_sig:
-    fun_symb sort_symbs
-    {
-      if ($2->size() == 1) {
-        $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0]));
-      }
-      else {
-        CVC4::Expr tmp(VC->listExpr("_ARROW", *$2));
-        $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp));
-      }
-      delete $1;
-      delete $2;
-    }
+status: 
+    SAT_TOK     { $$ = ParserState::SATISFIABLE;   }
+  | UNSAT_TOK   { $$ = ParserState::UNSATISFIABLE; }
+  | UNKNOWN_TOK { $$ = ParserState::UNKNOWN;       }
 ;
 
 pred_symb_decls:
     pred_symb_decl
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    pred_symb_decls pred_symb_decl
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
+  | pred_symb_decls pred_symb_decl
 ;
 
 pred_symb_decl:
     LPAREN_TOK pred_sig annotations RPAREN_TOK
-    {
-      $$ = $2;
-      delete $3;
-    }
   | LPAREN_TOK pred_sig RPAREN_TOK
-    {
-      $$ = $2;
-    }
 ;
 
 pred_sig:
-    pred_symb sort_symbs
-    {
-      std::vector<CVC4::Expr> tmp(*$2);
-      tmp.push_back(VC->idExpr("_BOOLEAN"));
-      CVC4::Expr tmp2(VC->listExpr("_ARROW", tmp));
-      $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2));
-      delete $1;
-      delete $2;
-    }
-  | pred_symb
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1),
-                                       VC->idExpr("_BOOLEAN")));
-      delete $1;
-    }
+  pred_symb { _global_parser_state->declareNewPredicate(*$1); delete $1; } 
 ;
 
 an_formulas:
-    an_formula
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    an_formulas an_formula
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
+    an_formula             { $$ = new vector<Expr*>; $$->push_back($1); delete $1; }
+  | an_formulas an_formula { $$ = $1;                $$->push_back($2); delete $2; }
 ;
 
 an_formula:
     an_atom
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK connective an_formulas annotations RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr(*$2, *$3));
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK connective an_formulas RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr(*$2, *$3));
-      delete $2;
-      delete $3;
-    }
-  | LPAREN_TOK quant_symb quant_vars an_formula patterns_annotations RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4, VC->listExpr((*$5).first)));
-      delete $2;
-      delete $3;
-      delete $4;
-      delete $5;
-    }
-  | LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4));
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-;
-
-patterns_annotations:
-     pattern
-     {
-       $$ = new std::pair<std::vector<CVC4::Expr>, std::vector<std::string> >;
-       $$->first.push_back(*$1);
-       delete $1;
-     }
-     | annotation
-     {
-       $$ = new std::pair<std::vector<CVC4::Expr>, std::vector<std::string> >;
-       $$->second.push_back(*$1);
-       delete $1;
-     }
-     | patterns_annotations pattern
-     {
-       $1->first.push_back(*$2);
-       $$ = $1;
-       delete $2;
-     }
-     | patterns_annotations annotation
-     {
-       $1->second.push_back(*$2);
-       $$ = $1;
-       delete $2;
-     }
-
-pattern:
-     PAT_TOK LCURBRACK_TOK an_exprs RCURBRACK_TOK
-     {
-       $$ = new CVC4::Expr(VC->listExpr(*$3));
-       delete $3;
-     }
-
-quant_vars:
-    quant_var
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  | quant_vars quant_var
-    {
-      $1->push_back(*$2);
-      $$ = $1; 
-      delete $2;
-    }
-;
-
-quant_var: 
-    LPAREN_TOK var sort_symb RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr(*$2, *$3));
-      delete $2;
-      delete $3;
-    }
-;
-
-quant_symb:
-    EXISTS_TOK
-    {
-      $$ = new std::string("_EXISTS");
-    }
-  | FORALL_TOK
-    {
-      $$ = new std::string("_FORALL");
-    }
+  | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; } 
 ;
 
 connective:
-    NOT_TOK
-    {
-      $$ = new std::string("_NOT");
-    }
-  | IMPLIES_TOK
-    {
-      $$ = new std::string("_IMPLIES");
-    }
-  | IF_THEN_ELSE_TOK
-    {
-      $$ = new std::string("_IF");
-    }
-  | AND_TOK
-    {
-      $$ = new std::string("_AND");
-    }
-  | OR_TOK
-    {
-      $$ = new std::string("_OR");
-    }
-  | XOR_TOK
-    {
-      $$ = new std::string("_XOR");
-    }
-  | IFF_TOK
-    {
-      $$ = new std::string("_IFF");
-    }
+    NOT_TOK                  { $$ = NOT;     }
+  | IMPLIES_TOK              { $$ = IMPLIES; }
+  | IF_THEN_ELSE_TOK         { $$ = ITE;     }
+  | AND_TOK                  { $$ = AND;     }
+  | OR_TOK                   { $$ = OR;      } 
+  | XOR_TOK                  { $$ = XOR;     }
+  | IFF_TOK                  { $$ = IFF;     }
 ;
 
-an_atom:
-    prop_atom 
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK prop_atom annotations RPAREN_TOK 
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK pred_symb an_terms annotations RPAREN_TOK
-    {
-      if ($4->size() == 1 && (*$4)[0] == "transclose" &&
-          $3->size() == 2) {
-        $$ = new CVC4::Expr(VC->listExpr("_TRANS_CLOSURE",
-                                        *$2, (*$3)[0], (*$3)[1]));
-      }
-      else {
-        std::vector<CVC4::Expr> tmp;
-        tmp.push_back(*$2);
-        tmp.insert(tmp.end(), $3->begin(), $3->end());
-        $$ = new CVC4::Expr(VC->listExpr(tmp));
-      }
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK pred_symb an_terms RPAREN_TOK
-    {
-      std::vector<CVC4::Expr> tmp;
-      tmp.push_back(*$2);
-      tmp.insert(tmp.end(), $3->begin(), $3->end());
-      $$ = new CVC4::Expr(VC->listExpr(tmp));
-      delete $2;
-      delete $3;
-    }
-  | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3));
-
-//       std::vector<CVC4::Expr> tmp;
-//       tmp.push_back(*$2);
-//       tmp.insert(tmp.end(), $3->begin(), $3->end());
-//       $$ = new CVC4::Expr(VC->listExpr(tmp));
-//       for (unsigned i = 0; i < (*$3).size(); ++i) {
-//         tmp.push_back(($3)[i])
-// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
-// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
-// 	}
-//       }
-//       $$ = new CVC4::Expr(VC->listExpr("_AND", tmp));
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3));
-//       std::vector<CVC4::Expr> tmp;
-//       for (unsigned i = 0; i < (*$3).size(); ++i) {
-// 	for (unsigned j = i+1; j < (*$3).size(); ++j) {
-// 	  tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j]));
-// 	}
-//       }
-//       $$ = new CVC4::Expr(VC->listExpr("_AND", tmp));
-      delete $3;
-    }
-;
+an_atom: prop_atom;
 
 prop_atom:
-    TRUE_TOK
-    {
-      $$ = new CVC4::Expr(VC->idExpr("_TRUE_EXPR"));
-    }
-  | FALSE_TOK
-    { 
-      $$ = new CVC4::Expr(VC->idExpr("_FALSE_EXPR"));
-    }
-  | fvar
-    {
-      $$ = $1;
-    }
-  | pred_symb 
-    {
-      $$ = $1;
-    }
+    TRUE_TOK     { $$ = _global_parser_state->getNewTrue();                         }
+  | FALSE_TOK    { $$ = _global_parser_state->getNewFalse();                        }
+  | pred_symb    { $$ = _global_parser_state->getNewVariableByName(*$1); delete $1; }
 ;  
 
-an_terms:
-    an_term
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  | an_terms an_term
-    {
-      $1->push_back(*$2);
-      $$ = $1; 
-      delete $2;
-    }
-;
-
-an_term:
-    basic_term 
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK basic_term annotations RPAREN_TOK 
-    {
-      $$ = $2;
-      delete $3;
-    }
-  | LPAREN_TOK fun_symb an_terms annotations RPAREN_TOK
-    {
-      $2->insert($2->end(), $3->begin(), $3->end());
-      $$ = new CVC4::Expr(VC->listExpr(*$2));
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK fun_symb an_terms RPAREN_TOK
-    {
-      $2->insert($2->end(), $3->begin(), $3->end());
-      $$ = new CVC4::Expr(VC->listExpr(*$2));
-      delete $2;
-      delete $3;
-    }
-  | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_IF", *$3, *$4, *$5));
-      delete $3;
-      delete $4;
-      delete $5;
-      delete $6;
-    }
-  | LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK
-    {
-      $$ = new CVC4::Expr(VC->listExpr("_IF", *$3, *$4, *$5));
-      delete $3;
-      delete $4;
-      delete $5;
-    }
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_term annotations RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_term RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_term annotations RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_term RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-;
-
-basic_term:
-    var
-    {
-      $$ = $1;
-    }
-  | fun_symb 
-    {
-      if ($1->size() == 1) {
-        $$ = new CVC4::Expr(((*$1)[0]));
-      }
-      else {
-        $$ = new CVC4::Expr(VC->listExpr(*$1));
-      }
-      delete $1;
-    }
-;
-
 annotations:
     annotation
-    {
-      $$ = new std::vector<std::string>;
-      $$->push_back(*$1);
-      delete $1;
-    }
   | annotations annotation
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
   ;
   
-
 annotation:
-    attribute
-    { $$ = $1; }
-  | attribute user_value
-    { $$ = $1; }
-;
-
-user_value:
-    USER_VAL_TOK
-    {
-      $$ = NULL;
-      delete $1;
-    }
-;
-
-
-sort_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      if (BVENABLED && *$1 == "BitVec") {
-        $$ = new CVC4::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)));
-      }
-      else {
-        $$ = new CVC4::Expr(VC->listExpr(*$1, VC->ratExpr(*$3)));
-      }
-      delete $1;
-      delete $3;
-    }
-  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      if (BVENABLED && ARRAYSENABLED && *$1 == "Array") {
-        $$ = new CVC4::Expr(VC->listExpr("_ARRAY",
-                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)),
-                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$5))));
-      }
-      else {
-        $$ = new CVC4::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5)));
-      }
-      delete $1;
-      delete $3;
-      delete $5;
-    }
-  | SYM_TOK 
-    { 
-      if (*$1 == "Real") {
-	$$ = new CVC4::Expr(VC->idExpr("_REAL"));
-      } else if (*$1 == "Int") {
-	$$ = new CVC4::Expr(VC->idExpr("_INT"));
-      } else {
-	$$ = new CVC4::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-;
-
-pred_symb:
-    SYM_TOK
-    {
-      if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
-        $$ = new CVC4::Expr(VC->idExpr("_BVLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
-        $$ = new CVC4::Expr(VC->idExpr("_BVLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
-        $$ = new CVC4::Expr(VC->idExpr("_BVGE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
-        $$ = new CVC4::Expr(VC->idExpr("_BVGT"));
-      }
-      else if (BVENABLED && *$1 == "bvslt") {
-        $$ = new CVC4::Expr(VC->idExpr("_BVSLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
-        $$ = new CVC4::Expr(VC->idExpr("_BVSLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
-        $$ = new CVC4::Expr(VC->idExpr("_BVSGE"));
-      }
-      else if (BVENABLED && *$1 == "bvsgt") {
-        $$ = new CVC4::Expr(VC->idExpr("_BVSGT"));
-      }
-      else {
-        $$ = new CVC4::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-  | AR_SYMB 
-    { 
-      if ($1->length() == 1) {
-	switch ((*$1)[0]) {
-	  case '=': $$ = new CVC4::Expr(VC->idExpr("_EQ")); break;
-	  case '<': $$ = new CVC4::Expr(VC->idExpr("_LT")); break;
-	  case '>': $$ = new CVC4::Expr(VC->idExpr("_GT")); break;
-	  default: $$ = new CVC4::Expr(VC->idExpr(*$1)); break;
-	}
-      }
-      else {
-	if (*$1 == "<=") {
-	  $$ = new CVC4::Expr(VC->idExpr("_LE"));
-	} else if (*$1 == ">=") {
-	  $$ = new CVC4::Expr(VC->idExpr("_GE"));
-	}
-	else $$ = new CVC4::Expr(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-;
-
-fun_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if (BVENABLED && *$1 == "repeat") {
-        $$->push_back(VC->idExpr("_BVREPEAT"));
-      }
-      else if (BVENABLED && *$1 == "zero_extend") {
-        $$->push_back(VC->idExpr("_BVZEROEXTEND"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
-      else if (BVENABLED && *$1 == "rotate_left") {
-        $$->push_back(VC->idExpr("_BVROTL"));
-      }
-      else if (BVENABLED && *$1 == "rotate_right") {
-        $$->push_back(VC->idExpr("_BVROTR"));
-      }
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        int i = 2;
-        while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-        if ((*$1)[i] == '\0') {
-          $$->push_back(VC->idExpr("_BVCONST"));
-          $$->push_back(VC->ratExpr($1->substr(2), 10));
-        }
-        else $$->push_back(VC->idExpr(*$1));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      delete $1;
-      delete $3;
-    }
-  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if (BVENABLED && *$1 == "extract") {
-        $$->push_back(VC->idExpr("_EXTRACT"));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      $$->push_back(VC->ratExpr(*$5));
-      delete $1;
-      delete $3;
-      delete $5;
-    }
-  | SYM_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if (ARRAYSENABLED && *$1 == "select") {
-        $$->push_back(VC->idExpr("_READ"));
-      }
-      else if (ARRAYSENABLED && *$1 == "store") {
-        $$->push_back(VC->idExpr("_WRITE"));
-      }
-      else if (BVENABLED && *$1 == "bit0") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(0));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "bit1") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(1));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "concat") {
-        $$->push_back(VC->idExpr("_CONCAT"));
-      }
-      else if (BVENABLED && *$1 == "bvnot") {
-        $$->push_back(VC->idExpr("_BVNEG"));
-      }
-      else if (BVENABLED && *$1 == "bvand") {
-        $$->push_back(VC->idExpr("_BVAND"));
-      }
-      else if (BVENABLED && *$1 == "bvor") {
-        $$->push_back(VC->idExpr("_BVOR"));
-      }
-      else if (BVENABLED && *$1 == "bvneg") {
-        $$->push_back(VC->idExpr("_BVUMINUS"));
-      }
-      else if (BVENABLED && *$1 == "bvadd") {
-        $$->push_back(VC->idExpr("_BVPLUS"));
-      }
-      else if (BVENABLED && *$1 == "bvmul") {
-        $$->push_back(VC->idExpr("_BVMULT"));
-      }
-      else if (BVENABLED && *$1 == "bvudiv") {
-        $$->push_back(VC->idExpr("_BVUDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvurem") {
-        $$->push_back(VC->idExpr("_BVUREM"));
-      }
-      else if (BVENABLED && *$1 == "bvshl") {
-        $$->push_back(VC->idExpr("_BVSHL"));
-      }
-      else if (BVENABLED && *$1 == "bvlshr") {
-        $$->push_back(VC->idExpr("_BVLSHR"));
-      }
-
-      else if (BVENABLED && *$1 == "bvnand") {
-        $$->push_back(VC->idExpr("_BVNAND"));
-      }
-      else if (BVENABLED && *$1 == "bvnor") {
-        $$->push_back(VC->idExpr("_BVNOR"));
-      }
-      else if (BVENABLED && *$1 == "bvxor") {
-        $$->push_back(VC->idExpr("_BVXOR"));
-      }
-      else if (BVENABLED && *$1 == "bvxnor") {
-        $$->push_back(VC->idExpr("_BVXNOR"));
-      }
-      else if (BVENABLED && *$1 == "bvcomp") {
-        $$->push_back(VC->idExpr("_BVCOMP"));
-      }
-
-      else if (BVENABLED && *$1 == "bvsub") {
-        $$->push_back(VC->idExpr("_BVSUB"));
-      }
-      else if (BVENABLED && *$1 == "bvsdiv") {
-        $$->push_back(VC->idExpr("_BVSDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvsrem") {
-        $$->push_back(VC->idExpr("_BVSREM"));
-      }
-      else if (BVENABLED && *$1 == "bvsmod") {
-        $$->push_back(VC->idExpr("_BVSMOD"));
-      }
-      else if (BVENABLED && *$1 == "bvashr") {
-        $$->push_back(VC->idExpr("_BVASHR"));
-      }
-
-      // For backwards compatibility:
-      else if (BVENABLED && *$1 == "shift_left0") {
-        $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "shift_right0") {
-        $$->push_back(VC->idExpr("_RIGHTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
-
-      // Bitvector constants
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        bool done = false;
-        if ((*$1)[2] >= '0' && (*$1)[2] <= '9') {
-          int i = 3;
-          while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-          if ((*$1)[i] == '\0') {
-            $$->push_back(VC->idExpr("_BVCONST"));
-            $$->push_back(VC->ratExpr($1->substr(2), 10));
-            $$->push_back(VC->ratExpr(32));
-            done = true;
-          }
-        }
-        else if ($1->size() > 5) {
-          std::string s = $1->substr(0,5);
-          if (s == "bvbin") {
-            int i = 5;
-            while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i;
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 2));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-          else if (s == "bvhex") {
-            int i = 5;
-            char c = (*$1)[i];
-            while ((c >= '0' && c <= '9') ||
-                   (c >= 'a' && c <= 'f') ||
-                   (c >= 'A' && c <= 'F')) {
-              ++i;
-              c =(*$1)[i];
-            }
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 16));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-        }
-        if (!done) $$->push_back(VC->idExpr(*$1));
-      }
-      else {
-        $$->push_back(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-  | AR_SYMB 
-    { 
-      $$ = new std::vector<CVC4::Expr>;
-      if ($1->length() == 1) {
-	switch ((*$1)[0]) {
-	case '+': $$->push_back(VC->idExpr("_PLUS")); break;
-	case '-': $$->push_back(VC->idExpr("_MINUS")); break;
-	case '*': $$->push_back(VC->idExpr("_MULT")); break;
-	case '~': $$->push_back(VC->idExpr("_UMINUS")); break;
-	case '/': $$->push_back(VC->idExpr("_DIVIDE")); break;
-          //        case '=': $$->push_back(VC->idExpr("_EQ")); break;
-          //        case '<': $$->push_back(VC->idExpr("_LT")); break;
-          //        case '>': $$->push_back(VC->idExpr("_GT")); break;
-	default: $$->push_back(VC->idExpr(*$1));
-	}
-      }
-      //      else {
-      //	if (*$1 == "<=") {
-      //	  $$->push_back(VC->idExpr("_LE"));
-      //	} else if (*$1 == ">=") {
-      //	  $$->push_back(VC->idExpr("_GE"));
-      //	}
-	else $$->push_back(VC->idExpr(*$1));
-      //      }
-      delete $1;
-    }
-  | NUMERAL_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(VC->ratExpr(*$1));
-      delete $1;
-    }
-;
-
-attribute:
-    COLON_TOK SYM_TOK
-    {
-      $$ = $2;
-    }
-;
-
-var:
-    QUESTION_TOK SYM_TOK
-    {
-      $$ = new CVC4::Expr(VC->idExpr("_"+*$2));
-      delete $2;
-    }
-;
-
-fvar:
-    DOLLAR_TOK SYM_TOK
-    {
-      $$ = new CVC4::Expr(VC->idExpr("_"+*$2));
-      delete $2;
-    }
-;
-
-an_exprs:
-    an_expr
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(*$1);
-      delete $1;
-    }
-  |
-    an_exprs an_expr
-    {
-      $1->push_back(*$2);
-      $$ = $1;
-      delete $2;
-    }
-;
-
-an_expr:
-    var
-    {
-      $$ = $1;
-    }
-  | fvar
-    {
-      $$ = $1;
-    }
-  | LPAREN_TOK fun_pred_symb an_terms annotations RPAREN_TOK
-    {
-      $2->insert($2->end(), $3->begin(), $3->end());
-      $$ = new CVC4::Expr(VC->listExpr(*$2));
-      delete $2;
-      delete $3;
-      delete $4;
-    }
-  | LPAREN_TOK fun_pred_symb an_terms RPAREN_TOK
-    {
-      $2->insert($2->end(), $3->begin(), $3->end());
-      $$ = new CVC4::Expr(VC->listExpr(*$2));
-      delete $2;
-      delete $3;
-    }
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_expr annotations RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
-  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_expr RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_expr annotations RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-      delete $8;
-    }
-  | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_expr RPAREN_TOK
-    {
-      CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
-      $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7));
-      delete $4;
-      delete $5;
-      delete $7;
-    }
-;
-
-fun_pred_symb:
-    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if (BVENABLED && *$1 == "repeat") {
-        $$->push_back(VC->idExpr("_BVREPEAT"));
-      }
-      else if (BVENABLED && *$1 == "zero_extend") {
-        $$->push_back(VC->idExpr("_BVZEROEXTEND"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
-      else if (BVENABLED && *$1 == "rotate_left") {
-        $$->push_back(VC->idExpr("_BVROTL"));
-      }
-      else if (BVENABLED && *$1 == "rotate_right") {
-        $$->push_back(VC->idExpr("_BVROTR"));
-      }
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        int i = 2;
-        while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-        if ((*$1)[i] == '\0') {
-          $$->push_back(VC->idExpr("_BVCONST"));
-          $$->push_back(VC->ratExpr($1->substr(2), 10));
-        }
-        else $$->push_back(VC->idExpr(*$1));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      delete $1;
-      delete $3;
-    }
-  | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if (BVENABLED && *$1 == "extract") {
-        $$->push_back(VC->idExpr("_EXTRACT"));
-      }
-      else $$->push_back(VC->idExpr(*$1));
-      $$->push_back(VC->ratExpr(*$3));
-      $$->push_back(VC->ratExpr(*$5));
-      delete $1;
-      delete $3;
-      delete $5;
-    }
-  | SYM_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      if (ARRAYSENABLED && *$1 == "select") {
-        $$->push_back(VC->idExpr("_READ"));
-      }
-      else if (ARRAYSENABLED && *$1 == "store") {
-        $$->push_back(VC->idExpr("_WRITE"));
-      }
-      else if (BVENABLED && *$1 == "bit0") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(0));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "bit1") {
-        $$->push_back(VC->idExpr("_BVCONST"));
-        $$->push_back(VC->ratExpr(1));
-        $$->push_back(VC->ratExpr(1));
-      }
-      else if (BVENABLED && *$1 == "concat") {
-        $$->push_back(VC->idExpr("_CONCAT"));
-      }
-      else if (BVENABLED && *$1 == "bvnot") {
-        $$->push_back(VC->idExpr("_BVNEG"));
-      }
-      else if (BVENABLED && *$1 == "bvand") {
-        $$->push_back(VC->idExpr("_BVAND"));
-      }
-      else if (BVENABLED && *$1 == "bvor") {
-        $$->push_back(VC->idExpr("_BVOR"));
-      }
-      else if (BVENABLED && *$1 == "bvneg") {
-        $$->push_back(VC->idExpr("_BVUMINUS"));
-      }
-      else if (BVENABLED && *$1 == "bvadd") {
-        $$->push_back(VC->idExpr("_BVPLUS"));
-      }
-      else if (BVENABLED && *$1 == "bvmul") {
-        $$->push_back(VC->idExpr("_BVMULT"));
-      }
-      else if (BVENABLED && *$1 == "bvudiv") {
-        $$->push_back(VC->idExpr("_BVUDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvurem") {
-        $$->push_back(VC->idExpr("_BVUREM"));
-      }
-      else if (BVENABLED && *$1 == "bvshl") {
-        $$->push_back(VC->idExpr("_BVSHL"));
-      }
-      else if (BVENABLED && *$1 == "bvlshr") {
-        $$->push_back(VC->idExpr("_BVLSHR"));
-      }
-
-      else if (BVENABLED && *$1 == "bvnand") {
-        $$->push_back(VC->idExpr("_BVNAND"));
-      }
-      else if (BVENABLED && *$1 == "bvnor") {
-        $$->push_back(VC->idExpr("_BVNOR"));
-      }
-      else if (BVENABLED && *$1 == "bvxor") {
-        $$->push_back(VC->idExpr("_BVXOR"));
-      }
-      else if (BVENABLED && *$1 == "bvxnor") {
-        $$->push_back(VC->idExpr("_BVXNOR"));
-      }
-      else if (BVENABLED && *$1 == "bvcomp") {
-        $$->push_back(VC->idExpr("_BVCOMP"));
-      }
-
-      else if (BVENABLED && *$1 == "bvsub") {
-        $$->push_back(VC->idExpr("_BVSUB"));
-      }
-      else if (BVENABLED && *$1 == "bvsdiv") {
-        $$->push_back(VC->idExpr("_BVSDIV"));
-      }
-      else if (BVENABLED && *$1 == "bvsrem") {
-        $$->push_back(VC->idExpr("_BVSREM"));
-      }
-      else if (BVENABLED && *$1 == "bvsmod") {
-        $$->push_back(VC->idExpr("_BVSMOD"));
-      }
-      else if (BVENABLED && *$1 == "bvashr") {
-        $$->push_back(VC->idExpr("_BVASHR"));
-      }
+    attribute                 { delete $1; }                
+  | attribute user_value      { delete $1; delete $2; }
+  ;
 
-      // predicates
-      else if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
-        $$->push_back(VC->idExpr("_BVLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
-        $$->push_back(VC->idExpr("_BVLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
-        $$->push_back(VC->idExpr("_BVGE"));
-      }
-      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
-        $$->push_back(VC->idExpr("_BVGT"));
-      }
-      else if (BVENABLED && *$1 == "bvslt") {
-        $$->push_back(VC->idExpr("_BVSLT"));
-      }
-      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
-        $$->push_back(VC->idExpr("_BVSLE"));
-      }
-      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
-        $$->push_back(VC->idExpr("_BVSGE"));
-      }
-      else if (BVENABLED && *$1 == "bvsgt") {
-        $$->push_back(VC->idExpr("_BVSGT"));
-      }
+user_value: USER_VAL_TOK;
 
-      // For backwards compatibility:
-      else if (BVENABLED && *$1 == "shift_left0") {
-        $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "shift_right0") {
-        $$->push_back(VC->idExpr("_RIGHTSHIFT"));
-      }
-      else if (BVENABLED && *$1 == "sign_extend") {
-        $$->push_back(VC->idExpr("_SX"));
-        $$->push_back(VC->idExpr("_smtlib"));
-      }
+pred_symb: SYM_TOK;
 
-      // Bitvector constants
-      else if (BVENABLED &&
-               $1->size() > 2 &&
-               (*$1)[0] == 'b' &&
-               (*$1)[1] == 'v') {
-        bool done = false;
-        if ((*$1)[2] >= '0' && (*$1)[2] <= '9') {
-          int i = 3;
-          while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i;
-          if ((*$1)[i] == '\0') {
-            $$->push_back(VC->idExpr("_BVCONST"));
-            $$->push_back(VC->ratExpr($1->substr(2), 10));
-            $$->push_back(VC->ratExpr(32));
-            done = true;
-          }
-        }
-        else if ($1->size() > 5) {
-          std::string s = $1->substr(0,5);
-          if (s == "bvbin") {
-            int i = 5;
-            while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i;
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 2));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-          else if (s == "bvhex") {
-            int i = 5;
-            char c = (*$1)[i];
-            while ((c >= '0' && c <= '9') ||
-                   (c >= 'a' && c <= 'f') ||
-                   (c >= 'A' && c <= 'F')) {
-              ++i;
-              c =(*$1)[i];
-            }
-            if ((*$1)[i] == '\0') {
-              $$->push_back(VC->idExpr("_BVCONST"));
-              $$->push_back(VC->ratExpr($1->substr(5), 16));
-              $$->push_back(VC->ratExpr(i-5));
-              done = true;
-            }
-          }
-        }
-        if (!done) $$->push_back(VC->idExpr(*$1));
-      }
-      else {
-        $$->push_back(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-  | AR_SYMB 
-    { 
-      $$ = new std::vector<CVC4::Expr>;
-      if ($1->length() == 1) {
-	switch ((*$1)[0]) {
-	case '+': $$->push_back(VC->idExpr("_PLUS")); break;
-	case '-': $$->push_back(VC->idExpr("_MINUS")); break;
-	case '*': $$->push_back(VC->idExpr("_MULT")); break;
-	case '~': $$->push_back(VC->idExpr("_UMINUS")); break;
-	case '/': $$->push_back(VC->idExpr("_DIVIDE")); break;
-        case '=': $$->push_back(VC->idExpr("_EQ")); break;
-        case '<': $$->push_back(VC->idExpr("_LT")); break;
-        case '>': $$->push_back(VC->idExpr("_GT")); break;
-	default: $$->push_back(VC->idExpr(*$1));
-	}
-      }
-      else {
-	if (*$1 == "<=") {
-	  $$->push_back(VC->idExpr("_LE"));
-	} else if (*$1 == ">=") {
-	  $$->push_back(VC->idExpr("_GE"));
-	}
-	else $$->push_back(VC->idExpr(*$1));
-      }
-      delete $1;
-    }
-  | NUMERAL_TOK
-    {
-      $$ = new std::vector<CVC4::Expr>;
-      $$->push_back(VC->ratExpr(*$1));
-      delete $1;
-    }
-;
+attribute: 
+    COLON_TOK SYM_TOK { $$ = $2; }
+  ;
 
 %%
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
index b367b0d93..4d9cb8213 100644
--- a/src/parser/smtlib_scanner.lpp
+++ b/src/parser/smtlib_scanner.lpp
@@ -19,190 +19,105 @@
 %option prefix="smtlib"
 
 %{
+
 #include <iostream>
-#include "parser/smtlib.hpp"
-#include "util/debug.h"
+#include "parser_state.h"
+#include "smtlib.hpp"
 
 namespace CVC4 {
-  extern ParserTemp* parserTemp;
+namespace parser {
+  extern ParserState* _global_parser_state;
 }
-
-extern int smtlib_inputLine;
-extern char *smtlibtext;
-
-extern int smtliberror (const char *msg);
-
-static int smtlibinput(std::istream& is, char* buf, int size) {
-  int res;
-  if(is) {
-    // If interactive, read line by line; otherwise read as much as we
-    // can gobble
-    if(CVC4::parserTemp->interactive) {
-      // Print the current prompt
-      std::cout << CVC4::parserTemp->getPrompt() << std::flush;
-      // Set the prompt to "middle of the command" one
-      CVC4::parserTemp->setPrompt2();
-      // Read the line
-      is.getline(buf, size-1);
-    } else // Set the terminator char to 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) smtliberror("Lexer bug: overfilled the buffer");
-    if(!partialStr) { // Insert \n into the buffer
-      buf[res++] = '\n';
-      buf[res] = '\0';
-    }
-  } else {
-    res = YY_NULL;
-  }
-  return res;
 }
 
-// Redefine the input buffer function to read from an istream
-#define YY_INPUT(buf,result,max_size) \
-  result = smtlibinput(*CVC4::parserTemp->is, buf, max_size);
+using CVC4::parser::_global_parser_state;
 
-int smtlib_bufSize() { return YY_BUF_SIZE; }
-YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
-
-/* some wrappers for methods that need to refer to a struct.
-   These are used by CVC4::Parser. */
-void *smtlib_createBuffer(int sz) {
-  return (void *)smtlib_create_buffer(NULL, sz);
-}
-void smtlib_deleteBuffer(void *buf_state) {
-  smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
-}
-void smtlib_switchToBuffer(void *buf_state) {
-  smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
-}
-void *smtlib_bufState() {
-  return (void *)smtlib_buf_state();
-}
-
-void smtlib_setInteractive(bool is_interactive) {
-  yy_set_interactive(is_interactive);
-}
-
-// File-static (local to this file) variables and functions
-static std::string _string_lit;
+extern char *smtlibtext;
 
- static char escapeChar(char c) {
-   switch(c) {
-   case 'n': return '\n';
-   case 't': return '\t';
-   default: return c;
-   }
- }
 
-// for now, we don't have subranges.  
-//
-// ".."		{ return DOTDOT_TOK; }
-/*OPCHAR	(['!#?\_$&\|\\@])*/
+// Redefine the input buffer function to read from an istream
+#define YY_INPUT(buffer,result,max_size) result = _global_parser_state->read(buffer, max_size);
 
 %}
 
-%x	COMMENT
-%x	STRING_LITERAL
-%x      USER_VALUE
-%s      PAT_MODE
+%x COMMENT
+%x STRING_LITERAL
+%x SYM_TOK
+%x USER_VALUE
 
 LETTER	([a-zA-Z])
-DIGIT	([0-9])
+DIGIT	  ([0-9])
 OPCHAR	(['\.\_])
 IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
+
 %%
 
-[\n]            { CVC4::parserTemp->lineNum++; }
-[ \t\r\f]	{ /* skip whitespace */ }
-
-{DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
-{DIGIT}+	{ smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; 
-		}
-
-";"		{ BEGIN COMMENT; }
-<COMMENT>"\n"	{ BEGIN INITIAL; /* return to normal mode */ 
-                  CVC4::parserTemp->lineNum++; }
-<COMMENT>.	{ /* stay in comment mode */ }
-
-<INITIAL>"\""		{ BEGIN STRING_LITERAL; 
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<STRING_LITERAL>"\\".	{ /* escape characters (like \n or \") */
-                          _string_lit.insert(_string_lit.end(),
-                                             escapeChar(smtlibtext[1])); }
-<STRING_LITERAL>"\""	{ BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return STRING_TOK; }
-<STRING_LITERAL>.	{ _string_lit.insert(_string_lit.end(),*smtlibtext); }
-
-<INITIAL>":pat"		{ BEGIN PAT_MODE;
-                          return PAT_TOK;}
-<PAT_MODE>"}"	        { BEGIN INITIAL; 
-                          return RCURBRACK_TOK; }
-<INITIAL>"{"		{ BEGIN USER_VALUE;
-                          _string_lit.erase(_string_lit.begin(),
-                                            _string_lit.end()); }
-<USER_VALUE>"\\"[{}] { /* escape characters */
-                          _string_lit.insert(_string_lit.end(),smtlibtext[1]); }
-
-<USER_VALUE>"}"	        { BEGIN INITIAL; /* return to normal mode */ 
-			  smtliblval.str = new std::string(_string_lit);
-                          return USER_VAL_TOK; }
-
-<USER_VALUE>"\n"        { _string_lit.insert(_string_lit.end(),'\n');
-                          CVC4::parserTemp->lineNum++; }
-<USER_VALUE>.	        { _string_lit.insert(_string_lit.end(),*smtlibtext); }
-
-"true"          { return TRUE_TOK; }
-"false"         { return FALSE_TOK; }
-"ite"           { return ITE_TOK; }
-"not"           { return NOT_TOK; }
-"implies"       { return IMPLIES_TOK; }
-"if_then_else"  { return IF_THEN_ELSE_TOK; }
-"and"           { return AND_TOK; }
-"or"            { return OR_TOK; }
-"xor"           { return XOR_TOK; }
-"iff"           { return IFF_TOK; }
-"exists"        { return EXISTS_TOK; }
-"forall"        { return FORALL_TOK; }
-"let"           { return LET_TOK; }
-"flet"          { return FLET_TOK; }
-"notes"         { return NOTES_TOK; }
-"cvc_command"   { return CVC_COMMAND_TOK; }
-"logic"         { return LOGIC_TOK; }
-"sat"           { return SAT_TOK; }
-"unsat"         { return UNSAT_TOK; }
-"unknown"       { return UNKNOWN_TOK; }
-"assumption"    { return ASSUMPTION_TOK; }
-"formula"       { return FORMULA_TOK; }
-"status"        { return STATUS_TOK; }
-"benchmark"     { return BENCHMARK_TOK; }
-"extrasorts"    { return EXTRASORTS_TOK; }
-"extrafuns"     { return EXTRAFUNS_TOK; }
-"extrapreds"    { return EXTRAPREDS_TOK; }
-"distinct"      { return DISTINCT_TOK; }
-":pattern"      { return PAT_TOK; } 
-":"             { return COLON_TOK; }
-"\["            { return LBRACKET_TOK; }
-"\]"            { return RBRACKET_TOK; }
-"{"             { return LCURBRACK_TOK;}
-"}"             { return RCURBRACK_TOK;}
-"("             { return LPAREN_TOK; }
-")"             { return RPAREN_TOK; }
-"$"             { return DOLLAR_TOK; }
-"?"             { return QUESTION_TOK; }
-
-[=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
-({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
+[\n]            { _global_parser_state->increaseLineNumber(); }
+[ \t\r\f]	      { /* skip whitespace */ }
+
+{DIGIT}+"\."{DIGIT}+ { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; }
+{DIGIT}+	           { smtliblval.p_string = new std::string(smtlibtext); return NUMERAL_TOK; }
+
+";"		               { BEGIN COMMENT; }
+<COMMENT>"\n"	       { BEGIN INITIAL; _global_parser_state->increaseLineNumber(); }
+<COMMENT>.	         { /* stay in comment mode */ }
+
+"\""                  { BEGIN STRING_LITERAL; _global_parser_state->newStringLiteral(); }
+<STRING_LITERAL>"\\". { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); }
+<STRING_LITERAL>"\""  { BEGIN INITIAL; 
+                        /* return to normal mode */ 
+                        smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral());
+                        return STRING_TOK; 
+                      }
+<STRING_LITERAL>.     { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); }
+
+"{"                   { BEGIN USER_VALUE; _global_parser_state->newStringLiteral(); }
+<USER_VALUE>"\\"[{}]  { _global_parser_state->appendCharToStringLiteral(smtlibtext, true); }
+<USER_VALUE>"}"       { BEGIN INITIAL; 
+                        /* return to normal mode */ 
+                        smtliblval.p_string = new std::string(_global_parser_state->getStringLiteral());
+                        return USER_VAL_TOK; 
+                      }
+<USER_VALUE>.         { _global_parser_state->appendCharToStringLiteral(smtlibtext, false); }
+
+
+"true"          { return TRUE_TOK;             }
+"false"         { return FALSE_TOK;            }
+"ite"           { return ITE_TOK;              }
+"not"           { return NOT_TOK;              }
+"implies"       { return IMPLIES_TOK;          }
+"if_then_else"  { return IF_THEN_ELSE_TOK;     }
+"and"           { return AND_TOK;              }
+"or"            { return OR_TOK;               }
+"xor"           { return XOR_TOK;              }
+"iff"           { return IFF_TOK;              }
+"let"           { return LET_TOK;              }
+"flet"          { return FLET_TOK;             }
+"notes"         { return NOTES_TOK;            }
+"logic"         { return LOGIC_TOK;            }
+"sat"           { return SAT_TOK;              }
+"unsat"         { return UNSAT_TOK;            }
+"unknown"       { return UNKNOWN_TOK;          }
+"assumption"    { return ASSUMPTION_TOK;       }
+"formula"       { return FORMULA_TOK;          }
+"status"        { return STATUS_TOK;           }
+"benchmark"     { return BENCHMARK_TOK;        }
+"extrasorts"    { return EXTRASORTS_TOK;       }
+"extrafuns"     { return EXTRAFUNS_TOK;        }
+"extrapreds"    { return EXTRAPREDS_TOK;       }
+"distinct"      { return DISTINCT_TOK;         }
+":"             { return COLON_TOK;            }
+"\["            { return LBRACKET_TOK;         }
+"\]"            { return RBRACKET_TOK;         }
+"("             { return LPAREN_TOK;           }
+")"             { return RPAREN_TOK;           }
+"$"             { return DOLLAR_TOK;           }
+"?"             { return QUESTION_TOK;         }
+
+({LETTER})({IDCHAR})* { smtliblval.p_string = new std::string(smtlibtext); return SYM_TOK; }
 
 <<EOF>>         { return EOF_TOK; }
 
-. { smtliberror("Illegal input character."); }
+. { _global_parser_state->parseError("Illegal input character."); }
+
 %%