Adding listeners to Options.

- Options
-- Added the new option attribute :notify. One can get a notify() call on the Listener after a the option's value is updated. This is the new preferred way to achieve dynamic dispatch for options.
-- Removed SmtOptionsHandler and pushed its functionality into OptionsHandler and Listeners.
-- Added functions to Options for registering listeners of the notify calls.
-- Changed a number of options to use the new listener infrastructure.
-- Fixed a number of warnings in options.
-- Added the ArgumentExtender class to better capture how arguments are inserted while parsing options and ease memory management. Previously this was the "preemptGetopt" procedure.
-- Moved options/options_handler_interface.{cpp,h} to options/options_handler.{cpp,h}.

- Theories
-- Reimplemented alternative theories to use a datastructure stored on TheoryEngine instead of on Options.

- Ostream Handling:
-- Added new functionality that generalized how ostreams are opened, options/open_stream.h.
-- Simplified the memory management for different ostreams, smt/managed_ostreams.h.
-- Had the SmtEnginePrivate manage the memory for the ostreams set by options.
-- Simplified how the setting of ostreams are updated, smt/update_ostream.h.

- Configuration and Tags:
-- Configuration can now be used during predicates and handlers for options.
-- Moved configuration.{cpp,h,i} and configuration_private.h from util/ into base/.
-- Moved {Debug,Trace}_tags.* from being generated in options/ into base/.

- cvc4_private.h
-- Upgraded #warning's in cvc4_private.h and cvc4_private_library.h to #error's.
-- Added public first-order (non-templatized) member functions for options get and set the value of options outside of libcvc4. Fixed all of the use locations.
-- Made lib/lib/clock_gettime.h a cvc4_private_library.h header.

- Antlr
-- Fixed antlr and cvc4 macro definition conflicts that caused warnings.

- SmtGlobals
-- Refactored replayStream and replayLog out of SmtGlobals.
-- Renamed SmtGlobals to LemmaChannels and moved the implementation into smt_util/lemma_channels.{h,cpp}.

12 files changed, 847 insertions, 38 deletions

diff --git a/src/base/Makefile.am b/src/base/Makefile.am
index f2fe3f306..bda063176 100644
--- a/src/base/Makefile.am
+++ b/src/base/Makefile.am
@@ -15,6 +15,9 @@ noinst_LTLIBRARIES = libbase.la
 libbase_la_SOURCES = \
 	Makefile.am \
 	Makefile.in \
+	configuration.cpp \
+	configuration.h \
+	configuration_private.h \
 	cvc4_assert.cpp \
 	cvc4_assert.h \
 	exception.cpp \
@@ -30,11 +33,52 @@ libbase_la_SOURCES = \
 BUILT_SOURCES = \
 	tls.h
 
+# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it
+# after building (if it does, we don't get the "cached" effect with
+# the .tmp files below, and we have to re-compile and re-link each
+# time, even when there are no changes).
+BUILT_SOURCES += \
+	Debug_tags.h \
+	Debug_tags \
+	Trace_tags.h \
+	Trace_tags
+
+MOSTLYCLEANFILES = \
+	Debug_tags \
+	Trace_tags \
+	Debug_tags.tmp \
+	Trace_tags.tmp \
+	Debug_tags.h \
+	Trace_tags.h
+
 EXTRA_DIST = \
+	configuration.i \
 	exception.i \
+	mktagheaders \
+	mktags \
 	modal_exception.i \
 	tls.h.in
 
 DISTCLEANFILES = \
 	tls.h.tmp \
 	tls.h
+
+%_tags.h: %_tags mktagheaders
+	$(AM_V_at)chmod +x @srcdir@/mktagheaders
+	$(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@"
+
+# This .tmp business is to keep from having to re-compile options.cpp
+# (and then re-link the libraries) if nothing has changed.
+%_tags: %_tags.tmp
+	$(AM_V_GEN)\
+	diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true
+# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
+.PHONY: Debug_tags.tmp Trace_tags.tmp
+# The "sed" invocation below is particularly obnoxious, but it works around
+# inconsistencies in REs on different platforms, using only a basic regular
+# expression (no |, no \<, ...).
+Debug_tags.tmp Trace_tags.tmp: mktags
+	$(AM_V_at)chmod +x @srcdir@/mktags
+	$(AM_V_GEN)(@srcdir@/mktags \
+    '$(@:_tags.tmp=)' \
+    "$$(find @srcdir@/../ -name '*.cpp' -o -name '*.h' -o -name '*.cc' -o -name '*.g')") >"$@"
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
new file mode 100644
index 000000000..c3ba39075
--- /dev/null
+++ b/src/base/configuration.cpp
@@ -0,0 +1,293 @@
+/*********************                                                        */
+/*! \file configuration.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): Liana Hadarean, Tim King, ACSYS, Christopher L. Conway, Dejan Jovanovic, Francois Bobot
+ ** 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 Implementation of Configuration class, which provides compile-time
+ ** configuration information about the CVC4 library
+ **
+ ** Implementation of Configuration class, which provides compile-time
+ ** configuration information about the CVC4 library.
+ **/
+#include "base/configuration.h"
+
+#include <stdlib.h>
+#include <string.h>
+
+#include <sstream>
+#include <string>
+
+#include "cvc4autoconfig.h"
+#include "base/configuration_private.h"
+
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+#  include "base/Debug_tags.h"
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+
+#ifdef CVC4_TRACING
+#  include "base/Trace_tags.h"
+#endif /* CVC4_TRACING */
+
+using namespace std;
+
+namespace CVC4 {
+
+string Configuration::getName() {
+  return PACKAGE_NAME;
+}
+
+bool Configuration::isDebugBuild() {
+  return IS_DEBUG_BUILD;
+}
+
+bool Configuration::isStatisticsBuild() {
+  return IS_STATISTICS_BUILD;
+}
+
+bool Configuration::isReplayBuild() {
+  return IS_REPLAY_BUILD;
+}
+
+bool Configuration::isTracingBuild() {
+  return IS_TRACING_BUILD;
+}
+
+bool Configuration::isDumpingBuild() {
+  return IS_DUMPING_BUILD;
+}
+
+bool Configuration::isMuzzledBuild() {
+  return IS_MUZZLED_BUILD;
+}
+
+bool Configuration::isAssertionBuild() {
+  return IS_ASSERTIONS_BUILD;
+}
+
+bool Configuration::isProofBuild() {
+  return IS_PROOFS_BUILD;
+}
+
+bool Configuration::isCoverageBuild() {
+  return IS_COVERAGE_BUILD;
+}
+
+bool Configuration::isProfilingBuild() {
+  return IS_PROFILING_BUILD;
+}
+
+bool Configuration::isCompetitionBuild() {
+  return IS_COMPETITION_BUILD;
+}
+
+string Configuration::getPackageName() {
+  return PACKAGE_NAME;
+}
+
+string Configuration::getVersionString() {
+  return CVC4_RELEASE_STRING;
+}
+
+unsigned Configuration::getVersionMajor() {
+  return CVC4_MAJOR;
+}
+
+unsigned Configuration::getVersionMinor() {
+  return CVC4_MINOR;
+}
+
+unsigned Configuration::getVersionRelease() {
+  return CVC4_RELEASE;
+}
+
+std::string Configuration::getVersionExtra() {
+  return CVC4_EXTRAVERSION;
+}
+
+std::string Configuration::about() {
+  return CVC4_ABOUT_STRING;
+}
+
+bool Configuration::licenseIsGpl() {
+  return IS_GPL_BUILD;
+}
+
+bool Configuration::isBuiltWithGmp() {
+  return IS_GMP_BUILD;
+}
+
+bool Configuration::isBuiltWithCln() {
+  return IS_CLN_BUILD;
+}
+
+bool Configuration::isBuiltWithGlpk() {
+  return IS_GLPK_BUILD;
+}
+
+bool Configuration::isBuiltWithAbc() {
+  return IS_ABC_BUILD;
+}
+
+bool Configuration::isBuiltWithReadline() {
+  return IS_READLINE_BUILD;
+}
+
+bool Configuration::isBuiltWithCudd() {
+  return false;
+}
+
+bool Configuration::isBuiltWithTlsSupport() {
+  return USING_TLS;
+}
+
+unsigned Configuration::getNumDebugTags() {
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+  /* -1 because a NULL pointer is inserted as the last value */
+  return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1;
+#else /* CVC4_DEBUG && CVC4_TRACING */
+  return 0;
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+}
+
+char const* const* Configuration::getDebugTags() {
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+  return Debug_tags;
+#else /* CVC4_DEBUG && CVC4_TRACING */
+  static char const* no_tags[] = { NULL };
+  return no_tags;
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+}
+
+int strcmpptr(const char **s1, const char **s2){
+  return strcmp(*s1,*s2);
+}
+
+bool Configuration::isDebugTag(char const *tag){
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
+  unsigned ntags = getNumDebugTags();
+  char const* const* tags = getDebugTags();
+  for (unsigned i = 0; i < ntags; ++ i) {
+    if (strcmp(tag, tags[i]) == 0) {
+      return true;
+    }
+  }
+#endif /* CVC4_DEBUG && CVC4_TRACING */
+  return false;
+}
+
+unsigned Configuration::getNumTraceTags() {
+#if CVC4_TRACING
+  /* -1 because a NULL pointer is inserted as the last value */
+  return sizeof(Trace_tags) / sizeof(Trace_tags[0]) - 1;
+#else /* CVC4_TRACING */
+  return 0;
+#endif /* CVC4_TRACING */
+}
+
+char const* const* Configuration::getTraceTags() {
+#if CVC4_TRACING
+  return Trace_tags;
+#else /* CVC4_TRACING */
+  static char const* no_tags[] = { NULL };
+  return no_tags;
+#endif /* CVC4_TRACING */
+}
+
+bool Configuration::isTraceTag(char const * tag){
+#if CVC4_TRACING
+  unsigned ntags = getNumTraceTags();
+  char const* const* tags = getTraceTags();
+  for (unsigned i = 0; i < ntags; ++ i) {
+    if (strcmp(tag, tags[i]) == 0) {
+      return true;
+    }
+  }
+#endif /* CVC4_TRACING */
+  return false;
+}
+
+bool Configuration::isGitBuild() {
+  return IS_GIT_BUILD;
+}
+
+const char* Configuration::getGitBranchName() {
+  return GIT_BRANCH_NAME;
+}
+
+const char* Configuration::getGitCommit() {
+  return GIT_COMMIT;
+}
+
+bool Configuration::hasGitModifications() {
+  return GIT_HAS_MODIFICATIONS;
+}
+
+std::string Configuration::getGitId() {
+  if(! isGitBuild()) {
+    return "";
+  }
+
+  const char* branchName = getGitBranchName();
+  if(*branchName == '\0') {
+    branchName = "-";
+  }
+
+  stringstream ss;
+  ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
+     << ( ::CVC4::Configuration::hasGitModifications() ? " (with modifications)" : "" );
+  return ss.str();
+}
+
+bool Configuration::isSubversionBuild() {
+  return IS_SUBVERSION_BUILD;
+}
+
+const char* Configuration::getSubversionBranchName() {
+  return SUBVERSION_BRANCH_NAME;
+}
+
+unsigned Configuration::getSubversionRevision() {
+  return SUBVERSION_REVISION;
+}
+
+bool Configuration::hasSubversionModifications() {
+  return SUBVERSION_HAS_MODIFICATIONS;
+}
+
+std::string Configuration::getSubversionId() {
+  if(! isSubversionBuild()) {
+    return "";
+  }
+
+  stringstream ss;
+  ss << "subversion " << getSubversionBranchName() << " r" << getSubversionRevision()
+     << ( ::CVC4::Configuration::hasSubversionModifications() ? " (with modifications)" : "" );
+  return ss.str();
+}
+
+std::string Configuration::getCompiler() {
+  stringstream ss;
+#ifdef __GNUC__
+  ss << "GCC";
+#else /* __GNUC__ */
+  ss << "unknown compiler";
+#endif /* __GNUC__ */
+#ifdef __VERSION__
+  ss << " version " << __VERSION__;
+#else /* __VERSION__ */
+  ss << ", unknown version";
+#endif /* __VERSION__ */
+  return ss.str();
+}
+
+std::string Configuration::getCompiledDateTime() {
+  return __DATE__ " " __TIME__;
+}
+
+}/* CVC4 namespace */
diff --git a/src/base/configuration.h b/src/base/configuration.h
new file mode 100644
index 000000000..818652db0
--- /dev/null
+++ b/src/base/configuration.h
@@ -0,0 +1,135 @@
+/*********************                                                        */
+/*! \file configuration.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): ACSYS, Liana Hadarean, Tim King, Francois Bobot
+ ** 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 Interface to a public class that provides compile-time information
+ ** about the CVC4 library.
+ **
+ ** Interface to a public class that provides compile-time information
+ ** about the CVC4 library.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__CONFIGURATION_H
+#define __CVC4__CONFIGURATION_H
+
+#include <string>
+
+namespace CVC4 {
+
+/**
+ * Represents the (static) configuration of CVC4.
+ */
+class CVC4_PUBLIC Configuration {
+private:
+  /** Private default ctor: Disallow construction of this class */
+  Configuration();
+
+  // these constants are filled in by the build system
+  static const bool IS_SUBVERSION_BUILD;
+  static const char* const SUBVERSION_BRANCH_NAME;
+  static const unsigned SUBVERSION_REVISION;
+  static const bool SUBVERSION_HAS_MODIFICATIONS;
+  static const bool IS_GIT_BUILD;
+  static const char* const GIT_BRANCH_NAME;
+  static const char* const GIT_COMMIT;
+  static const bool GIT_HAS_MODIFICATIONS;
+
+public:
+
+  static std::string getName();
+
+  static bool isDebugBuild();
+
+  static bool isStatisticsBuild();
+
+  static bool isReplayBuild();
+
+  static bool isTracingBuild();
+
+  static bool isDumpingBuild();
+
+  static bool isMuzzledBuild();
+
+  static bool isAssertionBuild();
+
+  static bool isProofBuild();
+
+  static bool isCoverageBuild();
+
+  static bool isProfilingBuild();
+
+  static bool isCompetitionBuild();
+
+  static std::string getPackageName();
+
+  static std::string getVersionString();
+
+  static unsigned getVersionMajor();
+
+  static unsigned getVersionMinor();
+
+  static unsigned getVersionRelease();
+
+  static std::string getVersionExtra();
+
+  static std::string about();
+
+  static bool licenseIsGpl();
+
+  static bool isBuiltWithGmp();
+
+  static bool isBuiltWithCln();
+
+  static bool isBuiltWithGlpk();
+
+  static bool isBuiltWithAbc();
+
+  static bool isBuiltWithReadline();
+
+  static bool isBuiltWithCudd();
+
+  static bool isBuiltWithTlsSupport();
+
+  /* Return the number of debug tags */
+  static unsigned getNumDebugTags();
+  /* Return a sorted array of the debug tags name */
+  static char const* const* getDebugTags();
+  /* Test if the given argument is a known debug tag name */
+  static bool isDebugTag(char const *);
+
+  /* Return the number of trace tags */
+  static unsigned getNumTraceTags();
+  /* Return a sorted array of the trace tags name */
+  static char const* const* getTraceTags();
+  /* Test if the given argument is a known trace tag name */
+  static bool isTraceTag(char const *);
+
+  static bool isGitBuild();
+  static const char* getGitBranchName();
+  static const char* getGitCommit();
+  static bool hasGitModifications();
+  static std::string getGitId();
+
+  static bool isSubversionBuild();
+  static const char* getSubversionBranchName();
+  static unsigned getSubversionRevision();
+  static bool hasSubversionModifications();
+  static std::string getSubversionId();
+
+  static std::string getCompiler();
+  static std::string getCompiledDateTime();
+
+};/* class Configuration */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONFIGURATION_H */
diff --git a/src/base/configuration.i b/src/base/configuration.i
new file mode 100644
index 000000000..3b92e2438
--- /dev/null
+++ b/src/base/configuration.i
@@ -0,0 +1,7 @@
+%{
+#include "base/configuration.h"
+%}
+
+%apply char **STRING_ARRAY { char const* const* }
+%include "base/configuration.h"
+%clear char const* const*;
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
new file mode 100644
index 000000000..902fdad09
--- /dev/null
+++ b/src/base/configuration_private.h
@@ -0,0 +1,164 @@
+/*********************                                                        */
+/*! \file configuration_private.h
+ ** \verbatim
+ ** Original author: Christopher L. Conway
+ ** Major contributors: ACSYS, Morgan Deters
+ ** Minor contributors (to current version): Liana Hadarean, Tim King
+ ** 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 Provides compile-time configuration information about the
+ ** CVC4 library.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONFIGURATION_PRIVATE_H
+#define __CVC4__CONFIGURATION_PRIVATE_H
+
+#include <string>
+
+#include "base/configuration.h"
+
+namespace CVC4 {
+
+#ifdef CVC4_DEBUG
+#  define IS_DEBUG_BUILD true
+#else /* CVC4_DEBUG */
+#  define IS_DEBUG_BUILD false
+#endif /* CVC4_DEBUG */
+
+#ifdef CVC4_STATISTICS_ON
+#  define IS_STATISTICS_BUILD true
+#else /* CVC4_STATISTICS_ON */
+#  define IS_STATISTICS_BUILD false
+#endif /* CVC4_STATISTICS_ON */
+
+#ifdef CVC4_REPLAY
+#  define IS_REPLAY_BUILD true
+#else /* CVC4_REPLAY */
+#  define IS_REPLAY_BUILD false
+#endif /* CVC4_REPLAY */
+
+#ifdef CVC4_TRACING
+#  define IS_TRACING_BUILD true
+#else /* CVC4_TRACING */
+#  define IS_TRACING_BUILD false
+#endif /* CVC4_TRACING */
+
+#ifdef CVC4_DUMPING
+#  define IS_DUMPING_BUILD true
+#else /* CVC4_DUMPING */
+#  define IS_DUMPING_BUILD false
+#endif /* CVC4_DUMPING */
+
+#ifdef CVC4_MUZZLE
+#  define IS_MUZZLED_BUILD true
+#else /* CVC4_MUZZLE */
+#  define IS_MUZZLED_BUILD false
+#endif /* CVC4_MUZZLE */
+
+#ifdef CVC4_ASSERTIONS
+#  define IS_ASSERTIONS_BUILD true
+#else /* CVC4_ASSERTIONS */
+#  define IS_ASSERTIONS_BUILD false
+#endif /* CVC4_ASSERTIONS */
+
+#ifdef CVC4_PROOF
+#  define IS_PROOFS_BUILD true
+#else  /* CVC4_PROOF */
+#  define IS_PROOFS_BUILD false
+#endif /* CVC4_PROOF */
+
+#ifdef CVC4_COVERAGE
+#  define IS_COVERAGE_BUILD true
+#else /* CVC4_COVERAGE */
+#  define IS_COVERAGE_BUILD false
+#endif /* CVC4_COVERAGE */
+
+#ifdef CVC4_PROFILING
+#  define IS_PROFILING_BUILD true
+#else /* CVC4_PROFILING */
+#  define IS_PROFILING_BUILD false
+#endif /* CVC4_PROFILING */
+
+#ifdef CVC4_COMPETITION_MODE
+#  define IS_COMPETITION_BUILD true
+#else /* CVC4_COMPETITION_MODE */
+#  define IS_COMPETITION_BUILD false
+#endif /* CVC4_COMPETITION_MODE */
+
+#ifdef CVC4_GMP_IMP
+#  define IS_GMP_BUILD true
+#else /* CVC4_GMP_IMP */
+#  define IS_GMP_BUILD false
+#endif /* CVC4_GMP_IMP */
+
+#ifdef CVC4_CLN_IMP
+#  define IS_CLN_BUILD true
+#else /* CVC4_CLN_IMP */
+#  define IS_CLN_BUILD false
+#endif /* CVC4_CLN_IMP */
+
+#if CVC4_USE_GLPK
+#  define IS_GLPK_BUILD true
+#else /* CVC4_USE_GLPK */
+#  define IS_GLPK_BUILD false
+#endif /* CVC4_USE_GLPK */
+
+#if CVC4_USE_ABC
+#  define IS_ABC_BUILD true
+#else /* CVC4_USE_ABC */
+#  define IS_ABC_BUILD false
+#endif /* CVC4_USE_ABC */
+
+#ifdef HAVE_LIBREADLINE
+#  define IS_READLINE_BUILD true
+#else /* HAVE_LIBREADLINE */
+#  define IS_READLINE_BUILD false
+#endif /* HAVE_LIBREADLINE */
+
+#if CVC4_GPL_DEPS
+#  define IS_GPL_BUILD true
+#else /* CVC4_GPL_DEPS */
+#  define IS_GPL_BUILD false
+#endif /* CVC4_GPL_DEPS */
+
+#ifdef TLS
+#  define USING_TLS true
+#else /* TLS */
+#  define USING_TLS false
+#endif /* TLS */
+
+#define CVC4_ABOUT_STRING ( ::std::string("\
+This is CVC4 version " CVC4_RELEASE_STRING ) + \
+    ( ::CVC4::Configuration::isGitBuild() \
+        ? ( ::std::string(" [") + ::CVC4::Configuration::getGitId() + "]" ) \
+        : \
+    ( ::CVC4::Configuration::isSubversionBuild() \
+        ? ( ::std::string(" [") + ::CVC4::Configuration::getSubversionId() + "]" ) \
+        : ::std::string("") \
+    )) + "\n\
+compiled with " + ::CVC4::Configuration::getCompiler() + "\n\
+on " + ::CVC4::Configuration::getCompiledDateTime() + "\n\n\
+Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014\n\
+  New York University and The University of Iowa\n\n" + \
+    ( IS_GPL_BUILD ? "\
+This build of CVC4 uses GPLed libraries, and is thus covered by the GNU\n\
+General Public License (GPL) version 3.  Versions of CVC4 are available\n\
+that are covered by the (modified) BSD license.  If you want to license\n\
+CVC4 under this license, please configure CVC4 with the \"--bsd\" option\n\
+before building from sources.\n\
+" : \
+"This CVC4 library uses GMP as its multi-precision arithmetic library.\n\n\
+CVC4 is open-source and is covered by the BSD license (modified).\n\n\
+" ) + "\
+THIS SOFTWARE PROVIDED AS-IS, WITHOUT ANY WARRANTIES. USE AT YOUR OWN RISK.\n\n\
+See the file COPYING (distributed with the source code, and with all binaries)\n\
+for the full CVC4 copyright, licensing, and (lack of) warranty information.\n" )
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONFIGURATION_PRIVATE_H */
diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index e1486e5bc..cdad92d5d 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -50,7 +50,7 @@ void LastExceptionBuffer::setContents(const char* string) {
   }
 }
 
-char* IllegalArgumentException::s_header = "Illegal argument detected";
+const char* IllegalArgumentException::s_header = "Illegal argument detected";
 
 std::string IllegalArgumentException::formatVariadic() {
   return std::string();
diff --git a/src/base/exception.h b/src/base/exception.h
index 02384b6cb..38bbe47a4 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -90,7 +90,7 @@ protected:
 
   static std::string format_extra(const char* condStr, const char* argDesc);
 
-  static char* s_header;
+  static const char* s_header;
 
 public:
 
@@ -155,8 +155,8 @@ public:
 
 private:
   /* Disallow copies */
-  LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNUSED;
-  LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNUSED;
+  LastExceptionBuffer(const LastExceptionBuffer&) CVC4_UNDEFINED;
+  LastExceptionBuffer& operator=(const LastExceptionBuffer&) CVC4_UNDEFINED;
 
   char* d_contents;
 
diff --git a/src/base/listener.cpp b/src/base/listener.cpp
index 62bec5990..2daced1f5 100644
--- a/src/base/listener.cpp
+++ b/src/base/listener.cpp
@@ -49,8 +49,8 @@ void ListenerCollection::notify() {
 bool ListenerCollection::empty() const { return d_listeners.empty(); }
 
 
-RegisterListener::RegisterListener(ListenerCollection* collection,
-                                   Listener* listener)
+ListenerCollection::Registration::Registration(
+    ListenerCollection* collection, Listener* listener)
     : d_listener(listener)
     , d_position()
     , d_collection(collection)
@@ -58,9 +58,42 @@ RegisterListener::RegisterListener(ListenerCollection* collection,
   d_position = d_collection->addListener(d_listener);
 }
 
-RegisterListener::~RegisterListener() {
+ListenerCollection::Registration::~Registration() {
   d_collection->removeListener(d_position);
   delete d_listener;
 }
 
+ ListenerCollection::Registration* ListenerCollection::registerListener(
+     Listener* listener)
+{
+  return new Registration(this, listener);
+}
+
+
+ListenerRegistrationList::ListenerRegistrationList()
+    : d_registrations()
+{}
+
+ListenerRegistrationList::~ListenerRegistrationList() {
+  clear();
+}
+
+void ListenerRegistrationList::add(
+    ListenerCollection::Registration* registration)
+{
+  d_registrations.push_back(registration);
+}
+
+void ListenerRegistrationList::clear(){
+  typedef std::list<ListenerCollection::Registration*>::iterator iterator;
+  for(iterator i = d_registrations.begin(), iend = d_registrations.end();
+      i != iend; ++i)
+  {
+    ListenerCollection::Registration* current = *i;
+    delete current;
+  }
+  d_registrations.clear();
+}
+
+
 }/* CVC4 namespace */
diff --git a/src/base/listener.h b/src/base/listener.h
index d6828818c..8094c634d 100644
--- a/src/base/listener.h
+++ b/src/base/listener.h
@@ -14,8 +14,8 @@
  ** Utilities for the development of a Listener interface class. This class
  ** provides a single notification that must be overwritten. This file also
  ** provides a utility class for a collection of listeners and an RAII style
- ** RegisterListener class for managing the relationship between Listeners
- ** and the manager.
+ ** Registration class for managing the relationship between Listeners
+ ** and the collection.
  **/
 
 #include "cvc4_public.h"
@@ -54,45 +54,111 @@ public:
   typedef std::list<Listener*> ListenerList;
   typedef ListenerList::iterator iterator;
 
+  /** Creates an empty listener collection. */
   ListenerCollection();
 
+  /**
+   * Destroys an iterator collection.
+   * If assertions are on, this throws an AssertionException if the collection
+   * is not empty().
+   */
   ~ListenerCollection();
 
+  /**
+   * This adds a listener to the current collection and returns
+   * an iterator to the listener in the collection.
+   * The user of the collection must call removeListener() using
+   * this iterator.
+   * The collection does not take over the memory for the listener.
+   */
   iterator addListener(Listener* listener);
 
+  /**
+   * Remove an listener using the iterator distributed when adding the
+   * listener.
+   */
   void removeListener(iterator position);
 
+  /** Calls notify() on all listeners in the collection. */
   void notify();
 
+  /** Returns true if the collection contains no listeners. */
   bool empty() const;
 
+  /**
+   * Registration is an RAII utility function for using Listener
+   * with ListenerCollection.
+   *
+   * On construction, the Registration takes a ListenerCollection,
+   * collection,
+   * and a Listener*, listener. It takes over the memory for listener. It then
+   * adds listener to collection. On destruction it removes listener and calls
+   * delete on listener.
+   *
+   * Because of this usage, a Registration must be destroyed before the
+   * ListenerCollection it is attached to.
+   */
+  class CVC4_PUBLIC Registration {
+  public:
+    Registration(ListenerCollection* collection, Listener* listener);
+    ~Registration();
+
+  private:
+    Listener* d_listener;
+    ListenerCollection::iterator d_position;
+    ListenerCollection* d_collection;
+  };/* class CVC4::ListenerCollection::Registration */
+
+
+  /**
+   * Returns a new Registration given a Listener that is attached to this
+   * ListenerCollection. Management of the memory is handed to the user of
+   * this function. To remove the listener, call the destructor for the
+   * Registration.
+   */
+  Registration* registerListener(Listener* listener);
+
 private:
+
+  /**
+   * Disabling the copy-constructor.
+   * The user of the class must be know to remove listeners on the collection.
+   * Allowing copies will only cause confusion.
+   */
+  ListenerCollection(const ListenerCollection& copy) CVC4_UNDEFINED;
+
+  /**
+   * Disabling the assignment operator.
+   * The user of the class must be know to remove listeners on the collection.
+   * Allowing copies will only cause confusion.
+   */
+  ListenerCollection& operator=(const ListenerCollection& copy) CVC4_UNDEFINED;
+
+  /** A list of the listeners in the collection.*/
   ListenerList d_listeners;
-};
+};/* class CVC4::ListenerCollection */
 
 /**
- * RegisterListener is an RAII utility function for using Listener
- * with ListenerCollection.
+ * A list of ListenerCollection::Registration* pointers.
  *
- * On construction, the RegisterListener takes a ListenerCollection, collection,
- * and a Listener*, listener. It takes over the memory for listener. It then
- * add listener to collection. On destruction it removes listener and calls
- * delete on listener.
- *
- * Because of this usage, a RegisterListener must be destroyed before
- * collection.
+ * This list assumes it has control over all of the memory of the registrations.
  */
-class CVC4_PUBLIC RegisterListener {
-public:
-  RegisterListener(ListenerCollection* collection, Listener* listener);
-  ~RegisterListener();
-
-private:
-  Listener* d_listener;
-  ListenerCollection::iterator d_position;
-  ListenerCollection* d_collection;
-};
-
+class ListenerRegistrationList {
+ public:
+  ListenerRegistrationList();
+  ~ListenerRegistrationList();
+
+  void add(ListenerCollection::Registration* registration);
+  void clear();
+
+ private:
+  /** Disallow copying.*/
+  ListenerRegistrationList(const ListenerRegistrationList&) CVC4_UNDEFINED;
+  /** Disallow assignment.*/
+  ListenerRegistrationList operator=(const ListenerRegistrationList&)
+      CVC4_UNDEFINED;
+  std::list<ListenerCollection::Registration*> d_registrations;
+};/* class CVC4::ListenerRegistrationList */
 
 }/* CVC4 namespace */
 
diff --git a/src/base/mktagheaders b/src/base/mktagheaders
new file mode 100755
index 000000000..af44cee8d
--- /dev/null
+++ b/src/base/mktagheaders
@@ -0,0 +1,24 @@
+#!/bin/bash
+#
+# mktagheaders
+#
+# The purpose of this script is to generate the *_tag.h header file from the
+# *_tags file.
+#
+# Invocation:
+#
+#    mktagheaders <tag-name> <tag-file>
+#
+# <tag-name> will be the name of the generated array.
+# <tag-file> each line of this file is turned into a string in the generated
+#   array.
+
+TAG_NAME=$1
+TAG_FILE=$2
+
+echo 'static char const* const '$TAG_NAME'[] = {';
+for tag in `cat $TAG_FILE`; do
+  echo "\"$tag\",";
+done;
+echo 'NULL';
+echo '};'
diff --git a/src/base/mktags b/src/base/mktags
new file mode 100755
index 000000000..090e57014
--- /dev/null
+++ b/src/base/mktags
@@ -0,0 +1,35 @@
+#!/bin/bash
+#
+# mktags
+#
+# The purpose of this script is to create Debug_tags and Trace_tags files.
+# Note that in the Makefile workflow these are first stored in a *_tags.tmp
+# file. This file contains a list of all of the strings that occur in things
+# like Debug("foo") or Debug.isOn("bar") in a given directory. The list is
+# seperated by newlines.  The expected Debug_tags file for the previous two
+# tags would be:
+# bar
+# foo
+#
+# Invocation:
+#
+#    mktags {Debug,Trace} <input-files>
+#
+# <input-files> is expected to be passed a single space separated list of files.
+#  One can use quotes to achieve this. This is one reason to use "$(...)"
+#  instead of back ticks `...`.
+
+DebugOrTrace=$1
+InputFiles=$2
+
+grep -h '\<'$DebugOrTrace'\(\.isOn\)* *( *\".*\" *)' \
+  $InputFiles | \
+  sed 's/\/\/.*//;s/^'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]'$DebugOrTrace'\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | \
+  LC_ALL=C sort | \
+  uniq
+
+
+# Reference copy of what this is replacing.
+# 	grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
+#		`find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
+#	sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq 
diff --git a/src/base/output.h b/src/base/output.h
index 0974591db..4bffad85f 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -212,11 +212,12 @@ public:
   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(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& setStream(std::ostream* os) { d_os = os; return *os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
 };/* class DebugC */
 
 /** The warning output class */
@@ -231,8 +232,9 @@ public:
 
   CVC4ostream operator()() { return CVC4ostream(d_os); }
 
-  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
 
   bool isOn() const { return d_os != &null_os; }
 
@@ -264,8 +266,9 @@ public:
 
   CVC4ostream operator()() { return CVC4ostream(d_os); }
 
-  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
 
   bool isOn() const { return d_os != &null_os; }
 };/* class MessageC */
@@ -281,8 +284,9 @@ public:
 
   CVC4ostream operator()() { return CVC4ostream(d_os); }
 
-  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
 
   bool isOn() const { return d_os != &null_os; }
 };/* class NoticeC */
@@ -298,8 +302,9 @@ public:
 
   CVC4ostream operator()() { return CVC4ostream(d_os); }
 
-  std::ostream& setStream(std::ostream& os) { d_os = &os; return os; }
+  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
 
   bool isOn() const { return d_os != &null_os; }
 };/* class ChatC */
@@ -340,8 +345,10 @@ public:
   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& setStream(std::ostream* os) { d_os = os; return *d_os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
+
 };/* class TraceC */
 
 /** The dump output class */
@@ -385,8 +392,9 @@ public:
   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& setStream(std::ostream* os) { d_os = os; return *d_os; }
   std::ostream& getStream() { return *d_os; }
+  std::ostream* getStreamPointer() { return d_os; }
 };/* class DumpOutC */
 
 /** The debug output singleton */