Added CVC3's parser for the SMT-LIB grammar.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73059 91177308-0d34-0410-b5e6-96231b3b80d8

10 files changed, 2127 insertions, 0 deletions

diff --git a/lib/SMT/LICENSE.CVC3 b/lib/SMT/LICENSE.CVC3
new file mode 100644
index 00000000..a70d12d5
--- /dev/null
+++ b/lib/SMT/LICENSE.CVC3
@@ -0,0 +1,53 @@
+/*!\page LICENSE LICENSE
+
+Copyright (C) 2003-2009 by the Board of Trustees of Leland Stanford Junior
+University, New York University, and the University of Iowa, hereafter
+designated as the Copyright Owners.
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification,
+are permitted provided that the following conditions are met:
+
+* Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.
+* Redistributions in binary form must reproduce the above copyright notice,
+this list of conditions and the following disclaimer in the documentation
+and/or other materials provided with the distribution.
+* Neither the names of the Copyright Owners nor the names of any contributors
+may be used to endorse or promote products derived from this software
+without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+Note:
+
+The following files contain code whose copyright does not belong to the
+Copyright Owners.  However, separate copyright notices in these files give
+express permission to copy, use, modify, sell, or distribute the code.  Please
+see the copyright notices in the individual files for details.
+
+<pre>
+src/include/fdstream.h
+src/include/hash_map.h
+src/include/hash_fun.h
+src/include/hash_set.h
+src/include/hash_table.h
+src/sat/minisat_varorder.h
+src/sat/minisat_solver.cpp
+src/sat/minisat_heap.h
+src/sat/minisat_types.h
+src/sat/minisat_solver.h
+src/sat/minisat_global.h
+</pre>
+
+*/
diff --git a/lib/SMT/Makefile b/lib/SMT/Makefile
new file mode 100644
index 00000000..ae9c2e18
--- /dev/null
+++ b/lib/SMT/Makefile
@@ -0,0 +1,59 @@
+MODULE = parser
+
+LIBRARY=libparser.a
+
+# Do not optimize the parser code - it compiles forever in some gcc versions
+EXTRAFLAGS = -O0
+
+TRANSIENT_CPP = \
+ parsePL.cpp lexPL.cpp \
+ parseLisp.cpp lexLisp.cpp \
+ parsesmtlib.cpp lexsmtlib.cpp
+
+TRANSIENT = $(TRANSIENT_CPP) \
+  parsePL_defs.h parsePL.output \
+  parseLisp_defs.h parseLisp.output \
+  parsesmtlib_defs.h parsesmtlib.output
+
+SRC = $(TRANSIENT_CPP) parser.cpp
+
+HEADERS = parser_temp.h
+
+# The actual source files for the parser that we want to include in a
+# distribution
+SRC_ORIG = PL.lex PL.y Lisp.lex Lisp.y smtlib.lex smtlib.y parser.cpp
+
+include ../../Makefile.local
+
+##################################################
+# Rules for transient files
+##################################################
+lexPL.cpp:      PL.lex parsePL_defs.h
+		$(LEX) $(LFLAGS) -I -PPL -olexPL.cpp PL.lex
+
+parsePL_defs.h: parsePL.cpp
+
+parsePL.cpp:    PL.y
+		$(YACC) $(YFLAGS) -o parsePL.cpp -p PL --debug -v PL.y
+		@if [ -f parsePL.cpp.h ]; then mv parsePL.cpp.h parsePL.hpp; fi
+		@mv parsePL.hpp parsePL_defs.h
+
+lexLisp.cpp:    Lisp.lex parseLisp_defs.h
+		$(LEX) $(LFLAGS) -I -PLisp -olexLisp.cpp Lisp.lex
+
+parseLisp_defs.h: parseLisp.cpp
+
+parseLisp.cpp:  Lisp.y
+		$(YACC) $(YFLAGS) -o parseLisp.cpp -p Lisp --debug -v Lisp.y
+		@if [ -f parseLisp.cpp.h ]; then mv parseLisp.cpp.h parseLisp.hpp; fi
+		@mv parseLisp.hpp parseLisp_defs.h
+
+lexsmtlib.cpp:  smtlib.lex parsesmtlib_defs.h
+		$(LEX) $(LFLAGS) -I -Psmtlib -olexsmtlib.cpp smtlib.lex
+
+parsesmtlib_defs.h: parsesmtlib.cpp
+
+parsesmtlib.cpp: smtlib.y
+		$(YACC) $(YFLAGS) -o parsesmtlib.cpp -p smtlib --debug -v smtlib.y
+		@if [ -f parsesmtlib.cpp.h ]; then mv parsesmtlib.cpp.h parsesmtlib.hpp; fi
+		@mv parsesmtlib.hpp parsesmtlib_defs.h
diff --git a/lib/SMT/exception.h b/lib/SMT/exception.h
new file mode 100644
index 00000000..97f79669
--- /dev/null
+++ b/lib/SMT/exception.h
@@ -0,0 +1,58 @@
+/*****************************************************************************/
+/*!
+ * \file exception.h
+ * 
+ * Author: Sergey Berezin
+ * 
+ * Created: Thu Feb  6 13:09:44 2003
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ * A generic exception.  Any thrown exception must inherit from this
+ * class and whenever possible, set the error message.
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__exception_h_
+#define _cvc3__exception_h_
+
+#include <string>
+#include <iostream>
+
+namespace CVC3 {
+
+  class Exception {
+  protected:
+    std::string d_msg;
+  public:
+    // Constructors
+    Exception(): d_msg("Unknown exception") { }
+    Exception(const std::string& msg): d_msg(msg) { }
+    Exception(const char* msg): d_msg(msg) { }
+    // Destructor
+    virtual ~Exception() { }
+    // NON-VIRTUAL METHODs for setting and printing the error message
+    void setMessage(const std::string& msg) { d_msg = msg; }
+    // Printing: feel free to redefine toString().  When inherited,
+    // it's recommended that this method print the type of exception
+    // before the actual message.
+    virtual std::string toString() const { return d_msg; }
+    // No need to overload operator<< for the inherited classes
+    friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+
+  }; // end of class Exception
+
+  inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+    return os << e.toString();
+  }
+
+} // end of namespace CVC3 
+
+#endif
diff --git a/lib/SMT/lang.h b/lib/SMT/lang.h
new file mode 100644
index 00000000..c021e63a
--- /dev/null
+++ b/lib/SMT/lang.h
@@ -0,0 +1,66 @@
+/*****************************************************************************/
+/*!
+ * \file lang.h
+ * \brief Definition of input and output languages to CVC3
+ * 
+ * Author: Mehul Trivedi
+ * 
+ * Created: Thu Jul 29 11:56:34 2004
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__lang_h_
+#define _cvc3__lang_h_
+
+#include "debug.h"
+
+namespace CVC3 {
+
+  //! Different input languages
+  typedef enum {
+    //! Nice SAL-like language for manually written specs
+    PRESENTATION_LANG,
+    //! SMT-LIB format
+    SMTLIB_LANG,
+    //! Lisp-like format for automatically generated specs
+    LISP_LANG,
+    AST_LANG,	
+
+    /* @brief AST is only for printing the Expr abstract syntax tree in lisp
+       format; there is no such input language <em>per se</em> */
+    SIMPLIFY_LANG,
+    //! for output into Simplify format
+    TPTP_LANG
+    //! for output in TPTP format
+  } InputLanguage;
+  
+  inline InputLanguage getLanguage(const std::string& lang) {
+    if (lang.size() > 0) {
+      if(lang[0] == 'p') return PRESENTATION_LANG;
+      if(lang[0] == 'l') return LISP_LANG;
+      if(lang[0] == 'a') return AST_LANG;
+      if(lang[0] == 't') return TPTP_LANG;
+      if(lang[0] == 's') {
+        if (lang.size() > 1 && lang[1] == 'i') return SIMPLIFY_LANG;
+        else return SMTLIB_LANG;
+      }
+      
+    }
+
+    throw Exception("Bad input language specified");
+    return AST_LANG;
+  }
+
+} // end of namespace CVC3
+
+#endif
diff --git a/lib/SMT/parser.cpp b/lib/SMT/parser.cpp
new file mode 100644
index 00000000..92693c35
--- /dev/null
+++ b/lib/SMT/parser.cpp
@@ -0,0 +1,235 @@
+/*****************************************************************************/
+/*!
+ * \file parser.cpp
+ * \brief The top-level API to the parser.  See parser.h for details.
+ * 
+ * Author: Sergey Berezin
+ * 
+ * Created: Wed Feb  5 11:46:57 2003
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ */
+/*****************************************************************************/
+
+#include <fstream>
+#include <iomanip>
+#include "parser_temp.h"
+#include "parser.h"
+#include "parser_exception.h"
+
+using namespace std;
+
+// 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 Lisp language (Lisp.y and Lisp.lex)
+extern int Lispparse(); 
+extern void *Lisp_createBuffer(int);
+extern void Lisp_deleteBuffer(void *);
+extern void Lisp_switchToBuffer(void *);
+extern int Lisp_bufSize();
+extern void *LispBufState();
+void Lisp_setInteractive(bool);
+
+// for Lisp language (Lisp.y and Lisp.lex)
+extern int Lispparse(); 
+extern void *Lisp_createBuffer(int);
+extern void Lisp_deleteBuffer(void *);
+extern void Lisp_switchToBuffer(void *);
+extern int Lisp_bufSize();
+extern void *LispBufState();
+void Lisp_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);
+
+namespace CVC3 {
+
+  // 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.  
+
+  // FIXME: This should probably go away eventually, when I figure out
+  // flex++   -- Sergey.
+  ParserTemp* parserTemp;
+
+  int ParserTemp::error(const string& s) {
+    throw ParserException(s);
+    return 0;
+  }
+
+  // Internal storage class; I'll use member names without 'd_'s here
+  class ParserData {
+  public:
+    // Which language to use
+    InputLanguage lang;
+    // Is the input given by the file name or as istream?
+    bool useName;
+    ParserTemp temp;
+    // Internal buffer used by the parser
+    void* buffer;
+  };
+
+  // Constructors
+  Parser::Parser(ValidityChecker* vc, InputLanguage lang,
+		 bool interactive,
+		 const std::string& fileName)
+    : d_data(new ParserData) {
+    d_data->temp.vc = vc;
+    d_data->lang = lang;
+    if(fileName == "") {
+      // Use std::cin
+      d_data->useName = false;
+      d_data->temp.is = &cin;
+      d_data->temp.fileName = "stdin";
+      d_data->temp.interactive = interactive;
+    } else {
+      // Open the file by name
+      d_data->useName = true;
+      d_data->temp.fileName = fileName;
+      d_data->temp.is = new ifstream(fileName.c_str());
+      if (!(*d_data->temp.is)) {
+        throw ParserException("File not found: "+fileName);
+      }
+      d_data->temp.interactive = false;
+    }
+    initParser();
+  }
+
+  Parser::Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
+		 bool interactive)
+    : d_data(new ParserData) {
+    d_data->temp.vc = vc;
+    d_data->lang = lang;
+    d_data->useName = false;
+    d_data->temp.is = &is;
+    d_data->temp.fileName = "stdin";
+    d_data->temp.interactive = interactive;
+    initParser();
+  }
+    
+  // Destructor
+  Parser::~Parser() {
+    if(d_data->useName) // Stream is ours; delete it
+      delete d_data->temp.is;
+    deleteParser();
+    delete d_data;
+  }
+
+  // Initialize the actual parser
+  void Parser::initParser() {
+    switch(d_data->lang) {
+    case PRESENTATION_LANG:
+      d_data->buffer = PL_createBuffer(PL_bufSize());
+      d_data->temp.lineNum = 1;
+      break;
+    case LISP_LANG:
+      d_data->buffer = Lisp_createBuffer(Lisp_bufSize());
+      d_data->temp.lineNum = 1;
+      break;
+    case SMTLIB_LANG:
+      d_data->buffer = smtlib_createBuffer(smtlib_bufSize());
+      d_data->temp.lineNum = 1;
+      break;
+    default: FatalAssert(false, "Bad input language specified"); exit(1);
+    }
+  }
+
+  // Clean up the parser's internal data structures
+  void Parser::deleteParser() {
+    switch(d_data->lang) {
+    case PRESENTATION_LANG:
+      PL_deleteBuffer(d_data->buffer);
+      break;
+    case LISP_LANG:
+      Lisp_deleteBuffer(d_data->buffer);
+      break;
+    case SMTLIB_LANG:
+      smtlib_deleteBuffer(d_data->buffer);
+      break;
+    default: FatalAssert(false, "Bad input language specified");
+    }
+  }
+    
+
+  Expr Parser::next() {
+    // If no more commands are available, return a Null Expr
+    if(d_data->temp.done) return Expr();
+    // Set the global var so the parser uses the right stream and EM
+    parserTemp = &(d_data->temp);
+    // Switch to our buffer, in case there are multiple instances of
+    // the parser running
+    try {
+      switch(d_data->lang) {
+      case PRESENTATION_LANG:
+      	PL_switchToBuffer(d_data->buffer);
+	PL_setInteractive(d_data->temp.interactive);
+	PLparse();
+	// Reset the prompt to the main one
+	d_data->temp.setPrompt1();
+	break;
+      case LISP_LANG:
+        Lisp_switchToBuffer(d_data->buffer);
+	Lisp_setInteractive(d_data->temp.interactive);
+	Lispparse();
+	// Reset the prompt to the main one
+	d_data->temp.setPrompt1();
+	break;
+      case SMTLIB_LANG:
+        smtlib_switchToBuffer(d_data->buffer);
+	smtlib_setInteractive(d_data->temp.interactive);
+	smtlibparse();
+	// Reset the prompt to the main one
+	d_data->temp.setPrompt1();
+	break;
+      default: {
+	ostringstream ss;
+	ss << "Bad input language specified: " << d_data->lang;
+	DebugAssert(false, ss.str().c_str()); exit(1);
+      }
+      }
+    } catch(Exception* e) {
+      cerr << d_data->temp.fileName << ":" << d_data->temp.lineNum
+	   << ": " << e << endl;
+      return Expr();
+    }
+    return d_data->temp.expr;
+  }
+
+  bool Parser::done() const { return d_data->temp.done; }
+
+  void Parser::printLocation(ostream & out) const
+  {
+      out << d_data->temp.fileName << ":" << d_data->temp.lineNum;
+  }
+
+  void Parser::reset()
+  {
+    d_data->temp.expr = Expr();
+  }
+  
+
+} // end of namespace CVC3
diff --git a/lib/SMT/parser.h b/lib/SMT/parser.h
new file mode 100644
index 00000000..2e580a31
--- /dev/null
+++ b/lib/SMT/parser.h
@@ -0,0 +1,79 @@
+/*****************************************************************************/
+/*!
+ * \file parser.h
+ * 
+ * Author: Sergey Berezin
+ * 
+ * Created: Wed Feb  5 11:46:57 2003
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ * The top-level API to the parser.  At this level, it is simply a
+ * stream of commands (Expr's) terminated by an infinite sequence of
+ * Null Expr.  It has a support to parse several different input
+ * languages (as many as we care to implement), and may take a file
+ * name, or an istream to read from (default: std::cin, or stdin).
+ * Using iostream means no more worries about whether to close files
+ * or not.
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__parser_h_
+#define _cvc3__parser_h_
+
+#include "exception.h"
+#include "lang.h"
+
+namespace CVC3 {
+
+  class ValidityChecker;
+  class Expr;
+  
+  // Internal parser state and other data
+  class ParserData;
+
+  class Parser {
+  private:
+    ParserData* d_data;
+    // Internal methods for constructing and destroying the actual parser
+    void initParser();
+    void deleteParser();
+  public:
+    // Constructors
+    Parser(ValidityChecker* vc, InputLanguage lang,
+	   // The 'interactive' flag is ignored when fileName != ""
+	   bool interactive = true,
+	   const std::string& fileName = "");
+    Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
+	   bool interactive = false);
+    // Destructor
+    ~Parser();
+    // Read the next command.  
+    Expr next();
+    // 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(); }
+    void printLocation(std::ostream & out) const;
+    // Reset any local data that depends on validity checker
+    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.
+  class ParserTemp;
+  extern ParserTemp* parserTemp;
+
+} // end of namespace CVC3
+
+#endif
diff --git a/lib/SMT/parser_exception.h b/lib/SMT/parser_exception.h
new file mode 100644
index 00000000..64a8f452
--- /dev/null
+++ b/lib/SMT/parser_exception.h
@@ -0,0 +1,46 @@
+/*****************************************************************************/
+/*!
+ * \file parser_exception.h
+ * \brief An exception thrown by the parser.
+ *
+ * Author: Sergey Berezin
+ *
+ * Created: Thu Feb  6 13:23:39 2003
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ *
+ * <hr>
+ *
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__parser_exception_h_
+#define _cvc3__parser_exception_h_
+
+#include "exception.h"
+#include <string>
+#include <iostream>
+
+namespace CVC3 {
+
+  class ParserException: public Exception {
+  public:
+    // Constructors
+    ParserException() { }
+    ParserException(const std::string& msg): Exception(msg) { }
+    ParserException(const char* msg): Exception(msg) { }
+    // Destructor
+    virtual ~ParserException() { }
+    virtual std::string toString() const {
+      return "Parse Error: " + d_msg;
+    }
+  }; // end of class ParserException
+
+} // end of namespace CVC3
+
+#endif
diff --git a/lib/SMT/parser_temp.h b/lib/SMT/parser_temp.h
new file mode 100644
index 00000000..2c6f6b38
--- /dev/null
+++ b/lib/SMT/parser_temp.h
@@ -0,0 +1,85 @@
+/*****************************************************************************/
+/*!
+ * \file parser_temp.h
+ *
+ * Author: Sergey Berezin
+ *
+ * Created: Wed Feb  5 17:53:02 2003
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ *
+ * <hr>
+ *
+ * A class used to communicate with the actual parser.  No one else
+ * should use it.
+ */
+/*****************************************************************************/
+
+#ifndef _cvc3__parser_temp_h_
+#define _cvc3__parser_temp_h_
+
+#include "expr.h"
+#include "exception.h"
+
+namespace CVC3 {
+
+  class ValidityChecker;
+
+  class ParserTemp {
+  private:
+    // Counter for uniqueID of bound variables
+    int d_uid;
+    // The main prompt when running interactive
+    std::string prompt1;
+    // The interactive prompt in the middle of a multi-line command
+    std::string prompt2;
+    // The currently used prompt
+    std::string prompt;
+  public:
+    ValidityChecker* vc;
+    std::istream* is;
+    // The current input line
+    int lineNum;
+    // File name
+    std::string fileName;
+    // The last parsed Expr
+    Expr expr;
+    // Whether we are done or not
+    bool done;
+    // Whether we are running interactive
+    bool interactive;
+    // Whether arrays are enabled for smt-lib format
+    bool arrFlag;
+    // Whether bit-vectors are enabled for smt-lib format
+    bool bvFlag;
+    // Size of bit-vectors for smt-lib format
+    int bvSize;
+    // Did we encounter a formula query (smtlib)
+    bool queryParsed;
+    // Default constructor
+    ParserTemp() : d_uid(0), prompt1("CVC> "), prompt2("- "),
+      prompt("CVC> "), lineNum(1), done(false), arrFlag(false), queryParsed(false) { }
+    // Parser error handling (implemented in parser.cpp)
+    int error(const std::string& s);
+    // Get the next uniqueID as a string
+    std::string uniqueID() {
+      std::ostringstream ss;
+      ss << d_uid++;
+      return ss.str();
+    }
+    // Get the current prompt
+    std::string getPrompt() { return prompt; }
+    // Set the prompt to the main one
+    void setPrompt1() { prompt = prompt1; }
+    // Set the prompt to the secondary one
+    void setPrompt2() { prompt = prompt2; }
+  };
+
+} // end of namespace CVC3
+
+#endif
diff --git a/lib/SMT/smtlib.lex b/lib/SMT/smtlib.lex
new file mode 100644
index 00000000..15c06fc5
--- /dev/null
+++ b/lib/SMT/smtlib.lex
@@ -0,0 +1,224 @@
+%{
+/*****************************************************************************/
+/*!
+ * \file smtlib.lex
+ * 
+ * Author: Clark Barrett
+ * 
+ * Created: 2005
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ */
+/*****************************************************************************/
+
+#include <iostream>
+#include "parser_temp.h"
+#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
+#include "parsesmtlib_defs.h"
+#include "debug.h"
+
+namespace CVC3 {
+  extern ParserTemp* parserTemp;
+}
+
+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(CVC3::parserTemp->interactive) {
+      // Print the current prompt
+      std::cout << CVC3::parserTemp->getPrompt() << std::flush;
+      // Set the prompt to "middle of the command" one
+      CVC3::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(*CVC3::parserTemp->is, buf, max_size);
+
+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 CVC3::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;
+
+ 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	(['!#?\_$&\|\\@])*/
+
+%}
+
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+
+%x	COMMENT
+%x	STRING_LITERAL
+%x      USER_VALUE
+%s      PAT_MODE
+
+LETTER	([a-zA-Z])
+DIGIT	([0-9])
+OPCHAR	(['\.\_])
+IDCHAR  ({LETTER}|{DIGIT}|{OPCHAR})
+%%
+
+[\n]            { CVC3::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 */ 
+                  CVC3::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');
+                          CVC3::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; }
+"sorts"         { return SORTS_TOK; }
+"funs"          { return FUNS_TOK; }
+"preds"         { return PREDS_TOK; }
+"extensions"    { return EXTENSIONS_TOK; }
+"definition"    { return DEFINITION_TOK; }
+"axioms"        { return AXIOMS_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; }
+"language"      { return LANGUAGE_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; }
+
+<<EOF>>         { return EOF_TOK; }
+
+. { smtliberror("Illegal input character."); }
+%%
+
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y
new file mode 100644
index 00000000..c9e7b990
--- /dev/null
+++ b/lib/SMT/smtlib.y
@@ -0,0 +1,1222 @@
+%{
+/*****************************************************************************/
+/*!
+ * \file smtlib.y
+ * 
+ * Author: Clark Barrett
+ * 
+ * Created: Apr 30 2005
+ *
+ * <hr>
+ *
+ * License to use, copy, modify, sell and/or distribute this software
+ * and its documentation for any purpose is hereby granted without
+ * royalty, subject to the terms and conditions defined in the \ref
+ * LICENSE file provided with this distribution.
+ * 
+ * <hr>
+ * 
+ */
+/*****************************************************************************/
+/* 
+   This file contains the bison code for the parser that reads in CVC
+   commands in SMT-LIB language.
+*/
+
+#include "vc.h"
+#include "parser_exception.h"
+#include "parser_temp.h"
+
+// Exported shared data
+namespace CVC3 {
+  extern ParserTemp* parserTemp;
+}
+// Define shortcuts for various things
+#define TMP CVC3::parserTemp
+#define EXPR CVC3::parserTemp->expr
+#define VC (CVC3::parserTemp->vc)
+#define ARRAYSENABLED (CVC3::parserTemp->arrFlag)
+#define BVENABLED (CVC3::parserTemp->bvFlag)
+#define BVSIZE (CVC3::parserTemp->bvSize)
+#define RAT(args) CVC3::newRational args
+#define QUERYPARSED CVC3::parserTemp->queryParsed
+
+// Suppress the bogus warning suppression in bison (it generates
+// compile error)
+#undef __GNUC_MINOR__
+
+/* stuff that lives in smtlib.lex */
+extern int smtliblex(void);
+
+int smtliberror(const char *s)
+{
+  std::ostringstream ss;
+  ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum
+     << ": " << s;
+  return CVC3::parserTemp->error(ss.str());
+}
+
+
+
+#define YYLTYPE_IS_TRIVIAL 1
+#define YYMAXDEPTH 10485760
+
+%}
+
+%union {
+  std::string *str;
+  std::vector<std::string> *strvec;
+  CVC3::Expr *node;
+  std::vector<CVC3::Expr> *vec;
+  std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann;
+};
+
+
+%start cmd
+
+/* strings are for better error messages.  
+   "_TOK" is so macros don't conflict with kind names */
+
+%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls
+%type <vec> an_formulas quant_vars an_terms fun_symb patterns
+%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_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 <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
+%token NOT_TOK
+%token IMPLIES_TOK
+%token IF_THEN_ELSE_TOK
+%token AND_TOK
+%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 SORTS_TOK
+%token FUNS_TOK
+%token PREDS_TOK
+%token EXTENSIONS_TOK
+%token DEFINITION_TOK
+%token AXIOMS_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
+%token ASSUMPTION_TOK
+%token FORMULA_TOK
+%token STATUS_TOK
+%token BENCHMARK_TOK
+%token EXTRASORTS_TOK
+%token EXTRAFUNS_TOK
+%token EXTRAPREDS_TOK
+%token LANGUAGE_TOK
+%token DOLLAR_TOK
+%token QUESTION_TOK
+%token DISTINCT_TOK
+%token SEMICOLON_TOK
+%token EOF_TOK
+%token PAT_TOK
+%%
+
+cmd:
+    benchmark
+    {
+      EXPR = *$1;
+      delete $1;
+      YYACCEPT;
+    }
+;
+
+benchmark:
+    LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK
+    {
+      if (!QUERYPARSED)
+        $4->push_back(CVC3::Expr(VC->listExpr("_CHECKSAT", CVC3::Expr(VC->idExpr("_TRUE_EXPR")))));
+      $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4));
+      delete $4;
+    }
+  | EOF_TOK
+    { 
+      TMP->done = true;
+      $$ = new CVC3::Expr();
+    }
+;
+
+bench_name:
+    SYM_TOK
+    {
+      $$ = NULL;
+      delete $1;
+    }
+;
+
+bench_attributes:
+    bench_attribute
+    {
+      $$ = new std::vector<CVC3::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 CVC3::Expr(VC->listExpr("_ASSERT", *$3));
+      delete $3;
+    }
+  | COLON_TOK FORMULA_TOK an_formula 
+    {
+      $$ = new CVC3::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;
+      if (*$3 == "QF_UF") {
+        $$ = new CVC3::Expr(VC->listExpr("_TYPE", VC->idExpr("U")));
+      }
+      else if (*$3 == "QF_A" ||
+               *$3 == "QF_AX") {
+        ARRAYSENABLED = true;
+        std::vector<CVC3::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"))));
+        $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp));
+      }
+      else if (*$3 == "QF_AUFLIA" ||
+               *$3 == "AUFLIA") {
+        ARRAYSENABLED = true;
+        std::vector<CVC3::Expr> tmp;
+        tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"),
+                                   VC->listExpr("_ARRAY",
+                                                VC->idExpr("_INT"),
+                                                VC->idExpr("_INT"))));
+        $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp));
+      }
+      else if (*$3 == "QF_AUFLIRA" ||
+               *$3 == "AUFLIRA" ||
+               *$3 == "QF_AUFNIRA" ||
+               *$3 == "AUFNIRA") {
+        ARRAYSENABLED = true;
+        std::vector<CVC3::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"))));
+        $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp));
+      }
+      else if (*$3 == "QF_AUFBV" ||
+               *$3 == "QF_ABV") {
+        ARRAYSENABLED = true;
+        BVENABLED = true;
+        $$ = NULL;
+//         $$ = new CVC3::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;
+        $$ = NULL;
+      }
+    // This enables the new arith for QF_LRA, but this results in assertion failures in DEBUG mode
+      else if (*$3 == "QF_LRA") {
+         $$ = new CVC3::Expr(VC->listExpr("_OPTION", VC->stringExpr("arith-new"), VC->ratExpr(1)));
+       }
+      else {
+        $$ = NULL;
+      }
+      delete $3;
+    }
+  | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr("_TYPE", *$4));
+      delete $4;
+    }
+  | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
+      delete $4;
+    }
+  | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4));
+      delete $4;
+    }
+  | COLON_TOK NOTES_TOK STRING_TOK
+    {
+      $$ = NULL;
+      delete $3;
+    }
+  | COLON_TOK CVC_COMMAND_TOK STRING_TOK
+    {
+      $$ = new CVC3::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<CVC3::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<CVC3::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;
+    }
+;
+
+fun_sig:
+    fun_symb sort_symbs
+    {
+      if ($2->size() == 1) {
+        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0]));
+      }
+      else {
+        CVC3::Expr tmp(VC->listExpr("_ARROW", *$2));
+        $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp));
+      }
+      delete $1;
+      delete $2;
+    }
+;
+
+pred_symb_decls:
+    pred_symb_decl
+    {
+      $$ = new std::vector<CVC3::Expr>;
+      $$->push_back(*$1);
+      delete $1;
+    }
+  |
+    pred_symb_decls pred_symb_decl
+    {
+      $1->push_back(*$2);
+      $$ = $1;
+      delete $2;
+    }
+;
+
+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<CVC3::Expr> tmp(*$2);
+      tmp.push_back(VC->idExpr("_BOOLEAN"));
+      CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp));
+      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2));
+      delete $1;
+      delete $2;
+    }
+  | pred_symb
+    {
+      $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1),
+                                       VC->idExpr("_BOOLEAN")));
+      delete $1;
+    }
+;
+
+an_formulas:
+    an_formula
+    {
+      $$ = new std::vector<CVC3::Expr>;
+      $$->push_back(*$1);
+      delete $1;
+    }
+  |
+    an_formulas an_formula
+    {
+      $1->push_back(*$2);
+      $$ = $1;
+      delete $2;
+    }
+;
+
+an_formula:
+    an_atom
+    {
+      $$ = $1;
+    }
+  | LPAREN_TOK connective an_formulas annotations RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr(*$2, *$3));
+      delete $2;
+      delete $3;
+      delete $4;
+    }
+  | LPAREN_TOK connective an_formulas RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr(*$2, *$3));
+      delete $2;
+      delete $3;
+    }
+  | LPAREN_TOK quant_symb quant_vars an_formula annotations RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4));
+      delete $2;
+      delete $3;
+      delete $4;
+      delete $5;
+    }
+  | LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4));
+      delete $2;
+      delete $3;
+      delete $4;
+    }
+  | LPAREN_TOK quant_symb quant_vars an_formula patterns_annotations RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4, VC->listExpr((*$5).first)));
+      delete $2;
+      delete $3;
+      delete $4;
+      delete $5;
+    }
+  | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK
+    {
+      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
+      $$ = new CVC3::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
+    {
+      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
+      $$ = new CVC3::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
+    {
+      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
+      $$ = new CVC3::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
+    {
+      CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5)));
+      $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7));
+      delete $4;
+      delete $5;
+      delete $7;
+    }
+;
+
+patterns_annotations:
+     patterns
+     {
+       $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<std::string> >;
+       $$->first = *$1;
+       delete $1;
+     }
+     | annotation
+     {
+       $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<std::string> >;
+       $$->second.push_back(*$1);
+       delete $1;
+     }
+     | patterns_annotations patterns
+     {
+       $1->first.insert($1->first.end(), $2->begin(), $2->end());
+       $$ = $1;
+       delete $2;
+     }
+     | patterns_annotations annotation
+     {
+       $1->second.push_back(*$2);
+       $$ = $1;
+       delete $2;
+     }
+
+patterns:
+     pattern
+     {
+       $$ = new std::vector<CVC3::Expr >;
+       $$->push_back(*$1);
+       delete $1;
+     }
+    | patterns pattern
+     {
+       $1->push_back(*$2);
+       $$ = $1;
+       delete $2;
+     }
+
+pattern:
+     PAT_TOK LCURBRACK_TOK an_terms RCURBRACK_TOK
+     {
+       $$ = new CVC3::Expr(VC->listExpr(*$3));
+       delete $3;
+     }
+     | PAT_TOK LCURBRACK_TOK an_formulas RCURBRACK_TOK
+     {
+       $$ = new CVC3::Expr(VC->listExpr(*$3));
+       delete $3;
+     }
+
+
+
+quant_vars:
+    quant_var
+    {
+      $$ = new std::vector<CVC3::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 CVC3::Expr(VC->listExpr(*$2, *$3));
+      delete $2;
+      delete $3;
+    }
+;
+
+quant_symb:
+    EXISTS_TOK
+    {
+      $$ = new std::string("_EXISTS");
+    }
+  | FORALL_TOK
+    {
+      $$ = new std::string("_FORALL");
+    }
+;
+
+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");
+    }
+;
+
+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 CVC3::Expr(VC->listExpr("_TRANS_CLOSURE",
+                                        *$2, (*$3)[0], (*$3)[1]));
+      }
+      else {
+        std::vector<CVC3::Expr> tmp;
+        tmp.push_back(*$2);
+        tmp.insert(tmp.end(), $3->begin(), $3->end());
+        $$ = new CVC3::Expr(VC->listExpr(tmp));
+      }
+      delete $2;
+      delete $3;
+      delete $4;
+    }
+  | LPAREN_TOK pred_symb an_terms RPAREN_TOK
+    {
+      std::vector<CVC3::Expr> tmp;
+      tmp.push_back(*$2);
+      tmp.insert(tmp.end(), $3->begin(), $3->end());
+      $$ = new CVC3::Expr(VC->listExpr(tmp));
+      delete $2;
+      delete $3;
+    }
+  | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
+
+//       std::vector<CVC3::Expr> tmp;
+//       tmp.push_back(*$2);
+//       tmp.insert(tmp.end(), $3->begin(), $3->end());
+//       $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_AND", tmp));
+      delete $3;
+      delete $4;
+    }
+  | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK
+    {
+      $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3));
+//       std::vector<CVC3::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 CVC3::Expr(VC->listExpr("_AND", tmp));
+      delete $3;
+    }
+;
+
+prop_atom:
+    TRUE_TOK
+    {
+      $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
+    }
+  | FALSE_TOK
+    { 
+      $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
+    }
+  | fvar
+    {
+      $$ = $1;
+    }
+  | pred_symb 
+    {
+      $$ = $1;
+    }
+;  
+
+an_terms:
+    an_term
+    {
+      $$ = new std::vector<CVC3::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 CVC3::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 CVC3::Expr(VC->listExpr(*$2));
+      delete $2;
+      delete $3;
+    }
+  | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK
+    {
+      $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_IF", *$3, *$4, *$5));
+      delete $3;
+      delete $4;
+      delete $5;
+    }
+;
+
+basic_term:
+  | TRUE_TOK
+    {
+      $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR"));
+    }
+  | FALSE_TOK
+    { 
+      $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR"));
+    }
+  | fvar
+    {
+      $$ = $1;
+    }
+  | var
+    {
+      $$ = $1;
+    }
+  | fun_symb 
+    {
+      if ($1->size() == 1) {
+        $$ = new CVC3::Expr(((*$1)[0]));
+      }
+      else {
+        $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)));
+      }
+      else {
+        $$ = new CVC3::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 CVC3::Expr(VC->listExpr("_ARRAY",
+                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)),
+                                         VC->listExpr("_BITVECTOR", VC->ratExpr(*$5))));
+      }
+      else {
+        $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5)));
+      }
+      delete $1;
+      delete $3;
+      delete $5;
+    }
+  | SYM_TOK 
+    { 
+      if (*$1 == "Real") {
+	$$ = new CVC3::Expr(VC->idExpr("_REAL"));
+      } else if (*$1 == "Int") {
+	$$ = new CVC3::Expr(VC->idExpr("_INT"));
+      } else {
+	$$ = new CVC3::Expr(VC->idExpr(*$1));
+      }
+      delete $1;
+    }
+;
+
+pred_symb:
+    SYM_TOK
+    {
+      if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) {
+        $$ = new CVC3::Expr(VC->idExpr("_BVLT"));
+      }
+      else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) {
+        $$ = new CVC3::Expr(VC->idExpr("_BVLE"));
+      }
+      else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) {
+        $$ = new CVC3::Expr(VC->idExpr("_BVGE"));
+      }
+      else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) {
+        $$ = new CVC3::Expr(VC->idExpr("_BVGT"));
+      }
+      else if (BVENABLED && *$1 == "bvslt") {
+        $$ = new CVC3::Expr(VC->idExpr("_BVSLT"));
+      }
+      else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) {
+        $$ = new CVC3::Expr(VC->idExpr("_BVSLE"));
+      }
+      else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) {
+        $$ = new CVC3::Expr(VC->idExpr("_BVSGE"));
+      }
+      else if (BVENABLED && *$1 == "bvsgt") {
+        $$ = new CVC3::Expr(VC->idExpr("_BVSGT"));
+      }
+      else {
+        $$ = new CVC3::Expr(VC->idExpr(*$1));
+      }
+      delete $1;
+    }
+  | AR_SYMB 
+    { 
+      if ($1->length() == 1) {
+	switch ((*$1)[0]) {
+	  case '=': $$ = new CVC3::Expr(VC->idExpr("_EQ")); break;
+	  case '<': $$ = new CVC3::Expr(VC->idExpr("_LT")); break;
+	  case '>': $$ = new CVC3::Expr(VC->idExpr("_GT")); break;
+	  default: $$ = new CVC3::Expr(VC->idExpr(*$1)); break;
+	}
+      }
+      else {
+	if (*$1 == "<=") {
+	  $$ = new CVC3::Expr(VC->idExpr("_LE"));
+	} else if (*$1 == ">=") {
+	  $$ = new CVC3::Expr(VC->idExpr("_GE"));
+	}
+	else $$ = new CVC3::Expr(VC->idExpr(*$1));
+      }
+      delete $1;
+    }
+;
+
+fun_symb:
+    SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK
+    {
+      $$ = new std::vector<CVC3::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<CVC3::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<CVC3::Expr>;
+      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"));
+      }
+      else 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 == "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<CVC3::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<CVC3::Expr>;
+      $$->push_back(VC->ratExpr(*$1));
+      delete $1;
+    }
+;
+
+attribute:
+    COLON_TOK SYM_TOK
+    {
+      $$ = $2;
+    }
+;
+
+var:
+    QUESTION_TOK SYM_TOK
+    {
+      $$ = new CVC3::Expr(VC->idExpr(*$2));
+      delete $2;
+    }
+;
+
+fvar:
+    DOLLAR_TOK SYM_TOK
+    {
+      $$ = new CVC3::Expr(VC->idExpr(*$2));
+      delete $2;
+    }
+;
+
+%%