From: Gereon Kremer Date: Tue, 9 Nov 2021 01:55:09 +0000 (-0800) Subject: Remove `CVC5Message` (#7610) X-Git-Tag: cvc5-1.0.0~855 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7391d16bf8669060043e9cff17b9e76ff15ef19e;p=cvc5.git Remove `CVC5Message` (#7610) This PR removes the few remaining usages of the CVC5Message() and gets rid of the whole thing. --- 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& 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& 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