From: Tim King <taking@google.com>
Date: Wed, 30 Dec 2015 19:45:37 +0000 (-0800)
Subject: Shuffling around public vs. private headers
X-Git-Tag: cvc5-1.0.0~6124
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa7f30a4ba08afe066604daee87006b4fb5f21f7;p=cvc5.git

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.
---

diff --git a/contrib/test_install_headers.sh b/contrib/test_install_headers.sh
new file mode 100755
index 000000000..6f6855e31
--- /dev/null
+++ b/contrib/test_install_headers.sh
@@ -0,0 +1,36 @@
+#!/bin/bash
+# contrib/test_install_headers.sh
+# Tim King <taking@google.com> for the CVC4 project, 24 December 2015
+#
+# ./contrib/test_install_headers.sh <INSTALL>
+#
+# This files tests the completeness of the public headers for CVC4.
+# Any header marked by #include "cvc4_public.h" in either the builds/
+# or src/ directory is installed into the path INSTALL/include/cvc4 where
+# INSTALL is set using the --prefix=INSTALL flag at configure time.
+# This test uses find to attempt to include all of the headers in
+# INSTALL/include/cvc4 and compiles a simple cpp file.
+
+INSTALLATION=$1
+CXX=g++
+LDFLAGS=-lcln
+CXXFILE=test_cvc4_header_install.cpp
+OUTFILE=test_cvc4_header_install
+
+echo $INSTALLATION
+
+echo "Generating $CXXFILE"
+find $INSTALLATION/include/cvc4/ -name *.h -printf '%P\n' | \
+		 awk '{ print "#include <cvc4/" $0 ">"}' > $CXXFILE
+echo "int main() { return 0; }" >> $CXXFILE
+
+echo "Compiling $CXXFILE into $OUTFILE"
+echo "$CXX -I$INSTALLATION/include -L$INSTALLATION/lib $LDFLAGS -o $OUTFILE $CXXFILE"
+$CXX -I$INSTALLATION/include -L$INSTALLATION/lib $LDFLAGS -o $OUTFILE $CXXFILE
+
+read -p "Do you want to delete $CXXFILE and $OUTFILE? [y/n]" yn
+case $yn in
+		[Nn]* ) exit;;
+		[Yy]* ) rm "$OUTFILE" "$CXXFILE";;
+		* ) echo "Did not get a yes or no answer. Exiting."; exit;;
+esac
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index 9ed4424ba..984cbde13 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -28,6 +28,7 @@
 #include <sstream>
 #include <string>
 
+#include "expr/expr_iomanip.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "sha1.hpp"
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 15c7d8728..9aac7bbe0 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -28,6 +28,7 @@
 #include <sstream>
 #include <string>
 
+#include "expr/expr_iomanip.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "sha1.hpp"
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index 2e638f64f..7aa37e91b 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -26,6 +26,12 @@
 
 #include <vector>
 
+#include "expr/expr.h"
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
+#include "options/language.h"
+#include "options/options.h"
+
 using namespace std;
 using namespace hashsmt;
 using namespace CVC4;
@@ -66,7 +72,7 @@ Word Word::concat(const Word words[], unsigned size) {
 }
 
 void Word::print(ostream& out) const {
-  out << CVC4::Expr::setdepth(-1) << d_expr;
+  out << CVC4::expr::ExprSetDepth(-1) << d_expr;
 }
 
 Word::Word(unsigned newSize, unsigned value) {
diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index db76390a7..56f326216 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -23,7 +23,9 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "expr/expr_iomanip.h"
 #include "options/language.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
@@ -49,7 +51,7 @@ int main(int argc, char* argv[])
   ExprManager exprManager(options);
 
   cout << language::SetLanguage(language::output::LANG_SMTLIB_V2)
-       << Expr::setdepth(-1);
+       << expr::ExprSetDepth(-1);
 
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index d59f9f4c4..c541a23fe 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -22,6 +22,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 97c5c5d04..56f323812 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -23,6 +23,8 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -46,7 +48,7 @@ int main(int argc, char* argv[])
   options.set(outputLanguage, language::output::LANG_SMTLIB_V2);
   ExprManager exprManager(options);
 
-  cout << Expr::dag(0) << Expr::setdepth(-1);
+  cout << expr::ExprDag(0) << expr::ExprSetDepth(-1);
   
   // Create the parser
   ParserBuilder parserBuilder(&exprManager, input, options);
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 9c94cdd43..8eb46dd2f 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index 86aaf786f..0ad5bbab5 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index 058fa8e0d..c74b0a110 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index 1ebd6ea59..7a6f87122 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "expr/expr.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 7e17e68f4..aef3843f8 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -24,6 +24,7 @@
 
 #include "expr/expr.h"
 #include "options/language.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 7d5e912e7..248dadd5f 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -23,6 +23,8 @@
 #include <iostream>
 
 #include "expr/expr.h"
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
@@ -211,7 +213,7 @@ int main(int argc, char* argv[]) {
       switch(c) {
       case 1:
         ++files;
-        *out << Expr::dag(dag_thresh);
+        *out << expr::ExprDag(dag_thresh);
         readFile(optarg, (!strcmp(optarg, "-") && fromLang == input::LANG_AUTO) ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out);
         break;
       case INPUT_LANG:
@@ -276,7 +278,7 @@ int main(int argc, char* argv[]) {
     }
 
     if(files == 0) {
-      *out << Expr::dag(dag_thresh);
+      *out << expr::ExprDag(dag_thresh);
       readFile("-", fromLang == input::LANG_AUTO ? input::LANG_CVC4 : fromLang, toLang, expand_definitions, combine_assertions, out);
       exit(0);
     }
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 3fa790f3e..24c4d8112 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -25,9 +25,11 @@
 
 #include "base/exception.h"
 #include "base/output.h"
+#include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/predicate.h"
 #include "expr/sexpr.h"
+#include "options/base_options.h"
 #include "options/expr_options.h"
 #include "options/parser_options.h"
 #include "options/set_language.h"
@@ -1560,8 +1562,8 @@ void ValidityChecker::printExpr(const Expr& e) {
 }
 
 void ValidityChecker::printExpr(const Expr& e, std::ostream& os) {
-  Expr::setdepth::Scope sd(os, -1);
-  Expr::printtypes::Scope pt(os, false);
+  CVC4::expr::ExprSetDepth::Scope sd(os, -1);
+  CVC4::expr::ExprPrintTypes::Scope pt(os, false);
   CVC4::language::SetLanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]);
   os << e;
 }
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 */
 
@@ -512,42 +507,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(...)
@@ -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
diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index e065466f2..daae9aabf 100644
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -14,7 +14,7 @@
  ** Replacement for clock_gettime() for systems without it (like Mac OS X).
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__LIB__CLOCK_GETTIME_H
 #define __CVC4__LIB__CLOCK_GETTIME_H
diff --git a/src/lib/ffs.h b/src/lib/ffs.h
index 2dc51d0e9..44fb40674 100644
--- a/src/lib/ffs.h
+++ b/src/lib/ffs.h
@@ -14,11 +14,14 @@
  ** Replacement for ffs() for systems without it (like Win32).
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__LIB__FFS_H
 #define __CVC4__LIB__FFS_H
 
+//We include this for HAVE_FFS
+#include "cvc4autoconfig.h"
+
 #ifdef HAVE_FFS
 
 // available in strings.h
diff --git a/src/lib/strtok_r.h b/src/lib/strtok_r.h
index 644ff7a31..cc737043b 100644
--- a/src/lib/strtok_r.h
+++ b/src/lib/strtok_r.h
@@ -14,7 +14,7 @@
  ** Replacement for strtok_r() for systems without it (like Win32).
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__LIB__STRTOK_R_H
 #define __CVC4__LIB__STRTOK_R_H
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 0b53c3cbe..aa43cff0f 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -22,6 +22,7 @@
 #include <string>
 
 #include "main/main.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/printer_options.h"
 #include "options/smt_options.h"
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index a1f737d1d..c471ae585 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -31,6 +31,7 @@
 #include "expr/pickler.h"
 #include "main/main.h"
 #include "main/portfolio.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/printer_options.h"
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 7e82e1bd1..3ad26c6a2 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -22,8 +22,11 @@
 #include <iostream>
 #include <new>
 
-#include "base/output.h"
+// This must come before PORTFOLIO_BUILD.
 #include "cvc4autoconfig.h"
+
+#include "base/output.h"
+#include "expr/expr_iomanip.h"
 #include "expr/expr_manager.h"
 #include "expr/result.h"
 #include "expr/statistics_registry.h"
@@ -35,6 +38,7 @@
 
 #include "main/interactive_shell.h"
 #include "main/main.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/quantifiers_options.h"
@@ -284,7 +288,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.set(options::replayStream, new Parser::ExprStream(replayParser));
   }
   if( opts[options::replayLog] != NULL ) {
-    *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
+    *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage])
+                              << expr::ExprSetDepth(-1);
   }
 
   int returnValue = 0;
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 7b146b3b0..6888d3af5 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -40,6 +40,7 @@
 
 #include "base/output.h"
 #include "options/language.h"
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/smt_options.h"
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 36a339d94..3f0842cc5 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -28,6 +28,7 @@
 #include "expr/statistics.h"
 #include "main/command_executor.h"
 #include "main/interactive_shell.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/main_options.h"
 #include "parser/parser.h"
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index 6b5fe4723..1ec0b961c 100644
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -12,11 +12,14 @@
  ** \brief Code relevant only for portfolio builds
  **/
 
+#include "main/portfolio_util.h"
+
 #include <unistd.h>
 
 #include <cassert>
 #include <vector>
 
+#include "options/base_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
 #include "options/prop_options.h"
@@ -96,4 +99,48 @@ vector<Options> parseThreadSpecificOptions(Options opts)
   return threadOptions;
 }
 
+void PortfolioLemmaOutputChannel::notifyNewLemma(Expr lemma) {
+  if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
+    return;
+  }
+  ++cnt;
+  Trace("sharing") << d_tag << ": " << lemma << std::endl;
+  expr::pickle::Pickle pkl;
+  try {
+    d_pickler.toPickle(lemma, pkl);
+    d_sharedChannel->push(pkl);
+    if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+      *options::out() << "thread #0: notifyNewLemma: " << lemma
+                      << std::endl;
+    }
+  } catch(expr::pickle::PicklingException& p){
+    Trace("sharing::blocked") << lemma << std::endl;
+  }
+}
+
+
+PortfolioLemmaInputChannel::PortfolioLemmaInputChannel(std::string tag,
+    SharedChannel<ChannelFormat>* c,
+    ExprManager* em,
+    VarMap& to,
+    VarMap& from)
+    : d_tag(tag), d_sharedChannel(c), d_pickler(em, to, from)
+{}
+
+bool PortfolioLemmaInputChannel::hasNewLemma(){
+  Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl;
+  return !d_sharedChannel->empty();
+}
+
+Expr PortfolioLemmaInputChannel::getNewLemma() {
+  Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl;
+  expr::pickle::Pickle pkl = d_sharedChannel->pop();
+
+  Expr e = d_pickler.fromPickle(pkl);
+  if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+    *options::out() << "thread #0: getNewLemma: " << e << std::endl;
+  }
+  return e;
+}
+
 }/*CVC4 namespace */
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index d6d6a2d02..2b1e22754 100644
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -20,6 +20,7 @@
 #include "base/output.h"
 #include "expr/pickler.h"
 #include "options/main_options.h"
+#include "smt/smt_engine.h"
 #include "smt_util/lemma_input_channel.h"
 #include "smt_util/lemma_output_channel.h"
 #include "util/channel.h"
@@ -49,25 +50,7 @@ public:
 
   ~PortfolioLemmaOutputChannel() throw() { }
 
-  void notifyNewLemma(Expr lemma) {
-    if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
-      return;
-    }
-    ++cnt;
-    Trace("sharing") << d_tag << ": " << lemma << std::endl;
-    expr::pickle::Pickle pkl;
-    try {
-      d_pickler.toPickle(lemma, pkl);
-      d_sharedChannel->push(pkl);
-      if(Trace.isOn("showSharing") && options::thread_id() == 0) {
-        *options::out() << "thread #0: notifyNewLemma: " << lemma
-                        << std::endl;
-      }
-    } catch(expr::pickle::PicklingException& p){
-      Trace("sharing::blocked") << lemma << std::endl;
-    }
-  }
-
+  void notifyNewLemma(Expr lemma);
 };/* class PortfolioLemmaOutputChannel */
 
 class PortfolioLemmaInputChannel : public LemmaInputChannel {
@@ -81,29 +64,12 @@ public:
                              SharedChannel<ChannelFormat>* c,
                              ExprManager* em,
                              VarMap& to,
-                             VarMap& from) :
-    d_tag(tag),
-    d_sharedChannel(c),
-    d_pickler(em, to, from){
-  }
+                               VarMap& from);
 
   ~PortfolioLemmaInputChannel() throw() { }
 
-  bool hasNewLemma(){
-    Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl;
-    return !d_sharedChannel->empty();
-  }
-
-  Expr getNewLemma() {
-    Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl;
-    expr::pickle::Pickle pkl = d_sharedChannel->pop();
-
-    Expr e = d_pickler.fromPickle(pkl);
-    if(Trace.isOn("showSharing") && options::thread_id() == 0) {
-      *options::out() << "thread #0: getNewLemma: " << e << std::endl;
-    }
-    return e;
-  }
+  bool hasNewLemma();
+  Expr getNewLemma();
 
 };/* class PortfolioLemmaInputChannel */
 
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 86272ee53..ce4e4509d 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -34,6 +34,7 @@
 #include "expr/statistics.h"
 #include "main/command_executor.h"
 #include "main/main.h"
+#include "options/base_options.h"
 #include "options/options.h"
 #include "smt/smt_engine.h"
 
diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h
index e43d2848e..c8c02ecaa 100644
--- a/src/options/base_options_template.h
+++ b/src/options/base_options_template.h
@@ -14,7 +14,7 @@
  ** Contains code for handling command-line options
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__OPTIONS__${module_id}_H
 #define __CVC4__OPTIONS__${module_id}_H
diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h
index 65cc7a8a5..81a0c661a 100644
--- a/src/options/boolean_term_conversion_mode.h
+++ b/src/options/boolean_term_conversion_mode.h
@@ -26,7 +26,7 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
-typedef enum {
+enum BooleanTermConversionMode {
   /**
    * Convert Boolean terms to bitvectors of size 1.
    */
@@ -41,7 +41,7 @@ typedef enum {
    */
   BOOLEAN_TERM_CONVERT_NATIVE
 
-} BooleanTermConversionMode;
+};
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 08a6e4077..f36021478 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -64,8 +64,8 @@ enum BvSlicerMode {
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
 
-std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
+std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
 
 }/* CVC4 namespace */
 
diff --git a/src/options/decision_mode.cpp b/src/options/decision_mode.cpp
index 168637e64..0aeae1baa 100644
--- a/src/options/decision_mode.cpp
+++ b/src/options/decision_mode.cpp
@@ -17,6 +17,8 @@
 
 #include "options/decision_mode.h"
 
+#include <iostream>
+
 namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) {
diff --git a/src/options/decision_mode.h b/src/options/decision_mode.h
index fb01c587b..420d00b4c 100644
--- a/src/options/decision_mode.h
+++ b/src/options/decision_mode.h
@@ -20,7 +20,7 @@
 #ifndef __CVC4__SMT__DECISION_MODE_H
 #define __CVC4__SMT__DECISION_MODE_H
 
-#include <iostream>
+#include <iosfwd>
 
 namespace CVC4 {
 namespace decision {
@@ -57,7 +57,7 @@ enum DecisionWeightInternal {
 
 }/* CVC4::decision namespace */
 
-std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, decision::DecisionMode mode);
 
 }/* CVC4 namespace */
 
diff --git a/src/options/decision_weight.h b/src/options/decision_weight.h
index 42f1d5b6d..89ebe8a21 100644
--- a/src/options/decision_weight.h
+++ b/src/options/decision_weight.h
@@ -21,7 +21,9 @@
 
 namespace CVC4 {
 namespace decision {
+
 typedef uint64_t DecisionWeight;
+
 }/* CVC4::decision namespace */
 }/* CVC4 namespace */
 
diff --git a/src/options/options.h b/src/options/options.h
index fc3bf40ac..a83de9acb 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -164,6 +164,4 @@ public:
 
 }/* CVC4 namespace */
 
-#include "options/base_options.h"
-
 #endif /* __CVC4__OPTIONS__OPTIONS_H */
diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp
index db0275e04..f68adbb45 100644
--- a/src/options/set_language.cpp
+++ b/src/options/set_language.cpp
@@ -18,6 +18,7 @@
 #include <iosfwd>
 #include <iomanip>
 
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 0e8a9e241..120f63987 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -26,6 +26,7 @@
 
 #include "base/output.h"
 #include "expr/expr.h"
+#include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/resource_manager.h"
 #include "expr/type.h"
@@ -331,7 +332,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
           j != j_end;
           ++j) {
         const DatatypeConstructor& ctor = *j;
-        Expr::printtypes::Scope pts(Debug("parser-idt"), true);
+        expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true);
         Expr constructor = ctor.getConstructor();
         Debug("parser-idt") << "+ define " << constructor << std::endl;
         string constructorName = ctor.getName();
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 08e0232aa..f473ae178 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -18,6 +18,7 @@
 #include <string>
 
 #include "expr/expr_manager.h"
+#include "options/base_options.h"
 #include "options/parser_options.h"
 #include "options/smt_options.h"
 #include "parser/input.h"
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 75d625edc..d4b99536e 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -17,6 +17,7 @@
 
 #include <string>
 
+#include "options/base_options.h"
 #include "options/language.h"
 #include "printer/ast/ast_printer.h"
 #include "printer/cvc/cvc_printer.h"
@@ -87,4 +88,29 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core, const std::map<
   }
 }/* Printer::toStream(UnsatCore, std::map<Expr, std::string>) */
 
+Printer* Printer::getPrinter(OutputLanguage lang) throw() {
+  if(lang == language::output::LANG_AUTO) {
+  // Infer the language to use for output.
+  //
+  // Options can be null in certain circumstances (e.g., when printing
+  // the singleton "null" expr.  So we guard against segfault
+  if(not Options::isCurrentNull()) {
+    if(options::outputLanguage.wasSetByUser()) {
+      lang = options::outputLanguage();
+    }
+    if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
+      lang = language::toOutputLanguage(options::inputLanguage());
+     }
+   }
+   if(lang == language::output::LANG_AUTO) {
+      lang = language::output::LANG_CVC4; // default
+    }
+  }
+  if(d_printers[lang] == NULL) {
+    d_printers[lang] = makePrinter(lang);
+  }
+  return d_printers[lang];
+}
+
+
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 30d33d46b..48787f70a 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -56,29 +56,7 @@ protected:
 
 public:
   /** Get the Printer for a given OutputLanguage */
-  static Printer* getPrinter(OutputLanguage lang) throw() {
-    if(lang == language::output::LANG_AUTO) {
-      // Infer the language to use for output.
-      //
-      // Options can be null in certain circumstances (e.g., when printing
-      // the singleton "null" expr.  So we guard against segfault
-      if(not Options::isCurrentNull()) {
-        if(options::outputLanguage.wasSetByUser()) {
-          lang = options::outputLanguage();
-        }
-        if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) {
-          lang = language::toOutputLanguage(options::inputLanguage());
-        }
-      }
-      if(lang == language::output::LANG_AUTO) {
-        lang = language::output::LANG_CVC4; // default
-      }
-    }
-    if(d_printers[lang] == NULL) {
-      d_printers[lang] = makePrinter(lang);
-    }
-    return d_printers[lang];
-  }
+  static Printer* getPrinter(OutputLanguage lang) throw();
 
   /** Write a Node out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, TNode n,
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 4a4d13977..37cc62aa0 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -16,6 +16,8 @@
 
 #include "proof/unsat_core.h"
 
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
 #include "printer/printer.h"
 #include "smt/smt_engine_scope.h"
 #include "smt_util/command.h"
@@ -36,13 +38,13 @@ UnsatCore::const_iterator UnsatCore::end() const {
 
 void UnsatCore::toStream(std::ostream& out) const {
   smt::SmtScope smts(d_smt);
-  Expr::dag::Scope scope(out, false);
+  expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
 }
 
 void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const {
   smt::SmtScope smts(d_smt);
-  Expr::dag::Scope scope(out, false);
+  expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names);
 }
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 23a740a26..d9b8bb4f8 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -18,6 +18,7 @@
 
 #include "prop/minisat/minisat.h"
 
+#include "options/base_options.h"
 #include "options/decision_options.h"
 #include "options/prop_options.h"
 #include "options/smt_options.h"
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 499cf1b56..2a1b05619 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -26,6 +26,7 @@
 #include "expr/expr.h"
 #include "expr/resource_manager.h"
 #include "expr/result.h"
+#include "options/base_options.h"
 #include "options/decision_options.h"
 #include "options/main_options.h"
 #include "options/options.h"
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 34776c245..e0446eb4a 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -14,12 +14,13 @@
  ** SAT Solver creation facility
  **/
 
-#pragma once
+#include "cvc4_private.h"
 
-#include "cvc4_public.h"
+#pragma once
 
 #include <string>
 #include <vector>
+
 #include "prop/sat_solver.h"
 
 namespace CVC4 {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f2c45eab9..c1d49d8c8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -26,11 +26,8 @@
 #include <utility>
 #include <vector>
 
-#include "options/boolean_term_conversion_mode.h"
-#include "options/decision_mode.h"
 #include "base/exception.h"
 #include "base/modal_exception.h"
-#include "options/option_exception.h"
 #include "base/output.h"
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
@@ -46,12 +43,16 @@
 #include "expr/resource_manager.h"
 #include "options/arith_options.h"
 #include "options/arrays_options.h"
+#include "options/base_options.h"
+#include "options/boolean_term_conversion_mode.h"
 #include "options/booleans_options.h"
 #include "options/booleans_options.h"
 #include "options/bv_options.h"
 #include "options/datatypes_options.h"
+#include "options/decision_mode.h"
 #include "options/decision_options.h"
 #include "options/main_options.h"
+#include "options/option_exception.h"
 #include "options/options_handler_interface.h"
 #include "options/printer_options.h"
 #include "options/prop_options.h"
@@ -65,8 +66,8 @@
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
 #include "proof/proof_manager.h"
-#include "proof/unsat_core.h"
 #include "proof/theory_proof.h"
+#include "proof/unsat_core.h"
 #include "prop/prop_engine.h"
 #include "smt/boolean_terms.h"
 #include "smt/command_list.h"
@@ -74,8 +75,8 @@
 #include "smt/model_postprocessor.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/smt_options_handler.h"
-#include "smt_util/command.h"
 #include "smt_util/boolean_simplification.h"
+#include "smt_util/command.h"
 #include "smt_util/ite_removal.h"
 #include "smt_util/nary_builder.h"
 #include "smt_util/node_visitor.h"
diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp
index 371cdcddd..e1a19d48b 100644
--- a/src/smt/smt_options_handler.cpp
+++ b/src/smt/smt_options_handler.cpp
@@ -25,6 +25,7 @@
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "cvc4autoconfig.h"
+#include "expr/expr_iomanip.h"
 #include "expr/metakind.h"
 #include "expr/node_manager.h"
 #include "expr/resource_manager.h"
@@ -32,6 +33,7 @@
 #include "options/arith_heuristic_pivot_rule.h"
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"
+#include "options/base_options.h"
 #include "options/boolean_term_conversion_mode.h"
 #include "options/bv_bitblast_mode.h"
 #include "options/bv_options.h"
@@ -1219,9 +1221,9 @@ void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw(
     bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \
     OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \
     __channel_set; \
-    __channel_get << Expr::dag(dagSetting); \
-    __channel_get << Expr::setdepth(exprDepthSetting); \
-    __channel_get << Expr::printtypes(printtypesSetting); \
+    __channel_get << expr::ExprDag(dagSetting);      \
+    __channel_get << expr::ExprSetDepth(exprDepthSetting); \
+    __channel_get << expr::ExprPrintTypes(printtypesSetting); \
     __channel_get << language::SetLanguage(languageSetting); \
   }
 
@@ -1418,12 +1420,12 @@ void SmtOptionsHandler::setDefaultExprDepth(std::string option, int depth) {
     throw OptionException("--default-expr-depth requires a positive argument, or -1.");
   }
 
-  Debug.getStream() << Expr::setdepth(depth);
-  Trace.getStream() << Expr::setdepth(depth);
-  Notice.getStream() << Expr::setdepth(depth);
-  Chat.getStream() << Expr::setdepth(depth);
-  Message.getStream() << Expr::setdepth(depth);
-  Warning.getStream() << Expr::setdepth(depth);
+  Debug.getStream() << expr::ExprSetDepth(depth);
+  Trace.getStream() << expr::ExprSetDepth(depth);
+  Notice.getStream() << expr::ExprSetDepth(depth);
+  Chat.getStream() << expr::ExprSetDepth(depth);
+  Message.getStream() << expr::ExprSetDepth(depth);
+  Warning.getStream() << expr::ExprSetDepth(depth);
   // intentionally exclude Dump stream from this list
 }
 
@@ -1432,22 +1434,22 @@ void SmtOptionsHandler::setDefaultDagThresh(std::string option, int dag) {
     throw OptionException("--default-dag-thresh requires a nonnegative argument.");
   }
 
-  Debug.getStream() << Expr::dag(dag);
-  Trace.getStream() << Expr::dag(dag);
-  Notice.getStream() << Expr::dag(dag);
-  Chat.getStream() << Expr::dag(dag);
-  Message.getStream() << Expr::dag(dag);
-  Warning.getStream() << Expr::dag(dag);
-  Dump.getStream() << Expr::dag(dag);
+  Debug.getStream() << expr::ExprDag(dag);
+  Trace.getStream() << expr::ExprDag(dag);
+  Notice.getStream() << expr::ExprDag(dag);
+  Chat.getStream() << expr::ExprDag(dag);
+  Message.getStream() << expr::ExprDag(dag);
+  Warning.getStream() << expr::ExprDag(dag);
+  Dump.getStream() << expr::ExprDag(dag);
 }
 
 void SmtOptionsHandler::setPrintExprTypes(std::string option) {
-  Debug.getStream() << Expr::printtypes(true);
-  Trace.getStream() << Expr::printtypes(true);
-  Notice.getStream() << Expr::printtypes(true);
-  Chat.getStream() << Expr::printtypes(true);
-  Message.getStream() << Expr::printtypes(true);
-  Warning.getStream() << Expr::printtypes(true);
+  Debug.getStream() << expr::ExprPrintTypes(true);
+  Trace.getStream() << expr::ExprPrintTypes(true);
+  Notice.getStream() << expr::ExprPrintTypes(true);
+  Chat.getStream() << expr::ExprPrintTypes(true);
+  Message.getStream() << expr::ExprPrintTypes(true);
+  Warning.getStream() << expr::ExprPrintTypes(true);
   // intentionally exclude Dump stream from this list
 }
 
diff --git a/src/smt_util/command.cpp b/src/smt_util/command.cpp
index ae4e1f1f0..5917d71da 100644
--- a/src/smt_util/command.cpp
+++ b/src/smt_util/command.cpp
@@ -25,6 +25,7 @@
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
+#include "expr/expr_iomanip.h"
 #include "expr/node.h"
 #include "expr/sexpr.h"
 #include "options/options.h"
@@ -984,7 +985,7 @@ void GetValueCommand::printResult(std::ostream& out, uint32_t verbosity) const t
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    Expr::dag::Scope scope(out, false);
+    expr::ExprDag::Scope scope(out, false);
     out << d_result << endl;
   }
 }
diff --git a/src/smt_util/model.cpp b/src/smt_util/model.cpp
index 3f0423f49..ddac7e263 100644
--- a/src/smt_util/model.cpp
+++ b/src/smt_util/model.cpp
@@ -16,10 +16,12 @@
 
 #include <vector>
 
-#include "smt_util/command.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/command_list.h"
+#include "expr/expr_iomanip.h"
+#include "options/base_options.h"
 #include "printer/printer.h"
+#include "smt/command_list.h"
+#include "smt/smt_engine_scope.h"
+#include "smt_util/command.h"
 
 using namespace std;
 
@@ -27,7 +29,7 @@ namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, const Model& m) {
   smt::SmtScope smts(&m.d_smt);
-  Expr::dag::Scope scope(out, false);
+  expr::ExprDag::Scope scope(out, false);
   Printer::getPrinter(options::outputLanguage())->toStream(out, m);
   return out;
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 36b24c51b..56f966426 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/term_database.h"
 
 #include "expr/datatype.h"
+#include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index 132d67b1c..d8a3a65d9 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -62,11 +62,11 @@ namespace CVC4 {
 
   }; /* class FloatingPointSize */
 
-
-
-#define ROLL(X,N) (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) ))
-
   struct CVC4_PUBLIC FloatingPointSizeHashFunction {
+    static inline size_t ROLL(size_t X, size_t N) {
+      return (((X) << (N)) | ((X) >> (8*sizeof((X)) - (N)) ));
+    }
+
     inline size_t operator() (const FloatingPointSize& fpt) const {
       return size_t(ROLL(fpt.exponent(), 4*sizeof(unsigned)) |
 		    fpt.significand());
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
index dd6cbccb8..d27ebd9b3 100644
--- a/test/system/ouroborous.cpp
+++ b/test/system/ouroborous.cpp
@@ -29,6 +29,7 @@
 #include <string>
 
 #include "expr/expr.h"
+#include "expr/expr_iomanip.h"
 #include "options/set_language.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
@@ -70,7 +71,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) {
   psr->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
   Expr e = psr->nextExpression();
   stringstream ss;
-  ss << language::SetLanguage(outlang) << Expr::setdepth(-1) << e;
+  ss << language::SetLanguage(outlang) << expr::ExprSetDepth(-1) << e;
   assert(psr->nextExpression().isNull());// next expr should be null
   assert(psr->done());// parser should be done
   string s = ss.str();
@@ -122,7 +123,7 @@ int runTest() {
 
   assert(psr->done());// parser should be done
 
-  cout << Expr::setdepth(-1);
+  cout << expr::ExprSetDepth(-1);
 
   runTestString("(= (f (f y)) x)");
   runTestString("~BVPLUS(3, 0bin00, 0bin11)[2:1] = 0bin10", input::LANG_CVC4);
diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp
index 99b4c625c..b202bcccc 100644
--- a/test/system/smt2_compliance.cpp
+++ b/test/system/smt2_compliance.cpp
@@ -19,6 +19,7 @@
 #include <sstream>
 
 #include "expr/expr_manager.h"
+#include "options/base_options.h"
 #include "options/set_language.h"
 #include "options/smt_options.h"
 #include "parser/parser.h"
diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index 6c3e73d2c..b351f5c3e 100644
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -22,6 +22,7 @@
 
 #include "expr/expr_manager.h"
 #include "main/interactive_shell.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/parser_builder.h"
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 9b700eda6..6ecc76c2b 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -22,6 +22,7 @@
 #include "base/output.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "options/base_options.h"
 #include "options/language.h"
 #include "options/options.h"
 #include "parser/parser.h"
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
index 355d4ff37..4c0eb81cc 100644
--- a/test/unit/util/boolean_simplification_black.h
+++ b/test/unit/util/boolean_simplification_black.h
@@ -18,6 +18,7 @@
 #include <set>
 #include <vector>
 
+#include "expr/expr_iomanip.h"
 #include "expr/kind.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
@@ -102,7 +103,7 @@ public:
     TS_ASSERT_LESS_THAN_EQUALS(10u,
       BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD);
 
-    cout << Expr::setdepth(-1)
+    cout << expr::ExprSetDepth(-1)
          << language::SetLanguage(language::output::LANG_CVC4);
   }