--show-debug-tags and --show-trace-tags now supported by Configuration API; also...

diff --git a/src/Makefile.am b/src/Makefile.am
index 9ffe249ee6455848d1fc5dba5c623988fd7167f8..e6c00c9435e1614b8dff175a3a164e29cb71467f 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -78,9 +78,11 @@ subversion_versioninfo.cpp: svninfo
          echo "const unsigned ::CVC4::Configuration::SUBVERSION_REVISION = $$rev;"; \
          echo "const bool ::CVC4::Configuration::SUBVERSION_HAS_MODIFICATIONS = $$mods;"; \
        ) >"$@"
+# This .tmp business is to keep from having to re-compile options.cpp
+# (and then re-link the libraries) if nothing has changed.
 svninfo: svninfo.tmp
        $(AM_V_GEN)diff -q svninfo.tmp svninfo &>/dev/null || mv svninfo.tmp svninfo || true
-# .PHONY ensures it's always rebuilt
+# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
 .PHONY: svninfo.tmp
 svninfo.tmp:
        $(AM_V_GEN)(cd "$(top_srcdir)" && svn info && echo "Modifications: `test -z \"\`svn status -q\`\" && echo false || echo true`") >"$@" 2>/dev/null || true

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index bf975d5136fcb2c32c2bb34731a9d6642cdaf40c..7f5fb459ec5477e8d340dbdd3c5008758ff75ae3 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -75,14 +75,31 @@ libutilcudd_la_SOURCES = \
 BUILT_SOURCES = \
        rational.h \
        integer.h \
-       tls.h \
-       debug_tags.h
+       tls.h
+if CVC4_DEBUG
+# 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
+# time, even when there are no changes).
+BUILT_SOURCES += \
+       Debug_tags.h \
+       Debug_tags
+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
+# the .tmp files below, and we have to re-compile and re-link each
+# time, even when there are no changes).
+BUILT_SOURCES += \
+       Trace_tags.h \
+       Trace_tags
+endif
 
-debug_tags.h: debug_tags
+%_tags.h: %_tags
        $(AM_V_GEN)( \
-       echo 'const char* debug_tags[] = {'; \
+       echo 'static char const *const $^[] = {'; \
        first=1; \
-       for tag in `cat debug_tags`; \
+       for tag in `cat $^`; \
        do \
            if [ $$first -eq 1 ]; then first=0; else echo ','; fi; \
                echo -n "\"$$tag\""; \
@@ -90,14 +107,19 @@ debug_tags.h: debug_tags
        echo; \
        echo '};' \
        ) >"$@"
-       
-debug_tags:
-       $(AM_V_GEN)\
-       grep 'Debug(\".*\")' `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
-       sed s/'.*Debug(\"'//g | sed s/'\".*'//g | sort | uniq >"$@"
-
-.PHONY: debug_tags
 
+# This .tmp business is to keep from having to re-compile options.cpp
+# (and then re-link the libraries) if nothing has changed.
+%_tags: %_tags.tmp
+       $(AM_V_GEN)\
+       diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true
+# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
+.PHONY: Debug_tags.tmp Trace_tags.tmp
+Debug_tags.tmp Trace_tags.tmp:
+       $(AM_V_GEN)\
+       grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \
+               `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
+       sed 's/.*\<$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/g' | sort | uniq >"$@"
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index c13b63e3fe3cf359da86bcf5a13f7a4fad6c043b..062aca4780b3cd013cd24b7dccc11e0f8e443061 100644 (file)
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -25,6 +25,14 @@
 #include "util/configuration_private.h"
 #include "cvc4autoconfig.h"
 
+#ifdef CVC4_DEBUG
+#  include "util/Debug_tags.h"
+#endif /* CVC4_DEBUG */
+
+#ifdef CVC4_TRACING
+#  include "util/Trace_tags.h"
+#endif /* CVC4_TRACING */
+
 using namespace std;
 
 namespace CVC4 {
@@ -117,6 +125,38 @@ bool Configuration::isBuiltWithTlsSupport() {
   return USING_TLS;
 }
 
+unsigned Configuration::getNumDebugTags() {
+#if CVC4_DEBUG
+  return sizeof(Debug_tags) / sizeof(Debug_tags[0]);
+#else /* CVC4_DEBUG */
+  return 0;
+#endif /* CVC4_DEBUG */
+}
+
+char const* const* Configuration::getDebugTags() {
+#if CVC4_DEBUG
+  return Debug_tags;
+#else /* CVC4_DEBUG */
+  return NULL;
+#endif /* CVC4_DEBUG */
+}
+
+unsigned Configuration::getNumTraceTags() {
+#if CVC4_TRACING
+  return sizeof(Trace_tags) / sizeof(Trace_tags[0]);
+#else /* CVC4_TRACING */
+  return 0;
+#endif /* CVC4_TRACING */
+}
+
+char const* const* Configuration::getTraceTags() {
+#if CVC4_TRACING
+  return Trace_tags;
+#else /* CVC4_TRACING */
+  return NULL;
+#endif /* CVC4_TRACING */
+}
+
 bool Configuration::isSubversionBuild() {
   return IS_SUBVERSION_BUILD;
 }

diff --git a/src/util/configuration.h b/src/util/configuration.h
index cb207298c4a50637aa802ea7a60ac34a47eaabf4..b4caf842c57a1b76d0730b9eca8cf346571f1a0b 100644 (file)
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -87,6 +87,12 @@ public:
 
   static bool isBuiltWithTlsSupport();
 
+  static unsigned getNumDebugTags();
+  static char const* const* getDebugTags();
+
+  static unsigned getNumTraceTags();
+  static char const* const* getTraceTags();
+
   static bool isSubversionBuild();
   static const char* getSubversionBranchName();
   static unsigned getSubversionRevision();

diff --git a/src/util/options.cpp b/src/util/options.cpp
index a6042c3a9f314b4b310d64b65676f1ac2978ce96..009bc73b895b3b7f9e445d82cc73324c3f0f055f 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -32,7 +32,6 @@
 #include "util/language.h"
 #include "util/options.h"
 #include "util/output.h"
-#include "util/debug_tags.h"
 
 #include "cvc4autoconfig.h"
 
@@ -117,7 +116,8 @@ static const string optionsDescription = "\
    --quiet | -q           decrease verbosity (may be repeated)\n\
    --trace | -t           trace something (e.g. -t pushpop), can repeat\n\
    --debug | -d           debug something (e.g. -d arith), can repeat\n\
-   --show-debug-tags      show all avalable tags for debug tracing\n\
+   --show-debug-tags      show all avalable tags for debugging\n\
+   --show-trace-tags      show all avalable tags for tracing\n\
    --stats                give statistics on exit\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
    --print-expr-types     print types with variables when printing exprs\n\
@@ -270,6 +270,7 @@ enum OptionValue {
   NO_THEORY_REGISTRATION,
   USE_MMAP,
   SHOW_DEBUG_TAGS,
+  SHOW_TRACE_TAGS,
   SHOW_CONFIG,
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
@@ -331,7 +332,8 @@ static struct option cmdlineOptions[] = {
   { "stats"      , no_argument      , NULL, STATS       },
   { "no-checking", no_argument      , NULL, NO_CHECKING },
   { "no-theory-registration", no_argument, NULL, NO_THEORY_REGISTRATION },
-  { "show-debug-tags", no_argument, NULL, SHOW_DEBUG_TAGS },
+  { "show-debug-tags", no_argument  , NULL, SHOW_DEBUG_TAGS },
+  { "show-trace-tags", no_argument  , NULL, SHOW_TRACE_TAGS },
   { "show-config", no_argument      , NULL, SHOW_CONFIG },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
   { "help"       , no_argument      , NULL, 'h'         },
@@ -768,15 +770,31 @@ throw(OptionException) {
       break;
 
     case SHOW_DEBUG_TAGS:
-      printf("available tags:");
-      if (Configuration::isTracingBuild()) {
-        unsigned nTags = sizeof(debug_tags) / sizeof(debug_tags[0]);
-        for (unsigned i = 0; i < nTags; ++ i) {
-          printf(" %s", debug_tags[i]);
+      if(Configuration::isDebugBuild()) {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumDebugTags();
+        char const* const* tags = Configuration::getDebugTags();
+        for(unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
         }
         printf("\n");
       } else {
-        printf(" not available in this build");
+        throw OptionException("debug tags not available in non-debug build");
+      }
+      exit(0);
+      break;
+
+    case SHOW_TRACE_TAGS:
+      if(Configuration::isTracingBuild()) {
+        printf("available tags:");
+        unsigned ntags = Configuration::getNumTraceTags();
+        char const* const* tags = Configuration::getTraceTags();
+        for (unsigned i = 0; i < ntags; ++ i) {
+          printf(" %s", tags[i]);
+        }
+        printf("\n");
+      } else {
+        throw OptionException("trace tags not available in non-tracing build");
       }
       exit(0);
       break;