Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

13 files changed, 96 insertions, 491 deletions

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index c24ed8372..b26a983be 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -13,20 +13,20 @@
  **
  ** The pretty-printer interface for the AST output language.
  **/
-
 #include "printer/ast/ast_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "expr/command.h"
-#include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
-#include "theory/substitutions.h"
 
 #include <iostream>
-#include <vector>
 #include <string>
 #include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "printer/dagification_visitor.h"
+#include "smt_util/command.h"
+#include "smt_util/node_visitor.h"
+#include "theory/substitutions.h"
 
 using namespace std;
 
@@ -398,4 +398,3 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
 }/* CVC4::printer::ast namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
-
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2e1170666..d33b97d66 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -15,25 +15,26 @@
  **/
 
 #include "printer/cvc/cvc_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager_attributes.h" // for VarNameAttr
-#include "expr/command.h"
-#include "theory/substitutions.h"
-#include "smt/smt_engine.h"
-#include "smt/options.h"
-#include "theory/theory_model.h"
-#include "theory/arrays/theory_arrays_rewriter.h"
-#include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
 
-#include <iostream>
-#include <vector>
-#include <string>
-#include <typeinfo>
 #include <algorithm>
+#include <iostream>
 #include <iterator>
 #include <stack>
+#include <string>
+#include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager_attributes.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "printer/dagification_visitor.h"
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "smt_util/command.h"
+#include "smt_util/node_visitor.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/substitutions.h"
+#include "theory/theory_model.h"
 
 using namespace std;
 
@@ -894,10 +895,6 @@ 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, bool cvc3Mode) throw();
 
@@ -1170,7 +1167,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool
 
 static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
   out << "% (set-info " << c->getFlag() << " ";
-  toStream(out, c->getSExpr());
+  OutputLanguage language =
+      cvc3Mode ? language::output::LANG_CVC3 : language::output::LANG_CVC4;
+  SExpr::toStream(out, c->getSExpr(), language);
   out << ")";
 }
 
@@ -1180,7 +1179,7 @@ static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode)
 
 static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
   out << "OPTION \"" << c->getFlag() << "\" ";
-  toStream(out, c->getSExpr());
+  SExpr::toStream(out, c->getSExpr(), language::output::LANG_CVC4);
   out << ";";
 }
 
diff --git a/src/printer/modes.cpp b/src/printer/modes.cpp
deleted file mode 100644
index 01b7fc833..000000000
--- a/src/printer/modes.cpp
+++ /dev/null
@@ -1,51 +0,0 @@
-/*********************                                                        */
-/*! \file modes.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "printer/modes.h"
-
-namespace CVC4 {
-
-std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) {
-  switch(mode) {
-  case MODEL_FORMAT_MODE_DEFAULT:
-    out << "MODEL_FORMAT_MODE_DEFAULT";
-    break;
-  case MODEL_FORMAT_MODE_TABLE:
-    out << "MODEL_FORMAT_MODE_TABLE";
-    break;
-  default:
-    out << "ModelFormatMode:UNKNOWN![" << unsigned(mode) << "]";
-  }
-
-  return out;
-}
-
-std::ostream& operator<<(std::ostream& out, InstFormatMode mode) {
-  switch(mode) {
-  case INST_FORMAT_MODE_DEFAULT:
-    out << "INST_FORMAT_MODE_DEFAULT";
-    break;
-  case INST_FORMAT_MODE_SZS:
-    out << "INST_FORMAT_MODE_SZS";
-    break;
-  default:
-    out << "InstFormatMode:UNKNOWN![" << unsigned(mode) << "]";
-  }
-  return out;
-}
-
-}/* CVC4 namespace */
diff --git a/src/printer/modes.h b/src/printer/modes.h
deleted file mode 100644
index 849e0d149..000000000
--- a/src/printer/modes.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/*********************                                                        */
-/*! \file modes.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__PRINTER__MODES_H
-#define __CVC4__PRINTER__MODES_H
-
-#include <iostream>
-
-namespace CVC4 {
-
-/** Enumeration of model_format modes (how to print models from get-model command). */
-typedef enum {
-  /** default mode (print expressions in the output language format) */
-  MODEL_FORMAT_MODE_DEFAULT,
-  /** print functional values in a table format */
-  MODEL_FORMAT_MODE_TABLE,
-} ModelFormatMode;
-
-/** Enumeration of inst_format modes (how to print models from get-model command). */
-typedef enum {
-  /** default mode (print expressions in the output language format) */
-  INST_FORMAT_MODE_DEFAULT,
-  /** print as SZS proof */
-  INST_FORMAT_MODE_SZS,
-} InstFormatMode;
-
-std::ostream& operator<<(std::ostream& out, ModelFormatMode mode) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out, InstFormatMode mode) CVC4_PUBLIC;
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__MODEL_FORMAT_H */
diff --git a/src/printer/options b/src/printer/options
deleted file mode 100644
index 4daa9c77d..000000000
--- a/src/printer/options
+++ /dev/null
@@ -1,14 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module PRINTER "printer/options.h" Printing
-
-option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::printer::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
- print format mode for models, see --model-format=help
-
-option instFormatMode --inst-format=MODE InstFormatMode :handler CVC4::printer::stringToInstFormatMode :default INST_FORMAT_MODE_DEFAULT :read-write :include "printer/modes.h" :handler-include "printer/options_handlers.h"
- print format mode for instantiations, see --inst-format=help
-
-endmodule
diff --git a/src/printer/options_handlers.h b/src/printer/options_handlers.h
deleted file mode 100644
index 64b585a94..000000000
--- a/src/printer/options_handlers.h
+++ /dev/null
@@ -1,77 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Custom handlers and predicates for printer options
- **
- ** Custom handlers and predicates for printer options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PRINTER__OPTIONS_HANDLERS_H
-#define __CVC4__PRINTER__OPTIONS_HANDLERS_H
-
-#include "printer/modes.h"
-
-namespace CVC4 {
-namespace printer {
-
-static const std::string modelFormatHelp = "\
-Model format modes currently supported by the --model-format option:\n\
-\n\
-default \n\
-+ Print model as expressions in the output language format.\n\
-\n\
-table\n\
-+ Print functional expressions over finite domains in a table format.\n\
-";
-
-static const std::string instFormatHelp = "\
-Inst format modes currently supported by the --model-format option:\n\
-\n\
-default \n\
-+ Print instantiations as a list in the output language format.\n\
-\n\
-szs\n\
-+ Print instantiations as SZS compliant proof.\n\
-";
-
-inline ModelFormatMode stringToModelFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "default") {
-    return MODEL_FORMAT_MODE_DEFAULT;
-  } else if(optarg == "table") {
-    return MODEL_FORMAT_MODE_TABLE;
-  } else if(optarg == "help") {
-    puts(modelFormatHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --model-format: `") +
-                          optarg + "'.  Try --model-format help.");
-  }
-}
-
-inline InstFormatMode stringToInstFormatMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg == "default") {
-    return INST_FORMAT_MODE_DEFAULT;
-  } else if(optarg == "szs") {
-    return INST_FORMAT_MODE_SZS;
-  } else if(optarg == "help") {
-    puts(instFormatHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --inst-format: `") +
-                          optarg + "'.  Try --inst-format help.");
-  }
-}
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__OPTIONS_HANDLERS_H */
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) {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 44e5ac9f4..30d33d46b 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -22,11 +22,11 @@
 #include <map>
 #include <string>
 
-#include "util/language.h"
-#include "util/sexpr.h"
-#include "util/model.h"
 #include "expr/node.h"
-#include "expr/command.h"
+#include "expr/sexpr.h"
+#include "options/language.h"
+#include "smt_util/command.h"
+#include "smt_util/model.h"
 
 namespace CVC4 {
 
@@ -91,18 +91,7 @@ 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.
-   *
-   * The default implementation writes a reasonable string in lowercase
-   * for sat, unsat, valid, invalid, or unknown results.  This behavior
-   * is overridable by each Printer, since sometimes an output language
-   * has a particular preference for how results should appear.
-   */
-  virtual void toStream(std::ostream& out, const Result& r) const throw();
 
   /** Write a Model out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const Model& m) const throw();
@@ -115,78 +104,6 @@ public:
 
 };/* class Printer */
 
-/**
- * IOStream manipulator to pretty-print SExprs.
- */
-class PrettySExprs {
-  /**
-   * The allocated index in ios_base for our setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * When this manipulator is used, the setting is stored here.
-   */
-  bool d_prettySExprs;
-
-public:
-  /**
-   * Construct a PrettySExprs with the given setting.
-   */
-  PrettySExprs(bool prettySExprs) : d_prettySExprs(prettySExprs) {}
-
-  inline void applyPrettySExprs(std::ostream& out) {
-    out.iword(s_iosIndex) = d_prettySExprs;
-  }
-
-  static inline bool getPrettySExprs(std::ostream& out) {
-    return out.iword(s_iosIndex);
-  }
-
-  static inline void setPrettySExprs(std::ostream& out, bool prettySExprs) {
-    out.iword(s_iosIndex) = prettySExprs;
-  }
-
-  /**
-   * Set the pretty-sexprs state on the output stream for the current
-   * stack scope.  This makes sure the old state is reset on the
-   * stream after normal OR exceptional exit from the scope, using the
-   * RAII C++ idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    bool d_oldPrettySExprs;
-
-  public:
-
-    inline Scope(std::ostream& out, bool prettySExprs) :
-      d_out(out),
-      d_oldPrettySExprs(PrettySExprs::getPrettySExprs(out)) {
-      PrettySExprs::setPrettySExprs(out, prettySExprs);
-    }
-
-    inline ~Scope() {
-      PrettySExprs::setPrettySExprs(d_out, d_oldPrettySExprs);
-    }
-
-  };/* class PrettySExprs::Scope */
-
-};/* class PrettySExprs */
-
-/**
- * Sets the default pretty-sexprs setting for an ostream.  Use like this:
- *
- *   // let out be an ostream, s an SExpr
- *   out << PrettySExprs(true) << s << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, PrettySExprs ps) {
-  ps.applyPrettySExprs(out);
-  return out;
-}
-
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PRINTER__PRINTER_H */
-
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
index 05714fbce..87880d3bc 100644
--- a/src/printer/smt1/smt1_printer.cpp
+++ b/src/printer/smt1/smt1_printer.cpp
@@ -13,17 +13,17 @@
  **
  ** The pretty-printer interface for the SMT output language.
  **/
-
 #include "printer/smt1/smt1_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager.h" // for VarNameAttr
-#include "expr/command.h"
 
 #include <iostream>
-#include <vector>
 #include <string>
 #include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "smt_util/command.h"
 
 using namespace std;
 
@@ -45,9 +45,6 @@ void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
   s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* Smt1Printer::toStream() */
 
-void Smt1Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
-}/* Smt1Printer::toStream() */
 
 void Smt1Printer::toStream(std::ostream& out, const Model& m) const throw() {
   Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
@@ -61,4 +58,3 @@ void Smt1Printer::toStream(std::ostream& out, const Model& m, const Command* c)
 }/* CVC4::printer::smt1 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
-
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 56ad9c35a..f93857796 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -17,22 +17,22 @@
 #include "printer/smt2/smt2_printer.h"
 
 #include <iostream>
-#include <vector>
 #include <string>
 #include <typeinfo>
+#include <vector>
 
-#include "util/boolean_simplification.h"
+#include "expr/node_manager_attributes.h"
+#include "options/language.h"
+#include "options/smt_options.h"
 #include "printer/dagification_visitor.h"
-#include "util/node_visitor.h"
-#include "theory/substitutions.h"
-#include "util/language.h"
 #include "smt/smt_engine.h"
-#include "smt/options.h"
-#include "expr/node_manager_attributes.h"
-
-#include "theory/theory_model.h"
+#include "smt_util/boolean_simplification.h"
+#include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/quantifiers/term_database.h"
+#include "theory/substitutions.h"
+#include "theory/theory_model.h"
+#include "util/smt2_quote_string.h"
 
 using namespace std;
 
@@ -40,6 +40,8 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
+static OutputLanguage variantToLanguage(Variant v) throw();
+
 static string smtKindString(Kind k) throw();
 
 static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
@@ -971,38 +973,14 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
 
 }/* Smt2Printer::toStream(Command*) */
 
-static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
-}
-
-// SMT-LIB quoting for symbols
-static std::string quoteSymbol(std::string s) {
-  if(s.find_first_not_of("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789~!@$%^&*_-+=<>.?/") == std::string::npos) {
-    // simple unquoted symbol
-    return s;
-  }
-
-  // must quote the symbol, but it cannot contain | or \, we turn those into _
-  size_t p;
-  while((p = s.find_first_of("\\|")) != std::string::npos) {
-    s = s.replace(p, 1, "_");
-  }
-  return "|" + s + "|";
-}
 
 static std::string quoteSymbol(TNode n) {
+#warning "check the old implementation. It seems off."
   std::stringstream ss;
   ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5);
-  return quoteSymbol(ss.str());
+  return CVC4::quoteSymbol(ss.str());
 }
 
-void Smt2Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  if(sexpr.isKeyword()) {
-    out << quoteSymbol(sexpr.getValue());
-  } else {
-    this->Printer::toStream(out, sexpr);
-  }
-}
 
 template <class T>
 static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw();
@@ -1047,29 +1025,33 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   const theory::TheoryModel& tm = (const theory::TheoryModel&) m;
   if(dynamic_cast<const DeclareTypeCommand*>(c) != NULL) {
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
-    if( options::modelUninterpDtEnum() && tn.isSort() &&
-        tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
+    const std::map< TypeNode, std::vector< Node > >& type_reps = tm.d_rep_set.d_type_reps;
+
+    std::map< TypeNode, std::vector< Node > >::const_iterator tn_iterator = type_reps.find( tn );
+    if( options::modelUninterpDtEnum() && tn.isSort() && tn_iterator != type_reps.end() ){
       out << "(declare-datatypes () ((" << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " ";
-      for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
-        out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
+
+      for( size_t i=0, N = tn_iterator->second.size(); i < N; i++ ){
+        out << "(" << (*tn_iterator).second[i] << ")";
       }
       out << ")))" << endl;
     } else {
       if( tn.isSort() ){
         //print the cardinality
-        if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << endl;
+        if( tn_iterator != type_reps.end() ) {
+          out << "; cardinality of " << tn << " is " << tn_iterator->second.size() << endl;
         }
       }
       out << c << endl;
       if( tn.isSort() ){
         //print the representatives
-        if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
-            if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
-              out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << endl;
+        if( tn_iterator != type_reps.end() ){
+          for( size_t i = 0, N = (*tn_iterator).second.size(); i < N; i++ ){
+            TNode current = (*tn_iterator).second[i];
+            if( current.isVar() ){
+              out << "(declare-fun " << quoteSymbol(current) << " () " << tn << ")" << endl;
             }else{
-              out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << endl;
+              out << "; rep: " << current << endl;
             }
           }
         }
@@ -1138,13 +1120,6 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
   }
 }
 
-void Smt2Printer::toStream(std::ostream& out, const Result& r) const throw() {
-  if(r.getType() == Result::TYPE_SAT && r.isSat() == Result::SAT_UNKNOWN) {
-    out << "unknown";
-  } else {
-    Printer::toStream(out, r);
-  }
-}
 
 static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "(assert " << c->getExpr() << ")";
@@ -1210,7 +1185,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() {
 
 static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
   Type type = c->getType();
-  out << "(declare-fun " << quoteSymbol(c->getSymbol()) << " (";
+  out << "(declare-fun " << CVC4::quoteSymbol(c->getSymbol()) << " (";
   if(type.isFunction()) {
     FunctionType ft = type;
     const vector<Type> argTypes = ft.getArgTypes();
@@ -1389,7 +1364,8 @@ static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) thro
   } else {
     out << "(meta-info :" << c->getFlag() << " ";
   }
-  toStream(out, c->getSExpr());
+
+  SExpr::toStream(out, c->getSExpr(), variantToLanguage(v));
   out << ")";
 }
 
@@ -1399,7 +1375,7 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
 
 static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
   out << "(set-option :" << c->getFlag() << " ";
-  toStream(out, c->getSExpr());
+  SExpr::toStream(out, c->getSExpr(), language::output::LANG_SMTLIB_V2_5);
   out << ")";
 }
 
@@ -1518,6 +1494,20 @@ static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) th
   return false;
 }
 
+static OutputLanguage variantToLanguage(Variant variant) throw() {
+  switch(variant) {
+  case smt2_0_variant:
+    return language::output::LANG_SMTLIB_V2_0;
+  case z3str_variant:
+    return language::output::LANG_Z3STR;
+  case sygus_variant:
+    return language::output::LANG_SYGUS;
+  case no_variant:
+  default:
+    return language::output::LANG_SMTLIB_V2_5;
+  }
+}
+
 }/* CVC4::printer::smt2 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index ba6276aa2..a57c4f8dc 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -45,7 +45,6 @@ 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 Result& r) const throw();
   void toStream(std::ostream& out, const SExpr& sexpr) const throw();
   void toStream(std::ostream& out, const Model& m) const throw();
   void toStream(std::ostream& out, const UnsatCore& core, const std::map<Expr, std::string>& names) const throw();
diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index 3c46a5849..923a7b3aa 100644
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -13,17 +13,17 @@
  **
  ** The pretty-printer interface for the TPTP output language.
  **/
-
 #include "printer/tptp/tptp_printer.h"
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "util/language.h" // for LANG_AST
-#include "expr/node_manager.h" // for VarNameAttr
-#include "expr/command.h"
 
 #include <iostream>
-#include <vector>
 #include <string>
 #include <typeinfo>
+#include <vector>
+
+#include "expr/expr.h" // for ExprSetDepth etc..
+#include "expr/node_manager.h" // for VarNameAttr
+#include "options/language.h" // for LANG_AST
+#include "smt_util/command.h"
 
 using namespace std;
 
@@ -45,9 +45,6 @@ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const thro
   s->toStream(out, language::output::LANG_SMTLIB_V2_5);
 }/* TptpPrinter::toStream() */
 
-void TptpPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, sexpr);
-}/* TptpPrinter::toStream() */
 
 void TptpPrinter::toStream(std::ostream& out, const Model& m) const throw() {
   out << "% SZS output start FiniteModel for " << m.getInputName() << endl;
@@ -62,21 +59,6 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c)
   Unreachable();
 }
 
-void TptpPrinter::toStream(std::ostream& out, const Result& r) const throw() {
-  out << "% SZS status ";
-  if(r.isSat() == Result::SAT) {
-    out << "Satisfiable";
-  } else if(r.isSat() == Result::UNSAT) {
-    out << "Unsatisfiable";
-  } else if(r.isValid() == Result::VALID) {
-    out << "Theorem";
-  } else if(r.isValid() == Result::INVALID) {
-    out << "CounterSatisfiable";
-  } else {
-    out << "GaveUp";
-  }
-  out << " for " << r.getInputName();
-}
 
 }/* CVC4::printer::tptp namespace */
 }/* CVC4::printer namespace */
diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index bc0633822..90a682bcc 100644
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -34,9 +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();
   void toStream(std::ostream& out, const Model& m) const throw();
-  void toStream(std::ostream& out, const Result& r) const throw();
 };/* class TptpPrinter */
 
 }/* CVC4::printer::tptp namespace */