Remove `Chat()` in favor of new `verbose()` (#7586)

This PR completely removes the first of several logging macros. Instead of Chat(), we now use verbose(2).

11 files changed, 16 insertions, 67 deletions

diff --git a/src/base/output.cpp b/src/base/output.cpp
index 4ef76a772..2b77a3b2a 100644
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -33,7 +33,6 @@ DebugC DebugChannel(&std::cout);
 WarningC WarningChannel(&std::cerr);
 MessageC MessageChannel(&std::cout);
 NoticeC NoticeChannel(&null_os);
-ChatC ChatChannel(&null_os);
 TraceC TraceChannel(&std::cout);
 std::ostream DumpOutC::dump_cout(std::cout.rdbuf());  // copy cout stream buffer
 DumpOutC DumpOutChannel(&DumpOutC::dump_cout);
diff --git a/src/base/output.h b/src/base/output.h
index cc6bfb316..2783f4bc6 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -297,23 +297,6 @@ public:
   bool isOn() const { return d_os != &null_os; }
 }; /* class NoticeC */
 
-/** The chat output class */
-class ChatC
-{
-  std::ostream* d_os;
-
-public:
-  explicit ChatC(std::ostream* os) : d_os(os) {}
-
-  Cvc5ostream operator()() const { return Cvc5ostream(d_os); }
-
-  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
-  std::ostream& getStream() const { return *d_os; }
-  std::ostream* getStreamPointer() const { return d_os; }
-
-  bool isOn() const { return d_os != &null_os; }
-}; /* class ChatC */
-
 /** The trace output class */
 class TraceC
 {
@@ -406,8 +389,6 @@ extern WarningC WarningChannel CVC5_EXPORT;
 extern MessageC MessageChannel CVC5_EXPORT;
 /** The notice output singleton */
 extern NoticeC NoticeChannel CVC5_EXPORT;
-/** The chat output singleton */
-extern ChatC ChatChannel CVC5_EXPORT;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC5_EXPORT;
 /** The dump output singleton */
@@ -424,7 +405,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel
 #define Notice \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::NoticeChannel
-#define Chat ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::ChatChannel
 #define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
 #define DumpOut \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
@@ -447,8 +427,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
   (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel
 #define Notice \
   (!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::NoticeChannel
-#define Chat \
-  (!::cvc5::ChatChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::ChatChannel
 #ifdef CVC5_TRACING
 #define Trace ::cvc5::TraceChannel
 #else /* CVC5_TRACING */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 4e92584a8..893a77cd9 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -160,7 +160,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
     DebugChannel.setStream(&cvc5::null_os);
     TraceChannel.setStream(&cvc5::null_os);
     NoticeChannel.setStream(&cvc5::null_os);
-    ChatChannel.setStream(&cvc5::null_os);
     MessageChannel.setStream(&cvc5::null_os);
     WarningChannel.setStream(&cvc5::null_os);
   }
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d5d61977c..060b7eeba 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -76,7 +76,6 @@ void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me)
   Warning.setStream(me);
   CVC5Message.setStream(me);
   Notice.setStream(me);
-  Chat.setStream(me);
   Trace.setStream(me);
 }
 
@@ -136,15 +135,9 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value)
     DebugChannel.setStream(&cvc5::null_os);
     TraceChannel.setStream(&cvc5::null_os);
     NoticeChannel.setStream(&cvc5::null_os);
-    ChatChannel.setStream(&cvc5::null_os);
     MessageChannel.setStream(&cvc5::null_os);
     WarningChannel.setStream(&cvc5::null_os);
   } else {
-    if(value < 2) {
-      ChatChannel.setStream(&cvc5::null_os);
-    } else {
-      ChatChannel.setStream(&std::cout);
-    }
     if(value < 1) {
       NoticeChannel.setStream(&cvc5::null_os);
     } else {
@@ -277,7 +270,6 @@ void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
   Debug.getStream() << Command::printsuccess(value);
   Trace.getStream() << Command::printsuccess(value);
   Notice.getStream() << Command::printsuccess(value);
-  Chat.getStream() << Command::printsuccess(value);
   CVC5Message.getStream() << Command::printsuccess(value);
   Warning.getStream() << Command::printsuccess(value);
   *d_options->base.out << Command::printsuccess(value);
@@ -361,7 +353,6 @@ void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth)
   Debug.getStream() << expr::ExprSetDepth(depth);
   Trace.getStream() << expr::ExprSetDepth(depth);
   Notice.getStream() << expr::ExprSetDepth(depth);
-  Chat.getStream() << expr::ExprSetDepth(depth);
   CVC5Message.getStream() << expr::ExprSetDepth(depth);
   Warning.getStream() << expr::ExprSetDepth(depth);
 }
@@ -371,7 +362,6 @@ void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
   Debug.getStream() << expr::ExprDag(dag);
   Trace.getStream() << expr::ExprDag(dag);
   Notice.getStream() << expr::ExprDag(dag);
-  Chat.getStream() << expr::ExprDag(dag);
   CVC5Message.getStream() << expr::ExprDag(dag);
   Warning.getStream() << expr::ExprDag(dag);
 }
diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 90685b9c7..99bded47a 100644
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -36,7 +36,7 @@ ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult ApplySubsts::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
-  Chat() << "applying substitutions..." << std::endl;
+  verbose(2) << "applying substitutions..." << std::endl;
   Trace("apply-substs") << "ApplySubsts::processAssertions(): "
                         << "applying substitutions" << std::endl;
   // TODO(#1255): Substitutions in incremental mode should be managed with a
diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 01b228ed5..433bca568 100644
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -99,9 +99,9 @@ Node ITESimp::simpITE(util::ITEUtilities* ite_utils, TNode assertion)
 
     if (options().smt.simplifyWithCareEnabled)
     {
-      Chat() << "starting simplifyWithCare()" << endl;
+      verbose(2) << "starting simplifyWithCare()" << endl;
       Node postSimpWithCare = ite_utils->simplifyWithCare(res_rewritten);
-      Chat() << "ending simplifyWithCare()"
+      verbose(2) << "ending simplifyWithCare()"
              << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
       result = rewrite(postSimpWithCare);
     }
@@ -130,14 +130,14 @@ bool ITESimp::doneSimpITE(AssertionPipeline* assertionsToPreprocess)
       NodeManager* nm = NodeManager::currentNM();
       if (nm->poolSize() >= options().smt.zombieHuntThreshold)
       {
-        Chat() << "..ite simplifier did quite a bit of work.. "
+        verbose(2) << "..ite simplifier did quite a bit of work.. "
                << nm->poolSize() << endl;
-        Chat() << "....node manager contains " << nm->poolSize()
+        verbose(2) << "....node manager contains " << nm->poolSize()
                << " nodes before cleanup" << endl;
         d_iteUtilities.clear();
         d_env.getRewriter()->clearCaches();
         nm->reclaimZombiesUntil(options().smt.zombieHuntThreshold);
-        Chat() << "....node manager contains " << nm->poolSize()
+        verbose(2) << "....node manager contains " << nm->poolSize()
                << " nodes after cleanup" << endl;
       }
     }
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index f7e300a2d..06e57c568 100644
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -30,7 +30,7 @@ PreprocessingPassResult PreprocessingPass::apply(
     AssertionPipeline* assertionsToPreprocess) {
   TimerStat::CodeTimer codeTimer(d_timer);
   Trace("preprocessing") << "PRE " << d_name << std::endl;
-  Chat() << d_name << "..." << std::endl;
+  verbose(2) << d_name << "..." << std::endl;
   PreprocessingPassResult result = applyInternal(assertionsToPreprocess);
   Trace("preprocessing") << "POST " << d_name << std::endl;
   return result;
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 897846698..945f12168 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -531,12 +531,12 @@ bool ITECompressor::compress(AssertionPipeline* assertionsToPreprocess)
   d_incoming.computeReachability(assertionsToPreprocess->ref());
 
   ++(d_statistics.d_compressCalls);
-  Chat() << "Computed reachability" << endl;
+  verbose(2) << "Computed reachability" << endl;
 
   bool nofalses = true;
   const std::vector<Node>& assertions = assertionsToPreprocess->ref();
   size_t original_size = assertions.size();
-  Chat() << "compressing " << original_size << endl;
+  verbose(2) << "compressing " << original_size << endl;
   for (size_t i = 0; i < original_size && nofalses; ++i)
   {
     Node assertion = assertions[i];
@@ -675,7 +675,7 @@ bool ITESimplifier::leavesAreConst(TNode e)
 
 void ITESimplifier::clearSimpITECaches()
 {
-  Chat() << "clear ite caches " << endl;
+  verbose(2) << "clear ite caches " << endl;
   for (size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i)
   {
     NodeVec* curr = d_allocatedConstantLeaves[i];
@@ -698,7 +698,7 @@ void ITESimplifier::clearSimpITECaches()
 bool ITESimplifier::doneALotOfWorkHeuristic() const
 {
   static const size_t SIZE_BOUND = 1000;
-  Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications
+  verbose(2) << "d_citeEqConstApplications size " << d_citeEqConstApplications
          << endl;
   return (d_citeEqConstApplications > SIZE_BOUND);
 }
diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index 013954d49..8cfecda01 100644
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -259,7 +259,7 @@ bool ProcessAssertions::apply(Assertions& as)
                     << endl;
   dumpAssertions("assertions::pre-simplify", as);
   Trace("assertions::pre-simplify") << std::endl;
-  Chat() << "simplifying assertions..." << endl;
+  verbose(2) << "simplifying assertions..." << std::endl;
   noConflict = simplifyAssertions(as);
   if (!noConflict)
   {
@@ -299,7 +299,7 @@ bool ProcessAssertions::apply(Assertions& as)
     Trace("smt-proc")
         << "ProcessAssertions::processAssertions() : pre-repeat-simplify"
         << endl;
-    Chat() << "re-simplifying assertions..." << endl;
+    verbose(2) << "re-simplifying assertions..." << std::endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions(as);
     Trace("smt-proc")
@@ -393,7 +393,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as)
       PreprocessingPassResult res = applyPass("ite-simp", as);
       if (res == PreprocessingPassResult::CONFLICT)
       {
-        Chat() << "...ITE simplification found unsat..." << endl;
+        verbose(2) << "...ITE simplification found unsat..." << std::endl;
         return false;
       }
     }
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index bd87ca35c..4530df774 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -155,7 +155,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
 
   TimerStat::CodeTimer solveTimer(d_stats.d_solveTime);
 
-  Chat() << "solving..." << endl;
+  d_env.verbose(2) << "solving..." << std::endl;
   Trace("smt") << "SmtSolver::check(): running check" << endl;
   Result result = d_propEngine->checkSat();
 
@@ -228,7 +228,7 @@ void SmtSolver::processAssertions(Assertions& as)
 
   // Push the formula to SAT
   {
-    Chat() << "converting to CNF..." << endl;
+    d_env.verbose(2) << "converting to CNF..." << endl;
     const std::vector<Node>& assertions = ap.ref();
     // It is important to distinguish the input assertions from the skolem
     // definitions, as the decision justification heuristic treates the latter
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index 8a98a9601..e1d803227 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -31,14 +31,12 @@ class TestUtilBlackOutput : public TestInternal
     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("");
     d_noticeStream.str("");
-    d_chatStream.str("");
     d_messageStream.str("");
     d_warningStream.str("");
   }
@@ -55,7 +53,6 @@ class TestUtilBlackOutput : public TestInternal
   std::stringstream d_debugStream;
   std::stringstream d_traceStream;
   std::stringstream d_noticeStream;
-  std::stringstream d_chatStream;
   std::stringstream d_messageStream;
   std::stringstream d_warningStream;
 };
@@ -71,7 +68,6 @@ TEST_F(TestUtilBlackOutput, output)
 
   CVC5Message() << "a message";
   Warning() << "bad warning!";
-  Chat() << "chatty";
   Notice() << "note";
 
   Trace.on("foo");
@@ -86,7 +82,6 @@ TEST_F(TestUtilBlackOutput, output)
   ASSERT_EQ(d_debugStream.str(), "");
   ASSERT_EQ(d_messageStream.str(), "");
   ASSERT_EQ(d_warningStream.str(), "");
-  ASSERT_EQ(d_chatStream.str(), "");
   ASSERT_EQ(d_noticeStream.str(), "");
   ASSERT_EQ(d_traceStream.str(), "");
 
@@ -100,7 +95,6 @@ TEST_F(TestUtilBlackOutput, output)
 
   ASSERT_EQ(d_messageStream.str(), "a message");
   ASSERT_EQ(d_warningStream.str(), "bad warning!");
-  ASSERT_EQ(d_chatStream.str(), "chatty");
   ASSERT_EQ(d_noticeStream.str(), "note");
 
 #ifdef CVC5_TRACING
@@ -138,7 +132,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   ASSERT_FALSE(Warning.isOn());
   ASSERT_FALSE(CVC5Message.isOn());
   ASSERT_FALSE(Notice.isOn());
-  ASSERT_FALSE(Chat.isOn());
 
   cout << "debug" << std::endl;
   Debug("foo") << failure() << std::endl;
@@ -150,8 +143,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   CVC5Message() << failure() << std::endl;
   cout << "notice" << std::endl;
   Notice() << failure() << std::endl;
-  cout << "chat" << std::endl;
-  Chat() << failure() << std::endl;
 #endif
 }
 
@@ -181,10 +172,6 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_warningStream.str(), std::string());
   d_warningStream.str("");
 
-  Chat() << "baz foo";
-  ASSERT_EQ(d_chatStream.str(), std::string());
-  d_chatStream.str("");
-
   CVC5Message() << "baz foo";
   ASSERT_EQ(d_messageStream.str(), std::string());
   d_messageStream.str("");
@@ -225,10 +212,6 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_warningStream.str(), std::string("baz foo"));
   d_warningStream.str("");
 
-  Chat() << "baz foo";
-  ASSERT_EQ(d_chatStream.str(), std::string("baz foo"));
-  d_chatStream.str("");
-
   CVC5Message() << "baz foo";
   ASSERT_EQ(d_messageStream.str(), std::string("baz foo"));
   d_messageStream.str("");