From: Kshitij Bansal Date: Fri, 6 Jun 2014 01:29:20 +0000 (-0400) Subject: -{d,t} help => --show-{debug,trace}-tags X-Git-Tag: cvc5-1.0.0~6852^2~2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d344d4874bda7e90692149d6989c8ca63f0db602;p=cvc5.git -{d,t} help => --show-{debug,trace}-tags --- diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index 15813a774..e701ee13d 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -121,6 +121,18 @@ inline std::string suggestTags(char const* const* validTags, std::string inputTa inline void addTraceTag(std::string option, std::string optarg, SmtEngine* smt) { if(Configuration::isTracingBuild()) { if(!Configuration::isTraceTag(optarg.c_str())) + + if(optarg == "help") { + 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"); + exit(0); + } + throw OptionException(std::string("trace tag ") + optarg + std::string(" not available.") + suggestTags(Configuration::getTraceTags(), optarg) ); @@ -134,6 +146,18 @@ inline void addDebugTag(std::string option, std::string optarg, SmtEngine* smt) if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) { if(!Configuration::isDebugTag(optarg.c_str()) && !Configuration::isTraceTag(optarg.c_str())) { + + if(optarg == "help") { + 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"); + exit(0); + } + throw OptionException(std::string("debug tag ") + optarg + std::string(" not available.") + suggestTags(Configuration::getDebugTags(), optarg, Configuration::getTraceTags()) );