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)

10 files changed, 284 insertions, 66 deletions

diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 0170296be..032735ff0 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -171,12 +171,14 @@ Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const {
 }
 
 void Expr::printAst(std::ostream & o, int indent) const{
-  getNode().printAst(o,indent);
+  getNode().printAst(o, indent);
 }
 
 void Expr::debugPrint(){
+#ifndef CVC4_MUZZLE
   printAst(Warning());
   Warning().flush();
+#endif /* ! CVC4_MUZZLE */
 }
 
 
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index f3115b17e..644570b24 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -133,7 +133,7 @@ static void indent(ostream & o, int indent){
     o << ' ';
 }
 
-void Node::printAst(ostream & o, int ind) const{
+void Node::printAst(ostream & o, int ind) const {
   indent(o, ind);
   o << '(';
   o << getKind();
@@ -143,17 +143,19 @@ void Node::printAst(ostream & o, int ind) const{
   }else if(getNumChildren() >= 1){
     for(Node::iterator child = begin(); child != end(); ++child){
       o << endl;
-      (*child).printAst(o, ind+1);
+      (*child).printAst(o, ind + 1);
     }
     o << endl;
     indent(o, ind);
   }
   o << ')';
 }
-  
-void Node::debugPrint(){
+
+void Node::debugPrint() {
+#ifndef CVC4_MUZZLE
   printAst(Warning(), 0);
   Warning().flush();
+#endif /* ! CVC4_MUZZLE */
 }
 
 }/* CVC4 namespace */
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 7c4f2d52d..04d717294 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -9,8 +9,7 @@ cvc4_SOURCES = \
 	getopt.cpp \
 	util.cpp \
 	main.h \
-	usage.h \
-	about.h
+	usage.h
 
 cvc4_LDADD = \
 	../parser/libcvc4parser.la \
diff --git a/src/main/about.h b/src/main/about.h
deleted file mode 100644
index 9dacdc8cc..000000000
--- a/src/main/about.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*********************                                                        */
-/** about.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** 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.
- **
- ** The "about" string for the CVC4 driver binary.
- **/
-
-#ifndef __CVC4__MAIN__ABOUT_H
-#define __CVC4__MAIN__ABOUT_H
-
-namespace CVC4 {
-namespace main {
-
-const char about[] = "\
-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::main namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__MAIN__ABOUT_H */
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 8ace8e778..190f7bbf3 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -27,7 +27,7 @@
 #include "main.h"
 #include "util/exception.h"
 #include "usage.h"
-#include "about.h"
+#include "util/configuration.h"
 #include "util/output.h"
 #include "util/options.h"
 #include "parser/parser.h"
@@ -52,21 +52,47 @@ CNF conversions currently supported as arguments to the --cnf option:\n\
   var     variable-introduction method (new vars, no exp. blow up in # clauses)\n\
 ";
 
-// FIXME add a comment here describing the purpose of this
+/**
+ * For the main getopt() routine, we need ways to switch on long
+ * options without clashing with short option characters.  This is an
+ * enum of those long options.  For long options (e.g. "--verbose")
+ * with a short option equivalent ("-v"), we use the single-letter
+ * short option; therefore, this enumeration starts at 256 to avoid
+ * any collision.
+ */
 enum OptionValue {
   CNF = 256, /* no clash with char options */
   SMTCOMP,
   STATS,
   SEGV_NOSPIN,
   PARSE_ONLY,
-  NO_CHECKING
+  NO_CHECKING,
+  SHOW_CONFIG
 };/* enum OptionValue */
 
-// FIXME add a comment here describing the option array
+/**
+ * This is a table of long options.  By policy, each short option
+ * should have an equivalent long option (but the reverse isn't the
+ * case), so this table should thus contain all command-line options.
+ *
+ * Each option in this array has four elements:
+ *
+ * 1. the long option string
+ * 2. argument behavior for the option:
+ *    no_argument - no argument permitted
+ *    required_argument - an argument is expected
+ *    optional_argument - an argument is permitted but not required
+ * 3. this is a pointer to an int which is set to the 4th entry of the
+ *    array if the option is present; or NULL, in which case
+ *    getopt_long() returns the 4th entry
+ * 4. the return value for getopt_long() when this long option (or the
+ *    value to set the 3rd entry to; see #3)
+ */
 static struct option cmdlineOptions[] = {
   // name, has_arg, *flag, val
   { "help"       , no_argument      , NULL, 'h'         },
   { "version"    , no_argument      , NULL, 'V'         },
+  { "about"      , no_argument      , NULL, 'V'         },
   { "verbose"    , no_argument      , NULL, 'v'         },
   { "quiet"      , no_argument      , NULL, 'q'         },
   { "lang"       , required_argument, NULL, 'L'         },
@@ -76,7 +102,8 @@ static struct option cmdlineOptions[] = {
   { "stats"      , no_argument      , NULL, STATS       },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
   { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
-  { "no-checking", no_argument      , NULL, NO_CHECKING }
+  { "no-checking", no_argument      , NULL, NO_CHECKING },
+  { "show-config", no_argument      , NULL, SHOW_CONFIG }
 };/* if you add things to the above, please remember to update usage.h! */
 
 /** Full argv[0] */
@@ -98,7 +125,17 @@ throw(OptionException) {
   }
   opts->binary_name = string(progName);
 
-  // FIXME add a comment here describing the option string
+  // The strange string in this call is the short option string.  The
+  // initial '+' means that option processing stops as soon as a
+  // non-option argument is encountered.  The initial ':' indicates
+  // that getopt_long() should return ':' instead of '?' for a missing
+  // option argument.  Then, each letter is a valid short option for
+  // getopt_long(), and if it's encountered, getopt_long() returns
+  // that character.  A ':' after an option character means an
+  // argument is required; two colons indicates an argument is
+  // optional; no colons indicate an argument is not permitted.
+  // cmdlineOptions specifies all the long-options and the return
+  // value for getopt_long() should they be encountered.
   while((c = getopt_long(argc, argv,
                          "+:hVvqL:d:",
                          cmdlineOptions, NULL)) != -1) {
@@ -109,7 +146,7 @@ throw(OptionException) {
       exit(1);
 
     case 'V':
-      fputs(about, stdout);
+      fputs(Configuration::about().c_str(), stdout);
       exit(0);
 
     case 'v':
@@ -182,14 +219,27 @@ throw(OptionException) {
       opts->semanticChecks = false;
       break;
 
+    case SHOW_CONFIG:
+      fputs(Configuration::about().c_str(), stdout);
+      printf("\n");
+      printf("version   : %s\n", Configuration::getVersionString().c_str());
+      printf("\n");
+      printf("debug code: %s\n", Configuration::isDebugBuild() ? "yes" : "no");
+      printf("tracing   : %s\n", Configuration::isTracingBuild() ? "yes" : "no");
+      printf("muzzled   : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
+      printf("assertions: %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
+      printf("coverage  : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
+      printf("profiling : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
+      exit(0);
+
     case '?':
-      throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'");
+      throw OptionException(string("can't understand option `") + argv[optind - 1] + "'");
 
     case ':':
-      throw OptionException(string("option missing its required argument"));// + argv[optind - 1] + "' missing its required argument");
+      throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
 
     default:
-      throw OptionException(string("can't understand option"));//: `") + argv[optind - 1] + "'");
+      throw OptionException(string("can't understand option:") + argv[optind - 1] + "'");
     }
 
   }
diff --git a/src/main/usage.h b/src/main/usage.h
index 79b906d88..9a8175e2a 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -37,6 +37,7 @@ CVC4 options:\n\
    --stats         give statistics on exit\n\
    --segv-nospin   (debug builds only) don't spin on segfault waiting for gdb\n\
    --parse-only    exit after parsing input\n\
+   --show-config   show CVC4 static configuration\n\
 ";
 
 }/* CVC4::main namespace */
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 */