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)

5 files changed, 247 insertions, 1 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 84465127b..c145cf752 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -4,7 +4,10 @@ UNIT_TESTS = \
 	expr/node_black \
 	parser/parser_black \
 	context/context_black \
-	context/context_mm_black
+	context/context_mm_black \
+	util/assert_white \
+	util/configuration_white \
+	util/output_white
 
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 0693b48db..102549c42 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -160,9 +160,11 @@ public:
   void testOperatorSquare() {  
     /*Node operator[](int i) const */
 
+#ifdef CVC4_ASSERTIONS
     //Basic bounds check on a node w/out children
     TS_ASSERT_THROWS(Node::null()[-1], AssertionException);
     TS_ASSERT_THROWS(Node::null()[0], AssertionException);
+#endif /* CVC4_ASSERTIONS */
 
     //Basic access check
     Node tb = d_nm->mkNode(TRUE);
@@ -177,9 +179,11 @@ public:
     TS_ASSERT(tb == ite[1]);
     TS_ASSERT(eb == ite[2]);
 
+#ifdef CVC4_ASSERTIONS
     //Bounds check on a node with children
     TS_ASSERT_THROWS(ite == ite[-1],AssertionException);
     TS_ASSERT_THROWS(ite == ite[4],AssertionException);    
+#endif /* CVC4_ASSERTIONS */
   }
 
   /*tests:   Node& operator=(const Node&); */
diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h
new file mode 100644
index 000000000..9425daa44
--- /dev/null
+++ b/test/unit/util/assert_white.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/** assert_white.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.
+ **
+ ** White box testing of CVC4::Configuration.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "util/Assert.h"
+
+using namespace CVC4;
+using namespace std;
+
+class AssertWhite : public CxxTest::TestSuite {
+public:
+
+  void testAssert() {
+#ifdef CVC4_ASSERTIONS
+    TS_ASSERT_THROWS( Assert(false), AssertionException );
+    TS_ASSERT_THROWS( AssertArgument(false, "x"), IllegalArgumentException );
+#else /* CVC4_ASSERTIONS */
+    TS_ASSERT_THROWS_NOTHING( Assert(false) );
+    TS_ASSERT_THROWS_NOTHING( AssertArgument(false, "x") );
+#endif /* CVC4_ASSERTIONS */
+
+    TS_ASSERT_THROWS_NOTHING( Assert(true) );
+    TS_ASSERT_THROWS( AlwaysAssert(false), AssertionException );
+    TS_ASSERT_THROWS( Unreachable(), UnreachableCodeException );
+    TS_ASSERT_THROWS( Unhandled(), UnhandledCaseException );
+    TS_ASSERT_THROWS( Unimplemented(), UnimplementedOperationException );
+    TS_ASSERT_THROWS( IllegalArgument("x"), IllegalArgumentException );
+    TS_ASSERT_THROWS( CheckArgument(false, "x"), IllegalArgumentException );
+    TS_ASSERT_THROWS( AlwaysAssertArgument(false, "x"), IllegalArgumentException );
+    TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
+    TS_ASSERT_THROWS_NOTHING( AssertArgument(true, "x") );
+  }
+
+};
diff --git a/test/unit/util/configuration_white.h b/test/unit/util/configuration_white.h
new file mode 100644
index 000000000..04cacc155
--- /dev/null
+++ b/test/unit/util/configuration_white.h
@@ -0,0 +1,95 @@
+/*********************                                                        */
+/** configuration_white.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.
+ **
+ ** White box testing of CVC4::Configuration.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "util/configuration.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ConfigurationWhite : public CxxTest::TestSuite {
+
+public:
+
+  void testStaticFlags() {
+    const bool debug =
+#ifdef CVC4_DEBUG
+      true;
+#else /* CVC4_DEBUG */
+      false;
+#endif /* CVC4_DEBUG */
+
+    const bool tracing =
+#ifdef CVC4_TRACING
+      true;
+#else /* CVC4_TRACING */
+      false;
+#endif /* CVC4_TRACING */
+
+    const bool muzzled =
+#ifdef CVC4_MUZZLE
+      true;
+#else /* CVC4_MUZZLE */
+      false;
+#endif /* CVC4_MUZZLE */
+
+    const bool assertions =
+#ifdef CVC4_ASSERTIONS
+      true;
+#else /* CVC4_ASSERTIONS */
+      false;
+#endif /* CVC4_ASSERTIONS */
+
+    const bool coverage =
+#ifdef CVC4_COVERAGE
+      true;
+#else /* CVC4_COVERAGE */
+      false;
+#endif /* CVC4_COVERAGE */
+
+    const bool profiling =
+#ifdef CVC4_PROFILING
+      true;
+#else /* CVC4_PROFILING */
+      false;
+#endif /* CVC4_PROFILING */
+
+    TS_ASSERT( Configuration::isDebugBuild() == debug );
+    TS_ASSERT( Configuration::isTracingBuild() == tracing );
+    TS_ASSERT( Configuration::isMuzzledBuild() == muzzled );
+    TS_ASSERT( Configuration::isAssertionBuild() == assertions );
+    TS_ASSERT( Configuration::isCoverageBuild() == coverage );
+    TS_ASSERT( Configuration::isProfilingBuild() == profiling );
+  }
+
+  void testPackageName() {
+    TS_ASSERT( Configuration::getPackageName() == "cvc4" );
+  }
+
+  void testVersions() {
+    // just test that the functions exist
+    Configuration::getVersionString();
+    Configuration::getVersionMajor();
+    Configuration::getVersionMinor();
+    Configuration::getVersionRelease();
+  }
+
+  void testAbout() {
+    // just test that the function exists
+    Configuration::about();
+  }
+
+};
diff --git a/test/unit/util/output_white.h b/test/unit/util/output_white.h
new file mode 100644
index 000000000..7eda3db9d
--- /dev/null
+++ b/test/unit/util/output_white.h
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/** output_white.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.
+ **
+ ** White box testing of CVC4::Configuration.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <sstream>
+
+#include "util/output.h"
+
+using namespace CVC4;
+using namespace std;
+
+class OutputWhite : public CxxTest::TestSuite {
+
+  stringstream d_debugStream;
+  stringstream d_traceStream;
+  stringstream d_noticeStream;
+  stringstream d_chatStream;
+  stringstream d_messageStream;
+  stringstream d_warningStream;
+
+public:
+
+  void setUp() {
+    Debug.setStream(d_debugStream);
+    Trace.setStream(d_traceStream);
+    Notice.setStream(d_noticeStream);
+    Chat.setStream(d_chatStream);
+    Message.setStream(d_messageStream);
+    Warning.setStream(d_warningStream);
+  }
+
+  void testOutput() {
+    Debug.on("foo");
+    Debug("foo") << "testing1";
+    Debug.off("foo");
+    Debug("foo") << "testing2";
+    Debug.on("foo");
+    Debug("foo") << "testing3";
+
+    Message() << "a message";
+    Warning() << "bad warning!";
+    Chat() << "chatty";
+    Notice() << "note";
+
+    Trace.on("foo");
+    Trace("foo") << "tracing1";
+    Trace.off("foo");
+    Trace("foo") << "tracing2";
+    Trace.on("foo");
+    Trace("foo") << "tracing3";
+
+#ifdef CVC4_MUZZLE
+
+    TS_ASSERT( d_debugStream.str() == "" );
+    TS_ASSERT( d_messageStream.str() == "" );
+    TS_ASSERT( d_warningStream.str() == "" );
+    TS_ASSERT( d_chatStream.str() == "" );
+    TS_ASSERT( d_noticeStream.str() == "" );
+    TS_ASSERT( d_traceStream.str() == "" );
+
+#else /* CVC4_MUZZLE */
+
+#  ifdef CVC4_DEBUG
+    TS_ASSERT( d_debugStream.str() == "testing1testing3" );
+#  else /* CVC4_DEBUG */
+    TS_ASSERT( d_debugStream.str() == "" );
+#  endif /* CVC4_DEBUG */
+
+    TS_ASSERT( d_messageStream.str() == "a message" );
+    TS_ASSERT( d_warningStream.str() == "bad warning!" );
+    TS_ASSERT( d_chatStream.str() == "chatty" );
+    TS_ASSERT( d_noticeStream.str() == "note" );
+
+#  ifdef CVC4_TRACING
+    TS_ASSERT( d_traceStream.str() == "tracing1tracing3" );
+#  else /* CVC4_TRACING */
+    TS_ASSERT( d_traceStream.str() == "" );
+#  endif /* CVC4_TRACING */
+
+#endif /* CVC4_MUZZLE */
+  }
+
+};