SMT-LIBv2 compliance updates:

* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
  (there were some minor differences from the spec)

13 files changed, 208 insertions, 133 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 5b889712d..f48e07887 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -991,7 +991,7 @@ std::string GetInfoCommand::getFlag() const throw() {
 void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     vector<SExpr> v;
-    v.push_back(SExpr(d_flag));
+    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
     v.push_back(smtEngine->getInfo(d_flag));
     stringstream ss;
     ss << SExpr(v);
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 577438d37..bddb64c3c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -174,9 +174,8 @@ command returns [CVC4::Command* cmd = NULL]
   SExpr sexpr;
 }
   : /* set the logic */
-    SET_LOGIC_TOK SYMBOL
-    { name = AntlrInput::tokenText($SYMBOL);
-      Debug("parser") << "set logic: '" << name << "'" << std::endl;
+    SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
+    { Debug("parser") << "set logic: '" << name << "'" << std::endl;
       if( PARSER_STATE->logicIsSet() ) {
         PARSER_STATE->parseError("Only one set-logic is allowed.");
       }
@@ -407,8 +406,8 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr]
     { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
   | str[s]
     { sexpr = SExpr(s); }
-  | SYMBOL
-    { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
+  | symbol[s,CHECK_NONE,SYM_SORT]
+    { sexpr = SExpr(s); }
   | builtinOp[k]
     { std::stringstream ss;
       ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
@@ -636,7 +635,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       // valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
 
-  | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK
+  | LPAREN_TOK INDEX_TOK bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL RPAREN_TOK
     { if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
         expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
       } else {
@@ -759,8 +758,8 @@ str[std::string& s]
   ;
 
 /**
-* Matches a builtin operator symbol and sets kind to its associated Expr kind.
-*/
+ * Matches a builtin operator symbol and sets kind to its associated Expr kind.
+ */
 builtinOp[CVC4::Kind& kind]
 @init {
   Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
@@ -952,12 +951,16 @@ symbolList[std::vector<std::string>& names,
 symbol[std::string& id,
        CVC4::parser::DeclarationCheck check,
        CVC4::parser::SymbolType type]
-  : SYMBOL
-    { id = AntlrInput::tokenText($SYMBOL);
-      Debug("parser") << "symbol: " << id
-                      << " check? " << check
-                      << " type? " << type << std::endl;
-      PARSER_STATE->checkDeclaration(id, check, type); }
+  : SIMPLE_SYMBOL
+    { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
+      PARSER_STATE->checkDeclaration(id, check, type);
+    }
+  | QUOTED_SYMBOL
+    { id = AntlrInput::tokenText($QUOTED_SYMBOL);
+      /* strip off the quotes */
+      id = id.substr(1, id.size() - 2);
+      PARSER_STATE->checkDeclaration(id, check, type);
+    }
   ;
 
 /**
@@ -1133,13 +1136,14 @@ BVSGT_TOK : 'bvsgt';
 BVSGE_TOK : 'bvsge';
 
 /**
- * Matches a symbol from the input. A symbol is a "simple" symbol or a
- * sequence of printable ASCII characters that starts and ends with | and
- * does not otherwise contain |.
+ * A sequence of printable ASCII characters (except backslash) that starts
+ * and ends with | and does not otherwise contain |.
+ *
+ * You shouldn't generally use this in parser rules, as the |quoting|
+ * will be part of the token text.  Use the symbol[] parser rule instead.
  */
-SYMBOL
-  : SIMPLE_SYMBOL
-  | '|' ~('|')+ '|'
+QUOTED_SYMBOL
+  : '|' ~('|' | '\\')* '|'
   ;
 
 /**
@@ -1147,17 +1151,18 @@ SYMBOL
  * with a colon.
  */
 KEYWORD
-  : ':' SIMPLE_SYMBOL
+  : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
   ;
 
-/** Matches a "simple" symbol: a non-empty sequence of letters, digits and
+/**
+ * Matches a "simple" symbol: a non-empty sequence of letters, digits and
  * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
- * digit, and is not the special reserved symbol '_'.
+ * digit, and is not the special reserved symbols '!' or '_'.
  */
-fragment SIMPLE_SYMBOL
+SIMPLE_SYMBOL
   : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
   | ALPHA
-  | SYMBOL_CHAR_NOUNDERSCORE
+  | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
   ;
 
 /**
@@ -1219,8 +1224,11 @@ BINARY_LITERAL
 
 
 /**
- * Matches a double quoted string literal. Escaping is supported, and
+ * Matches a double quoted string literal.  Escaping is supported, and
  * escape character '\' has to be escaped.
+ *
+ * You shouldn't generally use this in parser rules, as the quotes
+ * will be part of the token text.  Use the str[] parser rule instead.
  */
 STRING_LITERAL
   : '"' (ESCAPE | ~('"'|'\\'))* '"'
@@ -1250,18 +1258,22 @@ fragment DIGIT : '0'..'9';
 fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
 
 /**
- * Matches the characters that may appear in a "symbol" (i.e., an identifier)
+ * Matches the characters that may appear as a one-character "symbol"
+ * (which excludes _ and !, which are reserved words in SMT-LIBv2).
  */
-fragment SYMBOL_CHAR_NOUNDERSCORE
-  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
+fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
+  : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
   | '&' | '^' | '<' | '>' | '@'
   ;
 
+/**
+ * Matches the characters that may appear in a "symbol" (i.e., an identifier)
+ */
 fragment SYMBOL_CHAR
-  : SYMBOL_CHAR_NOUNDERSCORE | '_'
+  : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'
   ;
 
 /**
  * Matches an allowed escaped character.
  */
-fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
+fragment ESCAPE : '\\' ('"' | '\\');
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index e4a25e008..664ea58fc 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -709,6 +709,10 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
 
 }/* CvcPrinter::toStream(Command*) */
 
+static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+  Printer::getPrinter(language::output::LANG_CVC4)->toStream(out, sexpr);
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
 
@@ -725,29 +729,6 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
 
 }/* CvcPrinter::toStream(CommandStatus*) */
 
-static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  if(sexpr.isInteger()) {
-    out << sexpr.getIntegerValue();
-  } else if(sexpr.isRational()) {
-    out << sexpr.getRationalValue();
-  } else if(sexpr.isString()) {
-    string s = sexpr.getValue();
-    // escape backslash and quote
-    for(size_t i = 0; i < s.size(); ++i) {
-      if(s[i] == '"') {
-        s.replace(i, 1, "\\\"");
-        ++i;
-      } else if(s[i] == '\\') {
-        s.replace(i, 1, "\\\\");
-        ++i;
-      }
-    }
-    out << "\"" << s << "\"";
-  } else {
-    out << sexpr;
-  }
-}
-
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "ASSERT " << c->getExpr() << ";";
 }
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 5229400b5..0881b814b 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -25,6 +25,10 @@
 #include "printer/cvc/cvc_printer.h"
 #include "printer/ast/ast_printer.h"
 
+#include <string>
+
+using namespace std;
+
 namespace CVC4 {
 
 Printer* Printer::d_printers[language::output::LANG_MAX];
@@ -87,4 +91,40 @@ void Printer::toStream(std::ostream& out, const Result& r) const throw() {
   }
 }/* Printer::toStream() */
 
+void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+  if(sexpr.isInteger()) {
+    out << sexpr.getIntegerValue();
+  } else if(sexpr.isRational()) {
+    out << sexpr.getRationalValue();
+  } else if(sexpr.isKeyword()) {
+    out << sexpr.getValue();
+  } else if(sexpr.isString()) {
+    string s = sexpr.getValue();
+    // escape backslash and quote
+    for(size_t i = 0; i < s.length(); ++i) {
+      if(s[i] == '"') {
+        s.replace(i, 1, "\\\"");
+        ++i;
+      } else if(s[i] == '\\') {
+        s.replace(i, 1, "\\\\");
+        ++i;
+      }
+    }
+    out << "\"" << s << "\"";
+  } else {
+    out << '(';
+    const vector<SExpr>& kids = sexpr.getChildren();
+    bool first = true;
+    for(vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
+      if(first) {
+        first = false;
+      } else {
+        out << ' ';
+      }
+      out << *i;
+    }
+    out << ')';
+  }
+}/* Printer::toStream() */
+
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 8d1931a83..e3b1d6f40 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -22,6 +22,7 @@
 #define __CVC4__PRINTER__PRINTER_H
 
 #include "util/language.h"
+#include "util/sexpr.h"
 #include "expr/node.h"
 #include "expr/command.h"
 
@@ -62,6 +63,9 @@ public:
   /** Write a CommandStatus out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
 
+  /** Write an SExpr out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const SExpr& sexpr) const throw();
+
   /**
    * Write a Result out to a stream with this Printer.
    *
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index f74a1e07d..fa46523a4 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -47,6 +47,10 @@ void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw
   s->toStream(out, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
+void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+}/* SmtPrinter::toStream() */
+
 }/* CVC4::printer::smt namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 612dfd19e..6e1c607bf 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -34,6 +34,7 @@ public:
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
+  void toStream(std::ostream& out, const SExpr& sexpr) const throw();
 };/* class SmtPrinter */
 
 }/* CVC4::printer::smt namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 640f4209c..a3b22ac24 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -27,6 +27,7 @@
 #include "printer/dagification_visitor.h"
 #include "util/node_visitor.h"
 #include "theory/substitutions.h"
+#include "util/language.h"
 
 using namespace std;
 
@@ -503,27 +504,8 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
 
 }/* Smt2Printer::toStream(Command*) */
 
-static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  if(sexpr.isInteger()) {
-    out << sexpr.getIntegerValue();
-  } else if(sexpr.isRational()) {
-    out << sexpr.getRationalValue();
-  } else if(sexpr.isString()) {
-    string s = sexpr.getValue();
-    // escape backslash and quote
-    for(size_t i = 0; i < s.length(); ++i) {
-      if(s[i] == '"') {
-        s.replace(i, 1, "\\\"");
-        ++i;
-      } else if(s[i] == '\\') {
-        s.replace(i, 1, "\\\\");
-        ++i;
-      }
-    }
-    out << "\"" << s << "\"";
-  } else {
-    out << sexpr;
-  }
+static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+  Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
 }
 
 template <class T>
@@ -679,23 +661,23 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw
 }
 
 static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
-  out << "(set-info " << c->getFlag() << " ";
+  out << "(set-info :" << c->getFlag() << " ";
   toStream(out, c->getSExpr());
   out << ")";
 }
 
 static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
-  out << "(get-info " << c->getFlag() << ")";
+  out << "(get-info :" << c->getFlag() << ")";
 }
 
 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
-  out << "(set-option " << c->getFlag() << " ";
+  out << "(set-option :" << c->getFlag() << " ";
   toStream(out, c->getSExpr());
   out << ")";
 }
 
 static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
-  out << "(get-option " << c->getFlag() << ")";
+  out << "(get-option :" << c->getFlag() << ")";
 }
 
 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a182d8927..81a212edd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -660,7 +660,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value)
 }
 
 SExpr SmtEngine::getInfo(const std::string& key) const
-  throw(BadOptionException) {
+  throw(BadOptionException, ModalException) {
 
   SmtScope smts(this);
 
@@ -677,7 +677,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const
     }
     return stats;
   } else if(key == ":error-behavior") {
-    return SExpr("immediate-exit");
+    return SExpr::Keyword("immediate-exit");
   } else if(key == ":name") {
     return Configuration::getName();
   } else if(key == ":version") {
@@ -687,10 +687,10 @@ SExpr SmtEngine::getInfo(const std::string& key) const
   } else if(key == ":status") {
     return d_status.asSatisfiabilityResult().toString();
   } else if(key == ":reason-unknown") {
-    if(d_status.isUnknown()) {
+    if(!d_status.isNull() && d_status.isUnknown()) {
       stringstream ss;
       ss << d_status.whyUnknown();
-      return ss.str();
+      return SExpr::Keyword(ss.str());
     } else {
       throw ModalException("Can't get-info :reason-unknown when the "
                            "last result wasn't unknown!");
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 4df9054a7..efb2425a1 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -309,7 +309,7 @@ public:
    * Query information about the SMT environment.
    */
   SExpr getInfo(const std::string& key) const
-    throw(BadOptionException);
+    throw(BadOptionException, ModalException);
 
   /**
    * Set an aspect of the current SMT execution environment.
@@ -536,6 +536,13 @@ public:
   unsigned long getTimeRemaining() const throw(ModalException);
 
   /**
+   * Permit access to the underlying ExprManager.
+   */
+  ExprManager* getExprManager() const {
+    return d_exprManager;
+  }
+
+  /**
    * Permit access to the underlying StatisticsRegistry.
    */
   StatisticsRegistry* getStatisticsRegistry() const;
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 08b5d05f5..a3c6a00e9 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -46,6 +46,7 @@ libutil_la_SOURCES = \
 	matcher.h \
 	gmp_util.h \
 	sexpr.h \
+	sexpr.cpp \
 	stats.h \
 	stats.cpp \
 	dynamic_array.h \
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
new file mode 100644
index 000000000..ff6ff6872
--- /dev/null
+++ b/src/util/sexpr.cpp
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file sexpr.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  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.\endverbatim
+ **
+ ** \brief Simple representation of S-expressions
+ **
+ ** Simple representation of S-expressions.
+ **/
+
+#include <iostream>
+#include <vector>
+
+#include "util/sexpr.h"
+#include "util/Assert.h"
+#include "printer/printer.h"
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, SExpr::SExprTypes type) {
+  switch(type) {
+  case SExpr::SEXPR_STRING:
+    out << "SEXPR_STRING";
+    break;
+  case SExpr::SEXPR_KEYWORD:
+    out << "SEXPR_KEYWORD";
+    break;
+  case SExpr::SEXPR_INTEGER:
+    out << "SEXPR_INTEGER";
+    break;
+  case SExpr::SEXPR_RATIONAL:
+    out << "SEXPR_RATIONAL";
+    break;
+  case SExpr::SEXPR_NOT_ATOM:
+    out << "SEXPR_NOT_ATOM";
+    break;
+  default:
+    Unimplemented();
+    break;
+  }
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
+  Printer::getPrinter(Expr::setlanguage::getLanguage(out))->toStream(out, sexpr);
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 9d568bad8..a49da4b48 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -5,15 +5,15 @@
  ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012  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.\endverbatim
  **
- ** \brief Simple representation of SMT S-expressions.
+ ** \brief Simple representation of S-expressions
  **
- ** Simple representation of SMT S-expressions.
+ ** Simple representation of S-expressions.
  **/
 
 #include "cvc4_public.h"
@@ -36,13 +36,14 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC SExpr {
 
-  enum SexprTypes {
+  enum SExprTypes {
     SEXPR_STRING,
+    SEXPR_KEYWORD,
     SEXPR_INTEGER,
     SEXPR_RATIONAL,
     SEXPR_NOT_ATOM
   } d_sexprType;
-  friend std::ostream& operator<<(std::ostream&, SexprTypes);
+  friend std::ostream& operator<<(std::ostream&, SExprTypes);
 
   /** The value of an atomic integer-valued S-expression. */
   CVC4::Integer d_integerValue;
@@ -57,6 +58,13 @@ class CVC4_PUBLIC SExpr {
   std::vector<SExpr> d_children;
 
 public:
+
+  class Keyword : protected std::string {
+  public:
+    Keyword(const std::string& s) : std::string(s) {}
+    const std::string& getString() const { return *this; }
+  };/* class Keyword */
+
   SExpr() :
     d_sexprType(SEXPR_STRING),
     d_integerValue(0),
@@ -89,6 +97,14 @@ public:
     d_children() {
   }
 
+  SExpr(const Keyword& value) :
+    d_sexprType(SEXPR_KEYWORD),
+    d_integerValue(0),
+    d_rationalValue(0),
+    d_stringValue(value.getString()),
+    d_children() {
+  }
+
   SExpr(const std::vector<SExpr> children) :
     d_sexprType(SEXPR_NOT_ATOM),
     d_integerValue(0),
@@ -109,6 +125,9 @@ public:
   /** Is this S-expression a string? */
   bool isString() const;
 
+  /** Is this S-expression a string? */
+  bool isKeyword() const;
+
   /**
    * Get the string value of this S-expression. This will cause an
    * error if this S-expression is not an atom.
@@ -131,30 +150,11 @@ public:
    * 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;
+  const std::vector<SExpr>& getChildren() const;
 
 };/* class SExpr */
 
-inline std::ostream& operator<<(std::ostream& out, SExpr::SexprTypes type) {
-  switch(type) {
-  case SExpr::SEXPR_STRING:
-    out << "SEXPR_STRING";
-    break;
-  case SExpr::SEXPR_INTEGER:
-    out << "SEXPR_INTEGER";
-    break;
-  case SExpr::SEXPR_RATIONAL:
-    out << "SEXPR_RATIONAL";
-    break;
-  case SExpr::SEXPR_NOT_ATOM:
-    out << "SEXPR_NOT_ATOM";
-    break;
-  default:
-    Unimplemented();
-    break;
-  }
-  return out;
-}
+std::ostream& operator<<(std::ostream& out, SExpr::SExprTypes type) CVC4_PUBLIC;
 
 inline bool SExpr::isAtom() const {
   return d_sexprType != SEXPR_NOT_ATOM;
@@ -172,6 +172,10 @@ inline bool SExpr::isString() const {
   return d_sexprType == SEXPR_STRING;
 }
 
+inline bool SExpr::isKeyword() const {
+  return d_sexprType == SEXPR_KEYWORD;
+}
+
 inline const std::string SExpr::getValue() const {
   AlwaysAssert( isAtom() );
   switch(d_sexprType) {
@@ -180,6 +184,7 @@ inline const std::string SExpr::getValue() const {
   case SEXPR_RATIONAL:
     return d_rationalValue.toString();
   case SEXPR_STRING:
+  case SEXPR_KEYWORD:
     return d_stringValue;
   default:
     Unhandled(d_sexprType);
@@ -197,32 +202,12 @@ inline const CVC4::Rational& SExpr::getRationalValue() const {
   return d_rationalValue;
 }
 
-inline const std::vector<SExpr> SExpr::getChildren() const {
+inline const std::vector<SExpr>& SExpr::getChildren() const {
   AlwaysAssert( !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;
-}
+std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
 
 }/* CVC4 namespace */