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)

1 files changed, 40 insertions, 0 deletions

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 */