Remove `CVC5Message` (#7610)

This PR removes the few remaining usages of the CVC5Message() and gets rid of the whole thing.

11 files changed, 13 insertions, 72 deletions

diff --git a/src/base/output.cpp b/src/base/output.cpp
index f9946c4a8..2e9fc64ee 100644
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -31,7 +31,6 @@ const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc();
 
 DebugC DebugChannel(&std::cout);
 WarningC WarningChannel(&std::cerr);
-MessageC MessageChannel(&std::cout);
 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 dad354ad4..44bde9983 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -263,23 +263,6 @@ public:
 
 }; /* class WarningC */
 
-/** The message output class */
-class MessageC
-{
-  std::ostream* d_os;
-
-public:
-  explicit MessageC(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 MessageC */
-
 /** The trace output class */
 class TraceC
 {
@@ -368,8 +351,6 @@ public:
 extern DebugC DebugChannel CVC5_EXPORT;
 /** The warning output singleton */
 extern WarningC WarningChannel CVC5_EXPORT;
-/** The message output singleton */
-extern MessageC MessageChannel CVC5_EXPORT;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC5_EXPORT;
 /** The dump output singleton */
@@ -382,8 +363,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
 #define WarningOnce \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
-#define CVC5Message \
-  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel
 #define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
 #define DumpOut \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
@@ -402,8 +381,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
    || !::cvc5::WarningChannel.warnOnce(__FILE__, __LINE__)) \
       ? ::cvc5::nullStream                                  \
       : ::cvc5::WarningChannel
-#define CVC5Message \
-  (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel
 #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 e7f0a90b9..7b34ab6d3 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -159,7 +159,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&cvc5::null_os);
     TraceChannel.setStream(&cvc5::null_os);
-    MessageChannel.setStream(&cvc5::null_os);
     WarningChannel.setStream(&cvc5::null_os);
   }
 
@@ -183,18 +182,17 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
                              dopts.in(),
                              dopts.out());
 
-      CVC5Message() << Configuration::getPackageName() << " "
-                    << Configuration::getVersionString();
+      auto& out = solver->getDriverOptions().out();
+      out << Configuration::getPackageName() << " "
+          << Configuration::getVersionString();
       if (Configuration::isGitBuild())
       {
-        CVC5Message() << " [" << Configuration::getGitInfo() << "]";
+        out << " [" << Configuration::getGitInfo() << "]";
       }
-      CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-                    << " assertions:"
-                    << (Configuration::isAssertionBuild() ? "on" : "off")
-                    << endl
-                    << endl;
-      CVC5Message() << Configuration::copyright() << endl;
+      out << (Configuration::isDebugBuild() ? " DEBUG" : "") << " assertions:"
+          << (Configuration::isAssertionBuild() ? "on" : "off") << std::endl
+          << std::endl
+          << Configuration::copyright() << std::endl;
 
       while(true) {
         try {
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 5adce0a4f..aed851e8e 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -74,7 +74,6 @@ void OptionsHandler::setErrStream(const std::string& flag, const ManagedErr& me)
 {
   Debug.setStream(me);
   Warning.setStream(me);
-  CVC5Message.setStream(me);
   Trace.setStream(me);
 }
 
@@ -133,14 +132,11 @@ void OptionsHandler::setVerbosity(const std::string& flag, int value)
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&cvc5::null_os);
     TraceChannel.setStream(&cvc5::null_os);
-    MessageChannel.setStream(&cvc5::null_os);
     WarningChannel.setStream(&cvc5::null_os);
   } else {
     if(value < 0) {
-      MessageChannel.setStream(&cvc5::null_os);
       WarningChannel.setStream(&cvc5::null_os);
     } else {
-      MessageChannel.setStream(&std::cout);
       WarningChannel.setStream(&std::cerr);
     }
   }
@@ -262,7 +258,6 @@ void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
 {
   Debug.getStream() << Command::printsuccess(value);
   Trace.getStream() << Command::printsuccess(value);
-  CVC5Message.getStream() << Command::printsuccess(value);
   Warning.getStream() << Command::printsuccess(value);
   *d_options->base.out << Command::printsuccess(value);
 }
@@ -344,7 +339,6 @@ void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth)
 {
   Debug.getStream() << expr::ExprSetDepth(depth);
   Trace.getStream() << expr::ExprSetDepth(depth);
-  CVC5Message.getStream() << expr::ExprSetDepth(depth);
   Warning.getStream() << expr::ExprSetDepth(depth);
 }
 
@@ -352,7 +346,6 @@ void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
 {
   Debug.getStream() << expr::ExprDag(dag);
   Trace.getStream() << expr::ExprDag(dag);
-  CVC5Message.getStream() << expr::ExprDag(dag);
   Warning.getStream() << expr::ExprDag(dag);
 }
 
diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index 270904905..db6cb8b72 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -856,7 +856,6 @@ PreprocessingPassResult UnconstrainedSimplifier::applyInternal(
   if (!d_unconstrained.empty())
   {
     processUnconstrained();
-    //    d_substitutions.print(CVC5Message.getStream());
     for (size_t i = 0, asize = assertions.size(); i < asize; ++i)
     {
       Node a = assertions[i];
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 525db2726..dcb674bd4 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -690,9 +690,8 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
           Node ev = d_quant_models[f].evaluate(fmfmc, inst);
           if (ev == d_true)
           {
-            CVC5Message() << "WARNING: instantiation was true! " << f << " "
-                          << mcond[i] << std::endl;
-            AlwaysAssert(false);
+            AlwaysAssert(false) << "WARNING: instantiation was true! " << f
+                                << " " << mcond[i] << std::endl;
           }
           else
           {
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 18a039fbf..3afa2715b 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -195,9 +195,8 @@ void QuantAttributes::computeAttributes( Node q ) {
   {
     Node f = qa.d_fundef_f;
     if( d_fun_defs.find( f )!=d_fun_defs.end() ){
-      CVC5Message() << "Cannot define function " << f << " more than once."
-                    << std::endl;
-      AlwaysAssert(false);
+      AlwaysAssert(false) << "Cannot define function " << f
+                          << " more than once." << std::endl;
     }
     d_fun_defs[f] = true;
   }
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 8ca099dae..70e3deb63 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -215,8 +215,6 @@ void SubstitutionMap::print(ostream& out) const {
   }
 }
 
-void SubstitutionMap::debugPrint() const { print(CVC5Message.getStream()); }
-
 }  // namespace theory
 
 std::ostream& operator<<(std::ostream& out, const theory::SubstitutionMap::iterator& i) {
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 08936e3b6..1de636fb3 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -151,7 +151,6 @@ class SubstitutionMap
    * Print to the output stream
    */
   void print(std::ostream& out) const;
-  void debugPrint() const;
 
 }; /* class SubstitutionMap */
 
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp
index 9fc2915bf..f5f6ff565 100644
--- a/src/theory/uf/cardinality_extension.cpp
+++ b/src/theory/uf/cardinality_extension.cpp
@@ -1025,8 +1025,7 @@ int SortModel::addSplit(Region* r)
       }
       if (ss == b_t)
       {
-        CVC5Message() << "Bad split " << s << std::endl;
-        AlwaysAssert(false);
+        AlwaysAssert(false) << "Bad split " << s << std::endl;
       }
     }
     if (Trace.isOn("uf-ss-split-si"))
@@ -1432,8 +1431,6 @@ void CardinalityExtension::assertNode(Node n, bool isDecision)
           for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
             if( !it->second->hasCardinalityAsserted() ){
               Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
-              // CVC5Message() << "Error: constraint asserted before cardinality
-              // for " << it->first << std::endl; Unimplemented();
             }
           }
         }
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index 72067c496..54b1570d6 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -30,12 +30,10 @@ class TestUtilBlackOutput : public TestInternal
     TestInternal::SetUp();
     DebugChannel.setStream(&d_debugStream);
     TraceChannel.setStream(&d_traceStream);
-    MessageChannel.setStream(&d_messageStream);
     WarningChannel.setStream(&d_warningStream);
 
     d_debugStream.str("");
     d_traceStream.str("");
-    d_messageStream.str("");
     d_warningStream.str("");
   }
 
@@ -50,7 +48,6 @@ class TestUtilBlackOutput : public TestInternal
   }
   std::stringstream d_debugStream;
   std::stringstream d_traceStream;
-  std::stringstream d_messageStream;
   std::stringstream d_warningStream;
 };
 
@@ -63,7 +60,6 @@ TEST_F(TestUtilBlackOutput, output)
   Debug.on("foo");
   Debug("foo") << "testing3";
 
-  CVC5Message() << "a message";
   Warning() << "bad warning!";
 
   Trace.on("foo");
@@ -76,7 +72,6 @@ TEST_F(TestUtilBlackOutput, output)
 #ifdef CVC5_MUZZLE
 
   ASSERT_EQ(d_debugStream.str(), "");
-  ASSERT_EQ(d_messageStream.str(), "");
   ASSERT_EQ(d_warningStream.str(), "");
   ASSERT_EQ(d_traceStream.str(), "");
 
@@ -88,7 +83,6 @@ TEST_F(TestUtilBlackOutput, output)
   ASSERT_EQ(d_debugStream.str(), "");
 #endif /* CVC5_DEBUG */
 
-  ASSERT_EQ(d_messageStream.str(), "a message");
   ASSERT_EQ(d_warningStream.str(), "bad warning!");
 
 #ifdef CVC5_TRACING
@@ -124,7 +118,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   ASSERT_FALSE(Debug.isOn("foo"));
   ASSERT_FALSE(Trace.isOn("foo"));
   ASSERT_FALSE(Warning.isOn());
-  ASSERT_FALSE(CVC5Message.isOn());
 
   cout << "debug" << std::endl;
   Debug("foo") << failure() << std::endl;
@@ -132,8 +125,6 @@ TEST_F(TestUtilBlackOutput, evaluation_off_when_it_is_supposed_to_be)
   Trace("foo") << failure() << std::endl;
   cout << "warning" << std::endl;
   Warning() << failure() << std::endl;
-  cout << "message" << std::endl;
-  CVC5Message() << failure() << std::endl;
 #endif
 }
 
@@ -163,10 +154,6 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_warningStream.str(), std::string());
   d_warningStream.str("");
 
-  CVC5Message() << "baz foo";
-  ASSERT_EQ(d_messageStream.str(), std::string());
-  d_messageStream.str("");
-
 #else /* CVC5_MUZZLE */
 
   Debug.off("yo");
@@ -199,10 +186,6 @@ TEST_F(TestUtilBlackOutput, simple_print)
   ASSERT_EQ(d_warningStream.str(), std::string("baz foo"));
   d_warningStream.str("");
 
-  CVC5Message() << "baz foo";
-  ASSERT_EQ(d_messageStream.str(), std::string("baz foo"));
-  d_messageStream.str("");
-
 #endif /* CVC5_MUZZLE */
 }
 }  // namespace test