fix bug 22 (remove tracing from non-trace builds; remove all output

from muzzled builds)

add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)

add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class

main driver now gets about() information from CVC4::Configuration.

configure.ac now more flexible at specifying major/minor/release
versions of CVC4

add --show-config option that dumps CVC4's static configuration

commented option processing strings in src/main/getopt.cpp

fixed some compilation problems for muzzled builds.

fixed some test code for non-assertion builds (where no assertions are expected)

4 files changed, 213 insertions, 15 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 9bbf89fff..76414ebe1 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -19,4 +19,5 @@ libutil_la_SOURCES = \
 	output.cpp \
 	output.h \
 	result.h \
-	unique_id.h
+	unique_id.h \
+	configuration.h
diff --git a/src/util/configuration.h b/src/util/configuration.h
new file mode 100644
index 000000000..b761f1f22
--- /dev/null
+++ b/src/util/configuration.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/** configuration.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): taking
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** SmtEngine: the main public entry point of libcvc4.
+ **/
+
+#ifndef __CVC4__CONFIGURATION_H
+#define __CVC4__CONFIGURATION_H
+
+#include "config.h"
+#include "cvc4_config.h"
+
+namespace CVC4 {
+
+/**
+ * Represents the (static) configuration of CVC4.
+ */
+class CVC4_PUBLIC Configuration {
+
+  /** Private default ctor: Disallow construction of this class */
+  Configuration();
+
+public:
+
+  static bool isDebugBuild() {
+#ifdef CVC4_DEBUG
+    return true;
+#else /* CVC4_DEBUG */
+    return false;
+#endif /* CVC4_DEBUG */
+  }
+
+  static bool isTracingBuild() {
+#ifdef CVC4_TRACING
+    return true;
+#else /* CVC4_TRACING */
+    return false;
+#endif /* CVC4_TRACING */
+  }
+
+  static bool isMuzzledBuild() {
+#ifdef CVC4_MUZZLE
+    return true;
+#else /* CVC4_MUZZLE */
+    return false;
+#endif /* CVC4_MUZZLE */
+  }
+
+  static bool isAssertionBuild() {
+#ifdef CVC4_ASSERTIONS
+    return true;
+#else /* CVC4_ASSERTIONS */
+    return false;
+#endif /* CVC4_ASSERTIONS */
+  }
+
+  static bool isCoverageBuild() {
+#ifdef CVC4_COVERAGE
+    return true;
+#else /* CVC4_COVERAGE */
+    return false;
+#endif /* CVC4_COVERAGE */
+  }
+
+  static bool isProfilingBuild() {
+#ifdef CVC4_PROFILING
+    return true;
+#else /* CVC4_PROFILING */
+    return false;
+#endif /* CVC4_PROFILING */
+  }
+
+  static std::string getPackageName() {
+    return PACKAGE;
+  }
+
+  static std::string getVersionString() {
+    return VERSION;
+  }
+
+  static unsigned getVersionMajor() {
+    return 0;
+  }
+
+  static unsigned getVersionMinor() {
+    return 0;
+  }
+
+  static unsigned getVersionRelease() {
+    return 0;
+  }
+
+  static std::string about() {
+    return std::string("\
+This is a pre-release of CVC4.\n\
+Copyright (C) 2009, 2010\n\
+  The ACSys Group\n\
+  Courant Institute of Mathematical Sciences,\n\
+  New York University\n\
+  New York, NY  10012  USA\n");
+  }
+
+};
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONFIGURATION_H */
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 278158ad1..e7ac3de90 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -27,12 +27,17 @@ namespace CVC4 {
 null_streambuf null_sb;
 ostream null_os(&null_sb);
 
+NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
+NullC nullCvc4Stream CVC4_PUBLIC;
+
+#ifndef CVC4_MUZZLE
+
 DebugC   DebugOut(&cout);
-WarningC Warning (&cerr);
-MessageC Message (&cout);
-NoticeC  Notice  (&cout);
-ChatC    Chat    (&cout);
-TraceC   Trace   (&cout);
+WarningC WarningOut(&cerr);
+MessageC MessageOut(&cout);
+NoticeC  NoticeOut(&cout);
+ChatC    ChatOut(&cout);
+TraceC   TraceOut(&cout);
 
 void DebugC::printf(const char* tag, const char* fmt, ...) {
   if(d_tags.find(string(tag)) != d_tags.end()) {
@@ -122,4 +127,6 @@ void TraceC::printf(string tag, const char* fmt, ...) {
   }
 }
 
+#endif /* CVC4_MUZZLE */
+
 }/* CVC4 namespace */
diff --git a/src/util/output.h b/src/util/output.h
index 94841a1f5..ad42416d8 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -49,6 +49,8 @@ extern null_streambuf null_sb;
 /** A null output stream singleton */
 extern std::ostream null_os CVC4_PUBLIC;
 
+#ifndef CVC4_MUZZLE
+
 /** The debug output class */
 class CVC4_PUBLIC DebugC {
   std::set<std::string> d_tags;
@@ -115,10 +117,10 @@ public:
 /** The debug output singleton */
 extern DebugC DebugOut CVC4_PUBLIC;
 #ifdef CVC4_DEBUG
-  #define Debug DebugOut
-#else
-  #define Debug if(0) DebugOut
-#endif
+#  define Debug DebugOut
+#else /* CVC4_DEBUG */
+#  define Debug if(0) debugNullCvc4Stream
+#endif /* CVC4_DEBUG */
 
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
@@ -138,7 +140,8 @@ public:
 };/* class Warning */
 
 /** The warning output singleton */
-extern WarningC Warning CVC4_PUBLIC;
+extern WarningC WarningOut CVC4_PUBLIC;
+#define Warning WarningOut
 
 /** The message output class */
 class CVC4_PUBLIC MessageC {
@@ -158,7 +161,8 @@ public:
 };/* class Message */
 
 /** The message output singleton */
-extern MessageC Message CVC4_PUBLIC;
+extern MessageC MessageOut CVC4_PUBLIC;
+#define Message MessageOut
 
 /** The notice output class */
 class CVC4_PUBLIC NoticeC {
@@ -178,7 +182,8 @@ public:
 };/* class Notice */
 
 /** The notice output singleton */
-extern NoticeC Notice CVC4_PUBLIC;
+extern NoticeC NoticeOut CVC4_PUBLIC;
+#define Notice NoticeOut
 
 /** The chat output class */
 class CVC4_PUBLIC ChatC {
@@ -198,7 +203,8 @@ public:
 };/* class Chat */
 
 /** The chat output singleton */
-extern ChatC Chat CVC4_PUBLIC;
+extern ChatC ChatOut CVC4_PUBLIC;
+#define Chat ChatOut
 
 /** The trace output class */
 class CVC4_PUBLIC TraceC {
@@ -241,7 +247,75 @@ public:
 };/* class Trace */
 
 /** The trace output singleton */
-extern TraceC Trace CVC4_PUBLIC;
+extern TraceC TraceOut CVC4_PUBLIC;
+#ifdef CVC4_TRACING
+#  define Trace TraceOut
+#else /* CVC4_TRACING */
+#  define Trace if(0) debugNullCvc4Stream
+#endif /* CVC4_TRACING */
+
+#else /* ! CVC4_MUZZLE */
+
+#  define Debug if(0) debugNullCvc4Stream
+#  define Warning if(0) nullCvc4Stream
+#  define Message if(0) nullCvc4Stream
+#  define Notice if(0) nullCvc4Stream
+#  define Chat if(0) nullCvc4Stream
+#  define Trace if(0) debugNullCvc4Stream
+
+#endif /* ! CVC4_MUZZLE */
+
+/**
+ * Same shape as DebugC/TraceC, but does nothing; designed for
+ * compilation of muzzled builds.  None of these should ever be called
+ * in muzzled builds, but we offer this to the compiler so it doesn't complain.
+ */
+class CVC4_PUBLIC NullDebugC {
+public:
+  NullDebugC() {}
+  NullDebugC(std::ostream* os) {}
+
+  void operator()(const char* tag, const char*) {}
+  void operator()(const char* tag, std::string) {}
+  void operator()(std::string tag, const char*) {}
+  void operator()(std::string tag, std::string) {}
+
+  void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
+  void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 3, 4))) {}
+
+  std::ostream& operator()(const char* tag) { return null_os; }
+  std::ostream& operator()(std::string tag) { return null_os; }
+
+  void on (const char* tag) {}
+  void on (std::string tag) {}
+  void off(const char* tag) {}
+  void off(std::string tag) {}
+
+  void setStream(std::ostream& os) {}
+};/* class NullDebugC */
+
+/**
+ * Same shape as WarningC/etc., but does nothing; designed for
+ * compilation of muzzled builds.  None of these should ever be called
+ * in muzzled builds, but we offer this to the compiler so it doesn't
+ * complain. */
+class CVC4_PUBLIC NullC {
+public:
+  NullC() {}
+  NullC(std::ostream* os) {}
+
+  void operator()(const char*) {}
+  void operator()(std::string) {}
+
+  void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) {}
+
+  std::ostream& operator()() { return null_os; }
+
+  void setStream(std::ostream& os) {}
+};/* class NullC */
+
+extern NullDebugC debugNullCvc4Stream CVC4_PUBLIC;
+extern NullC nullCvc4Stream CVC4_PUBLIC;
 
 }/* CVC4 namespace */