From: Gereon Kremer Date: Fri, 5 Nov 2021 20:52:04 +0000 (-0700) Subject: Remove `Chat()` in favor of new `verbose()` (#7586) X-Git-Tag: cvc5-1.0.0~877 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d6d265e4de057510dbb6ae049446f47b047bcb8;p=cvc5.git 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). --- 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& 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& 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& 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("");