Shuffling around public vs. private headers

- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.

11 files changed, 422 insertions, 367 deletions

diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index dc6ad5833..63f31ed67 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -32,6 +32,8 @@ libexpr_la_SOURCES = \
 	chain.h \
 	emptyset.cpp \
 	emptyset.h \
+	expr_iomanip.cpp \
+	expr_iomanip.h \
 	expr_manager_scope.h \
 	expr_stream.h \
 	kind_map.h \
diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
new file mode 100644
index 000000000..4c7ab3c8b
--- /dev/null
+++ b/src/expr/expr_iomanip.cpp
@@ -0,0 +1,160 @@
+/*********************                                                        */
+/*! \file expr_iomanip.cpp
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr IO manipulation classes.
+ **
+ ** Expr IO manipulation classes.
+ **/
+
+#include "expr/expr_iomanip.h"
+
+#include <iomanip>
+#include <iostream>
+
+#include "options/options.h"
+#include "options/expr_options.h"
+
+namespace CVC4 {
+namespace expr {
+
+const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
+const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
+const int ExprDag::s_iosIndex = std::ios_base::xalloc();
+
+
+
+ExprSetDepth::ExprSetDepth(long depth) : d_depth(depth) {}
+
+void ExprSetDepth::applyDepth(std::ostream& out) {
+  out.iword(s_iosIndex) = d_depth;
+}
+
+long ExprSetDepth::getDepth(std::ostream& out) {
+  long& l = out.iword(s_iosIndex);
+  if(l == 0) {
+    // set the default print depth on this ostream
+    if(not Options::isCurrentNull()) {
+      l = options::defaultExprDepth();
+    }
+    if(l == 0) {
+      // if called from outside the library, we may not have options
+      // available to us at this point (or perhaps the output language
+      // is not set in Options).  Default to something reasonable, but
+      // don't set "l" since that would make it "sticky" for this
+      // stream.
+      return s_defaultPrintDepth;
+    }
+  }
+  return l;
+}
+
+void ExprSetDepth::setDepth(std::ostream& out, long depth) {
+  out.iword(s_iosIndex) = depth;
+}
+
+
+ExprSetDepth::Scope::Scope(std::ostream& out, long depth)
+  : d_out(out), d_oldDepth(ExprSetDepth::getDepth(out))
+{
+  ExprSetDepth::setDepth(out, depth);
+}
+
+ExprSetDepth::Scope::~Scope() {
+  ExprSetDepth::setDepth(d_out, d_oldDepth);
+}
+
+
+ExprPrintTypes::ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
+
+void ExprPrintTypes::applyPrintTypes(std::ostream& out) {
+  out.iword(s_iosIndex) = d_printTypes;
+}
+
+bool ExprPrintTypes::getPrintTypes(std::ostream& out) {
+  return out.iword(s_iosIndex);
+}
+
+void ExprPrintTypes::setPrintTypes(std::ostream& out, bool printTypes) {
+  out.iword(s_iosIndex) = printTypes;
+}
+
+ExprPrintTypes::Scope::Scope(std::ostream& out, bool printTypes)
+  : d_out(out),
+    d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
+  ExprPrintTypes::setPrintTypes(out, printTypes);
+}
+
+ExprPrintTypes::Scope::~Scope() {
+  ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
+}
+
+ExprDag::ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
+
+ExprDag::ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {}
+
+void ExprDag::applyDag(std::ostream& out) {
+  // (offset by one to detect whether default has been set yet)
+  out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1;
+}
+
+size_t ExprDag::getDag(std::ostream& out) {
+  long& l = out.iword(s_iosIndex);
+  if(l == 0) {
+    // set the default dag setting on this ostream
+    // (offset by one to detect whether default has been set yet)
+    if(not Options::isCurrentNull()) {
+      l = options::defaultDagThresh() + 1;
+    }
+    if(l == 0) {
+      // if called from outside the library, we may not have options
+      // available to us at this point (or perhaps the output language
+      // is not set in Options).  Default to something reasonable, but
+      // don't set "l" since that would make it "sticky" for this
+      // stream.
+      return s_defaultDag + 1;
+    }
+  }
+  return static_cast<size_t>(l - 1);
+}
+
+void ExprDag::setDag(std::ostream& out, size_t dag) {
+  // (offset by one to detect whether default has been set yet)
+  out.iword(s_iosIndex) = static_cast<long>(dag) + 1;
+}
+
+ExprDag::Scope::Scope(std::ostream& out, size_t dag)
+  : d_out(out),
+    d_oldDag(ExprDag::getDag(out)) {
+  ExprDag::setDag(out, dag);
+}
+
+ExprDag::Scope::~Scope() {
+  ExprDag::setDag(d_out, d_oldDag);
+}
+
+std::ostream& operator<<(std::ostream& out, ExprDag d) {
+  d.applyDag(out);
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
+  pt.applyPrintTypes(out);
+  return out;
+}
+
+std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
+  sd.applyDepth(out);
+  return out;
+}
+
+
+}/* namespace CVC4::expr */
+}/* namespace CVC4 */
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
new file mode 100644
index 000000000..b3370e75a
--- /dev/null
+++ b/src/expr/expr_iomanip.h
@@ -0,0 +1,239 @@
+/*********************                                                        */
+/*! \file expr_iomanip.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2015  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr IO manipulation classes.
+ **
+ ** Expr IO manipulation classes.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXPR__EXPR_IOMANIP_H
+#define __CVC4__EXPR__EXPR_IOMANIP_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+namespace expr {
+
+/**
+ * IOStream manipulator to set the maximum depth of Exprs when
+ * pretty-printing.  -1 means print to any depth.  E.g.:
+ *
+ *   // let a, b, c, and d be VARIABLEs
+ *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ *   out << setdepth(3) << e;
+ *
+ * gives "(OR a b (AND c (NOT d)))", but
+ *
+ *   out << setdepth(1) << [same expr as above]
+ *
+ * gives "(OR a b (...))".
+ *
+ * The implementation of this class serves two purposes; it holds
+ * information about the depth setting (such as the index of the
+ * allocated word in ios_base), and serves also as the manipulator
+ * itself (as above).
+ */
+class CVC4_PUBLIC ExprSetDepth {
+public:
+
+  /**
+   * Construct a ExprSetDepth with the given depth.
+   */
+  ExprSetDepth(long depth);
+
+  void applyDepth(std::ostream& out);
+
+  static long getDepth(std::ostream& out);
+
+  static void setDepth(std::ostream& out, long depth);
+
+  /**
+   * Set the expression depth on the output stream for the current
+   * stack scope.  This makes sure the old depth is reset on the stream
+   * after normal OR exceptional exit from the scope, using the RAII
+   * C++ idiom.
+   */
+  class Scope {
+  public:
+    Scope(std::ostream& out, long depth);
+    ~Scope();
+
+  private:
+    std::ostream& d_out;
+    long d_oldDepth;
+  };/* class ExprSetDepth::Scope */
+
+ private:
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default depth to print, for ostreams that haven't yet had a
+   * setdepth() applied to them.
+   */
+  static const int s_defaultPrintDepth = -1;
+
+  /**
+   * When this manipulator is used, the depth is stored here.
+   */
+  long d_depth;
+};/* class ExprSetDepth */
+
+/**
+ * IOStream manipulator to print type ascriptions or not.
+ *
+ *   // let a, b, c, and d be variables of sort U
+ *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
+ *   out << e;
+ *
+ * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+ */
+class CVC4_PUBLIC ExprPrintTypes {
+public:
+  /**
+   * Construct a ExprPrintTypes with the given setting.
+   */
+  ExprPrintTypes(bool printTypes);
+
+  void applyPrintTypes(std::ostream& out);
+
+  static bool getPrintTypes(std::ostream& out);
+
+  static void setPrintTypes(std::ostream& out, bool printTypes);
+
+  /**
+   * Set the print-types 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 {
+  public:
+    Scope(std::ostream& out, bool printTypes);
+    ~Scope();
+
+  private:
+    std::ostream& d_out;
+    bool d_oldPrintTypes;
+  };/* class ExprPrintTypes::Scope */
+
+ private:
+  /**
+   * 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_printTypes;
+};/* class ExprPrintTypes */
+
+/**
+ * IOStream manipulator to print expressions as a dag (or not).
+ */
+class CVC4_PUBLIC ExprDag {
+public:
+  /**
+   * Construct a ExprDag with the given setting (dagification on or off).
+   */
+  explicit ExprDag(bool dag);
+
+  /**
+   * Construct a ExprDag with the given setting (letify only common
+   * subexpressions that appear more than 'dag' times).  dag <= 0 means
+   * don't dagify.
+   */
+  explicit ExprDag(int dag);
+
+  void applyDag(std::ostream& out);
+
+  static size_t getDag(std::ostream& out);
+
+  static void setDag(std::ostream& out, size_t dag);
+
+  /**
+   * Set the dag 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 {
+  public:
+    Scope(std::ostream& out, size_t dag);
+    ~Scope();
+
+  private:
+    std::ostream& d_out;
+    size_t d_oldDag;
+  };/* class ExprDag::Scope */
+
+ private:
+  /**
+   * The allocated index in ios_base for our setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default setting, for ostreams that haven't yet had a
+   * dag() applied to them.
+   */
+  static const size_t s_defaultDag = 1;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  size_t d_dag;
+};/* class ExprDag */
+
+/**
+ * Sets the default dag setting when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::dag(true) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+std::ostream& operator<<(std::ostream& out, ExprDag d) CVC4_PUBLIC;
+
+
+/**
+ * Sets the default print-types setting when pretty-printing an Expr
+ * to an ostream.  Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::printtypes(true) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) CVC4_PUBLIC;
+
+/**
+ * Sets the default depth when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setdepth(n) << e << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) CVC4_PUBLIC;
+
+}/* namespace CVC4::expr */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__EXPR_IOMANIP_H */
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index dfbe179be..a6cdedd00 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -40,14 +40,6 @@ namespace CVC4 {
 
 class ExprManager;
 
-namespace expr {
-
-const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc();
-const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
-const int ExprDag::s_iosIndex = std::ios_base::xalloc();
-
-}/* CVC4::expr namespace */
-
 std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
   return out << e.getMessage() << ": " << e.getExpression();
 }
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 2e2f17742..7d82cb222 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -33,7 +33,6 @@ ${includes}
 #include <string>
 
 #include "base/exception.h"
-#include "options/expr_options.h"
 #include "options/language.h"
 #include "util/hash.h"
 
@@ -77,10 +76,6 @@ namespace smt {
 }/* CVC4::smt namespace */
 
 namespace expr {
-  class CVC4_PUBLIC ExprSetDepth;
-  class CVC4_PUBLIC ExprPrintTypes;
-  class CVC4_PUBLIC ExprDag;
-
   class ExportPrivate;
 }/* CVC4::expr namespace */
 
@@ -513,42 +508,6 @@ public:
   Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;
 
   /**
-   * IOStream manipulator to set the maximum depth of Exprs when
-   * pretty-printing.  -1 means print to any depth.  E.g.:
-   *
-   *   // let a, b, c, and d be VARIABLEs
-   *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
-   *   out << setdepth(3) << e;
-   *
-   * gives "(OR a b (AND c (NOT d)))", but
-   *
-   *   out << setdepth(1) << [same expr as above]
-   *
-   * gives "(OR a b (...))"
-   */
-  typedef expr::ExprSetDepth setdepth;
-
-  /**
-   * IOStream manipulator to print type ascriptions or not.
-   *
-   *   // let a, b, c, and d be variables of sort U
-   *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
-   *   out << printtypes(true) << e;
-   *
-   * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
-   *
-   *   out << printtypes(false) << [same expr as above]
-   *
-   * gives "(OR a b (AND c (NOT d)))"
-   */
-  typedef expr::ExprPrintTypes printtypes;
-
-  /**
-   * IOStream manipulator to print expressions as a DAG (or not).
-   */
-  typedef expr::ExprDag dag;
-
-  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -592,307 +551,10 @@ private:
 
 };/* class Expr */
 
-namespace expr {
-
-/**
- * IOStream manipulator to set the maximum depth of Exprs when
- * pretty-printing.  -1 means print to any depth.  E.g.:
- *
- *   // let a, b, c, and d be VARIABLEs
- *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
- *   out << setdepth(3) << e;
- *
- * gives "(OR a b (AND c (NOT d)))", but
- *
- *   out << setdepth(1) << [same expr as above]
- *
- * gives "(OR a b (...))".
- *
- * The implementation of this class serves two purposes; it holds
- * information about the depth setting (such as the index of the
- * allocated word in ios_base), and serves also as the manipulator
- * itself (as above).
- */
-class CVC4_PUBLIC ExprSetDepth {
-  /**
-   * The allocated index in ios_base for our depth setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * The default depth to print, for ostreams that haven't yet had a
-   * setdepth() applied to them.
-   */
-  static const int s_defaultPrintDepth = -1;
-
-  /**
-   * When this manipulator is used, the depth is stored here.
-   */
-  long d_depth;
-
-public:
-  /**
-   * Construct a ExprSetDepth with the given depth.
-   */
-  ExprSetDepth(long depth) : d_depth(depth) {}
-
-  inline void applyDepth(std::ostream& out) {
-    out.iword(s_iosIndex) = d_depth;
-  }
-
-  static inline long getDepth(std::ostream& out) {
-    long& l = out.iword(s_iosIndex);
-    if(l == 0) {
-      // set the default print depth on this ostream
-      if(not Options::isCurrentNull()) {
-        l = options::defaultExprDepth();
-      }
-      if(l == 0) {
-        // if called from outside the library, we may not have options
-        // available to us at this point (or perhaps the output language
-        // is not set in Options).  Default to something reasonable, but
-        // don't set "l" since that would make it "sticky" for this
-        // stream.
-        return s_defaultPrintDepth;
-      }
-    }
-    return l;
-  }
-
-  static inline void setDepth(std::ostream& out, long depth) {
-    out.iword(s_iosIndex) = depth;
-  }
-
-  /**
-   * Set the expression depth on the output stream for the current
-   * stack scope.  This makes sure the old depth is reset on the stream
-   * after normal OR exceptional exit from the scope, using the RAII
-   * C++ idiom.
-   */
-  class Scope {
-    std::ostream& d_out;
-    long d_oldDepth;
-
-  public:
-
-    inline Scope(std::ostream& out, long depth) :
-      d_out(out),
-      d_oldDepth(ExprSetDepth::getDepth(out)) {
-      ExprSetDepth::setDepth(out, depth);
-    }
-
-    inline ~Scope() {
-      ExprSetDepth::setDepth(d_out, d_oldDepth);
-    }
-
-  };/* class ExprSetDepth::Scope */
-
-};/* class ExprSetDepth */
-
-/**
- * IOStream manipulator to print type ascriptions or not.
- *
- *   // let a, b, c, and d be variables of sort U
- *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
- *   out << e;
- *
- * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
- */
-class CVC4_PUBLIC ExprPrintTypes {
-  /**
-   * 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_printTypes;
-
-public:
-  /**
-   * Construct a ExprPrintTypes with the given setting.
-   */
-  ExprPrintTypes(bool printTypes) : d_printTypes(printTypes) {}
-
-  inline void applyPrintTypes(std::ostream& out) {
-    out.iword(s_iosIndex) = d_printTypes;
-  }
-
-  static inline bool getPrintTypes(std::ostream& out) {
-    return out.iword(s_iosIndex);
-  }
-
-  static inline void setPrintTypes(std::ostream& out, bool printTypes) {
-    out.iword(s_iosIndex) = printTypes;
-  }
-
-  /**
-   * Set the print-types 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_oldPrintTypes;
-
-  public:
-
-    inline Scope(std::ostream& out, bool printTypes) :
-      d_out(out),
-      d_oldPrintTypes(ExprPrintTypes::getPrintTypes(out)) {
-      ExprPrintTypes::setPrintTypes(out, printTypes);
-    }
-
-    inline ~Scope() {
-      ExprPrintTypes::setPrintTypes(d_out, d_oldPrintTypes);
-    }
-
-  };/* class ExprPrintTypes::Scope */
-
-};/* class ExprPrintTypes */
-
-/**
- * IOStream manipulator to print expressions as a dag (or not).
- */
-class CVC4_PUBLIC ExprDag {
-  /**
-   * The allocated index in ios_base for our setting.
-   */
-  static const int s_iosIndex;
-
-  /**
-   * The default setting, for ostreams that haven't yet had a
-   * dag() applied to them.
-   */
-  static const size_t s_defaultDag = 1;
-
-  /**
-   * When this manipulator is used, the setting is stored here.
-   */
-  size_t d_dag;
-
-public:
-  /**
-   * Construct a ExprDag with the given setting (dagification on or off).
-   */
-  explicit ExprDag(bool dag) : d_dag(dag ? 1 : 0) {}
-
-  /**
-   * Construct a ExprDag with the given setting (letify only common
-   * subexpressions that appear more than 'dag' times).  dag <= 0 means
-   * don't dagify.
-   */
-  explicit ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {}
-
-  inline void applyDag(std::ostream& out) {
-    // (offset by one to detect whether default has been set yet)
-    out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1;
-  }
-
-  static inline size_t getDag(std::ostream& out) {
-    long& l = out.iword(s_iosIndex);
-    if(l == 0) {
-      // set the default dag setting on this ostream
-      // (offset by one to detect whether default has been set yet)
-      if(not Options::isCurrentNull()) {
-        l = options::defaultDagThresh() + 1;
-      }
-      if(l == 0) {
-        // if called from outside the library, we may not have options
-        // available to us at this point (or perhaps the output language
-        // is not set in Options).  Default to something reasonable, but
-        // don't set "l" since that would make it "sticky" for this
-        // stream.
-        return s_defaultDag + 1;
-      }
-    }
-    return static_cast<size_t>(l - 1);
-  }
-
-  static inline void setDag(std::ostream& out, size_t dag) {
-    // (offset by one to detect whether default has been set yet)
-    out.iword(s_iosIndex) = static_cast<long>(dag) + 1;
-  }
-
-  /**
-   * Set the dag 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;
-    size_t d_oldDag;
-
-  public:
-
-    inline Scope(std::ostream& out, size_t dag) :
-      d_out(out),
-      d_oldDag(ExprDag::getDag(out)) {
-      ExprDag::setDag(out, dag);
-    }
-
-    inline ~Scope() {
-      ExprDag::setDag(d_out, d_oldDag);
-    }
-
-  };/* class ExprDag::Scope */
-
-};/* class ExprDag */
-}/* CVC4::expr namespace */
-
 ${getConst_instantiations}
 
 #line 939 "${template}"
 
-namespace expr {
-
-/**
- * Sets the default depth when pretty-printing a Expr to an ostream.
- * Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::setdepth(n) << e << endl;
- *
- * The depth stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) {
-  sd.applyDepth(out);
-  return out;
-}
-
-/**
- * Sets the default print-types setting when pretty-printing an Expr
- * to an ostream.  Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::printtypes(true) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
-  pt.applyPrintTypes(out);
-  return out;
-}
-
-/**
- * Sets the default dag setting when pretty-printing a Expr to an ostream.
- * Use like this:
- *
- *   // let out be an ostream, e an Expr
- *   out << Expr::dag(true) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-inline std::ostream& operator<<(std::ostream& out, ExprDag d) {
-  d.applyDag(out);
-  return out;
-}
-
-}/* CVC4::expr namespace */
-
 inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
   return (size_t) e.getId();
 }
diff --git a/src/expr/node.h b/src/expr/node.h
index f345ba552..c0e2a5542 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -37,6 +37,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/expr.h"
+#include "expr/expr_iomanip.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "util/configuration.h"
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index dbe7d09eb..ab18973cb 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -24,6 +24,7 @@
 #include "expr/kind.h"
 #include "expr/metakind.h"
 #include "expr/node.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "printer/printer.h"
diff --git a/src/expr/statistics_registry.cpp b/src/expr/statistics_registry.cpp
index bf36236f7..3f9124a2f 100644
--- a/src/expr/statistics_registry.cpp
+++ b/src/expr/statistics_registry.cpp
@@ -21,10 +21,8 @@
 #include "expr/expr_manager.h"
 #include "lib/clock_gettime.h"
 #include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 
-#ifndef __BUILDING_STATISTICS_FOR_EXPORT
-#  include "smt/smt_engine_scope.h"
-#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
 
 #ifdef CVC4_STATISTICS_ON
 #  define __CVC4_USE_STATISTICS true
@@ -65,8 +63,6 @@ inline StatisticsRegistry* getStatisticsRegistry(ExprManager* em) {
 
 }/* CVC4::stats namespace */
 
-#ifndef __BUILDING_STATISTICS_FOR_EXPORT
-
 StatisticsRegistry* StatisticsRegistry::current() {
   return stats::getStatisticsRegistry(smt::currentSmtEngine());
 }
@@ -91,8 +87,6 @@ void StatisticsRegistry::unregisterStat(Stat* s) throw(CVC4::IllegalArgumentExce
 #endif /* CVC4_STATISTICS_ON */
 }/* StatisticsRegistry::unregisterStat() */
 
-#endif /* ! __BUILDING_STATISTICS_FOR_EXPORT */
-
 void StatisticsRegistry::registerStat_(Stat* s) throw(CVC4::IllegalArgumentException) {
 #ifdef CVC4_STATISTICS_ON
   PrettyCheckArgument(d_stats.find(s) == d_stats.end(), s);
diff --git a/src/expr/statistics_registry.h b/src/expr/statistics_registry.h
index 4793f1301..3feb0d5d7 100644
--- a/src/expr/statistics_registry.h
+++ b/src/expr/statistics_registry.h
@@ -32,7 +32,6 @@
 
 #include "base/exception.h"
 #include "expr/statistics.h"
-#include "lib/clock_gettime.h"
 
 namespace CVC4 {
 
@@ -617,10 +616,10 @@ public:
     d_prefix = d_name = name;
   }
 
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
   /** Get a pointer to the current statistics registry */
   static StatisticsRegistry* current();
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */
+#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
 
   /** Overridden to avoid the name being printed */
   void flushStat(std::ostream &out) const;
@@ -638,13 +637,13 @@ public:
     return SExpr(v);
   }
 
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
   /** Register a new statistic, making it active. */
   static void registerStat(Stat* s) throw(CVC4::IllegalArgumentException);
 
   /** Unregister an active statistic, making it inactive. */
   static void unregisterStat(Stat* s) throw(CVC4::IllegalArgumentException);
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) && ! __BUILDING_STATISTICS_FOR_EXPORT */
+#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB) */
 
   /** Register a new statistic */
   void registerStat_(Stat* s) throw(CVC4::IllegalArgumentException);
@@ -887,7 +886,7 @@ class RegisterStatistic {
 
 public:
 
-#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && ! defined(__BUILDING_STATISTICS_FOR_EXPORT)
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST))
   RegisterStatistic(Stat* stat) :
       d_reg(StatisticsRegistry::current()),
       d_stat(stat) {
@@ -896,7 +895,7 @@ public:
     }
     StatisticsRegistry::registerStat(d_stat);
   }
-#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && ! __BUILDING_STATISTICS_FOR_EXPORT */
+#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) */
 
   RegisterStatistic(StatisticsRegistry* reg, Stat* stat) :
     d_reg(reg),
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 659e80550..ea185f98b 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -13,12 +13,14 @@
  **
  ** Reference-counted encapsulation of a pointer to node information.
  **/
+#include "expr/type_node.h"
 
 #include <vector>
 
 #include "expr/node_manager_attributes.h"
-#include "expr/type_node.h"
 #include "expr/type_properties.h"
+#include "options/base_options.h"
+#include "options/expr_options.h"
 
 using namespace std;
 
@@ -564,4 +566,12 @@ bool TypeNode::isSortConstructor() const {
   return getKind() == kind::SORT_TYPE && hasAttribute(expr::SortArityAttr());
 }
 
+std::string TypeNode::toString() const {
+  std::stringstream ss;
+  OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
+  d_nv->toStream(ss, -1, false, 0, outlang);
+  return ss.str();
+}
+
+
 }/* CVC4 namespace */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index ce006a4f1..59f602f09 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -372,12 +372,7 @@ public:
    *
    * @return the string representation of this type.
    */
-  inline std::string toString() const {
-    std::stringstream ss;
-    OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage();
-    d_nv->toStream(ss, -1, false, 0, outlang);
-    return ss.str();
-  }
+  std::string toString() const;
 
   /**
    * Converts this node into a string representation and sends it to the