--disable-tracing at configure time now disables Trace() and Debug() gestures both.

5 files changed, 36 insertions, 29 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 87fa2c890..dddcbb38c 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -88,6 +88,7 @@ BUILT_SOURCES = \
 	integer.h \
 	tls.h
 if CVC4_DEBUG
+if CVC4_TRACING
 # listing Debug_tags too ensures that make doesn't auto-remove it
 # after building (if it does, we don't get the "cached" effect with
 # the .tmp files below, and we have to re-compile and re-link each
@@ -96,6 +97,7 @@ BUILT_SOURCES += \
 	Debug_tags.h \
 	Debug_tags
 endif
+endif
 if CVC4_TRACING
 # listing Trace_tags too ensures that make doesn't auto-remove it
 # after building (if it does, we don't get the "cached" effect with
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 6f01d6cf4..d0fc3cd1d 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -27,9 +27,9 @@
 #include "util/configuration_private.h"
 #include "cvc4autoconfig.h"
 
-#ifdef CVC4_DEBUG
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
 #  include "util/Debug_tags.h"
-#endif /* CVC4_DEBUG */
+#endif /* CVC4_DEBUG && CVC4_TRACING */
 
 #ifdef CVC4_TRACING
 #  include "util/Trace_tags.h"
@@ -132,21 +132,21 @@ bool Configuration::isBuiltWithTlsSupport() {
 }
 
 unsigned Configuration::getNumDebugTags() {
-#if CVC4_DEBUG
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
   /* -1 because a NULL pointer is inserted as the last value */
-  return sizeof(Debug_tags) / sizeof(Debug_tags[0]) - 1;
-#else /* CVC4_DEBUG */
+  return (sizeof(Debug_tags) / sizeof(Debug_tags[0])) - 1;
+#else /* CVC4_DEBUG && CVC4_TRACING */
   return 0;
-#endif /* CVC4_DEBUG */
+#endif /* CVC4_DEBUG && CVC4_TRACING */
 }
 
 char const* const* Configuration::getDebugTags() {
-#if CVC4_DEBUG
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
   return Debug_tags;
-#else /* CVC4_DEBUG */
+#else /* CVC4_DEBUG && CVC4_TRACING */
   static char const* no_tags[] = { NULL };
   return no_tags;
-#endif /* CVC4_DEBUG */
+#endif /* CVC4_DEBUG && CVC4_TRACING */
 }
 
 int strcmpptr(const char **s1, const char **s2){
@@ -154,7 +154,7 @@ int strcmpptr(const char **s1, const char **s2){
 }
 
 bool Configuration::isDebugTag(char const *tag){
-#if CVC4_DEBUG
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
   unsigned ntags = getNumDebugTags();
   char const* const* tags = getDebugTags();
   for (unsigned i = 0; i < ntags; ++ i) {
@@ -162,7 +162,7 @@ bool Configuration::isDebugTag(char const *tag){
       return true;
     }
   }
-#endif /* CVC4_DEBUG */
+#endif /* CVC4_DEBUG && CVC4_TRACING */
   return false;
 }
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index d72734f40..140850a28 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -559,18 +559,21 @@ throw(OptionException) {
           throw OptionException(string("trace tag ") + optarg +
                                 string(" not available"));
       } else {
-        throw OptionException("trace tags not available in non-tracing build");
+        throw OptionException("trace tags not available in non-tracing builds");
       }
       Trace.on(optarg);
       break;
 
     case 'd':
-      if(Configuration::isDebugBuild()) {
-        if(!Configuration::isDebugTag(optarg))
+      if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
+        if(!Configuration::isDebugTag(optarg)) {
           throw OptionException(string("debug tag ") + optarg +
                                 string(" not available"));
+        }
+      } else if(! Configuration::isDebugBuild()) {
+        throw OptionException("debug tags not available in non-debug builds");
       } else {
-        throw OptionException("debug tags not available in non-debug build");
+        throw OptionException("debug tags not available in non-tracing builds");
       }
       Debug.on(optarg);
       Trace.on(optarg);
@@ -993,7 +996,7 @@ throw(OptionException) {
       break;
 
     case SHOW_DEBUG_TAGS:
-      if(Configuration::isDebugBuild()) {
+      if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
         printf("available tags:");
         unsigned ntags = Configuration::getNumDebugTags();
         char const* const* tags = Configuration::getDebugTags();
@@ -1001,8 +1004,10 @@ throw(OptionException) {
           printf(" %s", tags[i]);
         }
         printf("\n");
+      } else if(! Configuration::isDebugBuild()) {
+        throw OptionException("debug tags not available in non-debug builds");
       } else {
-        throw OptionException("debug tags not available in non-debug build");
+        throw OptionException("debug tags not available in non-tracing builds");
       }
       exit(0);
       break;
@@ -1017,7 +1022,7 @@ throw(OptionException) {
         }
         printf("\n");
       } else {
-        throw OptionException("trace tags not available in non-tracing build");
+        throw OptionException("trace tags not available in non-tracing builds");
       }
       exit(0);
       break;
diff --git a/src/util/output.cpp b/src/util/output.cpp
index 48a7d51fd..5acee360f 100644
--- a/src/util/output.cpp
+++ b/src/util/output.cpp
@@ -45,7 +45,7 @@ DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout);
 
 #ifndef CVC4_MUZZLE
 
-#  ifdef CVC4_DEBUG
+#  if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
 
 int DebugC::printf(const char* tag, const char* fmt, ...) {
   if(d_tags.find(string(tag)) == d_tags.end()) {
@@ -77,7 +77,7 @@ int DebugC::printf(std::string tag, const char* fmt, ...) {
   return retval;
 }
 
-#  endif /* CVC4_DEBUG */
+#  endif /* CVC4_DEBUG && CVC4_TRACING */
 
 int WarningC::printf(const char* fmt, ...) {
   // chop off output after 1024 bytes
diff --git a/src/util/output.h b/src/util/output.h
index 308cfcac2..602fb69cb 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -430,13 +430,13 @@ inline int DumpOutC::printf(std::string tag, const char* fmt, ...) { return 0; }
 
 #else /* CVC4_MUZZLE */
 
-#  ifdef CVC4_DEBUG
+#  if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
 #    define Debug ::CVC4::DebugChannel
-#  else /* CVC4_DEBUG */
+#  else /* CVC4_DEBUG && CVC4_TRACING */
 #    define Debug ::CVC4::__cvc4_true() ? ::CVC4::nullCvc4Stream : ::CVC4::DebugChannel
 inline int DebugC::printf(const char* tag, const char* fmt, ...) { return 0; }
 inline int DebugC::printf(std::string tag, const char* fmt, ...) { return 0; }
-#  endif /* CVC4_DEBUG */
+#  endif /* CVC4_DEBUG && CVC4_TRACING */
 #  define Warning (! ::CVC4::WarningChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define WarningOnce (! ::CVC4::WarningChannel.isOn() || ! ::CVC4::WarningChannel.warnOnce(__FILE__,__LINE__)) ? ::CVC4::nullCvc4Stream : ::CVC4::WarningChannel
 #  define Message (! ::CVC4::MessageChannel.isOn()) ? ::CVC4::nullCvc4Stream : ::CVC4::MessageChannel
@@ -472,7 +472,7 @@ public:
   inline operator bool() { return true; }
 };/* __cvc4_true */
 
-#ifdef CVC4_DEBUG
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
 
 class CVC4_PUBLIC ScopedDebug {
   std::string d_tag;
@@ -509,7 +509,7 @@ public:
   }
 };/* class ScopedDebug */
 
-#else /* CVC4_DEBUG */
+#else /* CVC4_DEBUG && CVC4_TRACING */
 
 class CVC4_PUBLIC ScopedDebug {
 public:
@@ -517,7 +517,7 @@ public:
   ScopedDebug(const char* tag, bool newSetting = true) {}
 };/* class ScopedDebug */
 
-#endif /* CVC4_DEBUG */
+#endif /* CVC4_DEBUG && CVC4_TRACING */
 
 #ifdef CVC4_TRACING
 
@@ -579,13 +579,13 @@ public:
   inline ~IndentedScope();
 };/* class IndentedScope */
 
-#ifdef CVC4_DEBUG
+#if defined(CVC4_DEBUG) && defined(CVC4_TRACING)
 inline IndentedScope::IndentedScope(CVC4ostream out) : d_out(out) { d_out << push; }
 inline IndentedScope::~IndentedScope() { d_out << pop; }
-#else /* CVC4_DEBUG */
+#else /* CVC4_DEBUG && CVC4_TRACING */
 inline IndentedScope::IndentedScope(CVC4ostream out) {}
 inline IndentedScope::~IndentedScope() {}
-#endif /* CVC4_DEBUG */
+#endif /* CVC4_DEBUG && CVC4_TRACING */
 
 }/* CVC4 namespace */