Adding general support for SMT2 set-info command

15 files changed, 279 insertions, 106 deletions

diff --git a/src/expr/command.h b/src/expr/command.h
index 3be957feb..5061722f6 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -29,6 +29,7 @@
 #include "expr/expr.h"
 #include "expr/type.h"
 #include "util/result.h"
+#include "util/sexpr.h"
 
 namespace CVC4 {
 
@@ -142,6 +143,16 @@ protected:
   std::string d_logic;
 };/* class SetBenchmarkLogicCommand */
 
+class CVC4_PUBLIC SetInfoCommand : public Command {
+public:
+  SetInfoCommand(std::string flag, SExpr& sexpr);
+  void invoke(SmtEngine* smt);
+  void toStream(std::ostream& out) const;
+protected:
+  std::string d_flag;
+  SExpr d_sexpr;
+};/* class SetInfoCommand */
+
 class CVC4_PUBLIC CommandSequence : public Command {
 public:
   CommandSequence();
@@ -300,6 +311,17 @@ inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
   out << "SetBenchmarkLogic(" << d_logic << ")";
 }
 
+inline SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
+  d_flag(flag),
+  d_sexpr(sexpr) {
+}
+
+inline void SetInfoCommand::invoke(SmtEngine* smt) { }
+
+inline void SetInfoCommand::toStream(std::ostream& out) const {
+  out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
+}
+
 /* output stream insertion operator for benchmark statuses */
 inline std::ostream& operator<<(std::ostream& out,
                                 BenchmarkStatus status) {
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 5a34354e8..11e3ed604 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -43,6 +43,7 @@ namespace parser {
 AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
   InputStream(name),
   d_input(input) {
+  AlwaysAssert( input != NULL );
 }
 
 AntlrInputStream::~AntlrInputStream() {
@@ -53,34 +54,36 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
   return d_input;
 }
 
-AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) {
+AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap)
+  throw (InputStreamException) {
+  pANTLR3_INPUT_STREAM input = NULL;
   if( useMmap ) {
-    return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) );
+    input = MemoryMappedInputBufferNew(name);
   } else {
-    return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) );
+    input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str());
   }
-/*
-    if( d_inputStream == NULL ) {
-      throw ParserException("Couldn't open file: " + filename);
-    }
-*/
+  if( input == NULL ) {
+    throw InputStreamException("Couldn't open file: " + name);
+  }
+  return new AntlrInputStream( name, input );
 }
 
-AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{
+AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name)
+  throw (InputStreamException) {
   char* inputStr = strdup(input.c_str());
   char* nameStr = strdup(name.c_str());
-/*
-  if( inputStr==NULL || nameStr==NULL ) {
+  AlwaysAssert( inputStr!=NULL && nameStr!=NULL );
+  pANTLR3_INPUT_STREAM inputStream =
+      antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr,
+                                        input.size(),
+                                        (pANTLR3_UINT8) nameStr);
+  if( inputStream==NULL ) {
     throw InputStreamException("Couldn't initialize string input: '" + input + "'");
   }
-*/
-  return new AntlrInputStream( name,
-                               antlr3NewAsciiStringInPlaceStream(
-                                  (pANTLR3_UINT8)inputStr,input.size(),
-                                  (pANTLR3_UINT8)nameStr) );
+  return new AntlrInputStream( name, inputStream );
 }
 
-AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStream) {
+AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) {
   AntlrInput* input;
 
   switch(lang) {
@@ -102,12 +105,12 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStre
   return input;
 }
 
-AntlrInput::AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead) :
+AntlrInput::AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead) :
     Input(inputStream),
     d_lookahead(lookahead),
     d_lexer(NULL),
     d_parser(NULL),
-    d_antlr3InputStream( inputStream->getAntlr3InputStream() ),
+    d_antlr3InputStream( inputStream.getAntlr3InputStream() ),
     d_tokenStream(NULL) {
 }
 
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index d6d01b3cd..18317e4d8 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -62,7 +62,8 @@ public:
    * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
    * input will use the standard ANTLR3 I/O implementation.
    */
-  static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false);
+  static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false)
+    throw (InputStreamException);
 
   /** Create an input from an istream. */
   // AntlrInputStream newInputStream(std::istream& input, const std::string& name);
@@ -72,7 +73,8 @@ public:
    * @param input the string to read
    * @param name the "filename" to use when reporting errors
    */
-  static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name);
+  static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name)
+    throw (InputStreamException);
 };
 
 class Parser;
@@ -134,7 +136,7 @@ public:
    * @param inputStream the input stream
    *
    * */
-  static AntlrInput* newInput(InputLanguage lang, AntlrInputStream *inputStream);
+  static AntlrInput* newInput(InputLanguage lang, AntlrInputStream& inputStream);
 
   /** Retrieve the text associated with a token. */
   static std::string tokenText(pANTLR3_COMMON_TOKEN token);
@@ -153,7 +155,7 @@ protected:
    * @param lookahead the lookahead needed to parse the input (i.e., k for
    * an LL(k) grammar)
    */
-  AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead);
+  AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead);
 
   /** Retrieve the token stream for this parser. Must not be called before
    * <code>setLexer()</code>. */
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 7c879f5bc..d25d7b66b 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -114,6 +114,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     } else {
       if(ex->expecting == ANTLR3_TOKEN_EOF) {
         ss << "Missing end of file marker.";
+      } else if( ex->expecting == 0 ) {
+        ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
       } else {
         ss << "Missing " << tokenNames[ex->expecting] << ".";
       }
@@ -147,6 +149,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     } else {
       if(ex->expecting == ANTLR3_TOKEN_EOF) {
         ss << "Expected end of file.";
+      } else if( ex->expecting == 0 ) {
+        ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
       } else {
         ss << "Expected " << tokenNames[ex->expecting] << ".";
       }
diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp
index 48936a4c9..4a8551a7a 100644
--- a/src/parser/cvc/cvc_input.cpp
+++ b/src/parser/cvc/cvc_input.cpp
@@ -26,9 +26,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-CvcInput::CvcInput(AntlrInputStream *inputStream) :
+CvcInput::CvcInput(AntlrInputStream& inputStream) :
   AntlrInput(inputStream,2) {
-  pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
+  pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
   d_pCvcLexer = CvcLexerNew(input);
diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index ad7110bed..82c31813b 100644
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -45,7 +45,7 @@ public:
    *
    * @param inputStream the input to parse
    */
-  CvcInput(AntlrInputStream *inputStream);
+  CvcInput(AntlrInputStream& inputStream);
 
   /** Create a string input.
    *
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 3c1747759..9ee167897 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -31,12 +31,16 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace parser {
 
+InputStreamException::InputStreamException(const std::string& msg) :
+  Exception(msg) {
+}
+
 const std::string InputStream::getName() const {
   return d_name;
 }
 
-Input::Input(InputStream *inputStream) :
-    d_inputStream( inputStream ) {
+Input::Input(InputStream& inputStream) :
+    d_inputStream( &inputStream ) {
 }
 
 Input::~Input() {
@@ -48,15 +52,19 @@ InputStream *Input::getInputStream() {
 }
 
 Input* Input::newFileInput(InputLanguage lang,
-                           const std::string& filename, bool useMmap) {
+                           const std::string& filename,
+                           bool useMmap)
+  throw (InputStreamException) {
   AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap);
-  return AntlrInput::newInput(lang,inputStream);
+  return AntlrInput::newInput(lang,*inputStream);
 }
 
 Input* Input::newStringInput(InputLanguage lang,
-                             const std::string& str, const std::string& name) {
+                             const std::string& str,
+                             const std::string& name)
+  throw (InputStreamException) {
   AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name);
-  return AntlrInput::newInput(lang,inputStream);
+  return AntlrInput::newInput(lang,*inputStream);
 }
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/input.h b/src/parser/input.h
index 80849c034..b277f6428 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -36,6 +36,13 @@ class FunctionType;
 
 namespace parser {
 
+class CVC4_PUBLIC InputStreamException : public Exception {
+
+public:
+  InputStreamException(const std::string& msg);
+  virtual ~InputStreamException() throw() { }
+};
+
 /** Wrapper around an ANTLR3 input stream. */
 class InputStream {
 
@@ -89,7 +96,8 @@ public:
     * @param filename the input filename
     * @param useMmap true if the parser should use memory-mapped I/O (default: false)
     */
-  static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false);
+  static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false)
+      throw (InputStreamException);
 
   /** Create an input for the given stream.
    *
@@ -105,7 +113,8 @@ public:
    * @param input the input string
    * @param name the name of the stream, for use in error messages
    */
-  static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name);
+  static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name)
+    throw (InputStreamException);
 
 protected:
 
@@ -113,7 +122,7 @@ protected:
    *
    * @param inputStream the input stream
    */
-  Input(InputStream* inputStream);
+  Input(InputStream& inputStream);
 
   /** Retrieve the input stream for this parser. */
   InputStream *getInputStream();
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index 520e6a6d6..7c8bf19dd 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -27,9 +27,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-SmtInput::SmtInput(AntlrInputStream *inputStream) :
+SmtInput::SmtInput(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 2) {
-  pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
+  pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
   d_pSmtLexer = SmtLexerNew(input);
diff --git a/src/parser/smt/smt_input.h b/src/parser/smt/smt_input.h
index 429f4dad5..1d3f87668 100644
--- a/src/parser/smt/smt_input.h
+++ b/src/parser/smt/smt_input.h
@@ -47,7 +47,7 @@ public:
    *
    * @param inputStream the input stream to use
    */
-  SmtInput(AntlrInputStream *inputStream);
+  SmtInput(AntlrInputStream& inputStream);
 
   /**
    * Create a string input.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b062e6b33..76ce91fd0 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -100,8 +100,12 @@ setLogic(Parser *parser, const std::string& name) {
   }
 }
 
+static void
+setInfo(Parser *parser, const std::string& flag, const SExpr& sexpr) {
+  // TODO: ???
 }
 
+}
 
 /**
  * Parses an expression.
@@ -130,16 +134,19 @@ command returns [CVC4::Command* cmd]
   Expr expr;
   Type t;
   std::vector<Type> sorts;
+  SExpr sexpr;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
     { Debug("parser") << "set logic: '" << name << "' " << std::endl;
       setLogic(PARSER_STATE,name);
-      $cmd = new SetBenchmarkLogicCommand(name);   }
-  | SET_INFO_TOK c=setInfo
-    { cmd = c; }
+      $cmd = new SetBenchmarkLogicCommand(name); }
+  | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
+    { name = AntlrInput::tokenText($KEYWORD);
+      setInfo(PARSER_STATE,name,sexpr);    
+      cmd = new SetInfoCommand(name,sexpr); }
   | /* sort declaration */
-    DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL_TOK
+    DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL
     { Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl;
       if( AntlrInput::tokenToInteger(n) > 0 ) {
         Unimplemented("Parameterized user sorts.");
@@ -162,36 +169,31 @@ command returns [CVC4::Command* cmd]
   | /* checksat */
     CHECKSAT_TOK 
     { cmd = new CheckSatCommand(MK_CONST(true)); }
+  | EXIT_TOK
+    { // TODO: Explicitly represent exit as command?
+      cmd = 0; }
   ;
 
-setInfo returns [CVC4::Command* cmd]
-@declarations { 
-  BenchmarkStatus status; 
+symbolicExpr[CVC4::SExpr& sexpr]
+@declarations {
+  std::vector<SExpr> children;
 }
-  : CATEGORY_TOK sym=SYMBOL {
-      // FIXME?
-      cmd = new EmptyCommand(":category");
-    }
-  | DIFFICULTY_TOK RATIONAL_TOK {
-      // FIXME?
-      cmd = new EmptyCommand(":difficulty");
-    }
-  | NOTES_TOK sym=SYMBOL {
-      // FIXME?
-      cmd = new EmptyCommand(":notes");
-    }
-  | SMT_VERSION_TOK RATIONAL_TOK {
-      // FIXME?
-      cmd = new EmptyCommand(":smt-lib-version");
-    }
-  | SOURCE_TOK sym=SYMBOL {
-      // FIXME?
-      cmd = new EmptyCommand(":source");
-    }
-  | STATUS_TOK benchmarkStatus[status]
-    { cmd = new SetBenchmarkStatusCommand(status); }  
-;
-
+  : NUMERAL
+    { sexpr = SExpr(AntlrInput::tokenText($NUMERAL)); }
+  | RATIONAL
+    { sexpr = SExpr(AntlrInput::tokenText($RATIONAL)); }
+  | STRING_LITERAL
+    { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); }
+  | SYMBOL
+    { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
+  | KEYWORD
+    { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
+  | LPAREN_TOK 
+    (symbolicExpr[sexpr] { children.push_back(sexpr); } )* 
+  	RPAREN_TOK
+    { sexpr = SExpr(children); }
+  ;
+  
 /**
  * Matches a term.
  * @return the expression representing the formula
@@ -251,11 +253,11 @@ term[CVC4::Expr& expr]
     /* constants */
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
-  | NUMERAL_TOK
-    { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
-  | RATIONAL_TOK
+  | NUMERAL
+    { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL) ); }
+  | RATIONAL
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
-      expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
+      expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); }
     // NOTE: Theory constants go here
   ;
 
@@ -377,26 +379,27 @@ symbol[std::string& id,
 // Base SMT-LIB tokens
 ASSERT_TOK : 'assert';
 BOOL_TOK : 'Bool';
-CATEGORY_TOK : ':category';
+//CATEGORY_TOK : ':category';
 CHECKSAT_TOK : 'check-sat';
-DIFFICULTY_TOK : ':difficulty';
+//DIFFICULTY_TOK : ':difficulty';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
+EXIT_TOK : 'exit';
 FALSE_TOK : 'false';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
 LPAREN_TOK : '(';
-NOTES_TOK : ':notes';
+//NOTES_TOK : ':notes';
 RPAREN_TOK : ')';
-SAT_TOK : 'sat';
+//SAT_TOK : 'sat';
 SET_LOGIC_TOK : 'set-logic';
 SET_INFO_TOK : 'set-info';
-SMT_VERSION_TOK : ':smt-lib-version';
-SOURCE_TOK : ':source';
-STATUS_TOK : ':status';
+//SMT_VERSION_TOK : ':smt-lib-version';
+//SOURCE_TOK : ':source';
+//STATUS_TOK : ':status';
 TRUE_TOK : 'true';
-UNKNOWN_TOK : 'unknown';
-UNSAT_TOK : 'unsat';
+//UNKNOWN_TOK : 'unknown';
+//UNSAT_TOK : 'unsat';
 
 // operators (NOTE: theory symbols go here)
 AMPERSAND_TOK     : '&';
@@ -422,14 +425,29 @@ TILDE_TOK         : '~';
 XOR_TOK           : 'xor';
 
 /**
- * Matches a symbol from the input. A symbol a non-empty sequence of 
- * letters, digits and the characters + - / * = % ? ! . $ ~ & ^ < > @ that 
- * does not start with a digit or a sequence of printable ASCII characters 
- * that starts and ends with | and does not otherwise contain |.
+ * Matches a symbol from the input. A symbol is a "simple" symbole or a 
+ * sequence of printable ASCII characters that starts and ends with | and 
+ * does not otherwise contain |.
  */
 SYMBOL
+  : SIMPLE_SYMBOL
+  | '|' ~('|')+ '|'
+  ;
+
+/**
+ * Matches a keyword from the input. A keyword is a symbol symbol, prefixed
+ * with a colon.
+ */
+KEYWORD
+  : ':' SIMPLE_SYMBOL
+  ;
+
+/** Matches a "simple" symbol: a non-empty sequence of letters, digits and 
+ * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a 
+ * digit. 
+ */
+fragment SIMPLE_SYMBOL 
   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)*
-  | '|' ~('|') '|'
   ;
 
 /**
@@ -442,11 +460,11 @@ WHITESPACE
 /**
  * Matches a numeral from the input (non-empty sequence of digits).
  */
-NUMERAL_TOK
+NUMERAL
   : DIGIT+
   ;
 
-RATIONAL_TOK
+RATIONAL
   : DIGIT+ '.' DIGIT+
   ;
 
@@ -479,12 +497,12 @@ ALPHA
  * Matches the digits (0-9)
  */
 fragment DIGIT : '0'..'9';
-// fragment NON_ZERO_DIGIT : '1'..'9';
-// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
 
+/** Matches the characters that may appear in a "symbol" (i.e., an identifier) 
+ */
 fragment SYMBOL_CHAR 
-  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~' | '&' 
-  | '^' | '<' | '>' | '@'
+  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' 
+  | '&' | '^' | '<' | '>' | '@'
   ;
 
 /**
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index f962578e9..bcefe166b 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -27,9 +27,9 @@ namespace CVC4 {
 namespace parser {
 
 /* Use lookahead=2 */
-Smt2Input::Smt2Input(AntlrInputStream *inputStream) :
+Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
   AntlrInput(inputStream, 2) {
-  pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
+  pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
   AlwaysAssert( input != NULL );
 
   d_pSmt2Lexer = Smt2LexerNew(input);
diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 2937d4ed8..ad32edcbc 100644
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -40,6 +40,12 @@ class Smt2Input : public AntlrInput {
   /** The ANTLR3 CVC parser for the input. */
   pSmt2Parser d_pSmt2Parser;
 
+  /**
+   * Initialize the class. Called from the constructors once the input
+   * stream is initialized.
+   */
+  void init();
+
 public:
 
   /**
@@ -47,7 +53,7 @@ public:
    *
    * @param inputStream the input stream to use
    */
-  Smt2Input(AntlrInputStream *inputStream);
+  Smt2Input(AntlrInputStream& inputStream);
 
   /**
    * Create a string input.
@@ -59,7 +65,7 @@ public:
 //  Smt2Input(ExprManager* exprManager, const std::string& input, const std::string& name);
 
   /** Destructor. Frees the lexer and the parser. */
-  ~Smt2Input();
+  virtual ~Smt2Input();
 
 protected:
 
@@ -79,14 +85,6 @@ protected:
    */
   Expr parseExpr() throw(ParserException);
 
-private:
-
-  /**
-   * Initialize the class. Called from the constructors once the input
-   * stream is initialized.
-   */
-  void init();
-
 };/* class Smt2Input */
 
 }/* CVC4::parser namespace */
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 7820acb0a..7025c2952 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -28,4 +28,5 @@ libutil_la_SOURCES = \
 	integer.cpp \
 	bitvector.h \
 	bitvector.cpp \
-	gmp_util.h
+	gmp_util.h \
+	sexpr.h
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
new file mode 100644
index 000000000..cf9298c4e
--- /dev/null
+++ b/src/util/sexpr.h
@@ -0,0 +1,108 @@
+/*********************                                                        */
+/** sexpr.cpp
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  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.
+ **
+ ** Simple representation of SMT S-expressions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SEXPR_H_
+#define __CVC4__SEXPR_H_
+
+#include "util/Assert.h"
+
+#include <vector>
+#include <string>
+
+namespace CVC4 {
+
+/**
+ * A simple S-expression. An S-expression is either an atom with a string value, or a
+ * list of other S-expressions.
+ */
+class CVC4_PUBLIC SExpr {
+
+  /** Flag telling us if this is an atom or a list. */
+  bool d_isAtom;
+
+  /** The value of an atomic S-expression. */
+  std::string d_value;
+
+  /** The children of a list S-expression. */
+  std::vector<SExpr> d_children;
+
+public:
+  SExpr() :
+    d_isAtom(true) {
+  }
+
+  SExpr(const std::string& value) :
+    d_isAtom(true),
+    d_value(value) {
+  }
+
+  SExpr(const std::vector<SExpr> children) :
+    d_isAtom(false),
+    d_children(children) {
+  }
+
+  /** Is this S-expression an atom? */
+  bool isAtom() const;
+
+  /** Get the string value of this S-expression. This will cause an error if this S-expression
+   * is not an atom.
+   */
+  const std::string getValue() const;
+
+  /** Get the children of this S-expression. This will cause an error if this S-expression
+   * is not a list.
+   */
+  const std::vector<SExpr> getChildren() const;
+};
+
+inline bool SExpr::isAtom() const {
+  return d_isAtom;
+}
+
+inline const std::string SExpr::getValue() const {
+  AlwaysAssert( d_isAtom );
+  return d_value;
+}
+
+inline const std::vector<SExpr> SExpr::getChildren() const {
+  AlwaysAssert( !d_isAtom );
+  return d_children;
+}
+
+inline std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
+  if( sexpr.isAtom() ) {
+    out << sexpr.getValue();
+  } else {
+    std::vector<SExpr> children = sexpr.getChildren();
+    out << "(";
+    bool first = true;
+    for( std::vector<SExpr>::iterator it = children.begin(); it != children.end(); ++it ) {
+      if( first ) {
+        first = false;
+      } else {
+        out << " ";
+      }
+        out << *it;
+    }
+    out << ")";
+  }
+  return out;
+}
+
+}
+
+#endif /* __CVC4__SEXPR_H_ */