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.)

4 files changed, 41 insertions, 53 deletions

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 ? "<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 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);