1 files changed, 5 insertions, 90 deletions

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 242638f82..75d625edc 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -13,25 +13,22 @@
  **
  ** Base of the pretty-printer interface.
  **/
-
 #include "printer/printer.h"
 
-#include "util/language.h"
+#include <string>
 
+#include "options/language.h"
+#include "printer/ast/ast_printer.h"
+#include "printer/cvc/cvc_printer.h"
 #include "printer/smt1/smt1_printer.h"
 #include "printer/smt2/smt2_printer.h"
 #include "printer/tptp/tptp_printer.h"
-#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];
-const int PrettySExprs::s_iosIndex = std::ios_base::xalloc();
 
 Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   using namespace CVC4::language::output;
@@ -57,7 +54,7 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
 
   case LANG_SYGUS:
     return new printer::smt2::Smt2Printer(printer::smt2::sygus_variant);
-    
+
   case LANG_AST:
     return new printer::ast::AstPrinter();
 
@@ -69,89 +66,7 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   }
 }/* Printer::makePrinter() */
 
-void Printer::toStream(std::ostream& out, const Result& r) const throw() {
-  if(r.getType() == Result::TYPE_SAT) {
-    switch(r.isSat()) {
-    case Result::UNSAT:
-      out << "unsat";
-      break;
-    case Result::SAT:
-      out << "sat";
-      break;
-    case Result::SAT_UNKNOWN:
-      out << "unknown";
-      if(r.whyUnknown() != Result::UNKNOWN_REASON) {
-        out << " (" << r.whyUnknown() << ")";
-      }
-      break;
-    }
-  } else {
-    switch(r.isValid()) {
-    case Result::INVALID:
-      out << "invalid";
-      break;
-    case Result::VALID:
-      out << "valid";
-      break;
-    case Result::VALIDITY_UNKNOWN:
-      out << "unknown";
-      if(r.whyUnknown() != Result::UNKNOWN_REASON) {
-        out << " (" << r.whyUnknown() << ")";
-      }
-      break;
-    }
-  }
-}/* Printer::toStream() */
-
-static void toStreamRec(std::ostream& out, const SExpr& sexpr, int indent) throw() {
-  if(sexpr.isInteger()) {
-    out << sexpr.getIntegerValue();
-  } else if(sexpr.isRational()) {
-    out << fixed << sexpr.getRationalValue().getDouble();
-  } 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 {
-    const vector<SExpr>& kids = sexpr.getChildren();
-    out << (indent > 0 && kids.size() > 1 ? "( " : "(");
-    bool first = true;
-    for(vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
-      if(first) {
-        first = false;
-      } else {
-        if(indent > 0) {
-          out << "\n" << string(indent, ' ');
-        } else {
-          out << ' ';
-        }
-      }
-      toStreamRec(out, *i, indent <= 0 || indent > 2 ? 0 : indent + 2);
-    }
-    if(indent > 0 && kids.size() > 1) {
-      out << '\n';
-      if(indent > 2) {
-        out << string(indent - 2, ' ');
-      }
-    }
-    out << ')';
-  }
-}/* toStreamRec() */
 
-void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  toStreamRec(out, sexpr, PrettySExprs::getPrettySExprs(out) ? 2 : 0);
-}/* Printer::toStream(SExpr) */
 
 void Printer::toStream(std::ostream& out, const Model& m) const throw() {
   for(size_t i = 0; i < m.getNumCommands(); ++i) {