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 b89d43cc9e660a87cdf0b5714f07307588b7e802..0c64960530db0fa84e7b6c0c9de7f70897888cd1 100644 (file)
--- 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 ? "<stdin>" : 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 baaf03b5066f6e3ce829abec6297588057c3a9a8..f7d1a77d4b791f0d53af73d8eacf3deccde5bf43 100644 (file)
--- 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 76ba9e2954af0c01bf841019948763fd89d3f512..66dc9780842dc3efa7e493d1255c757620ffb888 100644 (file)
--- 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 5acee360fbfa443c5efb74498b91f87fa54135d6..692f3b8d11c763fb64bfd5cb0c07239b81c83f81 100644 (file)
--- 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 61b1f40d263588612c89ab85ff35bf3df5046d2e..84371f790697edc80c5b0cea6e9ca9c1ad1a0763 100644 (file)
--- 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("");