From: Morgan Deters Date: Fri, 21 Sep 2012 10:24:08 +0000 (+0000) Subject: better verbosity support (so it's sensible when the library is used via the API) X-Git-Tag: cvc5-1.0.0~7795 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9c543757e459bfae5ce1254322212f72af0d37a4;p=cvc5.git better verbosity support (so it's sensible when the library is used via the API) (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index b89d43cc9..0c6496053 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -140,28 +140,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin))); } - // Determine which messages to show based on smtcomp_mode and verbosity - if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(opts[options::verbosity] < 2) { - Chat.setStream(CVC4::null_os); - } - if(opts[options::verbosity] < 1) { - Notice.setStream(CVC4::null_os); - } - if(opts[options::verbosity] < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - } - // Auto-detect input language by filename extension const char* filename = inputFromStdin ? "" : filenames[0].c_str(); @@ -191,34 +169,13 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Determine which messages to show based on smtcomp_mode and verbosity if(Configuration::isMuzzledBuild()) { - Debug.setStream(CVC4::null_os); - Trace.setStream(CVC4::null_os); - Notice.setStream(CVC4::null_os); - Chat.setStream(CVC4::null_os); - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - Dump.setStream(CVC4::null_os); - } else { - if(opts[options::verbosity] < 2) { - Chat.setStream(CVC4::null_os); - } - if(opts[options::verbosity] < 1) { - Notice.setStream(CVC4::null_os); - } - if(opts[options::verbosity] < 0) { - Message.setStream(CVC4::null_os); - Warning.setStream(CVC4::null_os); - } - - Debug.getStream() << Expr::setlanguage(opts[options::outputLanguage]); - Trace.getStream() << Expr::setlanguage(opts[options::outputLanguage]); - Notice.getStream() << Expr::setlanguage(opts[options::outputLanguage]); - Chat.getStream() << Expr::setlanguage(opts[options::outputLanguage]); - Message.getStream() << Expr::setlanguage(opts[options::outputLanguage]); - Warning.getStream() << Expr::setlanguage(opts[options::outputLanguage]); - Dump.getStream() << Expr::setlanguage(opts[options::outputLanguage]) - << Expr::setdepth(-1) - << Expr::printtypes(false); + DebugChannel.setStream(CVC4::null_os); + TraceChannel.setStream(CVC4::null_os); + NoticeChannel.setStream(CVC4::null_os); + ChatChannel.setStream(CVC4::null_os); + MessageChannel.setStream(CVC4::null_os); + WarningChannel.setStream(CVC4::null_os); + DumpChannel.setStream(CVC4::null_os); } // important even for muzzled builds (to get result output right) diff --git a/src/options/base_options b/src/options/base_options index baaf03b50..f7d1a77d4 100644 --- a/src/options/base_options +++ b/src/options/base_options @@ -77,7 +77,7 @@ common-option outputLanguage output-language --output-lang=LANG OutputLanguage : force input language (default is "auto"; see --lang help) option languageHelp bool -option verbosity verbosity int :read-write :default 0 +option verbosity verbosity int :read-write :default 0 :predicate CVC4::options::setVerbosity :predicate-include "options/base_options_handlers.h" the verbosity level of CVC4 common-option - -v --verbose void :handler CVC4::options::increaseVerbosity increase verbosity (may be repeated) diff --git a/src/options/base_options_handlers.h b/src/options/base_options_handlers.h index 76ba9e295..66dc97808 100644 --- a/src/options/base_options_handlers.h +++ b/src/options/base_options_handlers.h @@ -29,12 +29,43 @@ namespace CVC4 { namespace options { +inline void setVerbosity(std::string option, int value, SmtEngine* smt) throw(OptionException) { + if(Configuration::isMuzzledBuild()) { + DebugChannel.setStream(CVC4::null_os); + TraceChannel.setStream(CVC4::null_os); + NoticeChannel.setStream(CVC4::null_os); + ChatChannel.setStream(CVC4::null_os); + MessageChannel.setStream(CVC4::null_os); + WarningChannel.setStream(CVC4::null_os); + } else { + if(value < 2) { + ChatChannel.setStream(CVC4::null_os); + } else { + ChatChannel.setStream(std::cout); + } + if(value < 1) { + NoticeChannel.setStream(CVC4::null_os); + } else { + NoticeChannel.setStream(std::cout); + } + if(value < 0) { + MessageChannel.setStream(CVC4::null_os); + WarningChannel.setStream(CVC4::null_os); + } else { + MessageChannel.setStream(std::cout); + WarningChannel.setStream(std::cerr); + } + } +} + inline void increaseVerbosity(std::string option, SmtEngine* smt) { options::verbosity.set(options::verbosity() + 1); + setVerbosity(option, options::verbosity(), smt); } inline void decreaseVerbosity(std::string option, SmtEngine* smt) { options::verbosity.set(options::verbosity() - 1); + setVerbosity(option, options::verbosity(), smt); } inline OutputLanguage stringToOutputLanguage(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { diff --git a/src/util/output.cpp b/src/util/output.cpp index 5acee360f..692f3b8d1 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -37,8 +37,8 @@ const int CVC4ostream::s_indentIosIndex = ios_base::xalloc(); DebugC DebugChannel CVC4_PUBLIC (&cout); WarningC WarningChannel CVC4_PUBLIC (&cerr); MessageC MessageChannel CVC4_PUBLIC (&cout); -NoticeC NoticeChannel CVC4_PUBLIC (&cout); -ChatC ChatChannel CVC4_PUBLIC (&cout); +NoticeC NoticeChannel CVC4_PUBLIC (&null_os); +ChatC ChatChannel CVC4_PUBLIC (&null_os); TraceC TraceChannel CVC4_PUBLIC (&cout); std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer DumpOutC DumpOutChannel CVC4_PUBLIC (&DumpOutC::dump_cout); diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index 61b1f40d2..84371f790 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -38,12 +38,12 @@ class OutputBlack : public CxxTest::TestSuite { public: void setUp() { - Debug.setStream(d_debugStream); - Trace.setStream(d_traceStream); - Notice.setStream(d_noticeStream); - Chat.setStream(d_chatStream); - Message.setStream(d_messageStream); - Warning.setStream(d_warningStream); + DebugChannel.setStream(d_debugStream); + TraceChannel.setStream(d_traceStream); + NoticeChannel.setStream(d_noticeStream); + ChatChannel.setStream(d_chatStream); + MessageChannel.setStream(d_messageStream); + WarningChannel.setStream(d_warningStream); d_debugStream.str(""); d_traceStream.str("");