Refactoring Options Handler & Library Cycle Breaking

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

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

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

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

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

More details about the directories:

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

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

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

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

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

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

13 files changed, 1919 insertions, 0 deletions

diff --git a/src/base/Makefile.am b/src/base/Makefile.am
new file mode 100644
index 000000000..b03b61aee
--- /dev/null
+++ b/src/base/Makefile.am
@@ -0,0 +1,40 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libbase.la
+
+# Do not list built sources (like tls.h) here!
+# Rather, list them under BUILT_SOURCES, and their .in versions under
+# EXTRA_DIST.  Otherwise, they're packaged up in the tarball, which is
+# no good---they belong in the configured builds/ directory.  If they
+# end up in the source directory, they build the cvc4 that was
+# configured at the time of the "make dist", which (1) may not be the
+# configuration that the user wants, and (2) might cause link errors.
+libbase_la_SOURCES = \
+	Makefile.am \
+	Makefile.in \
+	cvc4_assert.cpp \
+	cvc4_assert.h \
+	exception.cpp \
+	exception.h \
+	lemma_input_channel_forward.h \
+	lemma_output_channel_forward.h \
+	modal_exception.h \
+	output.cpp \
+	output.h
+
+
+
+BUILT_SOURCES = \
+	tls.h
+
+EXTRA_DIST = \
+	exception.i \
+	modal_exception.i \
+	tls.h.in
+
+DISTCLEANFILES = \
+	tls.h.tmp \
+	tls.h
diff --git a/src/base/cvc4_assert.cpp b/src/base/cvc4_assert.cpp
new file mode 100644
index 000000000..6e51845dd
--- /dev/null
+++ b/src/base/cvc4_assert.cpp
@@ -0,0 +1,166 @@
+/*********************                                                        */
+/*! \file cvc4_assert.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Assertion utility classes, functions, and exceptions.
+ **
+ ** Assertion utility classes, functions, and exceptions.  Implementation.
+ **/
+
+#include <new>
+#include <cstdarg>
+#include <cstdio>
+
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+#ifdef CVC4_DEBUG
+CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
+#endif /* CVC4_DEBUG */
+
+void AssertionException::construct(const char* header, const char* extra,
+                                   const char* function, const char* file,
+                                   unsigned line, const char* fmt,
+                                   va_list args) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 512;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s\n%s\n%s:%d\n",
+                      header, function, file, line);
+    } else {
+      size = snprintf(buf, n, "%s\n%s\n%s:%d:\n\n  %s\n",
+                      header, function, file, line, extra);
+    }
+
+    if(size < n) {
+      va_list args_copy;
+      va_copy(args_copy, args);
+      size += vsnprintf(buf + size, n - size, fmt, args_copy);
+      va_end(args_copy);
+
+      if(size < n) {
+        break;
+      }
+    }
+
+    if(size >= n) {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
+  delete [] buf;
+#endif /* CVC4_DEBUG */
+}
+
+void AssertionException::construct(const char* header, const char* extra,
+                                   const char* function, const char* file,
+                                   unsigned line) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 256;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s.\n%s\n%s:%d\n",
+                      header, function, file, line);
+    } else {
+      size = snprintf(buf, n, "%s.\n%s\n%s:%d:\n\n  %s\n",
+                      header, function, file, line, extra);
+    }
+
+    if(size < n) {
+      break;
+    } else {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+
+#ifdef CVC4_DEBUG
+  // we leak buf[] but only in debug mode with assertions failing
+  if(s_debugLastException == NULL) {
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
+  delete [] buf;
+#endif /* CVC4_DEBUG */
+}
+
+#ifdef CVC4_DEBUG
+
+/**
+ * Special assertion failure handling in debug mode; in non-debug
+ * builds, the exception is thrown from the macro.  We factor out this
+ * additional logic so as not to bloat the code at every Assert()
+ * expansion.
+ *
+ * Note this name is prefixed with "debug" because it is included in
+ * debug builds only; in debug builds, it handles all assertion
+ * failures (even those that exist in non-debug builds).
+ */
+void debugAssertionFailed(const AssertionException& thisException,
+                          const char* propagatingException) {
+  static CVC4_THREADLOCAL(bool) alreadyFired = false;
+
+  if(__builtin_expect( ( !std::uncaught_exception() ), true ) || alreadyFired) {
+    throw thisException;
+  }
+
+  alreadyFired = true;
+
+  // propagatingException is the propagating exception, but can be
+  // NULL if the propagating exception is not a CVC4::Exception.
+  Warning() << "===========================================" << std::endl
+            << "An assertion failed during stack unwinding:" << std::endl;
+  if(propagatingException != NULL) {
+    Warning() << "The propagating exception is:" << std::endl
+              << propagatingException << std::endl
+              << "===========================================" << std::endl;
+    Warning() << "The newly-thrown exception is:" << std::endl;
+  } else {
+    Warning() << "The propagating exception is unknown." << std::endl;
+  }
+  Warning() << thisException << std::endl
+            << "===========================================" << std::endl;
+
+  terminate();
+}
+
+#endif /* CVC4_DEBUG */
+
+}/* CVC4 namespace */
diff --git a/src/base/cvc4_assert.h b/src/base/cvc4_assert.h
new file mode 100644
index 000000000..6dca5c81d
--- /dev/null
+++ b/src/base/cvc4_assert.h
@@ -0,0 +1,311 @@
+/*********************                                                        */
+/*! \file cvc4_assert.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): ACSYS
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Assertion utility classes, functions, exceptions, and macros.
+ **
+ ** Assertion utility classes, functions, exceptions, and macros.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__ASSERT_H
+#define __CVC4__ASSERT_H
+
+#include <string>
+#include <sstream>
+#include <cstdio>
+#include <cstdlib>
+#include <cstdarg>
+
+#include "base/exception.h"
+#include "base/tls.h"
+
+
+// output.h not strictly needed for this header, but it _is_ needed to
+// actually _use_ anything in this header, so let's include it.
+// Tim : Disabling this and moving it into cvc4_assert.cpp
+//#include "util/output.h"
+
+namespace CVC4 {
+
+class AssertionException : public Exception {
+protected:
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* file,
+                 unsigned line, const char* fmt, ...) {
+    va_list args;
+    va_start(args, fmt);
+    construct(header, extra, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* file,
+                 unsigned line, const char* fmt, va_list args);
+
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* file,
+                 unsigned line);
+
+  AssertionException() : Exception() {}
+
+public:
+  AssertionException(const char* extra, const char* function,
+                     const char* file, unsigned line,
+                     const char* fmt, ...) :
+    Exception() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Assertion failure", extra, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  AssertionException(const char* extra, const char* function,
+                     const char* file, unsigned line) :
+    Exception() {
+    construct("Assertion failure", extra, function, file, line);
+  }
+};/* class AssertionException */
+
+class UnreachableCodeException : public AssertionException {
+protected:
+  UnreachableCodeException() : AssertionException() {}
+
+public:
+  UnreachableCodeException(const char* function, const char* file,
+                           unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Unreachable code reached",
+              NULL, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  UnreachableCodeException(const char* function, const char* file,
+                           unsigned line) :
+    AssertionException() {
+    construct("Unreachable code reached", NULL, function, file, line);
+  }
+};/* class UnreachableCodeException */
+
+class UnhandledCaseException : public UnreachableCodeException {
+protected:
+  UnhandledCaseException() : UnreachableCodeException() {}
+
+public:
+  UnhandledCaseException(const char* function, const char* file,
+                         unsigned line, const char* fmt, ...) :
+    UnreachableCodeException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Unhandled case encountered",
+              NULL, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  template <class T>
+  UnhandledCaseException(const char* function, const char* file,
+                         unsigned line, T theCase) :
+    UnreachableCodeException() {
+    std::stringstream sb;
+    sb << theCase;
+    construct("Unhandled case encountered",
+              NULL, function, file, line, "The case was: %s", sb.str().c_str());
+  }
+
+  UnhandledCaseException(const char* function, const char* file,
+                         unsigned line) :
+    UnreachableCodeException() {
+    construct("Unhandled case encountered", NULL, function, file, line);
+  }
+};/* class UnhandledCaseException */
+
+class UnimplementedOperationException : public AssertionException {
+protected:
+  UnimplementedOperationException() : AssertionException() {}
+
+public:
+  UnimplementedOperationException(const char* function, const char* file,
+                                  unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Unimplemented code encountered",
+              NULL, function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  UnimplementedOperationException(const char* function, const char* file,
+                                  unsigned line) :
+    AssertionException() {
+    construct("Unimplemented code encountered", NULL, function, file, line);
+  }
+};/* class UnimplementedOperationException */
+
+class AssertArgumentException : public AssertionException {
+protected:
+  AssertArgumentException() : AssertionException() {}
+
+public:
+  AssertArgumentException(const char* argDesc, const char* function,
+                          const char* file, unsigned line,
+                          const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Illegal argument detected",
+              ( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
+              function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  AssertArgumentException(const char* argDesc, const char* function,
+                          const char* file, unsigned line) :
+    AssertionException() {
+    construct("Illegal argument detected",
+              ( std::string("`") + argDesc + "' is a bad argument" ).c_str(),
+              function, file, line);
+  }
+
+  AssertArgumentException(const char* condStr, const char* argDesc,
+                          const char* function, const char* file,
+                          unsigned line, const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Illegal argument detected",
+              ( std::string("`") + argDesc + "' is a bad argument; expected " +
+                condStr + " to hold" ).c_str(),
+              function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  AssertArgumentException(const char* condStr, const char* argDesc,
+                          const char* function, const char* file,
+                          unsigned line) :
+    AssertionException() {
+    construct("Illegal argument detected",
+              ( std::string("`") + argDesc + "' is a bad argument; expected " +
+                condStr + " to hold" ).c_str(),
+              function, file, line);
+  }
+};/* class AssertArgumentException */
+
+class InternalErrorException : public AssertionException {
+protected:
+  InternalErrorException() : AssertionException() {}
+
+public:
+  InternalErrorException(const char* function, const char* file, unsigned line) :
+    AssertionException() {
+    construct("Internal error detected", "",
+              function, file, line);
+  }
+
+  InternalErrorException(const char* function, const char* file, unsigned line,
+                         const char* fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Internal error detected", "",
+              function, file, line, fmt, args);
+    va_end(args);
+  }
+
+  InternalErrorException(const char* function, const char* file, unsigned line,
+                         std::string fmt, ...) :
+    AssertionException() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Internal error detected", "",
+              function, file, line, fmt.c_str(), args);
+    va_end(args);
+  }
+
+};/* class InternalErrorException */
+
+#ifdef CVC4_DEBUG
+
+extern CVC4_THREADLOCAL(const char*) s_debugLastException;
+
+/**
+ * Special assertion failure handling in debug mode; in non-debug
+ * builds, the exception is thrown from the macro.  We factor out this
+ * additional logic so as not to bloat the code at every Assert()
+ * expansion.
+ *
+ * Note this name is prefixed with "debug" because it is included in
+ * debug builds only; in debug builds, it handles all assertion
+ * failures (even those that exist in non-debug builds).
+ */
+void debugAssertionFailed(const AssertionException& thisException, const char* lastException);
+
+// If we're currently handling an exception, print a warning instead;
+// otherwise std::terminate() is called by the runtime and we lose
+// details of the exception
+#  define AlwaysAssert(cond, msg...)                                    \
+    do {                                                                \
+      if(__builtin_expect( ( ! (cond) ), false )) {                                    \
+        /* save the last assertion failure */                           \
+        const char* lastException = ::CVC4::s_debugLastException;       \
+        ::CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+        ::CVC4::debugAssertionFailed(exception, lastException);         \
+      }                                                                 \
+    } while(0)
+
+#else /* CVC4_DEBUG */
+// These simpler (but less useful) versions for non-debug builds fails
+// will terminate() if thrown during stack unwinding.
+#  define AlwaysAssert(cond, msg...)                                    \
+     do {                                                               \
+       if(__builtin_expect( ( ! (cond) ), false )) {                                   \
+         throw ::CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+       }                                                                \
+     } while(0)
+#endif /* CVC4_DEBUG */
+
+#define Unreachable(msg...) \
+  throw ::CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unhandled(msg...) \
+  throw ::CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define Unimplemented(msg...) \
+  throw ::CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define InternalError(msg...) \
+  throw ::CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define IllegalArgument(arg, msg...) \
+  throw ::CVC4::IllegalArgumentException("", #arg, __PRETTY_FUNCTION__, ## msg)
+#define CheckArgument(cond, arg, msg...)         \
+  do { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
+      throw ::CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, ## msg); \
+    } \
+  } while(0)
+#define AlwaysAssertArgument(cond, arg, msg...)  \
+  do { \
+    if(__builtin_expect( ( ! (cond) ), false )) { \
+      throw ::CVC4::AssertArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+    } \
+  } while(0)
+
+#ifdef CVC4_ASSERTIONS
+#  define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
+#  define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
+#  define DebugCheckArgument(cond, arg, msg...) CheckArgument(cond, arg, ## msg)
+#else /* ! CVC4_ASSERTIONS */
+#  define Assert(cond, msg...) /*__builtin_expect( ( cond ), true )*/
+#  define AssertArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
+#  define DebugCheckArgument(cond, arg, msg...) /*__builtin_expect( ( cond ), true )*/
+#endif /* CVC4_ASSERTIONS */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__ASSERT_H */
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
new file mode 100644
index 000000000..d8eee50bc
--- /dev/null
+++ b/src/base/exception.cpp
@@ -0,0 +1,120 @@
+/*********************                                                        */
+/*! \file exception.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief CVC4's exception base class and some associated utilities
+ **
+ ** CVC4's exception base class and some associated utilities.
+ **/
+
+#include "base/exception.h"
+#include <string>
+#include <cstdio>
+#include <cstdlib>
+#include <cstdarg>
+
+#include "base/cvc4_assert.h"
+
+using namespace std;
+
+#warning "TODO: Remove the second definition of CheckArgument and DebugCheckArgument."
+
+namespace CVC4 {
+void IllegalArgumentException::construct(const char* header, const char* extra,
+                                         const char* function, const char* fmt,
+                                         va_list args) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 512;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s\n%s\n",
+                      header, function);
+    } else {
+      size = snprintf(buf, n, "%s\n%s\n\n  %s\n",
+                      header, function, extra);
+    }
+
+    if(size < n) {
+      va_list args_copy;
+      va_copy(args_copy, args);
+      size += vsnprintf(buf + size, n - size, fmt, args_copy);
+      va_end(args_copy);
+
+      if(size < n) {
+        break;
+      }
+    }
+
+    if(size >= n) {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
+  delete [] buf;
+#endif /* CVC4_DEBUG */
+}
+
+void IllegalArgumentException::construct(const char* header, const char* extra,
+                                         const char* function) {
+  // try building the exception msg with a smallish buffer first,
+  // then with a larger one if sprintf tells us to.
+  int n = 256;
+  char* buf;
+
+  for(;;) {
+    buf = new char[n];
+
+    int size;
+    if(extra == NULL) {
+      size = snprintf(buf, n, "%s.\n%s\n",
+                      header, function);
+    } else {
+      size = snprintf(buf, n, "%s.\n%s\n\n  %s\n",
+                      header, function, extra);
+    }
+
+    if(size < n) {
+      break;
+    } else {
+      // try again with a buffer that's large enough
+      n = size + 1;
+      delete [] buf;
+    }
+  }
+
+  setMessage(string(buf));
+
+#ifdef CVC4_DEBUG
+  if(s_debugLastException == NULL) {
+    // we leak buf[] but only in debug mode with assertions failing
+    s_debugLastException = buf;
+  }
+#else /* CVC4_DEBUG */
+  delete [] buf;
+#endif /* CVC4_DEBUG */
+}
+
+} /* namespace CVC4 */
diff --git a/src/base/exception.h b/src/base/exception.h
new file mode 100644
index 000000000..78bb160cc
--- /dev/null
+++ b/src/base/exception.h
@@ -0,0 +1,170 @@
+/*********************                                                        */
+/*! \file exception.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief CVC4's exception base class and some associated utilities
+ **
+ ** CVC4's exception base class and some associated utilities.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__EXCEPTION_H
+#define __CVC4__EXCEPTION_H
+
+#include <iostream>
+#include <string>
+#include <sstream>
+#include <stdexcept>
+#include <exception>
+#include <cstdlib>
+#include <cstdarg>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Exception : public std::exception {
+protected:
+  std::string d_msg;
+
+public:
+  // Constructors
+  Exception() throw() : d_msg("Unknown exception") {}
+  Exception(const std::string& msg) throw() : d_msg(msg) {}
+  Exception(const char* msg) throw() : d_msg(msg) {}
+
+  // Destructor
+  virtual ~Exception() throw() {}
+
+  // NON-VIRTUAL METHOD for setting and printing the error message
+  void setMessage(const std::string& msg) throw() { d_msg = msg; }
+  std::string getMessage() const throw() { return d_msg; }
+
+  // overridden from base class std::exception
+  virtual const char* what() const throw() { return d_msg.c_str(); }
+
+  /**
+   * Get this exception as a string.  Note that
+   *   cout << ex.toString();
+   * is subtly different from
+   *   cout << ex;
+   * which is equivalent to
+   *   ex.toStream(cout);
+   * That is because with the latter two, the output language (and
+   * other preferences) for exprs on the stream is respected.  In
+   * toString(), there is no stream, so the parameters are default
+   * and you'll get exprs and types printed using the AST language.
+   */
+  std::string toString() const throw() {
+    std::stringstream ss;
+    toStream(ss);
+    return ss.str();
+  }
+
+  /**
+   * Printing: feel free to redefine toStream().  When overridden in
+   * a derived class, it's recommended that this method print the
+   * type of exception before the actual message.
+   */
+  virtual void toStream(std::ostream& os) const throw() { os << d_msg; }
+
+};/* class Exception */
+
+class CVC4_PUBLIC IllegalArgumentException : public Exception {
+protected:
+  IllegalArgumentException() : Exception() {}
+
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* fmt, ...) {
+    va_list args;
+    va_start(args, fmt);
+    construct(header, extra, function, fmt, args);
+    va_end(args);
+  }
+
+  void construct(const char* header, const char* extra,
+                 const char* function, const char* fmt, va_list args);
+
+  void construct(const char* header, const char* extra,
+                 const char* function);
+
+public:
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function, const char* fmt, ...) :
+    Exception() {
+    va_list args;
+    va_start(args, fmt);
+    construct("Illegal argument detected",
+              ( std::string("`") + argDesc + "' is a bad argument"
+                + (*condStr == '\0' ? std::string() :
+                    ( std::string("; expected ") +
+                        condStr + " to hold" )) ).c_str(),
+              function, fmt, args);
+    va_end(args);
+  }
+
+  IllegalArgumentException(const char* condStr, const char* argDesc,
+                           const char* function) :
+    Exception() {
+    construct("Illegal argument detected",
+              ( std::string("`") + argDesc + "' is a bad argument"
+                + (*condStr == '\0' ? std::string() :
+                    ( std::string("; expected ") +
+                        condStr + " to hold" )) ).c_str(),
+              function);
+  }
+};/* class IllegalArgumentException */
+
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
+  e.toStream(os);
+  return os;
+}
+
+}/* CVC4 namespace */
+
+#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT)
+#  include "base/cvc4_assert.h"
+#endif /* (__BUILDING_CVC4LIB || __BUILDING_CVC4LIB_UNIT_TEST) && !__BUILDING_STATISTICS_FOR_EXPORT */
+
+namespace CVC4 {
+
+#ifndef CheckArgument
+template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg, const char* fmt, ...) {
+  if(__builtin_expect( ( !cond ), false )) { \
+    throw ::CVC4::IllegalArgumentException("", "", ""); \
+  } \
+}
+template <class T> inline void CheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
+template <class T> inline void CheckArgument(bool cond, const T& arg) {
+  if(__builtin_expect( ( !cond ), false )) { \
+    throw ::CVC4::IllegalArgumentException("", "", ""); \
+  } \
+}
+#endif /* CheckArgument */
+
+#ifndef DebugCheckArgument
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) CVC4_PUBLIC;
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg, const char* fmt, ...) {
+  if(__builtin_expect( ( !cond ), false )) { \
+    throw ::CVC4::IllegalArgumentException("", "", ""); \
+  } \
+}
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg) CVC4_PUBLIC;
+template <class T> inline void DebugCheckArgument(bool cond, const T& arg) {
+  if(__builtin_expect( ( !cond ), false )) { \
+    throw ::CVC4::IllegalArgumentException("", "", ""); \
+  } \
+}
+#endif /* DebugCheckArgument */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXCEPTION_H */
diff --git a/src/base/exception.i b/src/base/exception.i
new file mode 100644
index 000000000..083670567
--- /dev/null
+++ b/src/base/exception.i
@@ -0,0 +1,11 @@
+%{
+#include "base/exception.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const Exception&) throw();
+%ignore CVC4::Exception::Exception(const char*) throw();
+%typemap(javabase) CVC4::Exception "java.lang.RuntimeException";
+
+%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
+
+%include "base/exception.h"
diff --git a/src/base/lemma_input_channel_forward.h b/src/base/lemma_input_channel_forward.h
new file mode 100644
index 000000000..f74e24b4a
--- /dev/null
+++ b/src/base/lemma_input_channel_forward.h
@@ -0,0 +1,30 @@
+/*********************                                                        */
+/*! \file lemma_input_channel_forward.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) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Forward declaration of LemmaInputChannel.
+ **
+ ** This forward declaration of LemmaInputChannel is needed for the option
+ ** lemmaInputChannel (defined in smt_options) can be a LemmaInputChannel*
+ ** without including expr.h.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H
+#define __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H
+
+namespace CVC4 {
+
+class CVC4_PUBLIC LemmaInputChannel;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_INPUT_CHANNEL_FORWARD_H */
diff --git a/src/base/lemma_output_channel_forward.h b/src/base/lemma_output_channel_forward.h
new file mode 100644
index 000000000..c53bcc36f
--- /dev/null
+++ b/src/base/lemma_output_channel_forward.h
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file lemma_output_channel_forward.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) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Forward declaration of the LemmaOutputChannel
+ **
+ ** This forward declaration of LemmaOutputChannel is needed for the option
+ ** lemmaOutputChannel (defined in smt_options) can be a LemmaInputChannel*
+ ** without including expr.h.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H
+#define __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H
+
+namespace CVC4 {
+
+/**
+ * This interface describes a mechanism for the propositional and theory
+ * engines to communicate with the "outside world" about new lemmas being
+ * discovered.
+ */
+class CVC4_PUBLIC LemmaOutputChannel;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__LEMMA_OUTPUT_CHANNEL_FORWARD_H */
diff --git a/src/base/modal_exception.h b/src/base/modal_exception.h
new file mode 100644
index 000000000..44f133372
--- /dev/null
+++ b/src/base/modal_exception.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file modal_exception.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An exception that is thrown when an interactive-only
+ ** feature while CVC4 is being used in a non-interactive setting
+ **
+ ** An exception that is thrown when an interactive-only feature while
+ ** CVC4 is being used in a non-interactive setting (for example, the
+ ** "(get-assertions)" command in an SMT-LIBv2 script).
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__MODAL_EXCEPTION_H
+#define __CVC4__SMT__MODAL_EXCEPTION_H
+
+#include "base/exception.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC ModalException : public CVC4::Exception {
+public:
+  ModalException() :
+    Exception("Feature used while operating in "
+              "incorrect state") {
+  }
+
+  ModalException(const std::string& msg) :
+    Exception(msg) {
+  }
+
+  ModalException(const char* msg) :
+    Exception(msg) {
+  }
+};/* class ModalException */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */
diff --git a/src/base/modal_exception.i b/src/base/modal_exception.i
new file mode 100644
index 000000000..7df4c8f83
--- /dev/null
+++ b/src/base/modal_exception.i
@@ -0,0 +1,7 @@
+%{
+#include "base/modal_exception.h"
+%}
+
+%ignore CVC4::ModalException::ModalException(const char*);
+
+%include "base/modal_exception.h"
diff --git a/src/base/output.cpp b/src/base/output.cpp
new file mode 100644
index 000000000..be0f10fda
--- /dev/null
+++ b/src/base/output.cpp
@@ -0,0 +1,194 @@
+/*********************                                                        */
+/*! \file output.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Output utility classes and functions
+ **
+ ** Output utility classes and functions.
+ **/
+
+#include "base/output.h"
+
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+
+/* Definitions of the declared globals from output.h... */
+
+null_streambuf null_sb;
+ostream null_os(&null_sb);
+
+NullC nullCvc4Stream CVC4_PUBLIC;
+
+const std::string CVC4ostream::s_tab = "  ";
+const int CVC4ostream::s_indentIosIndex = ios_base::xalloc();
+
+DebugC DebugChannel CVC4_PUBLIC (&cout);
+WarningC WarningChannel CVC4_PUBLIC (&cerr);
+MessageC MessageChannel CVC4_PUBLIC (&cout);
+NoticeC NoticeChannel CVC4_PUBLIC (&null_os);
+ChatC ChatChannel CVC4_PUBLIC (&null_os);
+TraceC TraceChannel CVC4_PUBLIC (&cout);
+std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer
+DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout);
+
+#ifndef CVC4_MUZZLE
+
+#  if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+
+int DebugC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int DebugC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+#  endif /* CVC4_DEBUG && CVC4_TRACING */
+
+int WarningC::printf(const char* fmt, ...) {
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int MessageC::printf(const char* fmt, ...) {
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int NoticeC::printf(const char* fmt, ...) {
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int ChatC::printf(const char* fmt, ...) {
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+#  ifdef CVC4_TRACING
+
+int TraceC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int TraceC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+#  endif /* CVC4_TRACING */
+
+#  ifdef CVC4_DUMPING
+
+int DumpOutC::printf(const char* tag, const char* fmt, ...) {
+  if(d_tags.find(string(tag)) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+int DumpOutC::printf(std::string tag, const char* fmt, ...) {
+  if(d_tags.find(tag) == d_tags.end()) {
+    return 0;
+  }
+
+  // chop off output after 1024 bytes
+  char buf[1024];
+  va_list vl;
+  va_start(vl, fmt);
+  int retval = vsnprintf(buf, sizeof(buf), fmt, vl);
+  va_end(vl);
+  *d_os << buf;
+  return retval;
+}
+
+#  endif /* CVC4_DUMPING */
+
+#endif /* ! CVC4_MUZZLE */
+
+}/* CVC4 namespace */
diff --git a/src/base/output.h b/src/base/output.h
new file mode 100644
index 000000000..0974591db
--- /dev/null
+++ b/src/base/output.h
@@ -0,0 +1,590 @@
+/*********************                                                        */
+/*! \file output.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Tim King, Dejan Jovanovic
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Output utility classes and functions
+ **
+ ** Output utility classes and functions.
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef __CVC4__OUTPUT_H
+#define __CVC4__OUTPUT_H
+
+#include <ios>
+#include <iostream>
+#include <streambuf>
+#include <string>
+#include <cstdio>
+#include <cstdarg>
+#include <set>
+#include <utility>
+
+namespace CVC4 {
+
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) CVC4_PUBLIC;
+
+template <class T, class U>
+std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+  return out << "[" << p.first << "," << p.second << "]";
+}
+
+/**
+ * A utility class to provide (essentially) a "/dev/null" streambuf.
+ * If debugging support is compiled in, but debugging for
+ * e.g. "parser" is off, then Debug("parser") returns a stream
+ * attached to a null_streambuf instance so that output is directed to
+ * the bit bucket.
+ */
+class CVC4_PUBLIC null_streambuf : public std::streambuf {
+public:
+  /* Overriding overflow() just ensures that EOF isn't returned on the
+   * stream.  Perhaps this is not so critical, but recommended; this
+   * way the output stream looks like it's functioning, in a non-error
+   * state. */
+  int overflow(int c) { return c; }
+};/* class null_streambuf */
+
+/** A null stream-buffer singleton */
+extern null_streambuf null_sb;
+/** A null output stream singleton */
+extern std::ostream null_os CVC4_PUBLIC;
+
+class CVC4_PUBLIC CVC4ostream {
+  static const std::string s_tab;
+  static const int s_indentIosIndex;
+
+  /** The underlying ostream */
+  std::ostream* d_os;
+  /** Are we in the first column? */
+  bool d_firstColumn;
+
+  /** The endl manipulator (why do we need to keep this?) */
+  std::ostream& (*const d_endl)(std::ostream&);
+
+  // do not allow use
+  CVC4ostream& operator=(const CVC4ostream&);
+
+public:
+  CVC4ostream() :
+    d_os(NULL),
+    d_firstColumn(false),
+    d_endl(&std::endl) {
+  }
+  explicit CVC4ostream(std::ostream* os) :
+    d_os(os),
+    d_firstColumn(true),
+    d_endl(&std::endl) {
+  }
+
+  void pushIndent() {
+    if(d_os != NULL) {
+      ++d_os->iword(s_indentIosIndex);
+    }
+  }
+  void popIndent() {
+    if(d_os != NULL) {
+      long& indent = d_os->iword(s_indentIosIndex);
+      if(indent > 0) {
+        --indent;
+      }
+    }
+  }
+
+  CVC4ostream& flush() {
+    if(d_os != NULL) {
+      d_os->flush();
+    }
+    return *this;
+  }
+
+  bool isConnected() { return d_os != NULL; }
+  operator std::ostream&() { return isConnected() ? *d_os : null_os; }
+
+  template <class T>
+  CVC4ostream& operator<<(T const& t) CVC4_PUBLIC;
+
+  // support manipulators, endl, etc..
+  CVC4ostream& operator<<(std::ostream& (*pf)(std::ostream&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+
+      if(pf == d_endl) {
+        d_firstColumn = true;
+      }
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(std::ios& (*pf)(std::ios&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) {
+    if(d_os != NULL) {
+      d_os = &(*d_os << pf);
+    }
+    return *this;
+  }
+  CVC4ostream& operator<<(CVC4ostream& (*pf)(CVC4ostream&)) {
+    return pf(*this);
+  }
+};/* class CVC4ostream */
+
+inline CVC4ostream& push(CVC4ostream& stream) {
+  stream.pushIndent();
+  return stream;
+}
+
+inline CVC4ostream& pop(CVC4ostream& stream) {
+  stream.popIndent();
+  return stream;
+}
+
+template <class T>
+CVC4ostream& CVC4ostream::operator<<(T const& t) {
+  if(d_os != NULL) {
+    if(d_firstColumn) {
+      d_firstColumn = false;
+      long indent = d_os->iword(s_indentIosIndex);
+      for(long i = 0; i < indent; ++i) {
+        d_os = &(*d_os << s_tab);
+      }
+    }
+    d_os = &(*d_os << t);
+  }
+  return *this;
+}
+
+/**
+ * Does nothing; designed for compilation of non-debug/non-trace
+ * builds.  None of these should ever be called in such builds, but we
+ * offer this to the compiler so it doesn't complain.
+ */
+class CVC4_PUBLIC NullC {
+public:
+  operator bool() { return false; }
+  operator CVC4ostream() { return CVC4ostream(); }
+  operator std::ostream&() { return null_os; }
+};/* class NullC */
+
+extern NullC nullCvc4Stream CVC4_PUBLIC;
+
+/** The debug output class */
+class CVC4_PUBLIC DebugC {
+  std::set<std::string> d_tags;
+  std::ostream* d_os;
+
+public:
+  explicit DebugC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class DebugC */
+
+/** The warning output class */
+class CVC4_PUBLIC WarningC {
+  std::set< std::pair<const char*, size_t> > d_alreadyWarned;
+  std::ostream* d_os;
+
+public:
+  explicit WarningC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+
+  // This function supports the WarningOnce() macro, which allows you
+  // to easily indicate that a warning should be emitted, but only
+  // once for a given run of CVC4.
+  bool warnOnce(const char* file, size_t line) {
+    std::pair<const char*, size_t> pr = std::make_pair(file, line);
+    if(d_alreadyWarned.find(pr) != d_alreadyWarned.end()) {
+      // signal caller not to warn again
+      return false;
+    }
+
+    // okay warn this time, but don't do it again
+    d_alreadyWarned.insert(pr);
+    return true;
+  }
+
+};/* class WarningC */
+
+/** The message output class */
+class CVC4_PUBLIC MessageC {
+  std::ostream* d_os;
+
+public:
+  explicit MessageC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+};/* class MessageC */
+
+/** The notice output class */
+class CVC4_PUBLIC NoticeC {
+  std::ostream* d_os;
+
+public:
+  explicit NoticeC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+};/* class NoticeC */
+
+/** The chat output class */
+class CVC4_PUBLIC ChatC {
+  std::ostream* d_os;
+
+public:
+  explicit ChatC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+  CVC4ostream operator()() { return CVC4ostream(d_os); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+
+  bool isOn() const { return d_os != &null_os; }
+};/* class ChatC */
+
+/** The trace output class */
+class CVC4_PUBLIC TraceC {
+  std::ostream* d_os;
+  std::set<std::string> d_tags;
+
+public:
+  explicit TraceC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class TraceC */
+
+/** The dump output class */
+class CVC4_PUBLIC DumpOutC {
+  std::set<std::string> d_tags;
+  std::ostream* d_os;
+
+public:
+  /**
+   * A copy of cout for use by the dumper.  This is important because
+   * it has different settings (e.g., the expr printing depth is always
+   * unlimited). */
+  static std::ostream dump_cout;
+
+  explicit DumpOutC(std::ostream* os) : d_os(os) {}
+
+  int printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+  int printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4)));
+
+  CVC4ostream operator()(const char* tag) {
+    if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+  CVC4ostream operator()(std::string tag) {
+    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
+      return CVC4ostream(d_os);
+    } else {
+      return CVC4ostream();
+    }
+  }
+
+  bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; }
+  bool on (std::string tag) { d_tags.insert(tag); return true; }
+  bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; }
+  bool off(std::string tag) { d_tags.erase (tag); return false; }
+  bool off()                { d_tags.clear(); return false; }
+
+  bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); }
+  bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); }
+
+  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& getStream() { return *d_os; }
+};/* class DumpOutC */
+
+/** The debug output singleton */
+extern DebugC DebugChannel CVC4_PUBLIC;
+/** The warning output singleton */
+extern WarningC WarningChannel CVC4_PUBLIC;
+/** The message output singleton */
+extern MessageC MessageChannel CVC4_PUBLIC;
+/** The notice output singleton */
+extern NoticeC NoticeChannel CVC4_PUBLIC;
+/** The chat output singleton */
+extern ChatC ChatChannel CVC4_PUBLIC;
+/** The trace output singleton */
+extern TraceC TraceChannel CVC4_PUBLIC;
+/** The dump output singleton */
+extern DumpOutC DumpOutChannel CVC4_PUBLIC;
+
+#ifdef CVC4_MUZZLE
+
+#  define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+#  define Warning ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define Message ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#  define Notice ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+#  define Chat ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+#  define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+#  define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
+
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int WarningC::printf(const char* fmt, ...) { return 0; }
+inline int MessageC::printf(const char* fmt, ...) { return 0; }
+inline int NoticeC::printf(const char* fmt, ...) { return 0; }
+inline int ChatC::printf(const char* fmt, ...) { return 0; }
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
+
+#else /* CVC4_MUZZLE */
+
+#  if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+#    define Debug ::CVC4::DebugChannel
+#  else /* CVC4_DEBUG && CVC4_TRACING */
+#    define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
+inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_DEBUG && CVC4_TRACING */
+#  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
+#  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
+#  define Notice (! ::CVC4::NoticeChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::NoticeChannel
+#  define Chat (! ::CVC4::ChatChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::ChatChannel
+#  ifdef CVC4_TRACING
+#    define Trace ::CVC4::TraceChannel
+#  else /* CVC4_TRACING */
+#    define Trace ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::TraceChannel
+inline int TraceC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int TraceC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_TRACING */
+#  ifdef CVC4_DUMPING
+#    define DumpOut ::CVC4::DumpOutChannel
+#  else /* CVC4_DUMPING */
+#    define DumpOut ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DumpOutChannel
+inline int DumpOutC::printf(const char* tag, const char* fmt, ...) { return 0; }
+inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
+#  endif /* CVC4_DUMPING */
+
+#endif /* CVC4_MUZZLE */
+
+// Disallow e.g. !Debug("foo").isOn() forms
+// because the ! will apply before the ? .
+// If a compiler error has directed you here,
+// just parenthesize it e.g. !(Debug("foo").isOn())
+class __cvc4_true {
+  void operator!() CVC4_UNUSED;
+  void operator~() CVC4_UNUSED;
+  void operator-() CVC4_UNUSED;
+  void operator+() CVC4_UNUSED;
+public:
+  inline operator bool() { return true; }
+};/* __cvc4_true */
+
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+
+class CVC4_PUBLIC ScopedDebug {
+  std::string d_tag;
+  bool d_oldSetting;
+
+public:
+
+  ScopedDebug(std::string tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Debug.isOn(d_tag);
+    if(newSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+
+  ScopedDebug(const char* tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Debug.isOn(d_tag);
+    if(newSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+
+  ~ScopedDebug() {
+    if(d_oldSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+};/* class ScopedDebug */
+
+#else /* CVC4_DEBUG && CVC4_TRACING */
+
+class CVC4_PUBLIC ScopedDebug {
+public:
+  ScopedDebug(std::string tag, bool newSetting = true) {}
+  ScopedDebug(const char* tag, bool newSetting = true) {}
+};/* class ScopedDebug */
+
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+
+#ifdef CVC4_TRACING
+
+class CVC4_PUBLIC ScopedTrace {
+  std::string d_tag;
+  bool d_oldSetting;
+
+public:
+
+  ScopedTrace(std::string tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Trace.isOn(d_tag);
+    if(newSetting) {
+      Trace.on(d_tag);
+    } else {
+      Trace.off(d_tag);
+    }
+  }
+
+  ScopedTrace(const char* tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Trace.isOn(d_tag);
+    if(newSetting) {
+      Trace.on(d_tag);
+    } else {
+      Trace.off(d_tag);
+    }
+  }
+
+  ~ScopedTrace() {
+    if(d_oldSetting) {
+      Trace.on(d_tag);
+    } else {
+      Trace.off(d_tag);
+    }
+  }
+};/* class ScopedTrace */
+
+#else /* CVC4_TRACING */
+
+class CVC4_PUBLIC ScopedTrace {
+public:
+  ScopedTrace(std::string tag, bool newSetting = true) {}
+  ScopedTrace(const char* tag, bool newSetting = true) {}
+};/* class ScopedTrace */
+
+#endif /* CVC4_TRACING */
+
+/**
+ * Pushes an indentation level on construction, pop on destruction.
+ * Useful for tracing recursive functions especially, but also can be
+ * used for clearly separating different phases of an algorithm,
+ * or iterations of a loop, or... etc.
+ */
+class CVC4_PUBLIC IndentedScope {
+  CVC4ostream d_out;
+public:
+  inline IndentedScope(CVC4ostream out);
+  inline ~IndentedScope();
+};/* class IndentedScope */
+
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; }
+inline IndentedScope::~IndentedScope() { d_out << pop; }
+#else /* CVC4_DEBUG && CVC4_TRACING */
+inline IndentedScope::IndentedScope(CVC4ostream out) {}
+inline IndentedScope::~IndentedScope() {}
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__OUTPUT_H */
diff --git a/src/base/tls.h.in b/src/base/tls.h.in
new file mode 100644
index 000000000..88969e250
--- /dev/null
+++ b/src/base/tls.h.in
@@ -0,0 +1,198 @@
+/*********************                                                        */
+/*! \file tls.h.in
+ ** \verbatim
+ ** Original author: ACSYS
+ ** Major contributors: Morgan Deters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Header to define CVC4_THREAD whether or not TLS is
+ ** supported by the compiler/runtime platform
+ **
+ ** Header to define CVC4_THREAD whether or not TLS is supported by
+ ** the compiler/runtime platform.  If not, an implementation based on
+ ** pthread_getspecific() / pthread_setspecific() is given.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TLS_H
+#define __CVC4__TLS_H
+
+// A bit obnoxious: we have to take varargs to support multi-argument
+// template types in the threadlocals.
+// E.g. "CVC4_THREADLOCAL(hash_set<type, hasher>*)" fails otherwise,
+// due to the embedded comma.
+#if @CVC4_TLS_SUPPORTED@
+#  define CVC4_THREADLOCAL(__type...) @CVC4_TLS@ __type
+#  define CVC4_THREADLOCAL_PUBLIC(__type...) @CVC4_TLS@ CVC4_PUBLIC __type
+#  define CVC4_THREADLOCAL_TYPE(__type...) __type
+#else
+#  include <pthread.h>
+#  define CVC4_THREADLOCAL(__type...) ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL_PUBLIC(__type...) CVC4_PUBLIC ::CVC4::ThreadLocal< __type >
+#  define CVC4_THREADLOCAL_TYPE(__type...) ::CVC4::ThreadLocal< __type >
+
+namespace CVC4 {
+
+template <class T, bool small>
+class ThreadLocalImpl;
+
+template <class T>
+class ThreadLocalImpl<T, true> {
+  pthread_key_t d_key;
+
+  static void cleanup(void*) {
+  }
+
+public:
+  ThreadLocalImpl() {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+  }
+
+  ThreadLocalImpl(const T& t) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+  }
+
+  ThreadLocalImpl(const ThreadLocalImpl& tl) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl))));
+  }
+
+  ThreadLocalImpl& operator=(const T& t) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+    return *this;
+  }
+  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T&>(tl))));
+    return *this;
+  }
+
+  operator T() const {
+    return static_cast<T>(reinterpret_cast<size_t>(pthread_getspecific(d_key)));
+  }
+};/* class ThreadLocalImpl<T, true> */
+
+template <class T>
+class ThreadLocalImpl<T*, true> {
+  pthread_key_t d_key;
+
+  static void cleanup(void*) {
+  }
+
+public:
+  ThreadLocalImpl() {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+  }
+
+  ThreadLocalImpl(const T* t) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+  }
+
+  ThreadLocalImpl(const ThreadLocalImpl& tl) {
+    pthread_key_create(&d_key, ThreadLocalImpl::cleanup);
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
+  }
+
+  ThreadLocalImpl& operator=(const T* t) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(t)));
+    return *this;
+  }
+  ThreadLocalImpl& operator=(const ThreadLocalImpl& tl) {
+    pthread_setspecific(d_key, const_cast<void*>(reinterpret_cast<const void*>(static_cast<const T*>(tl))));
+    return *this;
+  }
+
+  operator T*() const {
+    return static_cast<T*>(pthread_getspecific(d_key));
+  }
+
+  T operator*() {
+    return *static_cast<T*>(pthread_getspecific(d_key));
+  }
+  T* operator->() {
+    return static_cast<T*>(pthread_getspecific(d_key));
+  }
+};/* class ThreadLocalImpl<T*, true> */
+
+template <class T>
+class ThreadLocalImpl<T, false> {
+};/* class ThreadLocalImpl<T, false> */
+
+template <class T>
+class ThreadLocal : public ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> {
+  typedef ThreadLocalImpl<T, sizeof(T) <= sizeof(void*)> super;
+
+public:
+  ThreadLocal() : super() {}
+  ThreadLocal(const T& t) : super(t) {}
+  ThreadLocal(const ThreadLocal<T>& tl) : super(tl) {}
+
+  ThreadLocal<T>& operator=(const T& t) {
+    return static_cast< ThreadLocal<T>& >(super::operator=(t));
+  }
+  ThreadLocal<T>& operator=(const ThreadLocal<T>& tl) {
+    return static_cast< ThreadLocal<T>& >(super::operator=(tl));
+  }
+};/* class ThreadLocal<T> */
+
+template <class T>
+class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> {
+  typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super;
+
+public:
+  ThreadLocal() : super() {}
+  ThreadLocal(T* t) : super(t) {}
+  ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {}
+
+  ThreadLocal<T*>& operator=(T* t) {
+    return static_cast< ThreadLocal<T*>& >(super::operator=(t));
+  }
+  ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) {
+    return static_cast< ThreadLocal<T*>& >(super::operator=(tl));
+  }
+  // special operators for pointers
+  T& operator*() {
+    return *static_cast<T*>(*this);
+  }
+  const T& operator*() const {
+    return *static_cast<const T*>(*this);
+  }
+  T* operator->() {
+    return static_cast<T*>(*this);
+  }
+  const T* operator->() const {
+    return static_cast<const T*>(*this);
+  }
+  T* operator++() {
+    T* p = *this;
+    *this = ++p;
+    return p;
+  }
+  T* operator++(int) {
+    T* p = *this;
+    *this = p + 1;
+    return p;
+  }
+  T* operator--() {
+    T* p = *this;
+    *this = --p;
+    return p;
+  }
+  T* operator--(int) {
+    T* p = *this;
+    *this = p - 1;
+    return p;
+  }
+};/* class ThreadLocal<T*> */
+
+}/* CVC4 namespace */
+
+#endif /* @CVC4_TLS_SUPPORTED@ */
+
+#endif /* __CVC4__TLS_H */