From dcb2ad496607e2f3821ee84a175a1b412f2f9a20 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Dejan=20Jovanovi=C4=87?= <dejan.jovanovic@gmail.com>
Date: Thu, 15 Sep 2011 18:17:11 +0000
Subject: [PATCH] adding --show-debug-tags to list all available debug tracing
 tags

---
 src/util/Makefile.am | 24 +++++++++++++++++++++++-
 src/util/options.cpp | 18 ++++++++++++++++++
 2 files changed, 41 insertions(+), 1 deletion(-)

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index f371a4d72..bf975d513 100644
--- 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 7e6011352..a6042c3a9 100644
--- 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");
-- 
2.30.2