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)

6 files changed, 60 insertions, 48 deletions

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() {