adding --show-debug-tags to list all available debug tracing tags

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index f371a4d7289db33aed0bc5e37863d749e5d80fb9..bf975d5136fcb2c32c2bb34731a9d6642cdaf40c 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -75,7 +75,29 @@ libutilcudd_la_SOURCES = \
 BUILT_SOURCES = \
        rational.h \
        integer.h \
-       tls.h
+       tls.h \
+       debug_tags.h
+
+debug_tags.h: debug_tags
+       $(AM_V_GEN)( \
+       echo 'const char* debug_tags[] = {'; \
+       first=1; \
+       for tag in `cat debug_tags`; \
+       do \
+           if [ $$first -eq 1 ]; then first=0; else echo ','; fi; \
+               echo -n "\"$$tag\""; \
+       done; \
+       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
+
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 7e601135238a0ee64fab15ec3eab2ef3b9a512d9..a6042c3a9f314b4b310d64b65676f1ac2978ce96 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -32,6 +32,7 @@
 #include "util/language.h"
 #include "util/options.h"
 #include "util/output.h"
+#include "util/debug_tags.h"
 
 #include "cvc4autoconfig.h"
 
@@ -116,6 +117,7 @@ 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\
    --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\
@@ -267,6 +269,7 @@ enum OptionValue {
   NO_CHECKING,
   NO_THEORY_REGISTRATION,
   USE_MMAP,
+  SHOW_DEBUG_TAGS,
   SHOW_CONFIG,
   STRICT_PARSING,
   DEFAULT_EXPR_DEPTH,
@@ -328,6 +331,7 @@ 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-config", no_argument      , NULL, SHOW_CONFIG },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
   { "help"       , no_argument      , NULL, 'h'         },
@@ -763,6 +767,20 @@ throw(OptionException) {
       arithPropagateMaxLength = atoi(optarg);
       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]);
+        }
+        printf("\n");
+      } else {
+        printf(" not available in this build");
+      }
+      exit(0);
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");