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, 62 insertions, 46 deletions

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 */