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)

1 files changed, 116 insertions, 0 deletions

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